cloning_constraint
plain-language theorem explainer
Any complex number z satisfying z squared equals z must be zero or one. Quantum information researchers cite this to show why no unitary can clone arbitrary unknown states. The proof rewrites the equation into a product equal to zero then splits cases via the zero-product property.
Claim. If a complex number $z$ satisfies $z^2 = z$, then $z = 0$ or $z = 1$. Here $z$ stands for the inner product between two quantum states that a cloning unitary would have to preserve.
background
The module Information.NoCloning derives the no-cloning theorem from Recognition Science ledger uniqueness: each ledger entry carries a unique identifier, copying demands a balancing entry, and total information is conserved. A cloning unitary U acting on an unknown state would require the inner product to obey $z = z^2$, which is possible only for $z$ in {0,1}. This lemma isolates the algebraic constraint that supports the argument. The proof relies on the mul_eq_zero lemma from Foundation.IntegersFromLogic, which states that a product equal to zero forces one factor to vanish.
proof idea
The tactic proof first applies ring to convert $z^2 = z$ into the factored equation $z(z-1)=0$. It then invokes mul_eq_zero to obtain the disjunction $z=0$ or $z-1=0$. Each branch is discharged by exact matching to produce the required or-statement.
why it matters
This lemma supplies the algebraic core for the downstream theorem no_cloning_algebraic_constraint, which concludes that universal cloning fails because superpositions yield inner products such as $1/√2$ outside {0,1}. It realizes the paper proposition on no-cloning from ledger structure. In the Recognition Science framework it illustrates how ledger uniqueness yields quantum information constraints without invoking the full forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.