Information No Cloning No Universal Cloning Witness Real

The witness against universal cloning

The quantum no-cloning theorem is a central result of quantum information theory: it is impossible to build a machine that takes an arbitrary unknown quantum state and produces two perfect copies of it. The proof rests on a simple algebraic fact. If a cloning machine worked for every state, then for any two states |ψ⟩ and |φ⟩, the inner product ⟨ψ|φ⟩ would have to equal its own square. That equation, z² = z, has only two solutions in the complex numbers: z = 0 and z = 1. But two distinct quantum states can have an inner product that is neither 0 nor 1, for instance 1/2. That single counterexample is enough to break the cloning argument.

The Recognition Science library encodes this reasoning in a machine-checked collection of formal theorems. Its declaration no_universal_cloning_witness_real (a ledger, a discrete record of events, here used as the formal bookkeeping for such proofs) establishes the concrete witness: it proves that there exists a real number z, namely 1/2, which is not 0, not 1, and whose square is not equal to itself. This is the arithmetic heartbeat of the no-cloning theorem. The library also proves the companion algebraic constraint: for any complex number z, if z² = z, then z must be 0 or 1. Together these two theorems show why a universal cloning machine cannot exist: the required equality fails for a perfectly ordinary number.

The declaration is deliberately narrow. It does not construct a physical cloning machine, nor does it describe how to build a quantum computer. It does not prove the full no-cloning theorem for all quantum states; that would require a more elaborate argument involving tensor products and unitary operators, which the library acknowledges in a separate remark. What the witness theorem does is isolate the essential algebraic obstruction in a single, checkable statement. It says: here is a number that violates the condition any cloning machine would need to satisfy. That is the precise, limited role it plays.

This matters because it shows the no-cloning theorem is not a mysterious physical prohibition but a consequence of ordinary arithmetic. The impossibility of perfect copying is built into the structure of complex numbers themselves. Once you see that z² = z forces z to be 0 or 1, the door to universal cloning closes. The witness theorem makes that closing explicit and verifiable, one small number at a time.

/-- **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

/-- **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

What this page does not claim

The declaration does not prove the full no-cloning theorem for all quantum states. The declaration does not construct a physical cloning machine or describe its operation. The declaration does not address the possibility of approximate cloning or its limits.

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: