Simon's problem

Simon's problem gives oracle access to a function on bit strings with an unknown nonzero mask s: two inputs have the same oracle value exactly when they are equal or differ by s [dW19, qcnotes.tex:1407, 1409-1410].

This module formalizes the problem at the standard post-sampling abstraction boundary. A run of Simon's quantum circuit yields a vector y satisfying the linear equation y · s = 0 over 𝔽₂ [dW19, qcnotes.tex:1459-1460]. Once the collected equations cut the solution set down to {0, s}, any nonzero candidate satisfying all of them is the hidden mask [dW19, qcnotes.tex:1460].

Main results

• LeanPool.LeanQuantumAlg.Simon.Promise — explicit Simon promise for an oracle and hidden mask over bit vectors Fin n → ZMod 2.
• LeanPool.LeanQuantumAlg.Simon.CompleteEquations — the collected 𝔽₂-linear equations have exactly the two expected solutions, 0 and s.
• LeanPool.LeanQuantumAlg.SimonsProblem.main — under the explicit promise and complete linear post-processing equations, every nonzero candidate satisfying the equations is the hidden nonzero mask.

@[reducible, inline]

abbrev QuantumAlg.Simon.F₂ : Type

The two-element field used for Simon bit strings.

Equations

• QuantumAlg.Simon.F₂ = ZMod 2

@[reducible, inline]

abbrev QuantumAlg.Simon.BitVec (n : ℕ) : Type

An n-bit vector, represented as a vector space over 𝔽₂.

Equations

• QuantumAlg.Simon.BitVec n = (Fin n → QuantumAlg.Simon.F₂)

@[reducible, inline]

abbrev QuantumAlg.Simon.Oracle (n : ℕ) (α : Type u) : Type u

A Simon oracle maps bit vectors to arbitrary classical values. The promise, not the codomain representation, carries the algorithmic content.

Equations

• QuantumAlg.Simon.Oracle n α = (QuantumAlg.Simon.BitVec n → α)

def QuantumAlg.Simon.dot {n : ℕ} (x y : BitVec n) : F₂

Dot product over 𝔽₂.

Equations

• QuantumAlg.Simon.dot x y = ∑ i : Fin n, x i * y i

def QuantumAlg.Simon.Orthogonal {n : ℕ} (x y : BitVec n) : Prop

Two bit vectors are orthogonal when their 𝔽₂ dot product vanishes.

Equations

• QuantumAlg.Simon.Orthogonal x y = (QuantumAlg.Simon.dot x y = 0)

def QuantumAlg.Simon.SameFiber {n : ℕ} (s x y : BitVec n) : Prop

The two-element fiber relation induced by a Simon mask: x and y are equal modulo the hidden period s.

Equations

• QuantumAlg.Simon.SameFiber s x y = (y = x ∨ y = x + s)

structure QuantumAlg.Simon.Promise {n : ℕ} {α : Type u} (f : Oracle n α) (s : BitVec n) : Prop

The explicit Simon promise: s is nonzero, and oracle fibers are exactly pairs of equal inputs or inputs separated by s.

• nonzero : s ≠ 0
• fiber_iff (x y : BitVec n) : f x = f y ↔ SameFiber s x y

def QuantumAlg.Simon.SatisfiesEquation {n : ℕ} (y t : BitVec n) : Prop

A sampled Simon equation says that the sampled vector is orthogonal to a candidate mask.

Equations

• QuantumAlg.Simon.SatisfiesEquation y t = QuantumAlg.Simon.Orthogonal y t

def QuantumAlg.Simon.SatisfiesEquations {n : ℕ} (samples : Finset (BitVec n)) (t : BitVec n) : Prop

A candidate mask satisfies every collected linear equation.

Equations

• QuantumAlg.Simon.SatisfiesEquations samples t = ∀ y ∈ samples, QuantumAlg.Simon.SatisfiesEquation y t

def QuantumAlg.Simon.CompleteEquations {n : ℕ} (samples : Finset (BitVec n)) (s : BitVec n) : Prop

The collected equations are complete when their common solution set is exactly {0, s}. This is the linear-algebraic post-processing condition implemented by Gaussian elimination over 𝔽₂.

Equations

• QuantumAlg.Simon.CompleteEquations samples s = ∀ (t : QuantumAlg.Simon.BitVec n), QuantumAlg.Simon.SatisfiesEquations samples t ↔ t = 0 ∨ t = s

def QuantumAlg.Simon.Candidate {n : ℕ} (samples : Finset (BitVec n)) (t : BitVec n) : Prop

