anchorIdentity_of_zeroWidthCert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish existence or validity of any zero-width certificate.
- Does not apply when the supplied certificate has positive width.
- Does not extend the identity beyond the integer anchors Z(i).
- Does not address species outside the defined inductive type.
formal statement (Lean)
131lemma anchorIdentity_of_zeroWidthCert {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ)
132 (res : Species → ℝ) (hres : ∀ i, memI ((zeroWidthCert Z Fgap).Ires i) (res i)) :
133 ∀ i : Species, res i = Fgap (Z i) := by
proof body
Term-mode proof.
134 intro i
135 have h := hres i
136 dsimp [zeroWidthCert, memI] at h
137 exact le_antisymm h.2 h.1
138
139end
140
141end Certification
142end Recognition
143end IndisputableMonolith