wideBand_width
plain-language theorem explainer
The width of a symmetric real band centered at x with half-width ε equals 2ε whenever ε ≥ 0. Certification and RecogSpec band lemmas cite this as the basic length identity for wide bands. The proof is a two-step unfold of Band.width and wideBand followed by ring arithmetic.
Claim. For $x,\varepsilon\in\mathbb{R}$ with $\varepsilon\ge 0$, the band $B=[x-\varepsilon,x+\varepsilon]$ satisfies $\mathrm{width}(B)=2\varepsilon$, where width is the difference of the upper and lower endpoints.
background
In RecogSpec.Bands, a Band is a real interval packaged by lower and upper endpoints. The constructor wideBand builds the symmetric interval with center $x$ and half-width $\varepsilon$, i.e. lo $= x-\varepsilon$ and hi $= x+\varepsilon$.
Width is the standard endpoint difference hi − lo (the same convention appears in Recognition.Certification for real intervals and in DeltaReal for rational intervals). The nonnegativity hypothesis on $\varepsilon$ keeps the band oriented and matches the downstream nonnegativity lemma for widths.
This module sits under RecogSpec and imports BridgeCore; the bands are the concrete interval objects used when stating sample and certification windows for recognition quantities.
proof idea
Term-mode proof by definitional simplification then algebra. Unfold Band.width and wideBand so the goal becomes $(x+\varepsilon)-(x-\varepsilon)=2\varepsilon$. Close with ring. No external lemmas are required beyond the two definitions.
why it matters
Gives the exact length of every wide band, which is the first arithmetic fact needed before nonnegativity, containment, and validity lemmas. The immediate parent is wideBand_width_nonneg, which rewrites through this identity and multiplies $2\ge 0$ by $\varepsilon\ge 0$.
In the broader RecogSpec stack these bands bound recognition observables (mass windows, coupling windows, and related certification intervals). A clean width formula keeps later sampleBandsFor and validity proofs free of ad-hoc arithmetic. It is local infrastructure rather than a forcing-chain step (T0–T8), but it is required wherever RecogSpec states interval claims about RS-native constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.