cert
plain-language theorem explainer
assembles the three structural hypotheses needed for the free-particle wave-packet spreading certificate: the domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the RS spreading time t_spread = 2mσ₀² J(φ)/ℏ · φ uses this bundle. The definition is a pure structure inhabitant wiring three already-proved sibling lemmas.
Claim. There exists a wave-packet certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module derives free-particle Gaussian spreading $\sigma(t)=\sigma_0\sqrt{1+(\hbar t/(2m\sigma_0^2))^2}$ from the Recognition Science J-cost. In RS units the packet reaches width $J(\varphi),\sigma_0$ at the structural time $t_{\mathrm{spread}}=2m\sigma_0^2 J(\varphi)/\hbar\cdot\varphi$.
domainCost is the local cost functional on mass and energy (or scale) parameters; it is built from the unique J-cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law. The canonical threshold is the positive scale at which spreading is declared to have occurred (tied to $J(\varphi)$).
Upstream, non-negativity of recognition cost is already settled: any recognition event has cost $\ge 0$ because $J$ itself is nonnegative on the positive reals. The three fields of the certificate simply specialise that fact, plus the diagonal vanishing and threshold positivity, to the wave-packet domain.
proof idea
One-line structure inhabitant. The three fields of WavePacketCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No additional tactics or algebraic work occur at this site.
why it matters
This certificate is the structural gate for the wave-packet spreading theorem in the module. Downstream consumers that need a single inhabited proof object of type WavePacketCert obtain it here; the module status line records the whole development as a structural theorem with zero sorry and zero axioms.
In the broader RS chain the construction sits downstream of T5 (J-uniqueness) and the non-negativity of J-cost. It supplies the cost-side hypotheses that let the free-particle spreading time be read off as a pure multiple of $J(\varphi)$, linking ordinary quantum dispersion to the forced self-similar scale $\varphi$. No open scaffolding remains at this declaration; it is pure packaging of already-closed lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.