CoreDownQuarkRungs
plain-language theorem explainer
CoreDownQuarkRungs records the integer positions on the phi-ladder for the down, strange, and bottom quarks in the core model. Physicists deriving parameter-free masses from geometry cite the structure when fixing the down-type sector yardstick before applying the mass formula. The definition is a direct structure with hardcoded defaults 4, 15, 21 that follow from the cube-geometry assignment in the integer-rung convention.
Claim. The core integer rungs for down-type quarks are the integers $r_d=4$, $r_s=15$, $r_b=21$ on the phi-ladder.
background
Recognition Science assigns every particle an integer rung on the phi-ladder. The mass formula is yardstick(Sector) times phi to the power (rung minus 8 plus gap(Z)). This structure belongs to Convention A, the canonical core layer that remains parameter-free. The module explicitly separates it from the exploratory quarter-ladder hypothesis used only for phenomenological fits below 2 percent accuracy.
proof idea
The declaration is a structure definition that directly supplies the three default integer fields. No lemmas or tactics are invoked; the values 4, 15, 21 are chosen once to match the geometric positions stated for down-type quarks.
why it matters
The structure supplies the rung values consumed by the core_down_rungs instance that appears in downstream mass derivations. It implements the integer-rung side of the layer separation described in the module, aligning with the eight-tick octave and the phi-ladder mass formula. The definition closes the coordinate convention gap for the down sector without touching the quarter-ladder hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.