WavePacketCert
plain-language theorem explainer
Certificate structure packing three algebraic facts used in free-particle wave-packet spreading from J-cost: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code builds a concrete inhabitant and a Nonempty proof. Pure structure definition with no proof body.
Claim. A wave-packet certificate is a triple of properties: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ whenever $r\neq 0$; (ii) $\mathrm{cost}(m,e)\ge 0$ for all $m>0$ and $e>0$; (iii) the canonical threshold $T$ satisfies $T>0$.
background
The module treats free-particle Gaussian wave-packet spreading as a structural consequence of J-cost. Classically $\sigma(t)=\sigma_0\sqrt{1+(\hbar t/(2m\sigma_0^2))^2}$. In Recognition Science the packet reaches width $J(\varphi),\sigma_0$ at a definite spread time built from $J(\varphi)$, $\varphi$, $m$, and $\hbar$.
The J-cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), nonnegative and minimized at the identity $x=1$. The local domain cost is the two-argument cost used in this physics layer; the canonical threshold is the positive scale (tied to $J(\varphi)$) at which spreading is declared complete.
Upstream, recognition-event costs are already known nonnegative via the observer-forcing lemma that any event cost satisfies $0\le e.\mathrm{cost}$ by $J$-cost nonnegativity on positive states.
proof idea
No proof: this is a structure whose three fields are propositions. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The Nonempty theorem is then a one-constructor wrap of that inhabitant.
why it matters
Gives a single named bundle for the three cost/threshold facts the spreading argument needs, so later lemmas can depend on one certificate rather than three loose hypotheses. Immediate parents are the concrete cert inhabitant and cert_inhabited (Nonempty). The module is marked structural (0 sorry, 0 axiom) and sits in the physics layer that reads free-particle spreading off J-cost, citing the T5 J-uniqueness landmark $J(x)=(x+x^{-1})/2-1$ and the forced self-similar scale $\varphi$. It does not itself close the full dynamical derivation; it only packages the algebraic side conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.