pith. sign in
theorem

up_rung_gen3_eq

proved
show as:
module
IndisputableMonolith.Masses.SectorDependentTorsion
domain
Masses
line
219 · github
papers citing
none yet

plain-language theorem explainer

The declaration establishes that the third-generation up-quark rung on the phi-ladder equals 28. Researchers modeling fermion masses via Recognition Science sector-dependent torsion would cite this numerical anchor for the phi-exponent in the mass formula. The proof is a one-line native computation that evaluates the recursive definition summing the prior rung and the two inter-generation steps.

Claim. Let $r_3$ be the third-generation up-quark rung defined as the sum of the first-generation rung, the step from generation 1 to 2, and the step from generation 2 to 3. Then $r_3 = 28$.

background

The Sector-Dependent Generation Torsion module verifies algebraic properties of the cell counts {13, 11, 6, 8} that arise in Q3 partitions for fermion sectors. Up-quark assignments {13, 11} remain data-supported hypotheses from PDG values, while the D = 3 coincidence W = 2V + 1 = N0 is derived independently. The upstream definition computes the third-generation up-quark rung as the sum of the first-generation rung plus the two inter-generation steps, and the module comment records the ordering 4 < 17 < 28.

proof idea

The proof is a one-line wrapper that invokes native_decide to evaluate the arithmetic expression in the definition of the third-generation up-quark rung and confirm equality to 28.

why it matters

This result supplies the concrete rung value 28 that enters the mass formula yardstick * phi^(rung - 8 + gap(Z)) for the third up-quark generation. It anchors numerical inputs inside the Recognition framework's phi-ladder while the surrounding module treats quark torsion assignments as hypotheses and derives the lepton torsion {11, 6}. The declaration touches the open question of first-principles forcing for the quark sector assignments.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.