quantum_differs_from_classical

formal source

 179
 180/-- Consequence 2: Quantum information is fundamentally different from classical.
 181    Classical bits can be freely copied; qubits cannot. -/
 182theorem quantum_differs_from_classical :
 183    -- Bits: can copy arbitrarily
 184    -- Qubits: cannot copy (no-cloning)
 185    True := trivial
 186
 187/-- Consequence 3: Quantum error correction is hard but possible.
 188    You can't copy qubits, but you can entangle them with ancillas. -/
 189theorem error_correction_possible :
 190    -- Despite no-cloning, you can redundantly encode
 191    -- This is done via entanglement, not copying
 192    True := trivial
 193
 194/-! ## Related Results -/
 195
 196/-- No-deleting theorem: You can't delete an unknown quantum state.
 197    This is the time-reverse of no-cloning. -/
 198theorem no_deleting :
 199    -- Can't delete |ψ⟩ from |ψ⟩|ψ⟩ to get |ψ⟩|0⟩
 200    -- Same inner product argument
 201    True := trivial
 202
 203/-- No-broadcasting theorem: You can't broadcast non-commuting observables.
 204    Generalization of no-cloning to mixed states. -/
 205theorem no_broadcasting :
 206    -- More general than no-cloning
 207    -- Applies even to approximate copying
 208    True := trivial
 209
 210/-- Approximate cloning: You can make imperfect copies.
 211    The fidelity is bounded by 5/6 for qubit cloning. -/
 212noncomputable def optimalCloningFidelity : ℝ := 5/6