wideBand_contains_lo
plain-language theorem explainer
For any center x and half-width ε ≥ 0, the lower endpoint of the symmetric real band [x−ε, x+ε] lies inside that band. Spec and numerics authors cite it when discharging endpoint membership for wide tolerance intervals. The proof is a one-line wrapper through band validity and the generic lower-endpoint containment lemma.
Claim. Let $x,\varepsilon\in\mathbb{R}$ with $\varepsilon\ge 0$. Write $B=[x-\varepsilon,x+\varepsilon]$. Then $B$ contains its own lower endpoint: $x-\varepsilon\in B$, i.e. $x-\varepsilon\le x-\varepsilon\le x+\varepsilon$.
background
In RecogSpec.Bands, a Band is a closed real interval given by endpoints lo and hi, with width hi − lo. Validity means the endpoints are ordered (lo ≤ hi). The constructor wideBand x ε builds the symmetric tolerance band with center $x$ and half-width $ε$, so lo = x − ε and hi = x + ε.
Containment of a real in a band is the standard closed-interval predicate: lo ≤ y ≤ hi (aligned with the interval contains notion used elsewhere in the numerics stack). The sibling lemma wideBand_valid records that nonnegativity of $ε$ forces the wide band to be valid, which is the only hypothesis needed for endpoint membership.
proof idea
One-line wrapper. Apply the generic fact that every valid band contains its lower endpoint (Band.contains_lo_of_valid) to wideBand x ε, discharging validity by wideBand_valid at the given hε : 0 ≤ ε. No further arithmetic is unfolded at the call site.
why it matters
Local infrastructure in the RecogSpec band layer used to certify that tolerance intervals around Recognition-spec targets are well-formed closed sets. Downstream consumers of wide bands (sample band packs, bridge checks against BridgeCore) need endpoint membership as a trivial but repeatedly invoked fact; this lemma packages it so callers do not re-prove x−ε ≤ x−ε ≤ x+ε from validity each time.
It does not itself touch the forcing chain (T5–T8), the Recognition Composition Law, or the φ-ladder mass formula. It is pure interval bookkeeping that keeps RecogSpec band reasoning short and uniform. No used_by edges are recorded yet; the lemma is available for any proof that must mention the lower edge of a wide band explicitly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.