neutrino_baseline_eq
plain-language theorem explainer
The declaration proves that the neutrino baseline integer equals -54 on the Recognition Science phi-ladder. Researchers anchoring fermion masses via 3-cube combinatorics would cite this to fix the neutrino rung before applying the mass formula yardstick * phi^(rung - 8 + gap(Z)). The proof is a term-mode reduction that unfolds the integer definition, rewrites via total geometric content at D = 3, and normalizes the arithmetic.
Claim. The neutrino baseline integer, defined as the negative of the sum of vertices, edges, faces, passive edges, and wallpaper groups of the three-dimensional cube, equals $-54$.
background
The Baseline Rung Derivations module upgrades prior boundary assumptions to derived results using only D = 3 as input. Key sibling definitions include total_geometric_content, which sums V + E + F + E_pass + W, and total_geometric_at_D3, which evaluates the sum at three dimensions; neutrino_baseline_int is the corresponding integer for the neutrino case. Upstream results supply the cube-face structure from CubeFaceUniversality and rung conventions from Compat.Constants and NucleosynthesisTiers.
proof idea
The term-mode proof unfolds neutrino_baseline_int, rewrites with the lemma total_geometric_at_D3, and applies norm_num to reduce the expression to the constant -54.
why it matters
This result supplies the B-13 neutrino baseline value and feeds directly into the downstream theorem neutrino_rung. It completes one entry in the module's derivation table by tracing the integer solely to the combinatorics of Q₃ at D = 3, consistent with the eight-tick octave and the Recognition Science mass ladder. The derivation closes a prior scaffolding assumption without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.