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