evalToBands_c_sampleBandsFor
plain-language theorem explainer
For any real x, the sample band collection around x certifies the speed of light when anchors are τ₀=1, ℓ₀=x, and c=x. RecogSpec verifiers use this to check light-cone band membership under matching anchors. The proof exhibits the wide band of half-width 1 and applies center containment.
Claim. For every real $x$, the speed-of-light band-evaluation predicate holds on the sample band collection at $x$, under anchors $\tau_0=1$, $\ell_0=x$, $c=x$ (which satisfy the light-cone identity $\ell_0=c\cdot\tau_0$).
background
Recognition Science fixes fundamental units τ₀ (tick duration), ℓ₀ (voxel length), and c linked by the light-cone identity ℓ₀ = c · τ₀. In native units one often takes c = 1 with ℓ₀ = τ₀, but the RecogSpec layer parameterizes anchors so band checks remain meaningful under rescaling.
A band is an interval used to certify that a predicted constant lies in an acceptable window. The wide band at center x with parameter ε is the standard interval witness; the sample collection for x is the singleton of that wide band at ε = 1. The speed-of-light evaluation predicate asks that c belong to some band in a supplied collection, given a record of anchors that already satisfies the light-cone identity.
Upstream, the identity c · τ₀ = ℓ₀ is proved by unfolding the native definitions (c, tick, ℓ₀). The center-containment fact for wide bands supplies the membership step used here.
proof idea
Term-mode refine builds an existential witness: the wide band centered at x with ε = 1. The first subgoal (membership of that band in the sample collection) closes by simp on the sample definition. The second (that x lies in the band) is discharged by simpa from the wide-band center-containment lemma at ε = 1, with the positivity side condition settled by norm_num. The anchor record is well-formed because c · τ₀ = ℓ₀ reduces by simp when τ₀ = 1 and ℓ₀ = c = x.
why it matters
This is a convenience lemma inside RecogSpec.Bands: it shows that the canonical sample bands around a candidate value of c succeed under the matching light-cone anchors. It sits on the verification bridge that checks RS-native constants against band windows, tying to the light-cone identity and the native choice c = 1 (here generalized to arbitrary x). No downstream consumers are recorded yet; the lemma is infrastructure for band-evaluation tests rather than a step in the T0–T8 forcing chain. It does not touch mass rungs, α, or the eight-tick octave directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.