anchor_identity_from_cert
plain-language theorem explainer
If a certificate C validates the residue intervals for each fermion species at the anchor, then the residue of every species lies within twice the certificate's per-Z epsilon of the closed-form gap evaluated at Z(f). Researchers deriving mass spectra or bounding RG flow residues in the Recognition framework would invoke this result to obtain machine-checked inequalities from external data. The proof reduces directly to the generic anchorIdentity_cert lemma by unfolding the module's abbreviations for the species type, the Z map, and the gap.
Claim. Let $C$ be an anchor certificate for fermion species. Suppose $C$ is valid with respect to the integer map $Z$ and the gap function $Fgap$. If a residue function $resAtAnchor$ satisfies $resAtAnchor(f) ∈ Ires(f)$ for every species $f$, then $|resAtAnchor(f) - Fgap(Z(f))| ≤ 2 · C.eps(Z(f))$ for all $f$.
background
This module supplies certified consequences for anchor policies in physics, replacing an axiomatic assumption on Standard-Model RG residues with an externally supplied certificate of intervals. The local definitions are: Species is the type of fermions; Z maps each species to its integer value via ZOf; Fgap is the gap function applied to an integer. The module states that it derives per-species closeness to gap(Z) and equal-Z degeneracy bounds without assuming equality.
proof idea
The proof is a one-line wrapper that applies the generic anchorIdentity_cert lemma. It uses simpa to unfold the local abbreviations Species, Z, and Fgap before invoking the upstream result with the supplied certificate validity and residue membership hypotheses.
why it matters
This theorem supplies one of the main certified consequences listed in the module, allowing derivation of residue bounds from external certificates rather than axioms. It supports the anchor identity in the mass framework by providing a machine-checkable path from certified data to closeness inequalities. In the Recognition Science setting it contributes to the certified interface for physics quantities without requiring RG integration inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.