Z
plain-language theorem explainer
Z supplies the integer map from fermion species to their anchor Z values. Ablation studies and atomic-radii comparisons cite it when testing residue stability under modified charge maps. The definition is a direct one-line alias to the upstream ZOf computation on tildeQ and sector.
Claim. $Z : \text{Fermion} \to \mathbb{Z}$ is given by $Z(f) = Z_{\text{Of}}(f)$, where $Z_{\text{Of}}$ returns $4 + q^2 + q^4$ for up/down quarks, $q^2 + q^4$ for charged leptons, and 0 for neutrinos with $q = \tilde{Q}(f)$.
background
The AnchorPolicyCertified module supplies a certificate-based interface that replaces an asserted global RG-residue axiom with externally validated interval bounds. Species is the alias for Fermion. ZOf (from both Masses.RSBridge.Anchor and RSBridge.Anchor) is the integer map used by the anchor relation: it applies the sector-dependent formula on tildeQ.
Upstream Z in Masses.Anchor is the integer map used by the anchor relation (Paper 1). The local setting avoids embedding SM RG kernels inside Lean and instead exposes per-species closeness to gap(Z) once certified bounds are supplied.
proof idea
One-line wrapper that applies the ZOf definition from the RSBridge.
why it matters
Z feeds the AnchorEq predicate and the ablation_contradictions test that rules out modified Z maps. It also appears in atomic-radii lemmas. The alias closes the certified interface described in the module doc, linking the mass-ladder Z computation to downstream checks without introducing an equality axiom for RG residues.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.