Exact Fourier circuits: pivot join

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

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

noncomputable def Complexity.ExactFourier.Pivot.ofMatrix {α β : Type} [Fintype β] [DecidableEq β] (K : Matrix (α ⊕ β) (α ⊕ β) ℂ) : Matrix (α ⊕ β) (α ⊕ β) ℂ

Apply the pivot transform to the four blocks of a square matrix on a sum type.

Equations

• Complexity.ExactFourier.Pivot.ofMatrix K = Complexity.ExactFourier.Pivot.matrix K.toBlocks₁₁ K.toBlocks₁₂ K.toBlocks₂₁ K.toBlocks₂₂

@[simp]

theorem Complexity.ExactFourier.Pivot.of_fromBlocks {α β : Type} [Fintype β] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : ofMatrix (Matrix.fromBlocks A C B D) = matrix A C B D

noncomputable def Complexity.ExactFourier.Pivot.reverseJoin {α β γ : Type} [Fintype β] (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (γ ⊕ β) (γ ⊕ β) ℂ) : Matrix ((α ⊕ γ) ⊕ β) ((α ⊕ γ) ⊕ β) ℂ

Join cells in reverse order and restore the original order of their data blocks.

Equations

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

theorem Complexity.ExactFourier.Pivot.reverseJoin_eq {α β γ : Type} [Fintype β] (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (γ ⊕ β) (γ ⊕ β) ℂ) : reverseJoin X Y = Matrix.fromBlocks (Matrix.fromBlocks X.toBlocks₁₁ (X.toBlocks₁₂ * Y.toBlocks₂₁) 0 Y.toBlocks₁₁) ((X.toBlocks₁₂ * Y.toBlocks₂₂).fromRows Y.toBlocks₁₂) (X.toBlocks₂₁.fromCols (X.toBlocks₂₂ * Y.toBlocks₂₁)) (X.toBlocks₂₂ * Y.toBlocks₂₂)

theorem Complexity.ExactFourier.Pivot.of_join {α β γ : Type} [Fintype β] [DecidableEq β] (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (γ ⊕ β) (γ ⊕ β) ℂ) (hD : IsUnit X.toBlocks₂₂) (hH : IsUnit Y.toBlocks₂₂) : ofMatrix (CellJoin.join X Y) = reverseJoin (ofMatrix X) (ofMatrix Y)

theorem Complexity.ExactFourier.CellJoin.scalar_price {α γ : Type} [Fintype α] [Fintype γ] [DecidableEq α] [DecidableEq γ] (p : MatrixPrice) (X : Matrix (α ⊕ PUnit.{1}) (α ⊕ PUnit.{1}) ℂ) (Y : Matrix (γ ⊕ PUnit.{1}) (γ ⊕ PUnit.{1}) ℂ) (hX : IsUnit X) (hY : IsUnit Y) : p.value (join X Y) = p.value X + p.value Y

