sdgt_nu3
plain-language theorem explainer
The SDGT rung constructor fixes the value 19 for the third neutrino. Researchers tabulating fermion masses on the phi-ladder in Recognition Science cite this assignment when building the lepton spectrum. The proof is a direct reflexivity reduction against the definition of the rung function.
Claim. The sector-dependent torsion rung for the third-generation neutrino fermion equals 19.
background
The SDGT rung constructor computes an integer rung for each species by combining a sector baseline with a generation-dependent tau_sdgt adjustment. For leptons the rungs are derived; for quarks they remain hypotheses drawn from PDG data. This declaration sits inside the module whose stated purpose is to verify that the rung constructor reproduces the charged lepton table, though the same function is applied to neutrinos.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity to the definition of compute_rung_sdgt on the input (.fermion .nu3).
why it matters
The result supplies the rung 19 that enters the mass formula yardstick times phi to the power (rung minus 8 plus gap). It thereby populates the derived lepton rung table required by the Recognition Science mass hierarchy. No downstream theorems are listed, but the assignment closes one entry in the fermion verification sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.