HUP3DeepCert
plain-language theorem explainer
A certificate packing three structural facts used by the recognition-side Heisenberg bound: the two-argument domain cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is strictly positive. Anyone citing the deep J-cost HUP derivation in this module will point at this bundle. It is a pure structure declaration; inhabitation is discharged later by the concrete `cert` witness.
Claim. A certificate consists of three properties of the domain cost $C$ and the canonical threshold $\tau$: (i) $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
The module derives a recognition-theoretic Heisenberg relation from J-cost: $\Delta_J\cdot\Delta_\sigma\ge\hbar_R/2$ with $\hbar_R=J(\varphi),\hbar$, as a structural counterpart of $\Delta x,\Delta p\ge\hbar/2$. Status is a structural theorem with no sorry and no extra axioms.
The domain cost is the two-argument cost that measures mismatch between a pair of positive scales (the siblings domainCost, domainCost_at_eq, domainCost_nonneg). The canonical threshold is the positive lower bound used as the recognition-side $\hbar_R/2$ scale (canonicalThreshold, canonicalThreshold_pos). Upstream, non-negativity of recognition-event cost is already known: any recognition event has cost $\ge 0$ via Jcost_nonneg on a positive state.
This structure simply names the three hypotheses the deep HUP argument needs in one place, so later lemmas can take a single certificate rather than three separate assumptions.
proof idea
No proof body: this is a structure declaration. The three fields are propositional requirements on domainCost and canonicalThreshold. Inhabitation is not claimed here; the sibling definition cert fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and cert_inhabited then records Nonempty of the structure.
why it matters
Gives the module a single named interface for the deep recognition-Heisenberg derivation. Downstream, cert is the concrete witness and cert_inhabited proves the type is nonempty, closing the structural package advertised in the module doc (0 sorry, 0 axiom).
In the broader Recognition chain this sits under Foundation work that ties uncertainty to J-cost rather than to an independent postulate. The J-cost uniqueness landmark (T5: $J(x)=(x+x^{-1})/2-1$) and the forced self-similar scale $\varphi$ (T6) fix the rung at which $\hbar_R=J(\varphi),\hbar$ is evaluated. The certificate does not itself prove the product bound; it packages the cost and threshold facts that bound uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.