r_boson
plain-language theorem explainer
This definition supplies the integer rung values for electroweak bosons on the Recognition Science phi-ladder. Mass derivations for W, Z, and Higgs particles cite it when evaluating the exponent rung - 8 + gap(Z). The body is a direct pattern match on the input string that returns 1 for the three named bosons and 0 for every other string.
Claim. The function $r_ {boson} : String → ℤ$ is given by $r_{boson}(``W'') = 1$, $r_{boson}(``Z'') = 1$, $r_{boson}(``H'') = 1$, and $r_{boson}(s) = 0$ for every other string $s$.
background
The Masses.Anchor module assembles parameter-free constants from cube geometry in D = 3 dimensions: E_total equals 12 edges, E_passive equals 11, and W equals the wallpaper-group count 17. Rung integers locate each species on the phi-ladder whose mass formula is yardstick times phi to the power (rung - 8 + gap(Z)). The sibling Z map returns an integer charge index that is zero for the Electroweak sector.
proof idea
The declaration is a pattern-matching definition. It inspects the input string and returns the constant 1 on the three boson cases, otherwise 0.
why it matters
It is invoked by the rung and rung_sdgt selectors in AnchorPolicy for the Electroweak sector, completing the dispatch that feeds the mass formula. The assignment supplies the structural baseline required by the cube-geometry derivation chain and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.