A nonzero candidate returned by the classical post-processing step.

Equations

• QuantumAlg.Simon.Candidate samples t = (t ≠ 0 ∧ QuantumAlg.Simon.SatisfiesEquations samples t)

def QuantumAlg.Simon.expectedResourceProfile (n : ℕ) : ResourceProfile

Trusted representative resource profile for the public Simon statement: expected linear oracle samples, quadratic Hadamard gates, and cubic classical linear algebra over ZMod 2.

Equations

• QuantumAlg.Simon.expectedResourceProfile n = { oracleQueries := n, hadamardGates := n ^ 2, elementaryGates := 0, classicalOps := n ^ 3 }

theorem QuantumAlg.Simon.expectedResourceProfile_exact (n : ℕ) : (expectedResourceProfile n).HasExactCounts n (n ^ 2) 0 (n ^ 3)

@[simp]

theorem QuantumAlg.Simon.dot_zero_left {n : ℕ} (x : BitVec n) : dot 0 x = 0

@[simp]

theorem QuantumAlg.Simon.dot_zero_right {n : ℕ} (x : BitVec n) : dot x 0 = 0

theorem QuantumAlg.Simon.dot_comm {n : ℕ} (x y : BitVec n) : dot x y = dot y x

The 𝔽₂ dot product is symmetric.

theorem QuantumAlg.Simon.dot_add_right {n : ℕ} (x y z : BitVec n) : dot x (y + z) = dot x y + dot x z

Right additivity of the 𝔽₂ dot product.

theorem QuantumAlg.Simon.dot_add_left {n : ℕ} (x y z : BitVec n) : dot (x + y) z = dot x z + dot y z

Left additivity of the 𝔽₂ dot product.

theorem QuantumAlg.Simon.satisfiesEquations_zero {n : ℕ} (samples : Finset (BitVec n)) : SatisfiesEquations samples 0

The zero vector satisfies every collected Simon equation.

theorem QuantumAlg.Simon.satisfiesEquations_add {n : ℕ} {samples : Finset (BitVec n)} {a b : BitVec n} (ha : SatisfiesEquations samples a) (hb : SatisfiesEquations samples b) : SatisfiesEquations samples (a + b)

Sums of solutions to the collected equations are again solutions; the solution set is a linear subspace over 𝔽₂.

theorem QuantumAlg.Simon.hiddenMask_satisfiesEquations {n : ℕ} {samples : Finset (BitVec n)} {s : BitVec n} (hcomplete : CompleteEquations samples s) : SatisfiesEquations samples s

If the equations are complete, the unknown nonzero string itself satisfies all of them.

theorem QuantumAlg.Simon.recover_from_complete_equations {n : ℕ} {samples : Finset (BitVec n)} {s t : BitVec n} (hcomplete : CompleteEquations samples s) (hcandidate : Candidate samples t) : t = s

Complete Simon equations identify the unknown nonzero string among nonzero candidates.

theorem QuantumAlg.Simon.promise_mask_unique {n : ℕ} {α : Type u} {f : Oracle n α} {s t : BitVec n} (hs : Promise f s) (ht : Promise f t) : s = t

The Simon promise determines a unique nonzero mask for an oracle.

theorem QuantumAlg.SimonsProblem.main {n : ℕ} {α : Type u} {f : Simon.Oracle n α} {s t : Simon.BitVec n} {samples : Finset (Simon.BitVec n)} (hpromise : Simon.Promise f s) (hcomplete : Simon.CompleteEquations samples s) (hcandidate : Simon.Candidate samples t) : t = s ∧ s ≠ 0

Simon correctness: assume an oracle satisfies Simon's promise with hidden nonzero mask s. If the sampled 𝔽₂-linear equations are complete and classical post-processing returns a nonzero candidate satisfying all of those equations, then that candidate is exactly the hidden nonzero mask.

theorem QuantumAlg.SimonsProblem.main_with_resources {n : ℕ} {α : Type u} {f : Simon.Oracle n α} {s t : Simon.BitVec n} {samples : Finset (Simon.BitVec n)} (hpromise : Simon.Promise f s) (hcomplete : Simon.CompleteEquations samples s) (hcandidate : Simon.Candidate samples t) : (t = s ∧ s ≠ 0) ∧ (Simon.expectedResourceProfile n).HasExactCounts n (n ^ 2) 0 (n ^ 3)

Simon supporting theorem for the public statement at the current post-sampling boundary: complete sampled equations recover the unknown nonzero string, and the trusted public resource profile records the accepted expected costs.