AnchorCert
plain-language theorem explainer
AnchorCert packages an interval for the base mass M0, a map from species to residue intervals, and charge-indexed center and non-negative width functions that define gap intervals. Researchers deriving certified residue bounds or equal-Z degeneracy statements in the Recognition mass framework cite this structure when stating certificate assumptions. The declaration is a plain structure definition with no computational reduction or lemmas.
Claim. An anchor certificate over a species type consists of a closed interval $M_0$, a function assigning to each species a closed residue interval, a center map from integers to reals, and a non-negative error map from integers to reals.
background
The Recognition.Certification module supplies interval-based data carriers for anchoring mass and residue calculations. Interval is the structure with real endpoints lo and hi satisfying lo ≤ hi. Species is the inductive type whose constructors are fermion, W, Z, and H. Upstream M0 is the constant 1. The center and eps fields together define the Igap intervals that appear in validity predicates.
proof idea
This is a structure definition that directly records the five fields M0, Ires, center, eps, and the non-negativity condition on eps. No lemmas or tactics are invoked; the declaration serves only as the data carrier for later Valid and identity statements.
why it matters
AnchorCert supplies the data type consumed by anchorIdentity_cert, equalZ_residue_of_cert, and the Physics.AnchorPolicyCertified theorems that convert certificate assumptions into residue closeness bounds. It occupies the certification layer that supports anchor-policy results and the broader Recognition forcing chain from T5 J-uniqueness through mass-ladder constructions. It leaves open how the eps widths are obtained from first-principles phi-ladder data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.