predicted_mass
plain-language theorem explainer
The predicted_mass definition supplies the quark mass as the product of the electron structural mass and phi raised to a rational residue on the phi-ladder. Researchers deriving particle masses from the Recognition Science quarter-ladder hypothesis would reference this formula when verifying numerical agreement with experimental quark masses. The implementation is a direct one-line scaling using the structural mass base and the phi exponentiation.
Claim. $m(r) = m_{struct} · φ^r$ where $m_{struct}$ denotes the electron structural mass and $r ∈ ℚ$ is the residue on the quarter-ladder.
background
The module formalizes T12 under the Quarter-Ladder Hypothesis: quarks share the structural base mass with leptons but sit at quarter-integer rungs on the phi-ladder. Ideal positions include top at 5.75, bottom at -2, charm at -4.5, with discrepancies in lighter quarks attributed to non-perturbative QCD effects. The phi-ladder itself arises from the self-similar fixed point in the forcing chain (T6) and the eight-tick octave (T7). Upstream, electron_structural_mass supplies the base from the lepton sector, while Mass is the native ℝ type in RS units.
proof idea
This definition is a one-line wrapper that multiplies electron_structural_mass by phi raised to the cast residue.
why it matters
It supplies the common formula used by the downstream match hypotheses H_top_mass_match, H_bottom_mass_match, and H_charm_mass_match, which certify agreement to 0.05%, 1%, and 2% respectively. The declaration therefore closes the mass-prediction step of T12 in the Recognition Science framework, linking the phi-ladder mass formula directly to the observed quark spectrum. Light-quark residuals remain open for later QCD corrections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.