Exact Fourier circuits: graph blocks

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/GraphBlocks.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

theorem Complexity.ExactFourier.GraphReflection.block_relations {α : Type} [Fintype α] [DecidableEq α] (B E F G H : Matrix α α ℂ) (hB : IsUnit B) (hp : graph B * (1 + Matrix.fromBlocks E F G H) = 1 + Matrix.fromBlocks E F G H) (hm : (graph B).transpose * (1 - Matrix.fromBlocks E F G H) = -(1 - Matrix.fromBlocks E F G H)) : B * G = 1 + E ∧ B * (1 + H) = F ∧ B.transpose * F = 1 - H ∧ B.transpose * (1 - E) = G

theorem Complexity.ExactFourier.GraphReflection.offdiagonal_unit {α : Type} [Fintype α] [DecidableEq α] (B E F G H : Matrix α α ℂ) (hB : IsUnit B) (hreal : ∀ (i j : α), star (B i j) = B i j) (hs : (Matrix.fromBlocks E F G H).IsSymm) (hp : graph B * (1 + Matrix.fromBlocks E F G H) = 1 + Matrix.fromBlocks E F G H) (hm : (graph B).transpose * (1 - Matrix.fromBlocks E F G H) = -(1 - Matrix.fromBlocks E F G H)) : IsUnit F ∧ IsUnit G

theorem Complexity.ExactFourier.GraphReflection.diagonalization {α : Type} [Fintype α] [DecidableEq α] (B E F G H : Matrix α α ℂ) (hB : IsUnit B) (hG : IsUnit G) (h1 : B * G = 1 + E) (h2 : B * (1 + H) = F) (h3 : B.transpose * F = 1 - H) (h4 : B.transpose * (1 - E) = G) : hadamard * (swap * Pivot.matrix F E H G) * hadamard⁻¹ = Matrix.fromBlocks B 0 0 (-B.transpose⁻¹)

theorem Complexity.ExactFourier.GraphReflection.lower_bound_blocks {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (B E F G H : Matrix α α ℂ) (hB : IsUnit B) (hreal : ∀ (i j : α), star (B i j) = B i j) (hR : IsUnit (Matrix.fromBlocks E F G H)) (hs : (Matrix.fromBlocks E F G H).IsSymm) (hp : graph B * (1 + Matrix.fromBlocks E F G H) = 1 + Matrix.fromBlocks E F G H) (hm : (graph B).transpose * (1 - Matrix.fromBlocks E F G H) = -(1 - Matrix.fromBlocks E F G H)) : 2 * p.value B ≤ p.value (Matrix.fromBlocks E F G H) + 8 * ↑(Fintype.card α)

def Complexity.ExactFourier.SignedBits.weight (m : ℕ) : Bits m → ℕ

The Hamming weight of a recursively represented bit string.

Equations

• Complexity.ExactFourier.SignedBits.weight 0 x_2 = 0
• Complexity.ExactFourier.SignedBits.weight m.succ (Sum.inl i) = Complexity.ExactFourier.SignedBits.weight m i
• Complexity.ExactFourier.SignedBits.weight m.succ (Sum.inr i) = Complexity.ExactFourier.SignedBits.weight m i + 1

theorem Complexity.ExactFourier.SignedBits.D_weight (m : ℕ) (i j : Bits m) (h : D m i j ≠ 0) : weight m i = weight m j + 1

def Complexity.ExactFourier.SignedBits.V : Matrix (Fin 2) (Fin 2) ℂ

The signed swap matrix with square equal to minus the identity.

Equations

• Complexity.ExactFourier.SignedBits.V = !![0, -1; 1, 0]

def Complexity.ExactFourier.SignedBits.Vi : Matrix (Fin 2) (Fin 2) ℂ

The inverse of the signed swap matrix V.

Equations

• Complexity.ExactFourier.SignedBits.Vi = !![0, 1; -1, 0]

def Complexity.ExactFourier.SignedBits.X : Matrix (Fin 2) (Fin 2) ℂ

The unsigned swap matrix on two coordinates.

Equations

• Complexity.ExactFourier.SignedBits.X = !![0, 1; 1, 0]

theorem Complexity.ExactFourier.SignedBits.ViV : Vi * V = 1

theorem Complexity.ExactFourier.SignedBits.XX : X * X = 1

theorem Complexity.ExactFourier.SignedBits.V_monomial : MonomialMatrix V

theorem Complexity.ExactFourier.SignedBits.Vi_monomial : MonomialMatrix Vi

theorem Complexity.ExactFourier.SignedBits.X_monomial : MonomialMatrix X

def Complexity.ExactFourier.SignedBits.gauge (m : ℕ) : Matrix (Fin 2 × Bits m) (Fin 2 × Bits m) ℂ

A block diagonal change of coordinates determined by bit-string Hamming weights.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.ExactFourier.SignedBits.Q (m : ℕ) : Matrix (Fin 2 × Bits m) (Fin 2 × Bits m) ℂ

The signed-bit matrix 1 + V ⊗ D m used in the graph-block decomposition.

Equations

• Complexity.ExactFourier.SignedBits.Q m = 1 + Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Complexity.ExactFourier.SignedBits.V (Complexity.ExactFourier.SignedBits.D m)

theorem Complexity.ExactFourier.SignedBits.gauge_monomial (m : ℕ) : MonomialMatrix (gauge m)

theorem Complexity.ExactFourier.SignedBits.blockDiagonal_mul_apply {α β : Type} [Fintype α] [Fintype β] [DecidableEq β] (A : β → Matrix α α ℂ) (B : Matrix (α × β) (α × β) ℂ) (a b : α) (i j : β) : (Matrix.blockDiagonal A * B) (a, i) (b, j) = ∑ c : α, A i a c * B (c, i) (b, j)

theorem Complexity.ExactFourier.SignedBits.mul_blockDiagonal_apply {α β : Type} [Fintype α] [Fintype β] [DecidableEq β] (A : Matrix (α × β) (α × β) ℂ) (B : β → Matrix α α ℂ) (a b : α) (i j : β) : (A * Matrix.blockDiagonal B) (a, i) (b, j) = ∑ c : α, A (a, i) (c, j) * B j c b

theorem Complexity.ExactFourier.SignedBits.gauge_intertwine (m : ℕ) : gauge m * Q m = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (T m) * gauge m

theorem Complexity.ExactFourier.SignedBits.Q_unit (m : ℕ) : IsUnit (Q m)

theorem Complexity.ExactFourier.SignedBits.Q_price (p : MatrixPrice) (m : ℕ) : p.value (Q m) = 2 * p.value (T m)

theorem Complexity.ExactFourier.SignedBits.Gamma_Q (m : ℕ) : Gamma m = (Matrix.reindex (twoProdEquiv (Bits m)) (twoProdEquiv (Bits m))) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) X 1 * Q m)

