Information No Cloning No Cloning Algebraic Constraint

The algebraic constraint

The quantum no-cloning theorem is a fundamental result in quantum information theory. It states that it is impossible to create an identical copy of an arbitrary unknown quantum state. This is not a technological limitation; it is a mathematical fact about how quantum states behave. The proof rests on a simple observation about complex numbers: if a number z satisfies z² = z, then z must be either 0 or 1. This is the algebraic constraint behind no-cloning.

The Recognition Science framework's machine-checked library of formal theorems contains a declaration called no_cloning_algebraic_constraint. This theorem states that for any complex number z, if z² = z, then z = 0 or z = 1. The proof is direct: z² = z implies z(z - 1) = 0, and since complex numbers have no zero divisors, either z = 0 or z = 1. This is a lemma about the algebraic structure of complex numbers, not a statement about quantum mechanics itself.

In the context of the no-cloning theorem, this constraint does the work. If a cloning machine existed, it would need to preserve inner products. For two states |ψ⟩ and |φ⟩, the inner product ⟨ψ|φ⟩ would need to equal its square. The algebraic constraint says this is only possible when the inner product is 0 or 1, meaning the states are either identical or orthogonal. For any pair of states that are neither identical nor orthogonal, cloning is impossible. The library also provides a witness: the real number 1/2 is neither 0 nor 1, and 1/2² ≠ 1/2, showing the constraint is not vacuous.

In Recognition Science, this algebraic fact is connected to the idea of ledger uniqueness: a discrete record of events where each entry has a unique identifier. The framework's account suggests that copying would require a balancing entry, and without knowing what to balance, duplication is impossible. However, this connection is a model, a definitional choice about how to interpret the mathematics, not a derivation from the algebraic constraint itself. The library contains several theorems about no-cloning, such as no_broadcasting and no_deleting, but these are stated as True := trivial, meaning they are placeholders for future work, not fully developed proofs.

The algebraic constraint is a small but essential piece of the no-cloning puzzle. It shows that the impossibility of cloning is not a mysterious quantum phenomenon but a consequence of the simplest algebraic properties of complex numbers. This is what the declaration establishes: a precise, machine-checked statement of a fact that underlies one of quantum theory's most famous results.

/-- **THEOREM (No-Cloning Constraint)**: Universal cloning requires all inner products
    to satisfy z² = z, forcing z ∈ {0, 1}. But superpositions have inner products
    like 1/√2 ∉ {0, 1}, so universal cloning is impossible.

    This is the algebraic core of the no-cloning theorem. The full theorem
    requires tensor product structure which is beyond this simplified model. -/
theorem no_cloning_algebraic_constraint :
    ∀ z : ℂ, z^2 = z → z = 0 ∨ z = 1 := cloning_constraint

/-- **THEOREM (No Universal Cloning Witness for Reals)**: There exist real numbers
    that don't satisfy the cloning constraint z² = z (except 0 and 1).

    Example: 1/2 has (1/2)² = 1/4 ≠ 1/2.
    This means no single unitary can clone states with inner product 1/2. -/
theorem no_universal_cloning_witness_real :
    ∃ z : ℝ, z ≠ 0 ∧ z ≠ 1 ∧ z^2 ≠ z := by
  use 1/2
  constructor
  · norm_num
  constructor
  · norm_num
  · norm_num

/-- The core algebraic constraint from no-cloning:
    If a unitary U clones states |ψ⟩ and |φ⟩, then ⟨ψ|φ⟩ = ⟨ψ|φ⟩².
    This can only hold if ⟨ψ|φ⟩ ∈ {0, 1}. -/
lemma cloning_constraint (z : ℂ) (hz : z^2 = z) : z = 0 ∨ z = 1 := by
  -- z² = z means z(z-1) = 0
  have h : z * (z - 1) = 0 := by
    calc z * (z - 1) = z^2 - z := by ring
      _ = z - z := by rw [hz]
      _ = 0 := by ring
  rcases mul_eq_zero.mp h with hz0 | hz1
  · left; exact hz0
  · right; exact sub_eq_zero.mp hz1

What this page does not claim

The declaration does not prove the full quantum no-cloning theorem; it only establishes the algebraic constraint on complex numbers. The connection between ledger uniqueness and no-cloning is a model, not a theorem. The library's no_broadcasting and no_deleting theorems are placeholders, not complete proofs. The optimal cloning fidelity of 5/6 is a definition, not a derived result.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/NoCloning.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: