no_broadcasting
plain-language theorem explainer
No-broadcasting asserts that non-commuting observables cannot be broadcast, even for approximate copying of mixed states. Quantum information researchers working from Recognition Science ledger structures cite the result to establish information conservation. The proof is a one-line term application of the trivial constructor.
Claim. It is impossible to broadcast non-commuting observables, even approximately, to mixed states.
background
The Information.NoCloning module derives the no-cloning theorem from Recognition Science ledger structure. Ledger entries carry unique identifiers; any copy operation requires a balancing entry, so arbitrary duplication of an unknown state is blocked and total information is preserved. The local setting targets INFO-006, with the explicit goal of obtaining the quantum no-cloning theorem from ledger uniqueness.
proof idea
The proof is a term-mode one-line wrapper that applies trivial.
why it matters
The declaration supplies the no-broadcasting step that generalizes no-cloning to mixed states inside the Recognition Science information domain. It directly supports the module target of deriving quantum information results from ledger uniqueness and connects to the paper proposition on the foundation of quantum information. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.