down_rung_gen2_eq
plain-language theorem explainer
The theorem confirms that the second-generation down-rung torsion equals 10. Mass-modeling work on the phi-ladder cites this value when placing down-quark rungs for the hypothesized cell counts. The proof is a direct native computation of the upstream definition.
Claim. The down-rung torsion for the second generation equals 10.
background
Sector-Dependent Generation Torsion assigns the integers {13, 11, 6, 8} as Q₃ cell counts satisfying cyclic chains and the partition 2D^D + 1 = 55. The module treats lepton torsion {11, 6} as derived while quark assignments remain data-supported hypotheses: down quarks use {F = 6, V = 8} together with a cross-sector +12 shift. The upstream definition computes the second-generation down-rung as the sum of the first-generation down-rung and the step of 12.
proof idea
One-line wrapper that applies native_decide to evaluate the definition of the second-generation down-rung.
why it matters
The equality fixes the rung coordinate used by the mass formula yardstick · ϕ^(rung − 8 + gap(Z)) for down quarks in generation 2. It supplies the numerical anchor for the hypothesized down-quark cell counts inside the SDGT module. The module notes that D = 3 remains the only dimension forcing W = 2V + 1 = N₀, while the specific quark assignments stay outside the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.