hypothesis_positions
plain-language theorem explainer
The declaration supplies the default rational residues for the quarter-ladder hypothesis on quark rungs. Physicists comparing mass hierarchies cite it when contrasting the exploratory quarter-ladder model against the integer-rung core. The definition is a one-line wrapper that instantiates the structure with its built-in defaults.
Claim. The canonical quarter-ladder positions assign the top quark residue $23/4$, bottom $-8/4$, charm $-18/4$, strange $-40/4$, down $-64/4$, and up $-71/4$.
background
QuarkQuarterLadderPositions is the structure holding the rational rung residues for the hypothesis layer in quark mass modeling. The module distinguishes this from the core integer-rung convention, where all particles occupy integer rungs on the φ-ladder derived from geometry. Upstream, the quarter embedding from RungFractions maps integers k to k/4, and PrimitiveDistinction supplies the foundational axioms.
proof idea
The definition is a one-line wrapper that instantiates QuarkQuarterLadderPositions with its default field values.
why it matters
This definition supplies the hypothesis positions used by the conventions_differ theorems to demonstrate that the quarter-ladder and integer-rung assignments are distinct. It supports the quark_fractional_rung_necessity marker and nearest_int_positions conversion. In the framework it fills the exploratory layer for quark coordinates, separate from the canonical integer-rung core derived from the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.