wideBand_width_nonneg
plain-language theorem explainer
Whenever ε ≥ 0, the symmetric real band centered at x with half-width ε has nonnegative width. Interval-certificate and sample-band arguments in RecogSpec cite this as the basic nonnegativity fact for wide bands. The proof rewrites width as 2ε via the companion identity, then multiplies the nonnegativity of 2 and ε.
Claim. For all real $x$ and $\varepsilon$ with $\varepsilon \ge 0$, if $B$ is the closed interval $[x-\varepsilon,\,x+\varepsilon]$, then its width satisfies $0 \le \mathrm{width}(B)$. Equivalently, $0 \le (x+\varepsilon)-(x-\varepsilon)$.
background
RecogSpec.Bands packages real intervals used as recognition-specification certificates. A band is an interval with real endpoints lo and hi; its width is the difference hi - lo, matching the real interval width used in Recognition.Certification (and the rational analogue in DeltaReal).
The constructor wideBand x ε builds the symmetric band with center $x$ and half-width $\varepsilon$, i.e. the closed interval $[x-\varepsilon,,x+\varepsilon]$. The sibling identity wideBand_width states that, under the hypothesis $\varepsilon \ge 0$, this band has width exactly $2\varepsilon$. The present lemma is the nonnegativity corollary of that identity.
Local setting: elementary real-interval bookkeeping that underpins later band-validity and sample-band lemmas in the same module.
proof idea
One short tactic proof. First apply the companion lemma wideBand_width to obtain (wideBand x ε).width = 2 * ε under 0 ≤ ε. Record 0 ≤ (2 : ℝ) by norm_num, then 0 ≤ 2 * ε by mul_nonneg. Finish by rewriting the width equality into the goal (simpa).
why it matters
Nonnegativity of band width is a prerequisite for treating wide bands as well-formed certificate intervals in RecogSpec. Among module siblings it sits next to wideBand_width, the containment facts (wideBand_contains_center, wideBand_contains_lo, wideBand_contains_hi), and wideBand_valid; those lemmas assemble the basic hygiene of symmetric bands before sample-band constructions (sampleBandsFor and its nonempty/singleton facts).
No external used_by edges are recorded yet, so the lemma is presently infrastructure rather than a cited step in a forcing-chain or constants proof. It does not touch T0–T8, RCL, or the φ-ladder; it only keeps the RecogSpec interval layer honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.