step_top_bottom
plain-language theorem explainer
The definition assigns the rational 31/4 to the top-to-bottom quark step on the phi-ladder. Researchers assembling CKM parameters and quark mass hierarchies cite this interval when building the generation structure inside the 8-tick cycle. The assignment is a direct literal with no reduction steps.
Claim. The top-to-bottom quark step equals $7.75$ rungs, or equivalently $31/4$, on the recognition ladder.
background
The MixingGeometry module formalizes cubic voxel topology constraints that force the CKM and PMNS mixing parameters. The step_top_bottom definition supplies one fixed interval in the quark hierarchy (top to bottom to charm to strange). Upstream, the PrimitiveDistinction.from theorem reduces seven independent axioms to four substantive structural conditions plus three definitional facts.
proof idea
This is a direct definition that sets the value to the rational 31/4. No lemmas or tactics are applied beyond the literal assignment.
why it matters
It supplies the delta1 value for the quark_hierarchy definition, which is used in the hierarchy_coherence theorem to establish that lepton and quark hierarchies are sub-structures of the same 8-tick recognition cycle. The step aligns with the T7 eight-tick octave and supports the geometric foundation for mixing matrices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.