inner_product_constraint
plain-language theorem explainer
The algebraic lemma shows that for any complex z distinct from 0 and 1, z squared cannot equal z. Quantum information researchers working in Recognition Science cite it when deriving the no-cloning theorem from ledger uniqueness, because a cloning unitary would force the inner product to satisfy s = s squared. The proof assumes equality, rewrites the difference as a product via ring algebra, then splits via the zero-divisor-free property of LogicInt to reach contradictions with the hypotheses.
Claim. For any complex number $z$ with $z ≠ 0$ and $z ≠ 1$, $z^2 ≠ z$.
background
The module Information.NoCloning derives the quantum no-cloning theorem from Recognition Science ledger uniqueness: each ledger entry carries a unique identifier, so arbitrary duplication would require a balancing entry that cannot be constructed without prior knowledge of the state. This lemma supplies the algebraic core of that argument. It rests on the theorem that LogicInt has no zero divisors, obtained from the ring isomorphism with Int: if a product equals zero then one factor is zero.
proof idea
Tactic-mode proof. Assume z² = z. A calc block rewrites z(z-1) = z² - z, substitutes the assumption, and simplifies to zero. Apply mul_eq_zero.mp to obtain z = 0 or z-1 = 0. The first case contradicts the hypothesis z ≠ 0 by exact application; the second uses sub_eq_zero.mp to recover z = 1 and contradicts the remaining hypothesis.
why it matters
The lemma supplies the algebraic step required by the no-cloning derivation in INFO-006, where ledger uniqueness forces information conservation and rules out arbitrary state duplication. It directly supports the claim that any cloning unitary preserves inner products only when those products lie in {0,1}. The result sits inside the information domain of the Recognition framework and closes one algebraic prerequisite for the full no-cloning statement from ledger structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.