wideBand_valid
plain-language theorem explainer
If the half-width ε is nonnegative, the symmetric real interval around a center x is a well-formed band: its lower endpoint does not exceed its upper. Containment lemmas for the band endpoints cite this. The proof unfolds the band and validity definitions, then finishes by linear arithmetic.
Claim. For all real numbers $x$ and $\varepsilon$ with $\varepsilon \ge 0$, the band with endpoints $x-\varepsilon$ and $x+\varepsilon$ is valid (lower endpoint $\le$ upper endpoint).
background
In RecogSpec.Bands, a band is a closed real interval packaged as a pair of endpoints (lo, hi). Validity of a band is the elementary well-formedness condition that the lower endpoint does not exceed the upper; without it, containment and width lemmas are meaningless.
The constructor wideBand x ε builds the symmetric interval with center $x$ and half-width $\varepsilon$, i.e. endpoints $x-\varepsilon$ and $x+\varepsilon$. Nonnegativity of $\varepsilon$ is exactly the hypothesis needed so that this construction lands in the valid locus.
The module sits under RecogSpec and feeds interval bookkeeping used by recognition certificates and bridge verification (via BridgeCore). The certificate-level Valid structure in Recognition.Certification is a separate, richer notion (positive mass floor, gap and residual interval nesting); here only the band-level predicate is at stake.
proof idea
Term-mode proof by simplification and arithmetic. Unfold the band-validity predicate and the definition of the symmetric band, which reduces the goal to $x-\varepsilon \le x+\varepsilon$. Discharge that inequality from $\varepsilon \ge 0$ with linarith. No external lemmas beyond the definitions.
why it matters
This is the well-formedness gate for every symmetric tolerance band in RecogSpec. Downstream, wideBand_contains_lo and wideBand_contains_hi apply it once each, via the generic facts that a valid band contains its own endpoints, so the constructed lower and upper bounds are members of the band.
Those containment facts underwrite sample-band constructions and any later check that a predicted display value or residual sits inside a wide tolerance window. In the broader Recognition stack, bands are the interval carriers for gap and residual certificates; a proved validity lemma keeps that layer free of sorry and of hidden endpoint-order assumptions. It does not itself touch the forcing chain (T5–T8), RCL, or the alpha band numerics; it is pure interval hygiene beneath those claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.