wideBand
plain-language theorem explainer
A closed real interval centered at a point x with half-width ε, packaged as a Band. Anyone building tolerance bands for RS constants (c, α, masses) cites this constructor. The body is a one-line structure literal: lower endpoint x−ε, upper endpoint x+ε.
Claim. For real numbers $x$ and $\varepsilon$, the wide band around $x$ of half-width $\varepsilon$ is the interval band with lower endpoint $x-\varepsilon$ and upper endpoint $x+\varepsilon$.
background
The RecogSpec.Bands module packages numerical acceptance windows for Recognition Science constants. A Band is a pair of reals (lo, hi) with width hi − lo; collections of bands are the targets that bridge evaluators check against measured or derived values.
wideBand is the canonical centered constructor: fix a center and a tolerance, obtain the symmetric interval. Downstream sample helpers hard-code unit tolerance (ε = 1) around a candidate anchor, and the c-band evaluator asks whether the RS speed-of-light constant lands inside some band of a supplied list.
Upstream, DeltaReal.lo only supplies lower endpoints of protocol approximations as reals; it is not used in the body of this definition, but sits in the same real-endpoint vocabulary the band layer consumes.
proof idea
Pure definition: the structure literal sets lo := x − ε and hi := x + ε. No proof obligations. Sibling lemmas (wideBand_contains_center, wideBand_width_nonneg, wideBand_valid) discharge the elementary interval facts once a nonnegativity hypothesis on ε is supplied.
why it matters
This is the workhorse band constructor for the RecogSpec layer. sampleBandsFor x is the singleton list [wideBand x 1]; lemmas center_in_sampleBandsFor, center_in_each_sample, and evalToBands_c_sampleBandsFor all reduce containment of the center to wideBand_contains_center at ε = 1. The c-invariance and c-wideBand-center lemmas use the same constructor to certify that RSUnits.c always sits inside a centered tolerance band, independent of units rescaling.
In the broader RS stack this is scaffolding for numerical bridge checks (α-band, mass ladder windows, c-fix), not a forcing-chain step. It does not itself constrain φ, the eight-tick octave, or D = 3; it only supplies the interval type those later checks inhabit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.