inner_product_self
plain-language theorem explainer
The result shows that for any normalized quantum state ψ the modulus of its inner product with itself equals one. Researchers deriving no-cloning from ledger uniqueness in Recognition Science would cite this identity to enforce preservation of inner products under hypothetical copying maps. The proof unfolds the inner product sum, rewrites it as the sum of squared moduli via conjugation identities, and substitutes the normalization condition to reach the unit value.
Claim. Let ψ be a quantum state whose amplitudes a_i satisfy ∑_i |a_i|^2 = 1. Then ‖⟨ψ|ψ⟩‖ = 1.
background
QuantumState is defined as a structure carrying amplitudes in Fin n → ℂ together with the normalization axiom that the sum of squared moduli equals one. The inner product is the sum over i of the conjugate of the first state's amplitude times the second state's amplitude. The module derives the no-cloning theorem from ledger uniqueness: each ledger entry is unique, copying would require an unbalanced entry, and information is conserved under the Recognition Composition Law.
proof idea
The tactic proof first simplifies the innerProduct definition. It then introduces an auxiliary equality that converts the sum of conjugate-multiplications into the sum of squared norms, using Complex.normSq_eq_conj_mul_self and normSq_eq_norm_sq. The normalized field of ψ is substituted, after which simp reduces the expression to norm_one.
why it matters
This identity supplies the unitarity step required by the module's no-cloning derivations, including no_cloning_theorem_remark and no_cloning_from_ledger. It directly supports the paper proposition on no-cloning from ledger structure by guaranteeing that inner products remain invariant, consistent with the eight-tick octave and information conservation in the Recognition framework. No open scaffolding remains for this basic fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.