QuantumState
plain-language theorem explainer
QuantumState defines a normalized map from a finite index set of size n to complex amplitudes, representing a unit vector in n-dimensional Hilbert space. Researchers deriving no-cloning from ledger uniqueness in Recognition Science cite this object when formalizing arbitrary unknown states for cloning-machine arguments. The definition is a direct structure whose only non-data field is the explicit sum-of-squares normalization predicate.
Claim. A quantum state in dimension $n$ is a function $a : [n] → ℂ$ such that $∑_{i=1}^n |a(i)|^2 = 1$.
background
The Information.NoCloning module derives the quantum no-cloning theorem from Recognition Science ledger uniqueness: each ledger entry is unique, so creating a copy requires a balancing entry that cannot be formed for an arbitrary unknown state. The module doc states that a cloning unitary U would have to satisfy U(|ψ⟩ ⊗ |0⟩) = |ψ⟩ ⊗ |ψ⟩, which fails to preserve inner products for distinct |ψ⟩, |φ⟩ because ⟨ψ|φ⟩² ≠ ⟨ψ|φ⟩ in general.
proof idea
Direct structure definition. The single predicate field simply records the normalization condition; no lemmas or tactics are applied.
why it matters
This supplies the basic state object used downstream by CloningMachine, innerProduct, and no_cloning_algebraic_constraint inside the same module, and by born_rule_jcost_connection and probability in QuantumLedger. It fills the paper proposition on the foundation of quantum information from ledger structure. The construction touches the open mapping between full ledger configurations (in QuantumLedger.QuantumState) and this amplitude-only representation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.