NoCloningFalsifier
plain-language theorem explainer
NoCloningFalsifier structures enumerate concrete experimental routes that would violate no-cloning, such as a device copying arbitrary unknown states, superluminal signaling, or undetected eavesdropping on quantum key distribution. Quantum information researchers applying Recognition Science to ledger conservation would cite the structure when bounding information duplication. The declaration is a plain record definition with two string fields that populates the experimentalStatus list.
Claim. A record type consisting of a claim string describing a potential violation of no-cloning and a status string recording its experimental standing, where violations include a universal cloning device, superluminal communication, and breaking quantum key distribution without detection.
background
The Information.NoCloning module derives the no-cloning theorem from ledger uniqueness in Recognition Science. Ledger entries carry unique identifiers; any copy operation requires a balancing entry that cannot be formed for an arbitrary unknown state. This follows from the Recognition Composition Law and the conservation properties built into the phi-ladder. Upstream structures supply the necessary ledger factorization and J-cost definitions that enforce uniqueness without reference to quantum inner products.
proof idea
The declaration is a structure definition that introduces two fields of type String. It contains no proof body and functions as a direct record constructor for use in downstream lists of falsifiers.
why it matters
The structure supplies the element type for the experimentalStatus definition in the same module, which catalogs three concrete falsifiers and their statuses. It completes the empirical side of the module's target to derive no-cloning from ledger uniqueness, as described in the module documentation for the Foundation of QI paper. The construction sits inside the information-conservation consequences of the T0-T8 forcing chain and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.