CloningMachine
The CloningMachine structure encodes a hypothetical device that maps any quantum state to a pair of identical copies while leaving the original intact. Quantum information researchers would cite it when setting up the no-cloning contradiction inside Recognition Science's ledger-uniqueness framework. The definition consists of a clone function from states to pairs together with two axioms forcing both output components to equal the input.
claimLet $Q_n$ be the set of normalized vectors in the Hilbert space of dimension $n$. A cloning machine is a map $C: Q_n → Q_n × Q_n$ such that the first component of $C(ψ)$ equals $ψ$ and the second component equals $ψ$, for every $ψ ∈ Q_n$.
background
In the Information.NoCloning module, QuantumState is the structure whose fields are amplitudes (Fin n → ℂ) and a normalization proof that the sum of squared moduli equals one; this encodes a unit vector in a finite-dimensional Hilbert space. The module derives the no-cloning theorem from ledger uniqueness: each ledger entry carries a unique identifier, so creating an arbitrary duplicate would require a balancing entry that cannot be supplied without prior knowledge of the state. Upstream results include the QuantumLedger.QuantumState definition, which represents superpositions over ledger configurations with complex amplitudes, and the OptionAEmpiricalProgram.is class that supplies collision-freeness.
proof idea
CloningMachine is introduced as a bare structure definition with an empty proof body. It directly assembles the clone operation (QuantumState n → QuantumState n × QuantumState n) and the two preservation axioms (preserves_original and copy_equals_original) as fields; no lemmas or tactics are invoked.
why it matters in Recognition Science
This definition supplies the hypothetical object discharged by the downstream theorems no_cloning_theorem_remark and no_universal_cloning_witness_real. The remark observes that the structure omits tensor-product and unitarity constraints, while the witness theorem exhibits a real number (1/2) whose square differs from itself, violating the inner-product condition required for cloning. It fills the INFO-006 paper target of obtaining no-cloning from ledger structure and connects to the Recognition Science forcing chain (T0–T8) and Recognition Composition Law that generate quantum information laws.
scope and limits
- Does not incorporate tensor-product structure of composite systems.
- Does not require the clone map to be linear or unitary.
- Does not encode inner-product preservation explicitly.
- Does not reference ledger balancing or uniqueness axioms from upstream modules.
formal statement (Lean)
76structure CloningMachine (n : ℕ) where
77 /-- The "copy" operation. Would take |ψ⟩|0⟩ → |ψ⟩|ψ⟩. -/
78 clone : QuantumState n → QuantumState n × QuantumState n
79 /-- The operation preserves the original. -/
80 preserves_original : ∀ ψ, (clone ψ).1 = ψ
81 /-- The copy equals the original. -/
82 copy_equals_original : ∀ ψ, (clone ψ).2 = ψ
83
84/-- Helper: Inner product squared is not equal to inner product for general complex numbers. -/