module module high

`IndisputableMonolith.Information.NoCloning`

The NoCloning module defines quantum states and derives the impossibility of universal cloning inside Recognition Science. It introduces QuantumState as unit vectors in Hilbert space together with inner-product constraints on any CloningMachine. Information theorists and quantum-foundations researchers cite it to embed standard no-cloning results inside the RS ledger. The argument rests on algebraic identities that force the inner-product constraint to fail for distinct states.

claimA quantum state is a unit vector $ψ ∈ ℋ$ with $‖ψ‖=1$. No map $C$ exists such that $C(ψ) = ψ ⊗ ψ$ for every $ψ$, because the inner-product condition $⟨ψ,φ⟩ = ⟨ψ,φ⟩²$ cannot hold for all pairs.

background

The module sits in the Information domain and imports Constants, where the fundamental RS time quantum satisfies τ₀ = 1 tick. It introduces QuantumState as a unit vector in a Hilbert space, innerProduct as the standard sesquilinear form, and CloningMachine as a hypothetical linear operator that would copy an arbitrary state. These objects rest on the discrete tick structure supplied by the upstream Constants module.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the algebraic no-cloning constraint that later siblings such as no_cloning_from_ledger and quantum_cryptography_possible rely on. It places the standard no-cloning theorem inside the Recognition framework by deriving it from inner-product identities grounded in the RS time quantum.

scope and limits

Does not derive the full Hilbert-space formalism from RS axioms.
Does not treat continuous or infinite-dimensional cases.
Does not address entanglement or multi-particle cloning.
Does not provide explicit RS-native cloning bounds beyond the algebraic constraint.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (20)

structure QuantumState L48
def innerProduct L55
theorem inner_product_self L59
structure CloningMachine L76
lemma inner_product_constraint L85
lemma cloning_constraint L102
theorem no_cloning_algebraic_constraint L118
theorem no_universal_cloning_witness_real L126
theorem no_cloning_theorem_remark L139
theorem no_cloning_from_ledger L158
theorem measurement_disturbs L165
theorem quantum_cryptography_possible L175
theorem quantum_differs_from_classical L182
theorem error_correction_possible L189
theorem no_deleting L198
theorem no_broadcasting L205
def optimalCloningFidelity L212
theorem approximate_cloning_bound L214
structure NoCloningFalsifier L224
def experimentalStatus L231