step_charm_strange
plain-language theorem explainer
The declaration defines the rung displacement separating the charm and strange quarks as the rational 5.5 within the Recognition Science phi-ladder. Researchers constructing CKM matrix elements from cubic voxel geometry cite this constant when matching quark residues to observed mass hierarchies. It is supplied by direct rational assignment with no lemmas or reductions applied.
Claim. The charm-to-strange transition corresponds to a displacement of $5.5$ rungs on the Recognition Science phi-ladder.
background
The module formalizes cubic voxel topology constraints that force the CKM and PMNS mixing parameters. Quark masses are obtained from the phi-ladder mass formula (yardstick times phi to the power of rung offset plus gap), so rung steps enter residue calculations directly. Upstream results supply the fine-structure constant alpha as the electromagnetic coupling and the phi-ladder finite-N correction factor 1 over phi times N.
proof idea
The definition is a direct rational assignment of 22 divided by 4. No lemmas are applied and no tactics are used; the value functions as a named constant for downstream residue arithmetic.
why it matters
This constant is required by the residues_match_steps theorem and the res_strange definition in QuarkMasses, and by derived_parameters in ParticleSummary. It supplies the specific charm-strange rung difference in the phi-ladder mass formula, supporting the self-similar fixed point and eight-tick octave structure of the forcing chain. The value aligns with the geometric vertex-edge weighting that also produces the 1.5 alpha radiative correction for the Cabibbo angle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.