CoreUpQuarkRungs
plain-language theorem explainer
CoreUpQuarkRungs fixes the integer rungs on the phi-ladder for up-type quarks at 4 for up, 15 for charm, and 21 for top. Mass derivations in the core model cite these values when applying the yardstick times phi to the power of rung minus 8 plus gap. The declaration is a structure whose body simply records the three default integers.
Claim. The canonical integer rungs for up-type quarks are $r_u=4$, $r_c=15$, $r_t=21$ on the phi-ladder, so that the mass of each is given by $m=y_S·ϕ^{r-8+g(Z)}$ with sector yardstick $y_S$ and gap function $g(Z)$.
background
Recognition Science places all particles on integer rungs of the phi-ladder derived from cube geometry. Up-type quarks occupy the set {4,15,21}. The module distinguishes this canonical integer-rung convention (core model, parameter-free) from the exploratory quarter-ladder hypothesis used only for phenomenological fits below 2 percent error on heavy quarks.
proof idea
One-line structure definition that supplies the three default integer values u:=4, c:=15, t:=21. No lemmas or tactics are invoked; the body is the literal assignment of the canonical core rungs.
why it matters
The structure supplies the fixed rungs consumed by the downstream core_up_rungs instance that enters mass calculations. It implements the integer-rung side of the coordinate-convention resolution stated in the module header and supports the T5-T8 forcing chain where phi is the self-similar fixed point and the mass formula is yardstick times phi to the appropriate power.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.