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. -/
depends on (23)
Lean names referenced from this declaration's body.