memI
plain-language theorem explainer
The predicate memI asserts that a real number lies between the lower and upper endpoints of a given closed interval. Researchers certifying residue bounds in the Recognition framework cite it to express that computed values satisfy interval constraints from certificates. The definition expands directly to the conjunction of two inequalities, enabling immediate use with linear arithmetic and simplification tactics.
Claim. Let $I$ be a closed interval with endpoints $I.lo$ and $I.hi$ satisfying $I.lo ≤ I.hi$, and let $x ∈ ℝ$. The predicate holds if and only if $I.lo ≤ x ≤ I.hi$.
background
The module defines Interval as a structure with real endpoints lo and hi together with the proof lo ≤ hi. This supplies the closed interval type used for residue certification. An upstream structure in Numerics.Interval.Basic provides the analogous construction over rationals, while the local version works directly over reals to interface with residue computations.
proof idea
The declaration is a direct definition that unfolds to the conjunction of the two endpoint inequalities. No lemmas are applied; it serves as the primitive predicate for all subsequent interval reasoning.
why it matters
This predicate appears in the hypotheses of anchor_identity_from_cert and equalZ_residue_from_cert, where it encodes that residues lie inside certified bands around gap(Z). It thereby converts abstract interval certificates into concrete bounds on anchor identities and equal-Z degeneracies. The definition closes the interface between certified data and the Recognition framework's residue calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.