neutrino_baseline_int
plain-language theorem explainer
The neutrino baseline integer rung is defined as the negation of the total geometric content of the three-cube. Researchers deriving mass ladders from Recognition Science geometry cite this integer as the fixed offset for neutrino rungs. The definition is realized as a direct cast of the natural-number sum to an integer followed by negation.
Claim. The neutrino baseline integer rung is defined by $n = -(V + E + F + E_{pass} + W)$ where the sum is the total geometric content of the three-dimensional cube and equals 54.
background
This definition sits inside the module that upgrades boundary assumptions about rung integers to derived status using only the combinatorics of the 3-cube Q_3. The upstream total geometric content sums the independent structural integers: cube vertices, cube edges, cube faces, passive field edges, and wallpaper groups. Its doc-comment states: Total geometric content of Q_D: sum of all independent structural integers. At D = 3 the sum is 8 + 12 + 6 + 11 + 17 = 54, so the baseline integer is -54.
proof idea
One-line definition that applies total_geometric_content at the fixed dimension D, casts the result to an integer, and negates it.
why it matters
The definition supplies the B-13 neutrino baseline that is invoked by the equality theorem neutrino_baseline_eq and the rung statement neutrino_rung. It closes the derivation of the neutrino offset from the single input D = 3, consistent with the eight-tick octave and the forcing of three spatial dimensions. The module thereby converts prior boundary assumptions into derived quantities inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.