abs_sub_le_width_of_memI
plain-language theorem explainer
The lemma shows that any two real numbers inside the same closed interval differ by at most the interval width. Certification routines that validate anchor residues and equal-Z degeneracies cite it to convert membership statements into explicit numerical bounds. The proof unfolds the two membership predicates into endpoint inequalities, applies linear arithmetic to bound the signed differences, and simplifies with the definitions of width and absolute value.
Claim. Let $I = [l, h]$ be a closed interval with $l ≤ h$. If $l ≤ x ≤ h$ and $l ≤ y ≤ h$, then $|x - y| ≤ h - l$.
background
The Recognition.Certification module defines Interval as a structure with real endpoints lo and hi satisfying lo ≤ hi. The predicate memI I x holds exactly when lo ≤ x and x ≤ hi. Width I is the difference hi minus lo. These objects package residue intervals and gap intervals inside AnchorCert objects.
proof idea
The tactic proof extracts the endpoint bounds from each membership hypothesis via two have statements. Linear arithmetic produces x - y ≤ hi - lo and y - x ≤ hi - lo. These are combined into the two-sided inequality required by abs_le. The final simpa step rewrites width and applies the absolute-value lemma.
why it matters
anchorIdentity_cert and equalZ_residue_of_cert invoke the bound to turn certificate validity into concrete inequalities on residues relative to the gap function. The lemma therefore supplies the metric control needed for the phi-ladder mass formulas and the eight-tick octave. It closes a basic numerical step in the T5–T8 forcing chain without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.