superposition
The declaration establishes that the J-cost is strictly positive for any positive real r distinct from one. Quantum modelers using recognition amplitudes to derive the Schrödinger equation would cite this to confirm that superposed states carry positive recognition cost. The proof is a one-line wrapper invoking the core positivity lemma for the J-cost function.
claimFor every real number $r$ with $0 < r$ and $r ≠ 1$, the J-cost satisfies $J(r) > 0$.
background
In the Recognition Science derivation of the Schrödinger equation, the wave function ψ is interpreted as a recognition amplitude whose normalized intensity enters the J-cost. Stationary states are defined as J-cost minima (equilibrium), while superpositions are characterized by strictly positive J. The module imports the positivity fact from the Cost module, where the lemma states that J(x) > 0 for x > 0 and x ≠ 1, proved by rewriting Jcost as a square over a positive denominator.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module (and its duplicates in JcostCore and LocalCache). That lemma rewrites the cost expression via Jcost_eq_sq and verifies positivity of the numerator square and denominator.
why it matters in Recognition Science
This result supplies the cost positivity needed for the quantum-uncertainty interpretation in the RS Schrödinger module. It feeds directly into ledger_cost_additive (QuantumLedger), coherence_defect_of_combined and SuperpositionJustification (WeakFieldSuperposition), forcing_chain_complete (AcousticPhaseLevitation), and lambda_PBM_approx (PhotobiomodulationDevice). It aligns with the framework distinction between J = 0 equilibrium and J > 0 uncertainty states, supporting the T5 J-uniqueness landmark.
scope and limits
- Does not derive the time-dependent Schrödinger equation itself.
- Does not specify the explicit algebraic form of the J-cost function.
- Does not address normalization conventions for the amplitude ψ.
- Does not provide bounds or estimates for the magnitude of J(r).
formal statement (Lean)
36theorem superposition {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
37 0 < Jcost r := Jcost_pos_of_ne_one r hr hne
proof body
38
used by (20)
-
lambda_PBM_approx -
ledger_cost_additive -
forcing_chain_complete -
coherence_defect_of_combined -
SuperpositionJustification -
ledger_universal -
predictions -
quantumSpeedups -
universalGateSet -
no_cloning_theorem_remark -
no_universal_cloning_witness_real -
schroedingerCert -
measurementBasisCount -
single_particle_interference -
which_path_destroys_interference -
cost_probability_relation -
LedgerBranch -
QuantumState -
macroscopic_decoherence_instant -
neutral_windows_from_jcost