Z
plain-language theorem explainer
This abbrev supplies the canonical integer Z map for each fermion species by forwarding directly to the upstream ZOf computation. Mass-ladder and ablation researchers cite it when they require the anchor Z values without duplicating sector logic. The definition is a one-line alias that forwards to the RSBridge ZOf.
Claim. For a fermion species $f$, define $Z(f) := Z_{Of}(f)$, where $Z_{Of}$ returns the integer $q^2 + q^4$ (plus 4 for up or down quarks) from the rescaled charge $q = 6Q$ of $f$.
background
The AnchorPolicyCertified module supplies a certificate-based interface that replaces an earlier axiom for Standard-Model RG residues. It lets Lean derive per-species closeness to gap(Z) and equal-Z degeneracy bounds once external residue intervals are supplied. Species is the alias for Fermion. The integer map Z is the one used by the anchor relation (Paper 1). Upstream ZOf implements the explicit formula: for leptons it is $q^2 + q^4$, for quarks it adds the offset 4, and for neutrinos it is zero.
proof idea
One-line wrapper that applies the ZOf definition from RSBridge.Anchor.
why it matters
Z supplies the reference map for the AnchorEq predicate and the ablation_contradictions check in the Ablation module. Those results verify that alternative integerizations (drop-plus-4, drop-Q4, break-6Q) fail to preserve the certified residues. The declaration therefore closes the dependency on the mass-framework Z computation for downstream physics statements such as atomic-radii inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.