r_boson
plain-language theorem explainer
The abbrev supplies the rung integers for electroweak bosons by direct alias to the Anchor definition. Mass modelers cite it when selecting baseline rungs for W, Z, and Higgs in the phi-ladder mass formula. It is realized as a one-line alias that inherits the pattern-matching structure from the upstream definition.
Claim. The map $r_ {boson} : String → ℤ$ sends W, Z, and H to rung value 1 and all other strings to 0.
background
AnchorPolicy defines sector-specific rung selectors that feed the mass formula yardstick ⋅ ϕ^(rung − 8 + gap(Z)). The rung selector dispatches the Electroweak case to the boson rung map. This map is supplied by the upstream Anchor.r_boson definition, whose doc-comment states it provides rung integers for electroweak bosons as a structural baseline.
proof idea
One-line wrapper that aliases the upstream pattern-matching definition from Anchor.
why it matters
The declaration supplies the electroweak rung values required by the rung and rung_sdgt selectors in the same module. Those selectors are used by predict_mass and predict_mass_sdgt to generate mass predictions on the phi-ladder. It anchors the T5 J-uniqueness and eight-tick octave structure for bosons within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.