superposition_has_cost
plain-language theorem explainer
Superposition states carry strictly positive recognition cost J(r) > 0 for any positive real r unequal to 1. Quantum measurement theorists cite the result to justify why a superposition is unstable relative to the J = 0 equilibrium that follows collapse. The proof is a one-line wrapper that forwards the positivity hypotheses directly to the upstream Jcost positivity lemma.
Claim. For every real number $r > 0$ with $r ≠ 1$, the recognition cost satisfies $0 < J(r)$.
background
Recognition cost J(r) measures deviation from equilibrium for a scaling ratio r; the upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 precisely when x > 0 and x ≠ 1, obtained by rewriting Jcost via its squared form and verifying positivity of the resulting expression. In the wave-function module the wave function is treated as a cost distribution over outcomes, so that pre-measurement superposition corresponds to J(r) > 0 while post-measurement equilibrium is J(1) = 0. The module enumerates five measurement bases (position, momentum, spin, energy, angular momentum) to match configDim D = 5.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module, passing the hypotheses 0 < r and r ≠ 1 directly.
why it matters
This theorem supplies the superposition_cost field inside the WaveFunctionCollapseCert definition that bundles the pre- and post-measurement cost statements. It fills the first item of the module's key formal content: before measurement J(r) > 0 for r ≠ 1. Within the Recognition framework it anchors the interpretation of quantum measurement as cost-driven collapse to the J = 0 minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.