down_rung_gen1_eq
plain-language theorem explainer
The declaration proves that the first-generation down-quark rung equals 4. Physicists computing baseline masses on the phi-ladder cite it to anchor down-type quark rungs before applying sector gaps. The proof is a one-line native decision that evaluates the power expression 2^(3-1) directly.
Claim. In the sector-dependent generation torsion framework the down-quark generation-1 rung satisfies $2^{3-1}=4$.
background
The module SectorDependentTorsion establishes that the integers {13,11,6,8} satisfy the algebraic constraints of Q3 cell counts and the partition 2D^D+1=55, while noting that lepton torsion is derived and quark assignments remain data-supported hypotheses. The upstream definition down_rung_gen1 sets the baseline rung for down quarks as 2^(3-1). The local setting includes the derived D=3 coincidence W=2V+1=N0 that forces three spatial dimensions.
proof idea
One-line wrapper that applies native_decide to evaluate the defining power expression 2^(3-1) and confirm equality with 4.
why it matters
This fixes the baseline rung value used in the mass formula yardstick * phi^(rung-8+gap(Z)) for down quarks. It supports the D=3 forcing condition derived in the module and the eight-tick octave structure of the Recognition chain. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.