prob_nonneg
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.