Exact Fourier circuits: prices

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

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

theorem Complexity.ExactFourier.Shear.act_sumInl {ι : Type u_1} {κ : Type u_2} (s : Shear ι) (v : ι → ℂ) (y : κ → ℂ) : act (Matrix.TransvectionStruct.sumInl κ s) (Sum.elim v y) = Sum.elim (s.act v) y

Lifting an in-place word to disjoint targets adds no auxiliary coordinates.

theorem Complexity.ExactFourier.runShears_sumInl {ι : Type u_1} {κ : Type u_2} (W : List (Shear ι)) (v : ι → ℂ) (y : κ → ℂ) : runShears (List.map (fun (s : Shear ι) => Matrix.TransvectionStruct.sumInl κ s) W) (Sum.elim v y) = Sum.elim (runShears W v) y

theorem Complexity.ExactFourier.Program.memorySweep_exists {n k : ℕ} (p : Program n k) (enabled : Bool) : ∃ (W : List (Shear (Fin n ⊕ Fin k))), W.length ≤ 2 * k ∧ ∀ (x : Fin n → ℂ) (z : Fin k → ℂ), runShears W (Sum.elim x z) = Sum.elim x (p.dirtyScratch (if enabled = true then x else 0) z)

theorem Complexity.ExactFourier.broadcast_subset_exists {ι : Type u_1} {κ : Type u_2} (S : Finset κ) (refs : κ → Option ι) : ∃ (W : List (Shear (ι ⊕ κ))), W.length ≤ S.card ∧ ∀ (v : ι → ℂ) (y : κ → ℂ), runShears W (Sum.elim v y) = Sum.elim v fun (j : κ) => y j + if j ∈ S then readCoord (refs j) v else 0

The designated outputs are individual reads, not uncharged arbitrary linear maps.

theorem Complexity.ExactFourier.broadcast_exists {ι : Type u_1} {κ : Type u_2} [Fintype κ] (refs : κ → Option ι) : ∃ (W : List (Shear (ι ⊕ κ))), W.length ≤ Fintype.card κ ∧ ∀ (v : ι → ℂ) (y : κ → ℂ), runShears W (Sum.elim v y) = Sum.elim v fun (j : κ) => y j + readCoord (refs j) v

theorem Complexity.ExactFourier.broadcast_reverse {ι : Type u_1} {κ : Type u_2} (W : List (Shear (ι ⊕ κ))) (R : (ι → ℂ) → κ → ℂ) (hW : ∀ (v : ι → ℂ) (y : κ → ℂ), runShears W (Sum.elim v y) = Sum.elim v fun (j : κ) => y j + R v j) (v : ι → ℂ) (y : κ → ℂ) : runShears (reverseShears W) (Sum.elim v y) = Sum.elim v fun (j : κ) => y j - R v j

Inverting the output-read word subtracts exactly the same reads.

theorem Complexity.ExactFourier.replay_readout {ι : Type u_1} {κ : Type u_2} (W : List (Shear ι)) (B : List (Shear (ι ⊕ κ))) (R : (ι → ℂ) → κ → ℂ) (hB : ∀ (v : ι → ℂ) (y : κ → ℂ), runShears B (Sum.elim v y) = Sum.elim v fun (j : κ) => y j + R v j) (v : ι → ℂ) (y : κ → ℂ) : runShears (List.map (fun (s : Shear ι) => Matrix.TransvectionStruct.sumInl κ s) W ++ B ++ reverseShears (List.map (fun (s : Shear ι) => Matrix.TransvectionStruct.sumInl κ s) W)) (Sum.elim v y) = Sum.elim v fun (j : κ) => y j + R (runShears W v) j

Forward/read/reverse on arbitrary memory. This is a word identity, not an assumption that dirty scratch starts at zero.

theorem Complexity.ExactFourier.dirty_coordinate_replay_count {n a : ℕ} (C : LinearDAG n a) : ∃ (W : List (Shear ((Fin n ⊕ Fin C.size) ⊕ Fin a))), W.length ≤ 8 * C.size + 2 * a ∧ ∀ (x : Fin n → ℂ) (y : Fin a → ℂ) (z : Fin C.size → ℂ), runShears W (Sum.elim (Sum.elim x z) y) = Sum.elim (Sum.elim x z) fun (j : Fin a) => y j + C.eval x j

