evalToBands_c_wideBand_center
plain-language theorem explainer
A centered tolerance band around the RS speed-of-light anchor always contains that anchor, so the c-evaluation-to-bands predicate holds for the singleton list of that band. Spec and bridge authors cite it as the default witness that a ledger meets the c-band check under any nonnegative tolerance. The proof is a short refine that packages the band and applies the center-containment lemma.
Claim. For any RS units bundle $U$ and any tolerance $\mathrm{tol}\ge 0$, the singleton list consisting of the centered wide band of half-width $\mathrm{tol}$ about $U.c$ satisfies the $c$-evaluation-to-bands predicate: that band is present and contains the anchor value $U.c$.
background
RecogSpec packages numerical acceptance bands for Recognition Science constants. A wide band about a real center $x$ with nonnegative half-width $\varepsilon$ is the closed interval $[x-\varepsilon,x+\varepsilon]$. The predicate evalToBands_c asks that a supplied list of bands include some band that contains the speed-of-light anchor $U.c$ from an RSUnits bundle (the minimal Core units record with $\tau_0$, $\ell_0$, $c$ and the relation $c\cdot\tau_0=\ell_0$).
In RS-native gauge one often takes $c=1$, but the lemma is stated for arbitrary units. Interval containment is the standard $I.lo\le x\le I.hi$. Sibling facts already record that a wide band is valid, has nonnegative width, and contains its center, lower endpoint, and upper endpoint whenever $\varepsilon\ge 0$.
proof idea
Term-mode refine builds the existential witness for evalToBands_c: the band is exactly wideBand U.c tol, list membership is discharged by simp on the singleton, and containment of $U.c$ is wideBand_contains_center at $x:=U.c$ and $\varepsilon:=\mathrm{tol}$, using the hypothesis $\mathrm{tol}\ge 0$. A final simpa aligns the goal.
why it matters
This is the default c-band witness inside RecogSpec. Downstream, meetsBands_any_param quotes it to obtain MeetsBands L B [wideBand U.c tol] for any ledger and bridge: a centered tolerance band around $U.c$ is enough to pass the band check. That closes the c-channel of the specification layer without forcing a particular numerical tolerance, so verification bridges can stay parametric in tol while still anchoring to the RS units speed of light (including the native gauge $c=1$). It does not touch the forcing chain T0–T8 or the mass ladder; it is pure band bookkeeping for the constants interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.