predicted_mass
The predicted mass formula scales the structural lepton mass by phi raised to a rational residue on the quarter-ladder. Physicists deriving quark masses from the Recognition Science phi-ladder cite this when checking numerical agreement with PDG values for top, bottom, and charm. It is a direct definition that multiplies the base structural mass by the appropriate power of phi.
claimThe predicted mass for residue $r$ is $m(r) = m_0 · φ^r$, where $m_0$ is the structural mass shared with the lepton sector and $r$ is a quarter-integer rung position.
background
The structural mass is given by $m_0 = Y · φ^{r_e - 8}$, with $Y$ the lepton yardstick and $r_e$ the electron rung (from upstream electron_structural_mass). The Quarter-Ladder Hypothesis states that quarks occupy quarter-integer positions on the same phi-ladder as leptons, with ideal residues such as 5.75 for top and -2 for bottom. This module works in the setting of T12, where light-quark discrepancies are attributed to QCD effects outside the bare geometric model.
proof idea
One-line definition that applies the structural mass definition and multiplies by phi raised to the real embedding of the rational residue.
why it matters in Recognition Science
This supplies the mass expression used by H_top_mass_match, H_bottom_mass_match, H_charm_mass_match and the residues_match_steps theorem. It fills the Quarter-Ladder Hypothesis step in the T12 quark masses module, extending the phi-ladder formula from the lepton sector and linking to the self-similar fixed point phi. The definition remains outside the parameter-free core until reconciliation with the Masses layer is shown.
scope and limits
- Does not include non-perturbative QCD corrections for light quarks.
- Does not claim parameter-free status without explicit reconciliation to the core mass model.
- Does not derive the residue values from first principles inside this file.
- Does not guarantee uniform precision across all six quark flavors.
Lean usage
theorem bottom_match : abs (predicted_mass res_bottom - mass_bottom_exp) / mass_bottom_exp < 0.01 := by simp [predicted_mass]formal statement (Lean)
91noncomputable def predicted_mass (res : ℚ) : ℝ :=
proof body
Definition body.
92 electron_structural_mass * (phi ^ (res : ℝ))
93