cert
plain-language theorem explainer
Packages the three structural facts needed for the deep J-cost Heisenberg certificate: domain cost vanishes on the equal-argument diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is strictly positive. Anyone citing the recognition-side HUP at the phi-rung uses this bundle. The body is a pure structure inhabitant wiring three sibling lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and (iii) the canonical threshold is strictly positive.
background
The module derives a recognition-theoretic Heisenberg bound from J-cost: $\Delta_J \cdot \Delta_\sigma \ge \hbar_R/2$ with $\hbar_R = J(\varphi),\hbar$, as a structural theorem (no sorry, no axioms). Domain cost is the local cost functional on a pair of positive scale parameters; the canonical threshold is the positive cutoff that appears in the deep HUP inequality.
The certificate structure HUP3DeepCert is the interface that packages exactly three properties: diagonal vanishing of domain cost, nonnegativity of domain cost on the positive quadrant, and positivity of that threshold. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J$-cost nonnegativity on positive states.
This definition does not prove those three facts; it only assembles the sibling lemmas that do.
proof idea
One-line structure construction. Field cost_at_eq is filled by the sibling domainCost_at_eq; cost_nonneg by domainCost_nonneg; threshold_pos by canonicalThreshold_pos. No further tactics or algebraic work.
why it matters
Gives a single named inhabitant of the deep HUP certificate so later lemmas can assume the three structural hypotheses in one place rather than threading them separately. Sits inside the Foundation forcing story that ties J-cost (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) to an uncertainty bound at the $\varphi$-rung, with $\hbar_R=J(\varphi),\hbar$.
No downstream users are recorded yet in the graph; the immediate role is to close the certificate interface for the module's structural HUP claim and for cert_inhabited. It does not itself derive $\Delta x,\Delta p\ge\hbar/2$; it only certifies the cost-side hypotheses that derivation needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.