sdgt_down_d
plain-language theorem explainer
The SDGT rung constructor fixes the down quark at rung 4. Researchers checking quark mass assignments on the phi-ladder cite this result when validating the hypothesis-derived values against the sector-dependent torsion definition. The proof is a direct reflexivity reduction to the case split inside compute_rung_sdgt.
Claim. The sector-dependent torsion rung number for the down quark fermion evaluates to $4$.
background
The SDGT rung constructor (compute_rung_sdgt) is defined by matching on species, extracting the sector and generation index, then returning ell_baseline sector plus tau_sdgt sector gen. Quark rungs are marked as hypotheses drawn from PDG data, while lepton rungs are derived. The local module setting is verification that the rung constructor reproduces assigned tables, here applied to the first-generation down-type quark.
proof idea
One-line wrapper that applies reflexivity to the definition of compute_rung_sdgt on the .fermion .d case.
why it matters
This anchors the down-quark rung at 4 inside the phi-ladder mass formula (yardstick times phi to the power of rung minus 8 plus gap). It supports the hypothesis interface for quark masses within the Recognition framework's T5 J-uniqueness and T7 eight-tick octave structure. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.