anchorIdentity_of_zeroWidthCert
plain-language theorem explainer
If a residue map lies inside the zero-width intervals supplied by a zero-width certificate, then each residue equals the gap function evaluated at the integer anchor Z(i). Researchers certifying mass spectra or anchor relations would cite this to convert interval bounds into exact point identities. The proof is a one-line wrapper that unfolds the certificate and interval membership, then applies antisymmetry to the resulting pair of inequalities.
Claim. Let $S$ be a set of species, $Z: S → ℤ$ the anchor map, $F_{gap}: ℤ → ℝ$ the gap function, and $r: S → ℝ$ a residue function. If for every species $i$ the value $r(i)$ belongs to the zero-width interval $I_{res}(i)$ generated by the zero-width certificate for $Z$ and $F_{gap}$, then $r(i) = F_{gap}(Z(i))$ for all $i ∈ S$.
background
The Recognition.Certification module encodes certificates that bound per-species residues relative to integer anchors. A zero-width certificate produces intervals of vanishing width centered exactly at the gap values. The predicate memI asserts that a real number lies inside one of these intervals. The gap function is the abbrev Fgap(z) := gap(z), which supplies the closed-form target for each integer anchor Z(i).
proof idea
The proof is a direct term-mode reduction. After introducing the species index i, obtain the membership fact hres i. Unfolding zeroWidthCert and memI converts membership into a pair of inequalities. Antisymmetry of the order relation (le_antisymm) applied to the lower and upper bounds then forces equality because the interval width is zero.
why it matters
This lemma converts a zero-width certificate into an exact anchor identity, supplying the pointwise equality needed for certified mass ladders. It supports the anchorIdentity_cert construction and the certified consequences in AnchorPolicyCertified. In the Recognition framework it reinforces the phi-ladder mass assignments by guaranteeing that certified residues match gap(Z) exactly, closing the interval-to-identity step in the forcing chain from T5 onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.