Pith. sign in
module module high

IndisputableMonolith.RecogSpec.Bands

show as:
view Lean formalization →

Defines closed numerical bands and the predicate that an RS anchor (notably the speed parameter c) lies in at least one candidate band. Spec writers and invariance certificates import it to state absolute-layer checks without committing to a single point prediction. The module is definitional: band constructors, width nonnegativity, and elementary containment lemmas for wide and sample bands.

claimA band is a closed real interval $B=[\ell,h]$. A finite list $X$ of bands is admissible for an anchor $U$ when there exists $B\in X$ with $U.c\in B$. A wide band about a center $m$ with half-width $w\ge 0$ is $[m-w,m+w]$; sample families include the singleton list containing one such band.

background

Recognition Spec verification compares dimensionless or unit-stable anchors against predicted intervals rather than exact floats. BridgeCore supplies the minimal bridge surface: UnitsRescaled (anchor rescaling that keeps $c$ fixed), observables, bridge evaluation, and anchor invariance. Under that relation the speed parameter is invariant, so band membership for $c$ is a meaningful absolute-layer claim.

This module introduces the interval type, a list-of-bands carrier, a wide-band constructor about a center, and small lemmas that the width is nonnegative and that the center and endpoints sit inside the wide band. Sample band families (including singletons) give concrete test data for downstream certificates without fixing the full RS constant table.

proof idea

Definition module: no deep theorem chain. Band and list carriers are data. Wide-band lemmas are direct interval arithmetic (nonnegative width, center and endpoint containment, a bundled validity fact). Sample-band lemmas are list nonemptiness and singleton shape. Nothing here invokes the forcing chain or mass ladder; those enter only in importers.

why it matters in Recognition Science

Parent surface is RecogSpec.Spec, which packages RS claims in band form. BandsInvariantCert audits that the absolute-layer check "$U.c$ lies in some band of $X$" is invariant under anchor rescalings because those rescalings fix $c$. DimensionCRT and Gap45DimensionCert import the same band vocabulary while certifying dimension forcing (eight-tick structure, the 45-count, and $\mathrm{lcm}(2^D,45)=360\Rightarrow D=3$). The module is the shared interval language for those certificates, not the forcing argument itself. Landmark contact is indirect: T8/$D=3$ and the $\alpha$ band live downstream; here only the band predicate is fixed.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (25)