no_cloning_informal

formal source

 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
 218    -(Real.log (‖ψ.amplitudes i‖^2))  -- Negative log probability = information cost
 219  else
 220    0  -- Infinite cost for impossible outcomes
 221
 222/-- **THEOREM (Cost-Probability Relation)**: Probability decreases with cost.
 223    P(i) = exp(-Cost(i)) when properly normalized.
 224
 225    Proof: P(i) = |ψᵢ|², Cost(i) = -log(|ψᵢ|²)
 226           exp(-Cost(i)) = exp(--log(|ψᵢ|²)) = exp(log(|ψᵢ|²)) = |ψᵢ|² = P(i) -/
 227theorem cost_probability_relation : ∀ {n : ℕ} (ψ : QuantumState n) (i : Fin n),
 228    ψ.amplitudes i ≠ 0 →
 229    measurementProbability ψ i = Real.exp (-(outcomeCost ψ i)) := by
 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