Simon's algorithm

Category: 3-Local (QM-validity).

Simon's problem: given f : {0,1}ⁿ → {0,1}ⁿ with the promise f x = f x' ↔ (x' = x ∨ x' = x ⊕ s) for a hidden nonzero period s, find s. After querying U_f once and measuring the second register, the first register collapses to a coset state

|x₀⟩ + |x₀ ⊕ s⟩ (up to normalisation)

for some x₀ (the measured second-register value's preimage). Applying H^⊗n to this coset state and measuring yields, by the Born rule, an outcome y whose amplitude is

simon_amplitude : (1/√2)^{n+1} · (-1)^{⟨x₀,y⟩} · (1 + (-1)^{⟨s,y⟩}).

The factor 1 + (-1)^{⟨s,y⟩} vanishes when ⟨s,y⟩ is odd, so:

• simon_orthogonal: every measured y satisfies ⟨s,y⟩ ≡ 0 (mod 2) — i.e. y ⊥ s — the orthogonality property; outcomes non-orthogonal to the hidden s have probability 0;
• simon_uniform: every y ∈ s^⊥ carries the same probability 2/2ⁿ. (What is proved in Lean is this per-outcome equal value; the distributional reading — that these are 2^{n-1} outcomes whose probabilities sum to 1 for s ≠ 0, i.e. genuine uniformity on s^⊥ — rests on |s^⊥| = 2^{n-1}, which is the classical remark below, not a Lean theorem here.)

Honest scope. This is the single-register reduced analysis: the second register is measured (or traced out) first, which is the standard textbook reduction; we do not model the full two-register tensor circuit H^⊗n ∘ U_f ∘ H^⊗n nor the classical post-processing. The classical recovery is a remark: the valid-outcome set {y : ⟨s,y⟩ even} is the hyperplane s^⊥ ⊆ 𝔽₂ⁿ, so uniform samples from it determine s by Gaussian elimination over 𝔽₂ — n−1 samples span it with constant probability ∏ₖ(1−2⁻ᵏ) ≈ 0.29, and O(n) samples succeed with high probability. This file captures the quantum core (orthogonality + uniformity), needing only the Hadamard action on basis states — not Hn unitarity.

The hypothesis s ≠ 0 is not load-bearing for simon_uniform (the amplitude formula and hence the probability 2/2ⁿ hold for every s, including s = 0 where the coset state is the unnormalised √2 |x₀⟩); it is retained for the physical reading (a genuine 2-element coset). It is load-bearing for cosetState_normalized (norm 1 requires the two basis states to be distinct).

def CSD.Empirical.QM.Simon.bitInner {n : ℕ} (x y : Fin n → Fin 2) : ℕ

The bitwise inner product ⟨x,y⟩ = ∑ᵢ xᵢ yᵢ of two bitstrings, as a natural number (its parity is all that matters for the sign (-1)^{⟨x,y⟩}).

Equations

• CSD.Empirical.QM.Simon.bitInner x y = ∑ i : Fin n, ↑(x i) * ↑(y i)

def CSD.Empirical.QM.Simon.bxor {n : ℕ} (x s : Fin n → Fin 2) : Fin n → Fin 2

Bitwise XOR (x ⊕ s)ᵢ = xᵢ + sᵢ (addition in Fin 2 is XOR).

Equations

• CSD.Empirical.QM.Simon.bxor x s i = x i + s i

theorem CSD.Empirical.QM.Simon.bitInner_comm {n : ℕ} (x y : Fin n → Fin 2) : bitInner x y = bitInner y x

The bitwise inner product is symmetric.

theorem CSD.Empirical.QM.Simon.Hn_apply_inner {n : ℕ} (x y : Fin n → Fin 2) : QuantumInfo.Hn x y = (-1) ^ bitInner x y / ↑√2 ^ n

General Hadamard entry as a sign over a single denominator: Hn x y = (-1)^{⟨x,y⟩} / (√2)ⁿ. The per-qubit signs collect into one parity sign and the per-qubit √2 factors into (√2)ⁿ.

theorem CSD.Empirical.QM.Simon.neg_one_bitInner_bxor {n : ℕ} (x₀ s y : Fin n → Fin 2) : (-1) ^ bitInner (bxor x₀ s) y = (-1) ^ bitInner x₀ y * (-1) ^ bitInner s y

XOR sign-additivity: (-1)^{⟨x₀ ⊕ s, y⟩} = (-1)^{⟨x₀,y⟩} · (-1)^{⟨s,y⟩}. Per qubit, (x₀ᵢ + sᵢ)·yᵢ ≡ x₀ᵢ·yᵢ + sᵢ·yᵢ (mod 2); summing and using that (-1)^· depends only on parity gives the identity.

noncomputable def CSD.Empirical.QM.Simon.cosetState {n : ℕ} (x₀ s : Fin n → Fin 2) : QuantumInfo.QReg n

The coset state (1/√2)(|x₀⟩ + |x₀ ⊕ s⟩): the first-register state after the oracle query and the second-register measurement.

Equations

• CSD.Empirical.QM.Simon.cosetState x₀ s = (↑√2)⁻¹ • (QuantumInfo.basisState x₀ + QuantumInfo.basisState (CSD.Empirical.QM.Simon.bxor x₀ s))

noncomputable def CSD.Empirical.QM.Simon.simonCircuit {n : ℕ} (x₀ s : Fin n → Fin 2) : QuantumInfo.QReg n

Simon's circuit (reduced): apply H^⊗n to the coset state, then measure.

Equations

• CSD.Empirical.QM.Simon.simonCircuit x₀ s = QuantumInfo.applyHn (CSD.Empirical.QM.Simon.cosetState x₀ s)

theorem CSD.Empirical.QM.Simon.applyHn_add {n : ℕ} (ψ φ : QuantumInfo.QReg n) : QuantumInfo.applyHn (ψ + φ) = QuantumInfo.applyHn ψ + QuantumInfo.applyHn φ

H^⊗n is additive (it is the linear map Matrix.toEuclideanLin Hn).

theorem CSD.Empirical.QM.Simon.applyHn_smul {n : ℕ} (c : ℂ) (ψ : QuantumInfo.QReg n) : QuantumInfo.applyHn (c • ψ) = c • QuantumInfo.applyHn ψ

H^⊗n is ℂ-homogeneous.

theorem CSD.Empirical.QM.Simon.applyHn_basisState {n : ℕ} (x y : Fin n → Fin 2) : (QuantumInfo.applyHn (QuantumInfo.basisState x)).ofLp y = QuantumInfo.Hn y x

H^⊗n of a basis state picks out a Hadamard column: applyHn |x⟩ y = Hn y x.

theorem CSD.Empirical.QM.Simon.simon_amplitude {n : ℕ} (x₀ s y : Fin n → Fin 2) : (simonCircuit x₀ s).ofLp y = (↑√2)⁻¹ ^ (n + 1) * (-1) ^ bitInner x₀ y * (1 + (-1) ^ bitInner s y)

The Simon amplitude. Measuring outcome y after H^⊗n on the coset state has amplitude (1/√2)^{n+1} · (-1)^{⟨x₀,y⟩} · (1 + (-1)^{⟨s,y⟩}).

theorem CSD.Empirical.QM.Simon.simon_orthogonal {n : ℕ} (x₀ s y : Fin n → Fin 2) (hodd : Odd (bitInner s y)) : QuantumInfo.prob (simonCircuit x₀ s) y = 0

Simon orthogonality: if ⟨s,y⟩ is odd, then y is never measured — prob = 0. Every outcome is orthogonal to the hidden period s over 𝔽₂.

theorem CSD.Empirical.QM.Simon.simon_uniform {n : ℕ} (x₀ s y : Fin n → Fin 2) (_hs : s ≠ 0) (heven : Even (bitInner s y)) : QuantumInfo.prob (simonCircuit x₀ s) y = 2 / 2 ^ n

Uniformity on s^⊥: if ⟨s,y⟩ is even (so y ⊥ s), the outcome y has probability 2/2ⁿ. The valid outcomes are uniform over the 2^{n-1}-element hyperplane s^⊥.

hs : s ≠ 0 is not load-bearing here (the formula holds for all s); see the module docstring.

theorem CSD.Empirical.QM.Simon.cosetState_normalized {n : ℕ} (x₀ s : Fin n → Fin 2) (hs : s ≠ 0) : ‖cosetState x₀ s‖ = 1

The coset state is normalised (when s ≠ 0): the two computational-basis components are distinct, hence orthonormal, so ‖|x₀⟩ + |x₀ ⊕ s⟩‖ = √2 and the (1/√2) prefactor gives norm 1.