cert_inhabited
plain-language theorem explainer
The RS wave-function collapse certificate is inhabited: a single package witnesses zero self-cost, nonnegative domain cost, and a positive canonical threshold. Anyone citing the structural collapse story (measurement as ledger posting via J-cost minimization) needs this existence fact. The proof is a one-line term that exhibits the concrete certificate already assembled in-module.
Claim. The type of RS wave-function collapse certificates is nonempty: there exists a record packing (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) the canonical threshold is strictly positive.
background
The module treats wave-function collapse as a recognition event: measurement equals ledger posting. Collapse is J-cost minimization to the nearest rung on the phi-ladder; the eight-tick octave fixes the minimal recognition time. No hidden variables are required. Status is structural (zero sorry, zero axiom).
The certificate structure packages three elementary cost facts used by that story. Domain cost is the local cost functional comparing a measured value to an expected rung value; it must vanish on the diagonal (exact match costs nothing) and stay nonnegative off-diagonal. The canonical threshold is the positive cutoff that separates a recognition event from noise; positivity is the only arithmetic demand at this layer.
Upstream, those three properties are exactly the fields of the certificate structure. Sibling lemmas already prove each field for the concrete domain-cost and threshold definitions imported from Constants and Cost.
proof idea
One-line term proof. The certificate structure is inhabited by exhibiting the already-constructed concrete certificate value, which itself assembles the three field proofs (diagonal vanishing, nonnegativity, and positive threshold). No further tactic work is required.
why it matters
This is the existence gate for the structural collapse theorem in the Foundation layer. Downstream consumers that need a Nonempty instance (typeclass search, certificate-passing APIs, or any proof that assumes the collapse package is available) cite this rather than re-proving the three cost facts. It sits under the module claim that collapse is J-cost minimization to the nearest rung, with the eight-tick cycle as minimal recognition time (T7 landmark) and no hidden variables. Used-by is currently empty, so the declaration is the public inhabitance witness rather than an intermediate lemma inside a larger chain. It closes the structural package: once the certificate exists, the collapse story is a pure cost-minimization statement rather than an extra dynamical postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.