superposition
plain-language theorem explainer
Superposition asserts that the J-cost is strictly positive for any positive real ratio r distinct from one. Quantum theorists deriving Schrödinger dynamics from Recognition Science primitives would cite this when quantifying uncertainty in superposed recognition states. The argument is a direct one-line wrapper around the core positivity lemma for the J-cost function.
Claim. For every real number $r$ with $0 < r$ and $r ≠ 1$, the J-cost satisfies $0 < J(r)$.
background
In the Schrödinger Equation from RS module, the wave function is identified with a recognition amplitude ψ whose normalized squared modulus supplies the quantum cost via the J-cost function. Stationary states are defined as J-cost minima (equilibrium, J = 0), while superpositions correspond to states carrying positive recognition cost (uncertainty). The module assumes the Recognition Composition Law and the T0–T8 forcing chain to obtain quantum evolution from RS primitives.
proof idea
This is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module (also present in JcostCore and LocalCache). The upstream lemma rewrites Jcost via its square form and invokes positivity of squares for the nonzero numerator.
why it matters
The declaration supports downstream results including ledger_cost_additive in QuantumLedger, coherence_defect_of_combined and SuperpositionJustification in WeakFieldSuperposition, and forcing_chain_complete in AcousticPhaseLevitation. It realizes the module distinction between J = 0 stationary states and J > 0 superpositions required by the RS derivation of the Schrödinger equation. It supplies the positive-cost ingredient for applications in photobiomodulation and Church-Turing universality claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.