experimentalStatus
plain-language theorem explainer
This definition supplies a list of three experimental claims that would falsify the no-cloning theorem if observed. Researchers in quantum foundations cite it to connect Recognition Science's ledger uniqueness to the standard no-cloning result. The body is a direct enumeration of structured pairs pairing each potential violation with its current status.
Claim. The experimental status is the list of pairs (claim, status) given by (``Universal cloning device'', ``Proven impossible by QM''), (``Superluminal communication'', ``Never observed''), (``Undetectable eavesdropping'', ``QKD security verified''), where each pair records a potential violation type and its observed status.
background
NoCloningFalsifier is the structure whose fields are a claim string and a status string; it records the three ways no-cloning would be falsified: a device copying unknown quantum states, superluminal communication, or undetected breaking of quantum key distribution. The module sets the local theoretical setting as INFO-006, deriving the no-cloning theorem from ledger uniqueness: each ledger entry is unique, copying requires a balancing entry, and arbitrary duplication is impossible without knowing the balance. The upstream structure NoCloningFalsifier supplies the exact record type used in the list.
proof idea
The definition is a direct list construction that populates three NoCloningFalsifier instances inline with their claim and status strings.
why it matters
It supports the module-level claim that no-cloning has never been violated and fills the experimental-status slot for the INFO-006 paper proposition on no-cloning from ledger structure. In the Recognition framework it reinforces information conservation that follows from ledger uniqueness, consistent with the RCL and the requirement that total information is preserved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.