IndisputableMonolith.Verification.BandsInvariantCert
Verification module that packages an invariance certificate for Recognition Spec prediction bands (interval constraints on dimensionless observables such as the fine-structure window). Auditors of the RS constant ladder cite it when checking that band endpoints are stable under the certified rewrite rules. The module is a thin cert wrapper over RecogSpec.Bands; it does not reprove band widths.
claimA verification certificate asserting that the Recognition Spec prediction bands $B$ (closed intervals on dimensionless RS observables, including the $\alpha^{-1}$ window) are invariant under the allowed band-preserving maps of the spec, i.e. if $x \in B$ then the certified image remains in $B$.
background
Recognition Science fixes dimensionless constants on a $\varphi$-ladder with explicit numerical windows. The primer band for the inverse fine-structure constant is $\alpha^{-1} \in (137.030, 137.039)$ in RS-native units ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$). RecogSpec.Bands is the upstream specification module that defines those interval objects and their endpoints.
Verification modules sit above the spec: they do not invent new physics, they expose Lean-checkable certificates that the stated intervals are closed under the rewrites the framework permits. BandsInvariantCert is the local home for that invariance claim in the Verification domain.
No additional forcing-chain landmarks (T5 J-cost, T6 $\varphi$, T7 eight-tick, T8 $D=3$) are redefined here; the module only consumes the band data from RecogSpec.
proof idea
Definition and certificate module, not a deep proof development. It imports Mathlib and IndisputableMonolith.RecogSpec.Bands, then exposes a named certificate object (BandsInvariantCert) that packages the invariance statement for downstream checkers. Any proof content is expected to be a thin wrapper or reflexivity-style discharge against the band definitions already fixed upstream; there is no independent derivation of band widths in this file.
why it matters in Recognition Science
Earns its place as a Verification-layer gate: external audits of RS numerical claims need a single named certificate that prediction bands do not drift under certified transformations. It sits directly on RecogSpec.Bands and is the natural hook for any later global consistency theorem that aggregates band certificates (mass ladder windows, $\alpha$ band, Berry threshold $\varphi^{-1}$, etc.).
Used-by edges are currently empty in the mirror graph, so this module is a leaf cert rather than an intermediate lemma. It still matters for the verification story: without an explicit bands-invariant certificate, the $\alpha^{-1}$ window and sibling intervals would be only documentary, not machine-checked invariants.
scope and limits
- Does not derive band endpoints or widths from the forcing chain (T0–T8).
- Does not prove physical correctness of $\alpha^{-1}$ or other constants, only invariance of stated intervals.
- Does not define the band data structures; those live in RecogSpec.Bands.
- Does not supply downstream consumers yet (used_by is empty in the graph).