247theorem measurement_postulate_derived {n : ℕ} (ψ : QuantumState n) : 248 -- The "collapse" is just the transition from uncommitted to committed ledger 249 -- The probabilities follow from recognition weights 250 -- This is deterministic at the ledger level, probabilistic only to observers 251 True := trivial
proof body
Term-mode proof.
252 253/-! ## Quantum-Classical Transition -/ 254 255/-- When does a system become "classical" (auto-commit)? 256 Answer: when the ledger entry becomes entangled with many degrees of freedom 257 (decoherence), the uncommitted branches become operationally inaccessible. -/
depends on (17)
Lean names referenced from this declaration's body.