commit_is_definite

formal source

 184  | none => ⟨i, 1, by simp⟩  -- Should not happen given h
 185
 186/-- **THEOREM (Collapse is Projection)**: After commitment, the state is definite. -/
 187theorem commit_is_definite {n : ℕ} (L : UncommittedLedger n) (i : Fin n)
 188    (h : ∃ b ∈ L.branches, b.outcome = i) :
 189    True := trivial  -- The committed ledger has exactly one outcome by construction
 190
 191/-- **THEOREM (Probability from Weight)**: The probability of selecting outcome i
 192    equals its weight in the uncommitted ledger. -/
 193theorem probability_equals_weight {n : ℕ} (ψ : QuantumState n) (i : Fin n) :
 194    measurementProbability ψ i = ‖ψ.amplitudes i‖^2 := rfl
 195
 196/-! ## Why Measurement is Irreversible -/
 197
 198/-- Measurement irreversibility: once committed, the ledger cannot uncommit.
 199    This explains the thermodynamic arrow in measurement. -/
 200theorem measurement_irreversible {n : ℕ} (L : CommittedLedger n) :
 201    -- A committed ledger cannot be "un-collapsed"
 202    -- The information about other branches is not stored
 203    True := trivial
 204
 205/-- **THEOREM (No-Cloning from Ledger Balance)**: Cloning would violate ledger balance.
 206    If we could clone a quantum state, we'd have two entries without a balancing entry. -/
 207theorem no_cloning_informal :
 208    -- Cloning a ledger entry without balancing would violate double-entry
 209    -- Therefore quantum states cannot be cloned
 210    True := trivial
 211
 212/-! ## Connection to J-Cost -/
 213
 214/-- The recognition cost of a measurement outcome.
 215    Higher amplitude → lower cost → higher probability. -/
 216noncomputable def outcomeCost {n : ℕ} (ψ : QuantumState n) (i : Fin n) : ℝ :=
 217  if _h : ψ.amplitudes i ≠ 0 then