absolute_layer_any
plain-language theorem explainer
Absolute-layer acceptance is exactly the conjunction of unique calibration to the anchors and satisfaction of the display bands. Anyone citing the RecogSpec absolute layer uses this as the canonical bundled witness. The proof is a one-line pairing of the two hypotheses.
Claim. For any ledger $L$, bridge $B$, anchors $A$, and bands $X$, if there is a unique units pack calibrated to $A$ and some units pack meets the band checks in $X$, then both hold simultaneously: unique calibration and band acceptance.
background
In RecogSpec, the absolute layer is the top acceptance criterion for a recognition ledger against physical anchors and numerical bands. UniqueCalibration asserts existence of a unique RSUnits pack calibrated to the given anchors (forcing the calibration ratio). MeetsBands asserts existence of some units pack for which the concrete band checker evalToBands_c succeeds.
A ledger is a double-entry collection of recognition events; a bridge maps native ledger data to display and observable objects with a commuting observation law. Anchors fix the laboratory scale; bands encode the allowed windows for RS-derived constants (including the fine-structure band near $137$).
This declaration does not derive either conjunct. It only names their conjunction as the absolute-layer acceptance predicate used elsewhere in the module.
proof idea
Term-mode pairing: apply And.intro to the two hypotheses. No lemmas, no rewriting, no case analysis. The conclusion is definitionally the product of the two input propositions.
why it matters
Gives a single named shape for absolute-layer acceptance so downstream constructors can return one object rather than two loose witnesses. The immediate consumer is absolute_layer_from_eval_invariant, which builds the absolute-layer witness from a concrete band evaluation together with an admissible units rescaling: it refines through this theorem after establishing unique calibration and band success.
In the broader Recognition stack this sits above the forcing chain (T5 J-cost, T6 $\varphi$, T7 eight-tick, T8 $D=3$) and the RS-native constants ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, $\alpha^{-1}$ in the stated band). It does not itself force those values; it packages the calibration-plus-bands gate that a full RecogSpec certificate must pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.