step_charm_strange
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value 5.5 from the Recognition Composition Law or J-uniqueness.
- Does not incorporate the 1.5 alpha radiative correction factor noted in the module comment.
- Does not compute absolute quark masses or verify agreement with experimental data.
- Does not address other transitions such as top-bottom or up-down.
Lean usage
def res_strange : ℚ := res_charm - step_charm_strangeformal statement (Lean)
83def step_charm_strange : ℚ := 22 / 4
proof body
Definition body.
84
85/-- The radiative correction factor for the Cabibbo angle.
86 Represented as 1.5 * alpha, derived from 6 faces / 4 vertex-edge weight. -/