canonicalZBands
plain-language theorem explainer
Canonical Z bands are supplied as the integer list 24, 276, 1332 for down quarks, up quarks, and leptons. Mass phenomenology papers cite these when assigning phi-ladder rungs via the anchor relation. The entry is a direct definition with no reduction steps.
Claim. The canonical Z-bands are the integers $24$, $276$, and $1332$, assigned respectively to the down-quark sector with $Q = -1/3$, the up-quark sector with $Q = +2/3$, and the lepton sector with $Q = -1$.
background
In the Single-Anchor RG Policy module the Z values label fermion sectors under the anchor relation. Upstream, the integer map Z (Paper 1) computes Z(sector, Q) as an offset of 4 for quarks plus (6Q)^2 + (6Q)^4; the companion ZOf extracts the effective charge tildeQ from a Fermion and applies the same sector formula. The module reuses Constants.phi and RSBridge.Anchor to state the RG residue hypothesis f_i(μ*) = gap(ZOf i).
proof idea
Direct definition that assigns the constant list [24, 276, 1332] with no lemmas or tactics.
why it matters
The definition fixes the three Z values referenced in the single-anchor mass framework for the main fermion classes. It supplies the concrete inputs that enter the gap function and subsequent phi-ladder mass formulas. It leaves open the derivation of these integers from the forcing chain T0-T8 rather than phenomenological assignment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.