cost_probability_relation
The cost-probability relation states that for any normalized finite-dimensional quantum state with a non-vanishing amplitude at basis index i, the Born probability of that outcome equals the exponential of the negative outcome cost. Quantum theorists deriving the measurement postulate from ledger commitment cite this result to obtain the Born rule without an extra axiom. The term-mode proof unfolds the probability and cost definitions, cancels a double negation after the non-zero case split, and invokes the exp-log identity on the positive norm
claimFor a normalized quantum state $ψ$ in dimension $n$ with non-zero amplitude at index $i$, the measurement probability $P(i)$ satisfies $P(i) = e^{-C(i)}$, where the outcome cost is $C(i) = -log(|ψ_i|^2)$.
background
The module derives the quantum measurement postulate from Recognition Science ledger commitment. Superposition is an uncommitted ledger entry; measurement forces commitment to one branch, with probabilities fixed by recognition weights. QuantumState is the structure that assigns an amplitude (complex number) to each of $n$ basis states subject to the normalization condition that the sum of squared moduli equals one.
proof idea
The term-mode proof introduces the variables, unfolds measurementProbability and outcomeCost, rewrites the conditional definition via dif_pos on the non-zero hypothesis, cancels the double negation, establishes positivity of the squared norm from norm_pos_iff, and concludes by symmetry of exp_log.
why it matters in Recognition Science
This theorem supplies the explicit link between recognition cost and Born probabilities, completing the derivation of the measurement postulate from ledger commitment stated in the module. It shows that the Born rule emerges directly from J-cost minimization on ledger branches rather than being postulated. In the framework it connects to the phi-ladder and eight-tick structures that determine the underlying costs.
scope and limits
- Does not apply when any amplitude vanishes.
- Does not address infinite-dimensional Hilbert spaces.
- Does not derive the full collapse dynamics or time evolution.
- Assumes finite n and the normalization condition on the state.
formal statement (Lean)
227theorem cost_probability_relation : ∀ {n : ℕ} (ψ : QuantumState n) (i : Fin n),
228 ψ.amplitudes i ≠ 0 →
229 measurementProbability ψ i = Real.exp (-(outcomeCost ψ i)) := by
proof body
Term-mode proof.
230 intro n ψ i hz
231 unfold measurementProbability outcomeCost
232 rw [dif_pos hz, neg_neg]
233 have hpos : ‖ψ.amplitudes i‖^2 > 0 := sq_pos_of_pos (norm_pos_iff.mpr hz)
234 exact (Real.exp_log hpos).symm
235
236/-! ## The Measurement Postulate Derived -/
237
238/-- **THEOREM (Measurement Postulate from Ledger)**:
239 The quantum measurement postulate follows from ledger commitment:
240
241 1. Before measurement: superposition (uncommitted ledger)
242 2. Measurement: ledger commitment to one branch
243 3. After measurement: definite state (committed ledger)
244 4. Probability: given by |amplitude|² (recognition weight)
245
246 This is not a postulate in RS - it's a theorem about how ledgers work. -/