Pith. sign in
module module high

IndisputableMonolith.RecogSpec.Bands

show as:
view Lean formalization →

Defines closed real intervals (bands) and the membership check that the RS speed anchor c lies in at least one candidate band. Spec and verification certificates import these structures when packaging dimensionless c-band invariance and dimension-forcing audits. The module is definitional: width, containment, and sample-band lemmas are elementary interval facts.

claimA band is a closed interval $[\ell,h]\subset\mathbb{R}$ with $\ell\le h$. Units $U$ meet a band list $X$ when $\exists b\in X$ with $U.c\in b$. Wide bands are symmetric windows about a center; sample band families supply concrete finite lists of such windows.

background

RecogSpec packages the Recognition Science certified surface: numerical anchors (including the speed parameter $c$) must sit inside declared tolerance windows before bridge-level claims are accepted. This module supplies the interval datatype and the existential membership predicate used by that surface.

Upstream, BridgeCore fixes the minimal invariance layer: UnitsRescaled rescales anchors while keeping $c$ fixed, and observables are required to be anchor-invariant. Band checks are therefore meaningful only if they talk about quantities that survive that rescaling; $c$ is the canonical such quantity.

Sibling definitions introduce a single band, lists of bands, a wide band about a center (with nonnegative width and containment of center, lo, and hi), and a sample family sampleBandsFor that is nonempty and, in the singleton case, exactly one band.

proof idea

Definition module. Band and Bands are data; wideBand builds a symmetric interval and the width/containment lemmas unfold the interval arithmetic. sampleBandsFor constructs a concrete list; nonemptiness and singleton lemmas are direct from that constructor. No deep forcing or physics proof lives here.

why it matters in Recognition Science

Feeds RecogSpec.Spec as the band vocabulary of the certified RS surface. BandsInvariantCert packages the audit that the absolute-layer check

evalToBands_c U X := ∃ b ∈ X, Band.contains b U.c

is invariant under UnitsRescaled, because rescalings keep $c$ fixed. DimensionCRT and Gap45DimensionCert import the same band layer when certifying dimension forcing: eight-tick structure plus Fibonacci yield 45, and $\mathrm{lcm}(2^D,45)=360$ forces $D=3$. Without a shared band type, those certificates could not state numerical windows uniformly.

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)