res_top_eq_575
plain-language theorem explainer
The equality establishes that the top quark's ideal residue on the phi-ladder equals exactly 5.75 when cast from rationals to reals. Researchers deriving quark masses under the quarter-ladder hypothesis cite this to fix the topological rung before invoking the mass formula. The proof is a direct term reduction that simplifies the defining expression for the residue and normalizes the resulting rational to the decimal target.
Claim. The ideal residue $R$ of the top quark on the phi-ladder satisfies $R = 5.75$ when embedded in the reals, where the residue is the rational $23/4$ supplied by the quarter-ladder assignment.
background
The module formalizes T12, the derivation of quark masses via the Quarter-Ladder Hypothesis. Quarks share the structural base mass with leptons but sit at quarter-integer rungs on the phi-ladder; the top quark is placed at the ideal position $R = 5.75 = 23/4$, with the module noting a match to observed mass below 0.03 percent. The local setting treats discrepancies in lighter quarks as arising from non-perturbative QCD effects outside the bare geometric model. The upstream definition res_top supplies the rational $23/4$ directly, while the sibling res_top in the parent QuarkMasses module records the same ideal residue.
proof idea
The term proof first applies simp only [res_top] to unfold the definition of the residue as the rational 23/4, then invokes norm_num to confirm the numerical identity with 5.75. A comment in the body notes that the bound 172756 is chosen to avoid precision issues with nlinarith while remaining safe for the subsequent mass interval.
why it matters
This equality anchors the top-quark rung inside the RRF quark-mass derivation and is invoked by the downstream theorem top_mass_pred_bounds, which combines it with structural_mass_bounds and the phi_pow_575 interval lemmas to obtain the concrete mass window (172722, 172756). It realizes the explicit T12 step that assigns quarter-integer positions on the phi-ladder, consistent with the self-similar fixed point and eight-tick octave of the forcing chain. The result closes the ideal-residue scaffolding for the top quark while leaving open the incorporation of chiral-symmetry-breaking corrections for the lighter generations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.