equalZ_residue_from_cert
plain-language theorem explainer
If two fermion species share the same integer Z, their residues at the anchor differ by at most twice the certificate epsilon at that Z. Researchers certifying Standard Model mass residues would invoke this to control degeneracy without exact equality axioms. The proof is a one-line wrapper invoking the general equalZ_residue_of_cert lemma after unfolding local abbreviations for Species, Z, and Fgap.
Claim. Let $C$ be an anchor certificate with validity witness $hC$ for the fermion type, residue intervals $Ires$, and epsilon bounds $eps$. Let $resAtAnchor$ be a function such that $resAtAnchor(f)$ lies in $C.Ires(f)$ for every fermion $f$. Then for any fermions $f,g$ with $Z(f)=Z(g)$, where $Z(f)$ denotes the integer map $ZOf(f)$, we have $|resAtAnchor(f)-resAtAnchor(g)|$ at most $2$ times $C.eps(Z(f))$.
background
This module supplies machine-checkable certificates for the anchor policy in the Recognition Science mass framework, replacing an earlier axiomatic treatment of Standard Model RG residues. The local abbreviations define Species as the fermion type, $Z(f)$ as the integer $ZOf(f)$ from the anchor relation, and $Fgap(z)$ as the gap function at integer $z$. The upstream AnchorCert structure from Recognition.Certification packages per-species residue intervals $Ires$ together with charge-wise $eps$ bounds and a validity predicate Valid.
proof idea
The proof is a one-line wrapper that applies equalZ_residue_of_cert after a simpa tactic unfolds the local Species, Z, and Fgap abbreviations.
why it matters
This declaration supplies the equal-Z degeneracy bound required by the certified anchor policy interface. It closes the dependency on external residue tables for cases where species share Z values, supporting the per-species closeness results in the same module. In the Recognition framework it supports the mass formula by controlling residue variations at fixed Z without invoking the full RG flow in Lean. It touches the open question of how tightly external computations must bound the eps intervals to match observed mass ladders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.