Recognition_Closure
plain-language theorem explainer
Recognition closure at a real parameter φ is the conjunction of dimensionless inevitability and absolute inevitability: every ledger/bridge matches the explicit universal dimensionless pack, that pack is non-vacuous, and calibration against anchors is unique. Spec and verification authors cite it as the single top-level RecogSpec success predicate. The body is a two-conjunct definition, not a proof.
Claim. For a real parameter $\varphi$, recognition closure holds when both of the following are true: (i) dimensionless inevitability at $\varphi$ (every ledger and bridge matches the explicit universal dimensionless target at $\varphi$, and that target's propositional fields are actually proved), and (ii) absolute inevitability at $\varphi$ (for every ledger, bridge, and anchor triple, calibration is unique).
background
RecogSpec packages the Recognition Science claim that dimensionless observables and unit calibration are forced once the golden-ratio parameter $\varphi$ is fixed. The module sits above anchors, bands, bridge cores, and the two-outcome Born certificate, and exports a small family of inevitability predicates rather than a single monolithic theorem.
Dimensionless inevitability at $\varphi$ asserts two things: every ledger $L$ and bridge $B$ matches the explicit universal dimensionless pack $\mathrm{UD}_{\mathrm{explicit}}(\varphi)$, and the propositional fields of that pack are inhabited (not mere symbols). Absolute inevitability asserts that for every ledger, bridge, and anchor triple, calibration is unique. Both are defined as propositions in this same Spec module; certified witnesses for them live elsewhere and are intentionally kept off the certified surface when they depend on placeholder evaluators.
Recognition closure is simply the conjunction of those two predicates. It is the named top-level success condition that downstream shims and non-vacuity certificates quantify over.
proof idea
There is no proof obligation. The declaration is a definitional abbreviation: recognition closure at $\varphi$ is defined to be the conjunction of dimensionless inevitability at $\varphi$ and absolute inevitability at $\varphi$. The adjacent constructor theorem packages that conjunction via And.intro once both conjuncts are supplied as hypotheses.
why it matters
This is the RecogSpec top-level closure predicate. Downstream, recognition_closure_from_inevitabilities turns the two inevitability hypotheses into an instance of the predicate, and recognition_closure_any derives closure for arbitrary $\varphi$ from the scaffold inevitability lemmas. The verification structure RecognitionClosureNonVacuityCert then quantifies over all $\varphi$ satisfying recognition closure, so non-vacuity of the certified surface is stated relative to this definition.
In framework terms it is the RecogSpec packaging of the claim that, once $\varphi$ is fixed (the self-similar fixed point forced at T6), dimensionless matching to the universal pack and unique absolute calibration both hold. It does not itself discharge the forcing chain T0–T8 or the Recognition Composition Law; it names the success condition those layers are meant to feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.