prob_nonneg
Non-negativity of Born-rule probabilities follows directly from defining probability as the squared modulus of the amplitude in a normalized quantum state over ledger configurations. Researchers deriving the Born rule from J-cost minimization in the Recognition Science ledger would cite this to confirm that extracted probabilities form a valid distribution for use in statistics and thermodynamics. The proof is a one-line term application of the non-negativity of the squared norm on complex numbers.
claimFor any natural number $n$, any normalized quantum state $ψ$ over $n$ ledger configurations (with complex amplitudes satisfying the sum of squared moduli equal to 1), and any index $i$, the probability of configuration $i$ satisfies $0 ≤ |ψ_i|^2$.
background
In the QuantumLedger module a QuantumState n is a structure with a map from Fin n to Ledger configurations, complex amplitudes for each configuration, and a normalization axiom requiring the sum of squared moduli of the amplitudes to equal 1. Probability of index i is defined as the squared modulus of the corresponding amplitude, expressing the Born rule in ledger terms. The module situates this inside the Recognition Science connection where quantum states are superpositions of ledger entries and the Born rule emerges from J-cost minimization rather than being postulated.
proof idea
The proof is a term-mode one-liner that applies Complex.normSq_nonneg directly to the amplitude of the chosen index i inside the given quantum state ψ.
why it matters in Recognition Science
This result guarantees that probabilities derived from the quantum ledger are non-negative, which is required for the ProbDist structure in VariationalFreeEnergyFromRCL and for the Boltzmann distribution in Thermodynamics. It supplies the elementary non-negativity step needed for the Born-rule derivation from J-cost in the Recognition Science framework and supports the forcing-chain steps that produce physical constants and D=3. It touches the open question of obtaining the full quantum formalism from the Recognition Composition Law without extra postulates.
scope and limits
- Does not prove that the probabilities sum to 1.
- Does not derive the Born rule from J-cost values.
- Does not establish normalization of the quantum state.
- Does not address measurement collapse or time evolution.
formal statement (Lean)
158theorem prob_nonneg {n : ℕ} (ψ : QuantumState n) (i : Fin n) :
159 0 ≤ probability ψ i :=
proof body
Term-mode proof.
160 Complex.normSq_nonneg _
161
162/-- Probabilities sum to 1. -/