Uniform superposition
DefinitionuniformSuperpositionThe uniform superposition |s> = (1/sqrt N) * sum_i |i> over N basis states, the starting state of Grover's search algorithm.
import Mathlib namespace Grover /-- The uniform superposition `|s⟩ = (1/√N) ∑ᵢ |i⟩` over `N` basis states, the starting state of Grover's search algorithm. -/ noncomputable def uniformSuperposition (N : ℕ) : EuclideanSpace ℂ (Fin N) := WithLp.toLp 2 (fun _ => ((1 / Real.sqrt N : ℝ) : ℂ)) end Grover
Read-back
What the Lean code literally says, in plain math · claude-sonnet-5
For a natural number (the sole, explicit argument), uniformSuperposition N is defined as the vector in (with the standard inner product ) all of whose coordinates take the same value, namely the complex number obtained by casting the real number into (i.e. the value in every coordinate ). Here and the reciprocal are the total (junk-valued) real-number operations of the ambient library: at , by convention and by convention, so the formula that would fill each coordinate evaluates to in that degenerate case — though for the space has no coordinates at all, so the vector is vacuously the unique element of regardless of this value. No hypothesis that (or that is a perfect square, etc.) is imposed anywhere.
Confirmed by the mission captain (proposal self-audit).