anchorIdentity_cert
plain-language theorem explainer
The lemma shows that if a valid anchor certificate bounds each species residue inside its certified interval, then the residue differs from the gap function at the charge by at most twice the certificate epsilon. Mass-spectrum calculations that replace exact anchor identities with interval certificates cite this result. The proof fixes a species, chains the residue into the gap interval by bound transitivity, applies the width-difference lemma, and simplifies the gap width to twice epsilon.
Claim. Let $C$ be an anchor certificate for species type $S$, with validity $V(Z,F,C)$ where $Z:S→ℤ$ and $F:ℤ→ℝ$. If $r_i$ lies in the residue interval of $C$ for each $i∈S$, then $|r_i - F(Z(i))| ≤ 2⋅ε_C(Z(i))$ for every $i$.
background
An anchor certificate is a structure containing a positive base-mass interval, per-species residue intervals, a center map, and a non-negative epsilon map indexed by integer charge. Validity of the certificate with respect to charge map $Z$ and gap function $F$ requires the gap values to lie inside the corresponding gap intervals, the residue intervals to be contained inside those gap intervals, and the base-mass interval to be positive. The lemma sits inside the Certification module that supplies certified replacements for the anchor identities of the mass framework. It relies on order transitivity from the arithmetic foundation and on the gap-function definition imported from the certified anchor policy.
proof idea
The tactic proof fixes species $i$, pulls membership of $F(Z(i))$ in the gap interval from validity, records the inclusion of the residue interval inside the gap interval, and constructs membership of the given residue in the gap interval by applying bound transitivity to the lower and upper endpoints. It invokes the sibling lemma that bounds absolute difference by interval width, proves the gap width equals twice epsilon by simplification and ring, and rewrites the bound.
why it matters
The result supplies the certified inequality form of the anchor identity that is invoked by the parent theorem anchor_identity_from_cert in the AnchorPolicyCertified module. It allows external certificates to replace exact gap-function identities inside mass-ladder computations. In the Recognition framework it supports the transition from exact identities to interval-certified residues at the anchor points, consistent with the phi-ladder mass formula and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.