sdgt_nu2
plain-language theorem explainer
The theorem states that the sector-dependent torsion rung for the second neutrino equals 11. Researchers verifying derived lepton assignments on the Recognition Science phi-ladder would cite this when checking the rung constructor output. The proof is a one-line reflexivity that follows directly from the definition of the rung constructor.
Claim. The sector-dependent torsion rung for the second neutrino fermion equals 11.
background
The module supplies proofs that the rung constructor reproduces the charged lepton table. The upstream definition of the sector-dependent torsion rung constructor matches on species: for a fermion it returns the baseline of its sector plus a tau correction that depends on sector and generation. This instance covers the second neutrino as part of the derived lepton rungs.
proof idea
The proof is a one-line wrapper that applies reflexivity. Reflexivity succeeds because the definition of the rung constructor evaluates directly to 11 for the second neutrino fermion.
why it matters
This result assigns rung 11 to the second neutrino, confirming a derived value in the lepton sector of the Recognition Science mass formula on the phi-ladder. It supports the claim that lepton rungs follow from the J-uniqueness and self-similar fixed point rather than data fitting. No downstream theorems are listed, so it functions as a verification step within the lepton table proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.