absolute_layer_from_eval_invariant
plain-language theorem explainer
From a concrete band-check on one RS units pack, together with a units-rescaling relation to another pack, one obtains the absolute-layer pair: unique calibration to the anchors and band acceptance. Verification and RecogSpec authors cite this when closing the absolute layer from an evaluated checker rather than from an abstract witness. The proof transports the evaluation across the rescaling and hands both halves to the absolute-layer constructor.
Claim. Let $L$ be a ledger, $B$ a bridge on $L$, $A$ anchors, and $X$ bands. Let $U,U'$ be RS unit packs related by units rescaling. If $U$ passes the concrete band evaluation against $X$, then there exists a unique RS units pack calibrated to $A$, and there exists some RS units pack that meets the bands $X$.
background
RecogSpec packages the absolute layer of Recognition Science as two witnesses on a ledger $L$ and bridge $B$. Unique calibration asserts a unique RS units pack matching the anchors $A$ (forcing the calibration ratio). Band acceptance asserts existence of some units pack for which the concrete band checker succeeds against $X$.
RS units are the minimal triple $(\tau_0,\ell_0,c)$ with $c,\tau_0=\ell_0$. Units rescaling relates two such packs by an overall scale change that preserves the physical ratios the checker cares about. The evaluation predicate evalToBands_c is the concrete numeric check that a fixed units pack lands inside the prescribed bands.
The local setting is the RecogSpec specification module: anchors fix the calibration target; bands fix the acceptance window; the absolute layer is their conjunction as a Prop-level witness rather than a numeric certificate.
proof idea
Term-mode proof via refine on the absolute-layer constructor absolute_layer_any, which expects unique calibration and band acceptance separately.
Unique calibration is supplied immediately by uniqueCalibration_any (independent of the evaluation hypothesis). For band acceptance, evalToBands_c_invariant transports the given evaluation from $U$ to the rescaled pack $U'$ along the units-rescaling hypothesis. The transported evaluation is then fed to meetsBands_any_of_eval, which turns a concrete successful check on $U'$ into the existential MeetsBands witness.
why it matters
Closes the absolute-layer witness from a runnable checker rather than from an abstract existence claim: once any units pack passes the band evaluation, and packs are identified up to rescaling, both unique calibration and band acceptance are available as Props. That is the RecogSpec bridge between numeric evaluation and the specification-level absolute layer (doc: "Construct the absolute-layer witness from a concrete checker").
No downstream consumers are recorded yet in the graph; the declaration sits at the leaf of the Spec module's absolute-layer API, alongside siblings such as Calibrated, UniqueCalibration, MeetsBands, and the anchor-transport lemmas. In the broader framework it supports the claim that RS units and band windows (including the $\alpha^{-1}$ band near $137$) can be certified from a single evaluated pack once rescaling invariance is in hand. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those live upstream in the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.