cert_inhabited
plain-language theorem explainer
The three-factor certificate for a J-cost wavefunction-collapse threshold is inhabited: diagonal vanishing of the domain cost, nonnegativity for positive arguments, and a strictly positive canonical threshold all hold simultaneously. Anyone citing the structural GRW-style collapse package from Recognition cost would point here. The proof is a one-line term that wraps the concrete certificate object into a Nonempty witness.
Claim. The type of certificates for the J-cost wavefunction-collapse package is nonempty: there exists a witness bundling (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
This module packages a structural (not numerical) account of objective wavefunction collapse in the GRW spirit, with the collapse rate written schematically as $\lambda=J(\varphi)/(m_{\mathrm{nucleon}}\varphi^{20})$. The module status is zero sorry and zero axiom; the numerical GRW scale is off by many orders of magnitude, so the claim is only structural.
The domain cost is the local cost functional on mass/energy (or ratio) arguments built from the Recognition J-cost $J(x)=(x+x^{-1})/2-1$. The certificate structure demands three elementary properties of that cost and of the canonical threshold: vanishing on the diagonal away from zero, nonnegativity on the positive orthant, and positivity of the threshold constant used to mark collapse.
Upstream, the structure itself is the sole dependency: inhabitation is exactly the statement that some concrete record of those three propositions exists in the module.
proof idea
One-line term proof. The module already constructs a concrete certificate object satisfying the three fields of the structure. The theorem simply introduces that object as a witness for Nonempty, via the standard angle-bracket constructor. No tactics, no further lemmas.
why it matters
Closes the inhabitation obligation for the structural collapse-from-J-cost package in this module. Downstream use is not yet wired in the graph (zero used-by edges), so the immediate role is local: any later theorem that needs a collapse certificate can obtain one by classical choice or by naming the concrete witness.
In the broader Recognition framework this sits under the physics layer that treats objective collapse thresholds as consequences of J-cost geometry rather than as independent postulates. The module doc is explicit that the GRW numerical target is not matched (orders-of-magnitude gap); the theorem therefore certifies only the algebraic package (diagonal cost zero, cost nonnegative, threshold positive), not a fitted collapse rate. It does not touch the forcing chain T0–T8, the RCL identity, or the alpha band; it is a local structural seal on the cost-side hypotheses of the collapse story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.