step_bottom_charm
plain-language theorem explainer
Assigns the rational value 2.5 to the bottom-to-charm rung step within the deep-ladder quark hierarchy. Physicists assembling mass residues or CKM elements from geometric constraints cite this constant when populating the generation structure. The declaration is a direct rational assignment with no further reduction.
Claim. The rung displacement separating the bottom quark from the charm quark equals $2.5$ on the phi-ladder.
background
The module formalizes cubic voxel topology constraints that force the CKM and PMNS mixing parameters. Rung steps populate the GenerationStructure for the quarter-ladder hierarchy Top to Bottom to Charm to Strange. The upstream theorem from PrimitiveDistinction extracts four structural conditions plus three definitional facts from seven independent axioms that underwrite these geometric assignments.
proof idea
Direct definition that sets the value to the rational 10/4.
why it matters
Supplies the delta2 component of the GenerationStructure inside quark_hierarchy. It is invoked by derived_parameters for CKM predictions and by residues_match_steps to confirm residues align at -2, -4.5, -10. In the Recognition framework the step implements the phi-ladder mass formula and connects to the self-similar fixed point, though the precise forcing of 2.5 remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.