zeroWidthCert
plain-language theorem explainer
zeroWidthCert constructs an AnchorCert in which the M0 interval and all per-species residue intervals Ires(i) are singletons centered exactly at Fgap(Z(i)) and 1. Researchers deriving exact residue identities from certified anchors in Recognition Science cite it to convert interval bounds into equalities. It is realized by a direct structure construction that sets eps to zero and verifies the singleton bounds with norm_num and linarith.
Claim. Let $S$ be a species type, $Z : S → ℤ$ an integer map, and $F_{gap} : ℤ → ℝ$ a gap function. The zero-width certificate is the AnchorCert$(S)$ structure with $M_0 = [1,1]$, residue intervals $I_{res}(i) = [F_{gap}(Z(i)), F_{gap}(Z(i))]$ for each $i$, center map $z ↦ F_{gap}(z)$, and error map identically zero.
background
AnchorCert is the structure that records an interval for the base mass M0, per-species residue intervals Ires, a center function from integer charge to real value, and a non-negative error function eps. The Recognition.Certification module uses certificates of this form to certify that residues lie within prescribed intervals around the gap values. Upstream, Z is the integer map from the anchor relation in Masses.Anchor, Fgap is the abbreviation for the gap function on integers from AnchorPolicyCertified, M0 is the constant 1 in RS-native units, and Species is the inductive type of standard-model particles. This definition supplies the degenerate case of the certificate.
proof idea
Direct record construction of the AnchorCert structure. M0 is instantiated as the singleton interval [1,1] with lo_le_hi proved by norm_num. Each Ires(i) is set to the singleton [Fgap(Z i), Fgap(Z i)] with bounds verified by linarith. The center field is defined pointwise as Fgap and eps as the zero function, with eps_nonneg proved by norm_num.
why it matters
zeroWidthCert supplies the zero-width instance of AnchorCert, which is invoked by anchorIdentity_of_zeroWidthCert to obtain the exact equality res(i) = Fgap(Z(i)) and by zeroWidthCert_valid to confirm validity of the certificate. It completes the degenerate case in the anchor certification chain of Recognition Science, where the phi-ladder and J-uniqueness fix the gap values. It touches the open question of whether every physical anchor admits a zero-width certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.