QuarkQuarterLadderPositions
plain-language theorem explainer
QuarkQuarterLadderPositions records the six fixed rational residues on the quarter ladder assigned to top, bottom, charm, strange, down, and up quarks. A physicist comparing the exploratory hypothesis layer to the canonical integer-rung core would cite these values when testing phenomenological mass accuracy below 2 percent for heavy quarks. The declaration is a plain structure that supplies the six default rationals with no computation or proof steps.
Claim. The quarter-ladder residues are the structure whose fields are top quark at $23/4$, bottom at $-8/4$, charm at $-18/4$, strange at $-40/4$, down at $-64/4$, and up at $-71/4$.
background
The module distinguishes two quark coordinate conventions. Convention A places all particles on integer rungs of the phi-ladder with sector-specific yardsticks derived from cube geometry and the mass formula yardstick times phi to the power of rung minus 8 plus gap of Z. Convention B, the quarter-ladder, is labeled hypothesis and supplies quarter-integer residues relative to the electron structural mass for improved numerical matches. The upstream quarter definition supplies the embedding that maps each integer k to the rational k/4.
proof idea
The declaration is a structure definition that directly supplies the six default rational values to the named fields.
why it matters
It supplies the concrete data for the hypothesis_positions definition that follows in the same module. The structure therefore anchors the exploratory quarter-ladder convention whose purpose is phenomenological accuracy rather than parameter-free derivation. It marks the explicit separation between the core integer-rung model and the hypothesis layer, leaving open the question of whether the quarter residues can be derived from the Recognition Composition Law or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.