theorem Complexity.ExactFourier.SignedBits.Gamma_price (p : MatrixPrice) (m : ℕ) : p.value (Gamma m) = ↑m * 2 ^ m

theorem Complexity.ExactFourier.reflection_inequality (p : MatrixPrice) (m : ℕ) : ↑m * (2 ^ (m + 1)) ^ 2 ≤ 3 / 4 * (2 * ((↑m + 2) * 2 ^ m) * 2 ^ (m + 1)) + 6 * (2 ^ (m + 1)) ^ 2

theorem Complexity.ExactFourier.no_matrixPrice (p : MatrixPrice) : False

theorem Complexity.ExactFourier.finite_win : FiniteWinStatement

The missing finite-win theorem, from exact comparison packing and the sparse reflection contradiction. No global price is taken as an assumption.

inductive Complexity.ExactFourier.Layered {α : Type} [Fintype α] [DecidableEq α] : Matrix α α ℂ → ℕ → Prop

Exact-width mixed rounds. Monomial rounds are counted, not silently free scalar multiplications. Disjoint parallel blocks share a round.

• identity {α : Type} [Fintype α] [DecidableEq α] : Layered 1 0
• mono {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : MonomialMatrix M) : Layered M 1
• pair (M : Matrix (Fin 2) (Fin 2) ℂ) (hM : IsUnit M) : Layered M 1
• mul {α : Type} [Fintype α] [DecidableEq α] {M N : Matrix α α ℂ} {d e : ℕ} (hM : Layered M d) (hN : Layered N e) : Layered (M * N) (d + e)
• reindex {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (f : α ≃ β) {M : Matrix α α ℂ} {d : ℕ} (hM : Layered M d) : Layered ((Matrix.reindex f f) M) d
• sum {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {N : Matrix β β ℂ} {d : ℕ} (hM : Layered M d) (hN : Layered N d) : Layered (Matrix.fromBlocks M 0 0 N) d
• weaken {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} {d e : ℕ} (h : Layered M d) (hde : d ≤ e) : Layered M e

theorem Complexity.ExactFourier.Layered.unit {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} {d : ℕ} (h : Layered M d) : IsUnit M

theorem Complexity.ExactFourier.Layered.parallel {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {N : Matrix β β ℂ} {d e : ℕ} (hM : Layered M d) (hN : Layered N e) : Layered (Matrix.fromBlocks M 0 0 N) (max d e)

theorem Complexity.ExactFourier.Layered.embed {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ↪ β) {M : Matrix α α ℂ} {d : ℕ} (h : Layered M d) : Layered (Embedded.matrix e M) d