prob_sum_one
Probabilities over ledger configurations in a quantum state sum to one by construction. Researchers formalizing the emergence of the Born rule from J-cost minimization in Recognition Science would cite this to confirm normalization carries over from the ledger. The proof is a direct one-line application of the normalization condition already present in the quantum state definition.
claimFor any natural number $n$ and any quantum state over $n$ ledger configurations with complex amplitudes $c_i$, the sum over all configurations of $|c_i|^2$ equals 1.
background
The Quantum Ledger module formalizes quantum states as superpositions over ledger configurations, with the Born rule emerging from J-cost minimization rather than being postulated. A quantum state over $n$ configurations consists of a function assigning ledger entries to each index, complex amplitudes for each, and an explicit normalization condition that the sum of squared moduli of the amplitudes equals one. Probability for each configuration is defined as the squared modulus of its amplitude, matching the standard Born rule. Upstream results supply the J-cost function from multiplicative recognizers and observer forcing, which interpret the amplitudes in terms of recognition costs.
proof idea
The proof is the one-line term that directly applies the normalization field of the quantum state structure. This field asserts that the sum of squared moduli of amplitudes equals one, and since probability is defined as the squared modulus, the sum of probabilities is identically one.
why it matters in Recognition Science
This result ensures the probability measure on ledger configurations is properly normalized, supporting the module's derivation of the Born rule from J-cost minimization. It aligns with Recognition Science landmarks including T5 J-uniqueness and the emergence of quantum behavior from ledger superpositions. The theorem sits alongside related results on ledger conservation and cost non-negativity, providing a consistency check before full Born-rule derivations from cost functions.
scope and limits
- Does not derive the explicit form of probabilities from J-cost values.
- Does not address measurement collapse or state reduction.
- Does not treat time evolution or unitary dynamics of the state.
- Does not prove that this normalization is the unique probability measure compatible with the ledger.
formal statement (Lean)
163theorem prob_sum_one {n : ℕ} (ψ : QuantumState n) :
164 (Finset.univ.sum fun i => probability ψ i) = 1 :=
proof body
Term-mode proof.
165 ψ.normalized
166
167/-! ## Born Rule from J-Cost Minimization -/
168
169/-- The expected J-cost of a quantum state. -/