match_rsbridge_rung_neutrinos
plain-language theorem explainer
The theorem shows that the rung constructor matches the legacy RSBridge rung assignments for the three neutrino generations. Particle physicists checking consistency of the Recognition Science mass ladder would reference this when confirming the neutrino sector. The proof is a direct term-mode application of reflexivity to the three equalities.
Claim. The rung value assigned by the constructor to the electron neutrino fermion equals the legacy RSBridge assignment for the electron neutrino, and likewise for the muon neutrino and the tau neutrino.
background
In Recognition Science, particle masses are set by positions on the phi-ladder, with the rung number entering the mass formula as yardstick times phi to the power of (rung minus 8 plus gap of Z). Neutrinos start at rung zero because Z equals zero and use a generation step of plus eight rather than plus six. The RungConstructor.Proofs module supplies matching results between the new constructor and prior tables, with this declaration covering the neutrino case. Upstream, the rung function in AnchorPolicy maps each sector to an integer, while compute_rung in Motif encodes the constructor logic.
proof idea
The proof is a one-line term that constructs the conjunction of three reflexivity proofs, one for each neutrino generation.
why it matters
This declaration completes the neutrino portion of the master matching result that the constructor reproduces legacy rung values across sectors. It anchors neutrino mass assignments inside the Recognition framework, consistent with the eight-tick octave and the mass formula on the phi-ladder. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.