cert_inhabited
plain-language theorem explainer
The deep recognition-Heisenberg certificate type is inhabited: a concrete pack of the three structural cost and threshold facts exists. Anyone citing the structural HUP derivation in this module uses this existence fact. The proof is a one-line term witness via the prebuilt cert instance.
Claim. The type of certificates packing (i) vanishing of the domain cost on the diagonal $r\neq 0$, (ii) nonnegativity of the domain cost for positive mass and energy arguments, and (iii) positivity of the canonical threshold, is nonempty.
background
This module derives a recognition form of the Heisenberg bound from the J-cost: $\Delta_J\cdot\Delta_\sigma\ge\hbar_R/2$ with $\hbar_R=J(\phi)\hbar$, as a structural theorem (no sorry, no axioms). The domain cost is the local cost functional on mass/energy-like arguments; the canonical threshold is the positive scale that appears in the bound.
The certificate structure packages three elementary properties: the domain cost vanishes when its two arguments coincide and are nonzero; it is nonnegative for positive arguments; and the canonical threshold is strictly positive. Those three fields are exactly the hypotheses a downstream inequality proof needs to quote without reopening the cost definitions.
proof idea
One-line term proof: inhabit Nonempty by the anonymous constructor applied to the already-defined concrete certificate cert. No tactics, no further lemmas.
why it matters
Closes the certificate layer of the structural recognition-Heisenberg development (Plan v7). Downstream consumers that need a single object asserting diagonal vanishing, nonnegativity, and positive threshold can take any element of this nonempty type rather than re-proving the three facts. It sits inside the Foundation forcing story that ties J-cost uniqueness (T5) and the $\phi$-rung scale to an uncertainty bound consistent with $\hbar_R=J(\phi)\hbar$. No further used-by edges are recorded yet; the declaration is the existence seal on the cert pack itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.