optimalCloningFidelity
plain-language theorem explainer
The definition supplies the numerical value 5/6 as the optimal fidelity for approximate 1-to-2 cloning of an unknown qubit. Quantum information researchers cite this constant when bounding cloning machines derived from ledger uniqueness in Recognition Science. The declaration is a direct constant assignment with no lemmas or computation required.
Claim. The optimal fidelity for approximate 1-to-2 cloning of an unknown qubit state is $5/6$.
background
The Information.NoCloning module derives the quantum no-cloning theorem from Recognition Science ledger structure. Ledger entries carry unique identifiers, so any copy operation requires a balancing entry that cannot be formed for an arbitrary unknown state without prior knowledge of its content. The module imports Mathlib for real arithmetic and Constants for framework values, with the core insight that information conservation prevents perfect duplication while permitting bounded approximation.
proof idea
The declaration is a direct constant definition that assigns the real number 5/6 with no lemmas, tactics, or upstream results applied.
why it matters
This constant is referenced by the downstream theorem approximate_cloning_bound, which asserts that the best possible fidelity for 1-to-2 qubit cloning equals 5/6. It supplies the numerical value required by the paper proposition on the foundation of quantum information from ledger structure. Within the Recognition Science framework it supports information conservation arguments that align with the recognition composition law and the overall forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.