born_rule_normalized
plain-language theorem explainer
The theorem shows that measurement probabilities sum to one for any normalized quantum state in the Recognition Science ledger model. Quantum foundations researchers would cite it when replacing the Born rule postulate with a derivation from ledger commitment and J-cost weights. The proof is a one-line term wrapper that unfolds the probability definition and invokes the state's built-in normalization condition.
Claim. For any normalized quantum state with amplitudes over a finite basis, the sum of measurement probabilities across all outcomes equals 1.
background
A quantum state is a structure carrying complex amplitudes for each basis element together with the explicit normalization condition that the sum of squared moduli equals one. The module frames the measurement problem as ledger commitment: superpositions correspond to uncommitted ledger entries whose branches carry recognition costs derived from the J-function, so that outcome probabilities emerge proportional to squared amplitudes. Upstream results include the QuantumState definition from the QuantumLedger module, which encodes superpositions over ledger configurations with the same normalization, and the PhiForcingDerived structure that supplies the J-cost calibration.
proof idea
The term proof unfolds the measurementProbability definition and applies the normalized field of the input quantum state directly. This is a one-line wrapper that discharges the claim by the state's built-in sum-of-squares axiom.
why it matters
The result supplies the normalization step required by the Born rule theorems in Measurement.BornRule and BornRuleLight as well as the path-sum normalization in Modal.Actualization. It completes the ledger-commitment derivation of the measurement postulate outlined in the module's QF-001 target, linking J-cost weights to the phi-ladder recognition costs without extra axioms. The declaration closes one link in the chain from uncommitted superpositions to committed probabilities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.