theorem Complexity.ExactFourier.Pivot.of_unit {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (K : Matrix (α ⊕ β) (α ⊕ β) ℂ) (hA : IsUnit K.toBlocks₁₁) (hD : IsUnit K.toBlocks₂₂) : IsUnit (ofMatrix K)

theorem Complexity.ExactFourier.Pivot.of_reindex_data {α β γ : Type} [Fintype β] [DecidableEq β] (e : α ≃ γ) (K : Matrix (α ⊕ β) (α ⊕ β) ℂ) : ofMatrix ((Matrix.reindex (e.sumCongr (Equiv.refl β)) (e.sumCongr (Equiv.refl β))) K) = (Matrix.reindex (e.sumCongr (Equiv.refl β)) (e.sumCongr (Equiv.refl β))) (ofMatrix K)

@[simp]

theorem Complexity.ExactFourier.Pivot.of_one {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] : ofMatrix 1 = 1

theorem Complexity.ExactFourier.Pivot.run_block_units {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (K : Matrix (α ⊕ β) (α ⊕ β) ℂ) (hA : IsUnit K.toBlocks₁₁) (hD : IsUnit K.toBlocks₂₂) (t : ℕ) : IsUnit (CellStream.run K t).toBlocks₁₁ ∧ IsUnit (CellStream.run K t).toBlocks₂₂

theorem Complexity.ExactFourier.Pivot.reverseJoin_scalar_price {α γ : Type} [Fintype α] [Fintype γ] [DecidableEq α] [DecidableEq γ] (p : MatrixPrice) (X : Matrix (α ⊕ PUnit.{1}) (α ⊕ PUnit.{1}) ℂ) (Y : Matrix (γ ⊕ PUnit.{1}) (γ ⊕ PUnit.{1}) ℂ) (hX : IsUnit X) (hY : IsUnit Y) : p.value (reverseJoin X Y) = p.value X + p.value Y

theorem Complexity.ExactFourier.Pivot.run_scalar_price {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (K : Matrix (α ⊕ PUnit.{1}) (α ⊕ PUnit.{1}) ℂ) (hK : IsUnit K) (t : ℕ) : p.value (CellStream.run K t) = ↑t * p.value K

theorem Complexity.ExactFourier.Pivot.run_pivot_price {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (K : Matrix (α ⊕ PUnit.{1}) (α ⊕ PUnit.{1}) ℂ) (hA : IsUnit K.toBlocks₁₁) (hD : IsUnit K.toBlocks₂₂) (t : ℕ) : p.value (ofMatrix (CellStream.run K t)) = ↑t * p.value (ofMatrix K)

theorem Complexity.ExactFourier.MatrixPrice.scalar_pivot_le {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (A : Matrix α α ℂ) (C : Matrix α PUnit.{1} ℂ) (B : Matrix PUnit.{1} α ℂ) (D : Matrix PUnit.{1} PUnit.{1} ℂ) (hA : IsUnit A) (hD : IsUnit D) (hK : IsUnit (Matrix.fromBlocks A C B D)) : p.value (Pivot.matrix A C B D) ≤ p.value (Matrix.fromBlocks A C B D)

theorem Complexity.ExactFourier.MatrixPrice.scalar_pivot {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (A : Matrix α α ℂ) (C : Matrix α PUnit.{1} ℂ) (B : Matrix PUnit.{1} α ℂ) (D : Matrix PUnit.{1} PUnit.{1} ℂ) (hA : IsUnit A) (hD : IsUnit D) (hK : IsUnit (Matrix.fromBlocks A C B D)) : p.value (Pivot.matrix A C B D) = p.value (Matrix.fromBlocks A C B D)

Exact scalar pivot invariance, 07-pivots:175--240. The proof uses finite single-port chains; its constant four is amortized without any continuity law.

noncomputable def Complexity.ExactFourier.BasisExchange.mix {α : Type} (U : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_2 + 1}) ℂ) (V : Matrix (α ⊕ PUnit.{u_3 + 1}) (α ⊕ PUnit.{u_2 + 1}) ℂ) : Matrix (α ⊕ PUnit.{u_3 + 1}) (α ⊕ PUnit.{u_2 + 1}) ℂ

Take the data rows from U and the selected-coordinate row from V.

Equations

• Complexity.ExactFourier.BasisExchange.mix U V = Matrix.fromBlocks U.toBlocks₁₁ U.toBlocks₁₂ V.toBlocks₂₁ V.toBlocks₂₂

theorem Complexity.ExactFourier.BasisExchange.mix_mul {α : Type} [Fintype α] (U : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_2 + 1}) ℂ) (V W : Matrix (α ⊕ PUnit.{u_2 + 1}) (α ⊕ PUnit.{u_2 + 1}) ℂ) : mix U V * W = mix (U * W) (V * W)

theorem Complexity.ExactFourier.BasisExchange.mix_one_left {α : Type} [DecidableEq α] (T : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_2 + 1}) ℂ) : mix 1 T = Matrix.fromBlocks 1 0 T.toBlocks₂₁ T.toBlocks₂₂

theorem Complexity.ExactFourier.BasisExchange.mix_one_right {α : Type} [DecidableEq α] (T : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_2 + 1}) ℂ) : mix T 1 = Matrix.fromBlocks T.toBlocks₁₁ T.toBlocks₁₂ 0 1

