equalZ_residue_of_cert
plain-language theorem explainer
If two species share the same integer charge Z, their residue values differ by at most twice the certified epsilon width of the common gap interval. Researchers certifying mass anchors or residue bounds in the Recognition framework cite this to control degeneracy within equal-Z sectors. The proof transfers per-species Ires intervals into the shared Igap interval via validity and applies the absolute-difference width bound.
Claim. Let $C$ be an anchor certificate. Suppose $Valid(Z, F_{gap}, C)$ holds and $res(i) ∈ C.Ires(i)$ for each species $i$. Then for any species $i,j$ with $Z(i)=Z(j)$, $|res(i)-res(j)| ≤ 2·C.eps(Z(i))$.
background
AnchorCert packages per-species residue intervals Ires together with charge-wise eps widths and centers; Valid requires that each Igap interval contains both the display value Fgap(Z i) and the corresponding Ires interval. The lemma lives in Recognition.Certification and relies on interval membership and width operations to certify anchor policies for the mass ladder. Upstream, le_trans from ArithmeticFromLogic chains the interval bounds, while Z and Species from the Masses and Physics modules supply the charge map used in the hypothesis.
proof idea
Extract Ires-in-Igap containments from the Valid hypothesis. Use Z-equality to equate the two Igap intervals and apply le_trans to place both res i and res j inside the single interval Igap C (Z i). Invoke abs_sub_le_width_of_memI on that common interval to obtain the difference bound. Simplify the width of Igap to 2·eps(Z i) and finish by simpa.
why it matters
The lemma supplies the equal-Z degeneracy bound invoked by equalZ_residue_from_cert in AnchorPolicyCertified, thereby completing the certified consequences of anchor certificates. It supports residue control on the phi-ladder by limiting variation inside each charge sector and closes one step in the chain from certificate validity to mass-anchor bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.