up_generation_ordering
plain-language theorem explainer
The theorem establishes the rung ordering 4 < 17 < 28 for the three up-quark generations on the Recognition Science phi-ladder. Modelers of fermion mass hierarchies via sector-dependent torsion cite it to confirm the generation sequence before applying the mass exponent formula. The proof is a direct numerical check that splits the conjunction and decides the concrete inequalities.
Claim. The up-quark generation rungs satisfy $4 < 17$ and $17 < 28$.
background
In the Sector-Dependent Generation Torsion module, rung is the integer exponent offset assigned to each fermion sector and generation name, obtained by matching the sector (Lepton, UpQuark, DownQuark, Electroweak) to precomputed integer tables derived from D-cube cell counts. The module treats the up-quark cell counts {13, 11} as data-supported hypotheses while the D = 3 relation W = 2V + 1 = N0 is derived from geometry. Upstream results supply the Sector inductive type and the rung definition that dispatches on sector to the appropriate integer table.
proof idea
The term proof applies constructor to split the conjunction into two goals, then invokes native_decide on each to verify the numerical comparisons 4 < 17 and 17 < 28 hold for the concrete up-quark rung values.
why it matters
The result verifies the up-quark generation hierarchy inside the SDGT module, ensuring the phi-ladder exponents increase across generations before the mass formula yardstick * phi^(rung - 8 + gap(Z)) is applied. It contributes to the D = 3 coincidence derived from cube geometry and supports the eight-tick octave structure. The module explicitly flags the quark rung assignments as hypotheses rather than forced derivations from the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.