theorem Complexity.ExactFourier.BasisExchange.price_split {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (U V : Matrix (α ⊕ PUnit.{1}) (α ⊕ PUnit.{1}) ℂ) (hU : IsUnit U) (hV : IsUnit V) (hU' : IsUnit (mix U V)) (hV' : IsUnit (mix V U)) : p.value (mix V U * (mix U V)⁻¹) = p.value (V * U⁻¹)

def Complexity.ExactFourier.BasisExchange.isolate {ι : Type} [DecidableEq ι] (i : ι) : ι ≃ { j : ι // j ≠ i } ⊕ PUnit.{u_1 + 1}

Split one selected coordinate from the complement of that coordinate.

Equations

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

theorem Complexity.ExactFourier.BasisExchange.update_isolate {ι : Type} [DecidableEq ι] (U V : Matrix ι ι ℂ) (i : ι) : (Matrix.reindex (isolate i) (isolate i)) (U.updateRow i (V i)) = mix ((Matrix.reindex (isolate i) (isolate i)) U) ((Matrix.reindex (isolate i) (isolate i)) V)

theorem Complexity.ExactFourier.BasisExchange.price {ι : Type} [Fintype ι] [DecidableEq ι] (p : MatrixPrice) (U V : Matrix ι ι ℂ) (i : ι) (hU : IsUnit U) (hV : IsUnit V) (hU' : IsUnit (U.updateRow i (V i))) (hV' : IsUnit (V.updateRow i (U i))) : p.value (V.updateRow i (U i) * (U.updateRow i (V i))⁻¹) = p.value (V * U⁻¹)

Exchange any corresponding members of two bases, assuming exactly that both original and both exchanged lists are bases.

def Complexity.ExactFourier.DensePair.J (l : ℂ) : Matrix (Fin 4) (Fin 4) ℂ

The weighted four-cycle whose wraparound entry is l.

Equations

• Complexity.ExactFourier.DensePair.J l = !![0, 1, 0, 0; 0, 0, 1, 0; 0, 0, 0, 1; l, 0, 0, 0]

def Complexity.ExactFourier.DensePair.X (l : ℂ) : Matrix (Fin 4) (Fin 4) ℂ

The identity plus the weighted four-cycle J l.

Equations

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

def Complexity.ExactFourier.DensePair.Xb (l : ℂ) : Matrix (Fin 4) (Fin 4) ℂ

The four-cycle construction with its middle forward link removed.

Equations

• Complexity.ExactFourier.DensePair.Xb l = !![1, 1, 0, 0; 0, 1, 0, 0; 0, 0, 1, 1; l, 0, 0, 1]

def Complexity.ExactFourier.DensePair.Xd : Matrix (Fin 4) (Fin 4) ℂ

The identity plus the three forward links, with no wraparound link.

Equations

• Complexity.ExactFourier.DensePair.Xd = !![1, 1, 0, 0; 0, 1, 1, 0; 0, 0, 1, 1; 0, 0, 0, 1]

def Complexity.ExactFourier.DensePair.Y1 : Matrix (Fin 4) (Fin 4) ℂ

The first intermediate shear matrix in the dense-pair factorization.

Equations

• Complexity.ExactFourier.DensePair.Y1 = !![1, 0, 0, 0; 0, 1, 1, 0; 0, 0, 1, 0; 0, 0, 0, 1]

def Complexity.ExactFourier.DensePair.Y2 : Matrix (Fin 4) (Fin 4) ℂ

The second intermediate matrix, adding the first row's two forward links.

Equations

• Complexity.ExactFourier.DensePair.Y2 = !![1, 1, 1, 0; 0, 1, 1, 0; 0, 0, 1, 0; 0, 0, 0, 1]

def Complexity.ExactFourier.DensePair.Y3 : Matrix (Fin 4) (Fin 4) ℂ

The third intermediate matrix, retaining only the first row's added links.

Equations

• Complexity.ExactFourier.DensePair.Y3 = !![1, 1, 1, 0; 0, 1, 0, 0; 0, 0, 1, 0; 0, 0, 0, 1]

def Complexity.ExactFourier.DensePair.Y4 (l : ℂ) : Matrix (Fin 4) (Fin 4) ℂ

The fourth intermediate matrix, introducing the weighted wraparound link.

Equations

• Complexity.ExactFourier.DensePair.Y4 l = !![1, 1, 1, 0; 0, 1, 0, 0; 0, 0, 1, 0; l, 0, 0, 1]

def Complexity.ExactFourier.DensePair.Y5 (l : ℂ) : Matrix (Fin 4) (Fin 4) ℂ

The fifth intermediate matrix in the dense-pair row-operation sequence.

Equations

• Complexity.ExactFourier.DensePair.Y5 l = !![1, 1, 1, 0; 0, 1, 0, 0; l, 0, 1, 1; l, 0, 0, 1]

def Complexity.ExactFourier.DensePair.Y6 (l : ℂ) : Matrix (Fin 4) (Fin 4) ℂ

The final intermediate matrix before the rank-one correction.

Equations

• Complexity.ExactFourier.DensePair.Y6 l = !![1, 1, 1, 0; 0, 1, 0, 0; l, 0, 1, 1; 0, 0, 0, 1]

def Complexity.ExactFourier.DensePair.cycle : Equiv.Perm (Fin 4)

The backward cyclic permutation of four coordinates.

Equations

• Complexity.ExactFourier.DensePair.cycle = { toFun := ![3, 0, 1, 2], invFun := ![1, 2, 3, 0], left_inv := ⋯, right_inv := ⋯ }

theorem Complexity.ExactFourier.DensePair.J_monomial (l : ℂ) (hl : l ≠ 0) : MonomialMatrix (J l)

theorem Complexity.ExactFourier.DensePair.X_eq (l : ℂ) : X l = 1 + J l

theorem Complexity.ExactFourier.DensePair.det_J (l : ℂ) : (J l).det = -l

theorem Complexity.ExactFourier.DensePair.det_X (l : ℂ) : (X l).det = 1 - l

theorem Complexity.ExactFourier.DensePair.det_Xb (l : ℂ) : (Xb l).det = 1

theorem Complexity.ExactFourier.DensePair.det_Xd : Xd.det = 1

theorem Complexity.ExactFourier.DensePair.det_Y1 : Y1.det = 1

theorem Complexity.ExactFourier.DensePair.det_Y2 : Y2.det = 1

theorem Complexity.ExactFourier.DensePair.det_Y3 : Y3.det = 1

theorem Complexity.ExactFourier.DensePair.det_Y4 (l : ℂ) : (Y4 l).det = 1

theorem Complexity.ExactFourier.DensePair.det_Y5 (l : ℂ) : (Y5 l).det = 1

theorem Complexity.ExactFourier.DensePair.det_Y6 (l : ℂ) : (Y6 l).det = 1 - l

theorem Complexity.ExactFourier.DensePair.exchange01 (l : ℂ) : Matrix.updateRow 1 1 (X l 1) = Y1 ∧ (X l).updateRow 1 (1 1) = Xb l

theorem Complexity.ExactFourier.DensePair.exchange23 (l : ℂ) : Y2.updateRow 1 (Xb l 1) = Y3 ∧ (Xb l).updateRow 1 (Y2 1) = X l

theorem Complexity.ExactFourier.DensePair.exchange34 (l : ℂ) : Y3.updateRow 3 (X l 3) = Y4 l ∧ (X l).updateRow 3 (Y3 3) = Xd

theorem Complexity.ExactFourier.DensePair.exchange56 (l : ℂ) : (Y5 l).updateRow 3 (Xd 3) = Y6 l ∧ Xd.updateRow 3 (Y5 l 3) = X l

theorem Complexity.ExactFourier.DensePair.shear12 : Y2 = Matrix.transvection 0 1 1 * Y1

theorem Complexity.ExactFourier.DensePair.shear45 (l : ℂ) : Y5 l = Matrix.transvection 2 3 1 * Y4 l