neutrino_rung
plain-language theorem explainer
The declaration establishes that the neutrino baseline integer rung equals negative fifty-four on the Recognition Science mass ladder. Researchers calibrating lepton placements from three-cube combinatorics would cite this when fixing the phi-ladder origin for neutrinos. The proof is a one-line term wrapper that applies the already-proved neutrino baseline equation.
Claim. The neutrino baseline rung equals $-54$, obtained as the negation of the total geometric content (vertices plus edges plus faces plus passive edges plus wallpaper groups) of the three-cube at $D=3$.
background
The module upgrades prior boundary assumptions to derived status by evaluating standard combinatorial counts on the 3-cube $Q_3$ once $D=3$ is fixed. The neutrino baseline integer is defined directly as the negation of total geometric content, which aggregates vertices, edges, faces, passive field edges, and wallpaper groups. Upstream, the temporal ordering before from TimeEmergence supplies the arrow-of-time monotonicity used in defect counting, while sibling results such as lepton_baseline_eq fix the lepton rung at 2 for cross-checks against the Anchor module.
proof idea
The proof is a one-line term wrapper that applies neutrino_baseline_eq. That equation unfolds the definition of the neutrino baseline integer, rewrites via total geometric content evaluated at $D=3$, and reduces the sum to the integer $-54$ by norm_num.
why it matters
This result closes boundary item B-13 by deriving the neutrino rung from cube geometry, supplying the offset that enters the mass formula yardstick times phi to the power of (rung minus 8 plus gap of Z). It aligns with the eight-tick octave and the forcing-chain step that sets $D=3$. With zero downstream uses recorded, the declaration functions as a calibration anchor rather than an active lemma in further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.