down_generation_ordering
plain-language theorem explainer
The theorem asserts that down-quark generation rungs satisfy the strict ordering 4 < 10 < 18. Researchers constructing the phi-ladder mass spectrum in the Recognition Science framework would cite this when assigning sector-dependent torsion values to fermions. The proof is a one-line term that splits the conjunction and decides both inequalities by native computation.
Claim. The down-quark generation rungs satisfy $4 < 10$ and $10 < 18$.
background
The Sector-Dependent Generation Torsion module establishes that the integers {13, 11, 6, 8} are Q3 cell counts obeying a cyclic chain and the partition of 2D^{D+1} = 55. Down quarks receive the pair {F = 6, V = 8} together with a cross-sector +12 shift, while the rung definition supplies the base tier value 1. Upstream results include the inflaton potential defined by Jcost on the recognition manifold and the cellular-automata step that applies a local rule to each tape cell.
proof idea
The proof is a one-line wrapper that applies constructor to split the conjunction into two goals and then invokes native_decide on each inequality.
why it matters
This ordering supplies the numerical input required for the down-quark mass formula on the phi-ladder. It supports the module's derived D = 3 coincidence that W = 2V + 1 holds only in three spatial dimensions. The declaration verifies algebraic properties of data-identified cell-count assignments rather than deriving those assignments from the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.