theorem Complexity.ExactFourier.Shear.act_eq_mulVec {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : Shear ι) (v : ι → ℂ) : s.act v = (Matrix.TransvectionStruct.toMatrix s).mulVec v

The operational shears above are the ordinary elementary matrices.

noncomputable def Complexity.ExactFourier.shearMatrix {ι : Type u_1} [Fintype ι] [DecidableEq ι] (W : List (Shear ι)) : Matrix ι ι ℂ

The matrix representing execution of a list of elementary shears in order.

Equations

• Complexity.ExactFourier.shearMatrix W = (List.map Matrix.TransvectionStruct.toMatrix W).reverse.prod

theorem Complexity.ExactFourier.runShears_eq_mulVec {ι : Type u_1} [Fintype ι] [DecidableEq ι] (W : List (Shear ι)) (v : ι → ℂ) : runShears W v = (shearMatrix W).mulVec v

theorem Complexity.ExactFourier.shearMatrix_isUnit {ι : Type u_1} [Fintype ι] [DecidableEq ι] (W : List (Shear ι)) : IsUnit (shearMatrix W)

def Complexity.ExactFourier.replayMatrix {n a k : ℕ} (G : Matrix (Fin a) (Fin n) ℂ) : Matrix ((Fin n ⊕ Fin k) ⊕ Fin a) ((Fin n ⊕ Fin k) ⊕ Fin a) ℂ

Jam the arbitrary dirty memory in an identity summand. The lower-left block is the designated rectangular map extended by zero on dirty scratch.

Equations

• Complexity.ExactFourier.replayMatrix G = Matrix.fromBlocks 1 0 (G.fromCols 0) 1

theorem Complexity.ExactFourier.replayMatrix_mulVec {n a k : ℕ} (G : Matrix (Fin a) (Fin n) ℂ) (x : Fin n → ℂ) (z : Fin k → ℂ) (y : Fin a → ℂ) : (replayMatrix G).mulVec (Sum.elim (Sum.elim x z) y) = Sum.elim (Sum.elim x z) fun (j : Fin a) => y j + G.mulVec x j

theorem Complexity.ExactFourier.dirty_coordinate_replay_matrix {n a : ℕ} (C : LinearDAG n a) (G : Matrix (Fin a) (Fin n) ℂ) (hG : ∀ (x : Fin n → ℂ), C.eval x = G.mulVec x) : ∃ (W : List (Shear ((Fin n ⊕ Fin C.size) ⊕ Fin a))), W.length ≤ 8 * C.size + 2 * a ∧ shearMatrix W = replayMatrix G

Matrix endpoint of the dirty replay, necessary for the price and boundary laws.

def Complexity.ExactFourier.MonomialMatrix {ι : Type u_1} [DecidableEq ι] (A : Matrix ι ι ℂ) : Prop

Literal permutation-times-invertible-diagonal form on a finite index type.

Equations

• Complexity.ExactFourier.MonomialMatrix A = ∃ (σ : Equiv.Perm ι) (d : ι → ℂ), (∀ (j : ι), d j ≠ 0) ∧ ∀ (i j : ι), A i j = if i = σ j then d j else 0

structure Complexity.ExactFourier.MatrixPrice : Type 1

An abstract nonnegative matrix cost obeying the stated invariance and composition laws.

• value {ι : Type} [Fintype ι] [DecidableEq ι] : Matrix ι ι ℂ → ℝ

  The real-valued cost assigned to a finite square complex matrix.

• nonneg {ι : Type} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℂ) : IsUnit A → 0 ≤ self.value A
• zero_iff {ι : Type} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℂ) : IsUnit A → (self.value A = 0 ↔ MonomialMatrix A)
• reindex {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (A : Matrix ι ι ℂ) : IsUnit A → self.value ((Matrix.reindex e e) A) = self.value A
• monomial {ι : Type} [Fintype ι] [DecidableEq ι] (A L R : Matrix ι ι ℂ) : IsUnit A → MonomialMatrix L → MonomialMatrix R → self.value (L * A * R) = self.value A
• mul_le {ι : Type} [Fintype ι] [DecidableEq ι] (A B : Matrix ι ι ℂ) : IsUnit A → IsUnit B → self.value (A * B) ≤ self.value A + self.value B
• tensor {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A : Matrix ι ι ℂ) (B : Matrix κ κ ℂ) : IsUnit A → IsUnit B → self.value (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B) = ↑(Fintype.card κ) * self.value A + ↑(Fintype.card ι) * self.value B
• directSum {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A : Matrix ι ι ℂ) (B : Matrix κ κ ℂ) : IsUnit A → IsUnit B → self.value (Matrix.fromBlocks A 0 0 B) = self.value A + self.value B
• inverse {ι : Type} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℂ) : IsUnit A → self.value A⁻¹ = self.value A
• transpose {ι : Type} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℂ) : IsUnit A → self.value A.transpose = self.value A
• normalized : self.value (Matrix.transvection 1 0 1) = 1

