sdgt_down_b
plain-language theorem explainer
sdgt_down_b establishes that the sector-dependent torsion rung for the bottom quark fermion equals 18. Researchers building mass spectra on the phi-ladder cite this as a verification step for down-type quarks. The proof is a direct reflexivity reduction that evaluates the definition of compute_rung_sdgt on the third-generation down fermion.
Claim. The sector-dependent torsion rung for the bottom quark fermion equals 18.
background
The SDGT rung constructor computes an integer rung for each species. For a fermion it identifies the sector via sectorOf, extracts the generation index via genOf, and returns ell_baseline of the sector plus tau_sdgt of the sector and generation. Lepton rungs are derived while quark rungs are hypothesized from PDG data. The module supplies explicit checks that the constructor reproduces the expected rungs for each listed species.
proof idea
The proof is a one-line reflexivity tactic. It unfolds compute_rung_sdgt on the bottom fermion species and evaluates the sector and generation arithmetic directly to 18.
why it matters
This verification supports the mass formula yardstick times phi to the power of (rung minus 8 plus gap) for down-type quarks. It aligns with the phi-ladder construction in the forcing chain but leaves quark rungs as an open hypothesis drawn from data rather than derived from the Recognition Composition Law. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.