res_charm
plain-language theorem explainer
The res_charm definition supplies the charm quark residue of -4.5 on the phi-ladder under the quarter-ladder hypothesis for deriving quark masses from geometric positions. Researchers verifying particle mass predictions against experiment cite this constant when checking the charm slot. It is introduced by direct assignment of the rational -18/4 to match the ideal topological rung R = -18/4.
Claim. The charm quark residue is defined as the rational number $r_c = -18/4$.
background
The module implements the Quarter-Ladder Hypothesis, under which quarks occupy quarter-integer rungs on the phi-ladder while sharing the same structural base mass as leptons. Charm is assigned the ideal position R = -4.50 = -18/4. This residue is used in the mass formula that scales the structural yardstick by powers of phi offset from rung -8. The parent module defines sequential residues via subtraction of generation steps, with res_charm obtained as res_bottom minus the bottom-to-charm step.
proof idea
This is a direct definition that assigns the constant rational value -18/4 to the charm residue, encoding the hypothesized topological position without invoking lemmas or reductions.
why it matters
The definition supplies the input residue for the charm_mass_match theorem, which certifies a predicted mass near 1245-1247 MeV against the experimental 1270 MeV within 2 percent. It fills the charm position in the T12 quark masses derivation and the quarter-ladder hypothesis. The placement is consistent with the phi-ladder mass scaling and the eight-tick octave from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.