theorem Complexity.ExactFourier.MonomialMatrix.diagonal {ι : Type u_1} [DecidableEq ι] (d : ι → ℂ) (hd : ∀ (i : ι), d i ≠ 0) : MonomialMatrix (Matrix.diagonal d)

theorem Complexity.ExactFourier.MonomialMatrix.one {ι : Type u_1} [DecidableEq ι] : MonomialMatrix 1

@[simp]

theorem Complexity.ExactFourier.MatrixPrice.one (p : MatrixPrice) {ι : Type} [Fintype ι] [DecidableEq ι] : p.value 1 = 0

theorem Complexity.ExactFourier.MatrixPrice.identity_pad (p : MatrixPrice) {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A : Matrix ι ι ℂ) (hA : IsUnit A) : p.value (Matrix.fromBlocks A 0 0 1) = p.value A

theorem Complexity.ExactFourier.MatrixPrice.transvection_isUnit {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j) (c : ℂ) : IsUnit (Matrix.transvection i j c)

theorem Complexity.ExactFourier.MatrixPrice.shear_two (p : MatrixPrice) (c : ℂ) (hc : c ≠ 0) : p.value (Matrix.transvection 1 0 c) = 1

Diagonal conjugation varies the shear coefficient, including all complex values.

noncomputable def Complexity.ExactFourier.MatrixPrice.pairComplement {ι : Type u_1} (i j : ι) (hij : i ≠ j) : Fin 2 ⊕ { t : ι // t ≠ i ∧ t ≠ j } ≃ ι

An ordered pair and its untouched complement, used for exact identity padding.

Equations

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

@[simp]

theorem Complexity.ExactFourier.MatrixPrice.pairComplement_left₀ {ι : Type u_1} (i j : ι) (hij : i ≠ j) : (pairComplement i j hij) (Sum.inl 0) = j

@[simp]

theorem Complexity.ExactFourier.MatrixPrice.pairComplement_left₁ {ι : Type u_1} (i j : ι) (hij : i ≠ j) : (pairComplement i j hij) (Sum.inl 1) = i

@[simp]

theorem Complexity.ExactFourier.MatrixPrice.pairComplement_right {ι : Type u_1} (i j : ι) (hij : i ≠ j) (t : { t : ι // t ≠ i ∧ t ≠ j }) : (pairComplement i j hij) (Sum.inr t) = ↑t

theorem Complexity.ExactFourier.MatrixPrice.transvection_le_one (p : MatrixPrice) {ι : Type} [Fintype ι] [DecidableEq ι] (i j : ι) (hij : i ≠ j) (c : ℂ) : p.value (Matrix.transvection i j c) ≤ 1

Every coordinate shear is a single two-coordinate shear, with literal identity padding.

theorem Complexity.ExactFourier.MatrixPrice.transvection_list_isUnit {ι : Type} [Fintype ι] [DecidableEq ι] (L : List (Matrix.TransvectionStruct ι ℂ)) : IsUnit (List.map Matrix.TransvectionStruct.toMatrix L).prod

theorem Complexity.ExactFourier.MatrixPrice.transvection_list_le (p : MatrixPrice) {ι : Type} [Fintype ι] [DecidableEq ι] (L : List (Matrix.TransvectionStruct ι ℂ)) : p.value (List.map Matrix.TransvectionStruct.toMatrix L).prod ≤ ↑L.length

Every literal shear in an implementing word is charged.

theorem Complexity.ExactFourier.MatrixPrice.difference_le (p : MatrixPrice) {ι : Type} [Fintype ι] [DecidableEq ι] (A B : Matrix ι ι ℂ) (hA : IsUnit A) (hB : IsUnit B) : |p.value B - p.value A| ≤ p.value (A⁻¹ * B)

Inverse symmetry and subadditivity control a relative transformation in both directions.