residues_match_steps
plain-language theorem explainer
The theorem confirms exact numerical agreement between the derived residues for bottom, charm, and strange quarks and the target quarter-ladder positions on the phi-ladder. Mass-model builders in Recognition Science cite it to lock the topological assignments before feeding into the predicted-mass formula. The proof is a term-mode expansion that unfolds the residue and step definitions then reduces the arithmetic directly.
Claim. $r_b = -2$, $r_c = -4.5$, $r_s = -10$, where each residue is obtained from the cumulative quarter-integer steps on the phi-ladder starting from the top-quark position.
background
The module implements the Quarter-Ladder Hypothesis for quarks, which places them on quarter-integer rungs of the same phi-ladder used for leptons. Ideal positions are given explicitly: bottom at R = -2, charm at R = -4.5, strange at R = -10. Residues are computed from generation steps (top to bottom = 7.75 rungs, bottom to charm = 2.5 rungs, charm to strange = 5.5 rungs) via the structural mass base shared with leptons. Upstream results supply the step definitions (step_bottom_charm and step_charm_strange) and the underlying Mass type as a real number in RS-native units.
proof idea
Constructor splits the three-way conjunction. The first goal unfolds res_bottom, res_top and step_top_bottom then applies norm_num. The second goal unfolds the additional res_charm and step_bottom_charm before norm_num. The third goal unfolds res_strange together with step_charm_strange and normalizes the resulting arithmetic expression.
why it matters
The result verifies the residue assignments that feed the predicted-mass formula m = m_struct * phi^res inside the T12 quark-mass hypothesis lane. It sits downstream of the step lemmas in MixingGeometry and supports the broader claim that quark masses arise from the same phi-ladder geometry as leptons. The module itself flags that light-quark discrepancies remain open pending inclusion of non-perturbative QCD effects and a future parameter-free reconciliation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.