Igap
plain-language theorem explainer
Igap supplies the gap interval for each integer charge z from the center and eps fields of an AnchorCert. Researchers certifying residue bounds or anchor identities in Recognition Science invoke it to obtain the concrete interval that must contain Fgap(z). The definition is a direct record constructor that subtracts and adds eps(z) around center(z), with the ordering proved by a one-line linarith application of eps_nonneg.
Claim. Let $C$ be an anchor certificate and $z$ an integer charge. The gap interval $I(C,z)$ is the closed real interval $[c(z) - e(z), c(z) + e(z)]$, where $c$ and $e$ denote the center and eps fields of $C$.
background
In Recognition.Certification an AnchorCert packages a positive mass interval M0, per-species residue intervals Ires, and charge-indexed center and eps functions together with the proof that eps is nonnegative. The Interval structure is simply a pair of reals lo, hi with the ordering lo ≤ hi. Igap(C,z) is the interval that the Valid predicate requires to contain the gap function value Fgap(z) for every species whose charge is z.
proof idea
The definition builds the Interval record by direct substitution of center(z) - eps(z) for lo and center(z) + eps(z) for hi. The single ordering obligation is discharged by a one-line linarith tactic that applies the eps_nonneg hypothesis already present in the AnchorCert structure.
why it matters
Igap supplies the concrete interval object demanded by the Valid structure and by the downstream lemmas anchorIdentity_cert and equalZ_residue_of_cert. It therefore bridges the abstract certificate fields to the inequality statements used in mass anchoring. Within the Recognition framework this supports discrete phi-ladder assignments by furnishing explicit bounds around gap-function values at each integer charge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.