Exact Fourier circuits: port matrices

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

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

theorem Complexity.ExactFourier.Reindexed.unit {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (A : Matrix ι ι ℂ) (hA : IsUnit A) : IsUnit ((Matrix.reindex e e) A)

theorem Complexity.ExactFourier.Reindexed.mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (A B : Matrix ι ι ℂ) : (Matrix.reindex e e) (A * B) = (Matrix.reindex e e) A * (Matrix.reindex e e) B

theorem Complexity.ExactFourier.Reindexed.symm_apply_apply {ι : Type fourierU1} {κ : Type fourierU2} (e : ι ≃ κ) (A : Matrix ι ι ℂ) : (Matrix.reindex e.symm e.symm) ((Matrix.reindex e e) A) = A

theorem Complexity.ExactFourier.Reindexed.apply_symm_apply {ι : Type fourierU1} {κ : Type fourierU2} (e : ι ≃ κ) (A : Matrix κ κ ℂ) : (Matrix.reindex e e) ((Matrix.reindex e.symm e.symm) A) = A

def Complexity.ExactFourier.OnePort.splitRight (ι : Type u_1) (κ : Type u_2) : ι × (PUnit.{u_3 + 1} ⊕ κ) ≃ ι ⊕ ι × κ

The shared coordinate is explicitly a single PUnit port, not an unspecified padding block.

Equations

• Complexity.ExactFourier.OnePort.splitRight ι κ = (Equiv.prodSumDistrib ι PUnit.{?u.1 + 1} κ).trans ((Equiv.prodPUnit ι).sumCongr (Equiv.refl (ι × κ)))

def Complexity.ExactFourier.OnePort.splitLeft (ι : Type u_1) (κ : Type u_2) : (ι ⊕ PUnit.{u_3 + 1}) × κ ≃ ι × κ ⊕ κ

Distribute a product over a sum whose distinguished left factor is a singleton.

Equations

• Complexity.ExactFourier.OnePort.splitLeft ι κ = (Equiv.sumProdDistrib ι PUnit.{?u.1 + 1} κ).trans ((Equiv.refl (ι × κ)).sumCongr (Equiv.punitProd κ))

noncomputable def Complexity.ExactFourier.OnePort.firstSelected {α β : Type} [DecidableEq α] [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_1 + 1}) ℂ) : Matrix ((α ⊕ PUnit.{u_1 + 1}) × (PUnit.{u_2 + 1} ⊕ β)) ((α ⊕ PUnit.{u_1 + 1}) × (PUnit.{u_3 + 1} ⊕ β)) ℂ

Apply the first matrix on the selected singleton port and fix the remaining block.

Equations

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

noncomputable def Complexity.ExactFourier.OnePort.firstRest {α β : Type} [DecidableEq α] [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_1 + 1}) ℂ) : Matrix ((α ⊕ PUnit.{u_1 + 1}) × (PUnit.{u_2 + 1} ⊕ β)) ((α ⊕ PUnit.{u_1 + 1}) × (PUnit.{u_3 + 1} ⊕ β)) ℂ

Apply copies of the first matrix away from the selected singleton port.

Equations

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

noncomputable def Complexity.ExactFourier.OnePort.secondSelected {α β : Type} [DecidableEq α] [DecidableEq β] (B : Matrix (PUnit.{u_1 + 1} ⊕ β) (PUnit.{u_1 + 1} ⊕ β) ℂ) : Matrix ((α ⊕ PUnit.{u_2 + 1}) × (PUnit.{u_1 + 1} ⊕ β)) ((α ⊕ PUnit.{u_3 + 1}) × (PUnit.{u_1 + 1} ⊕ β)) ℂ

Apply the second matrix on the selected singleton port of the first factor.

Equations

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

noncomputable def Complexity.ExactFourier.OnePort.secondRest {α β : Type} [DecidableEq α] [DecidableEq β] (B : Matrix (PUnit.{u_1 + 1} ⊕ β) (PUnit.{u_1 + 1} ⊕ β) ℂ) : Matrix ((α ⊕ PUnit.{u_2 + 1}) × (PUnit.{u_1 + 1} ⊕ β)) ((α ⊕ PUnit.{u_3 + 1}) × (PUnit.{u_1 + 1} ⊕ β)) ℂ

Apply copies of the second matrix away from the first factor's selected port.

Equations

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

theorem Complexity.ExactFourier.OnePort.reindex_first_all {α β : Type} [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_2 + 1}) ℂ) : (Matrix.reindex (splitRight (α ⊕ PUnit.{u_1 + 1}) β) (splitRight (α ⊕ PUnit.{u_2 + 1}) β)) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A 1) = Matrix.fromBlocks A 0 0 (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A 1)

theorem Complexity.ExactFourier.OnePort.reindex_second_all {α β : Type} [DecidableEq α] (B : Matrix (PUnit.{u_1 + 1} ⊕ β) (PUnit.{u_2 + 1} ⊕ β) ℂ) : (Matrix.reindex (splitLeft α (PUnit.{u_1 + 1} ⊕ β)) (splitLeft α (PUnit.{u_2 + 1} ⊕ β))) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 B) = Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 B) 0 0 B

theorem Complexity.ExactFourier.OnePort.first_factorization {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_1 + 1}) ℂ) : firstSelected A * firstRest A = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A 1

theorem Complexity.ExactFourier.OnePort.second_factorization {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (B : Matrix (PUnit.{u_1 + 1} ⊕ β) (PUnit.{u_1 + 1} ⊕ β) ℂ) : secondRest B * secondSelected B = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 B

def Complexity.ExactFourier.OnePort.plane {α β : Type} : (α ⊕ PUnit.{u_2 + 1}) × (PUnit.{u_1 + 1} ⊕ β) ≃ ((α ⊕ PUnit.{u_2 + 1}) ⊕ β) ⊕ α × β

The selected row and column have one shared coordinate. Their complement is exactly the Cartesian product of the two unshared data sets.

Equations

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

noncomputable def Complexity.ExactFourier.OnePort.unionFirst {α β : Type} [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_2 + 1}) ℂ) : Matrix ((α ⊕ PUnit.{u_1 + 1}) ⊕ β) ((α ⊕ PUnit.{u_2 + 1}) ⊕ β) ℂ

Extend the first port matrix by the identity on the second matrix's remaining coordinates.

Equations

• Complexity.ExactFourier.OnePort.unionFirst A = Matrix.fromBlocks A 0 0 1

noncomputable def Complexity.ExactFourier.OnePort.unionSecond {α β : Type} [DecidableEq α] (B : Matrix (PUnit.{u_1 + 1} ⊕ β) (PUnit.{u_2 + 1} ⊕ β) ℂ) : Matrix ((α ⊕ PUnit.{u_1 + 1}) ⊕ β) ((α ⊕ PUnit.{u_2 + 1}) ⊕ β) ℂ

Extend the second port matrix by the identity on the first matrix's remaining coordinates.

Equations

• Complexity.ExactFourier.OnePort.unionSecond B = (Matrix.reindex (Equiv.sumAssoc α PUnit.{?u.2 + 1} β).symm (Equiv.sumAssoc α PUnit.{?u.1 + 1} β).symm) (Matrix.fromBlocks 1 0 0 B)

noncomputable def Complexity.ExactFourier.OnePort.product {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_1 + 1}) ℂ) (B : Matrix (PUnit.{u_1 + 1} ⊕ β) (PUnit.{u_1 + 1} ⊕ β) ℂ) : Matrix ((α ⊕ PUnit.{u_1 + 1}) ⊕ β) ((α ⊕ PUnit.{u_1 + 1}) ⊕ β) ℂ

Apply the first and then the second matrix on their union with one shared port.

Equations

• Complexity.ExactFourier.OnePort.product A B = Complexity.ExactFourier.OnePort.unionSecond B * Complexity.ExactFourier.OnePort.unionFirst A

theorem Complexity.ExactFourier.OnePort.plane_first {α β : Type} [DecidableEq α] [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_1 + 1}) ℂ) : (Matrix.reindex plane plane) (firstSelected A) = Matrix.fromBlocks (unionFirst A) 0 0 1

theorem Complexity.ExactFourier.OnePort.plane_second {α β : Type} [DecidableEq α] [DecidableEq β] (B : Matrix (PUnit.{u_1 + 1} ⊕ β) (PUnit.{u_1 + 1} ⊕ β) ℂ) : (Matrix.reindex plane plane) (secondSelected B) = Matrix.fromBlocks (unionSecond B) 0 0 1

theorem Complexity.ExactFourier.OnePort.selected_unit {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_1 + 1}) ℂ) (B : Matrix (PUnit.{u_2 + 1} ⊕ β) (PUnit.{u_2 + 1} ⊕ β) ℂ) (hA : IsUnit A) (hB : IsUnit B) : IsUnit (firstSelected A) ∧ IsUnit (secondSelected B)

theorem Complexity.ExactFourier.OnePort.rest_unit {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_1 + 1}) ℂ) (B : Matrix (PUnit.{u_2 + 1} ⊕ β) (PUnit.{u_2 + 1} ⊕ β) ℂ) (hA : IsUnit A) (hB : IsUnit B) : IsUnit (firstRest A) ∧ IsUnit (secondRest B)

theorem Complexity.ExactFourier.OnePort.union_unit {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_1 + 1}) ℂ) (B : Matrix (PUnit.{u_2 + 1} ⊕ β) (PUnit.{u_2 + 1} ⊕ β) ℂ) (hA : IsUnit A) (hB : IsUnit B) : IsUnit (unionFirst A) ∧ IsUnit (unionSecond B)

theorem Complexity.ExactFourier.OnePort.product_isUnit {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix (α ⊕ PUnit.{u_1 + 1}) (α ⊕ PUnit.{u_1 + 1}) ℂ) (B : Matrix (PUnit.{u_1 + 1} ⊕ β) (PUnit.{u_1 + 1} ⊕ β) ℂ) (hA : IsUnit A) (hB : IsUnit B) : IsUnit (product A B)

theorem Complexity.ExactFourier.OnePort.union_prices {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (A : Matrix (α ⊕ PUnit.{1}) (α ⊕ PUnit.{1}) ℂ) (B : Matrix (PUnit.{1} ⊕ β) (PUnit.{1} ⊕ β) ℂ) (hA : IsUnit A) (hB : IsUnit B) : p.value (unionFirst A) = p.value A ∧ p.value (unionSecond B) = p.value B

theorem Complexity.ExactFourier.OnePort.rest_prices {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (A : Matrix (α ⊕ PUnit.{1}) (α ⊕ PUnit.{1}) ℂ) (B : Matrix (PUnit.{1} ⊕ β) (PUnit.{1} ⊕ β) ℂ) (hA : IsUnit A) (hB : IsUnit B) : p.value (firstRest A) = ↑(Fintype.card β) * p.value A ∧ p.value (secondRest B) = ↑(Fintype.card α) * p.value B

theorem Complexity.ExactFourier.OnePort.selected_product_price {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (A : Matrix (α ⊕ PUnit.{1}) (α ⊕ PUnit.{1}) ℂ) (B : Matrix (PUnit.{1} ⊕ β) (PUnit.{1} ⊕ β) ℂ) (hA : IsUnit A) (hB : IsUnit B) : p.value (secondSelected B * firstSelected A) = p.value (product A B)

theorem Complexity.ExactFourier.OnePort.price {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (A : Matrix (α ⊕ PUnit.{1}) (α ⊕ PUnit.{1}) ℂ) (B : Matrix (PUnit.{1} ⊕ β) (PUnit.{1} ⊕ β) ℂ) (hA : IsUnit A) (hB : IsUnit B) : p.value (product A B) = p.value A + p.value B

noncomputable def Complexity.ExactFourier.rectangularShear {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] (G : Matrix ι κ ℂ) : Matrix (ι ⊕ κ) (ι ⊕ κ) ℂ

The upper block shear with identity diagonal and off-diagonal block G.

Equations

• Complexity.ExactFourier.rectangularShear G = Matrix.fromBlocks 1 G 0 1

theorem Complexity.ExactFourier.rectangularShear_unit {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (G : Matrix ι κ ℂ) : IsUnit (rectangularShear G)

def Complexity.ExactFourier.replayOrder {n a k : ℕ} : (Fin a ⊕ Fin n) ⊕ Fin k ≃ (Fin n ⊕ Fin k) ⊕ Fin a

Move the dirty gate memory into a literal identity summand.

Equations

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

theorem Complexity.ExactFourier.replayMatrix_reindex {n a k : ℕ} (G : Matrix (Fin a) (Fin n) ℂ) : (Matrix.reindex replayOrder replayOrder) (Matrix.fromBlocks (rectangularShear G) 0 0 1) = replayMatrix G

theorem Complexity.ExactFourier.MatrixPrice.rectangularShear_bound (p : MatrixPrice) {n a : ℕ} (C : LinearDAG n a) (G : Matrix (Fin a) (Fin n) ℂ) (hG : ∀ (x : Fin n → ℂ), C.eval x = G.mulVec x) : p.value (rectangularShear G) ≤ 8 * ↑C.size + 2 * ↑a

theorem Complexity.ExactFourier.rectangularShear_mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (G H : Matrix ι κ ℂ) : rectangularShear G * rectangularShear H = rectangularShear (G + H)

theorem Complexity.ExactFourier.rectangularShear_inv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (G : Matrix ι κ ℂ) : (rectangularShear G)⁻¹ = rectangularShear (-G)

theorem Complexity.ExactFourier.MatrixPrice.rectangularShear_neg (p : MatrixPrice) {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (G : Matrix ι κ ℂ) : p.value (rectangularShear (-G)) = p.value (rectangularShear G)

noncomputable def Complexity.ExactFourier.lowerShear {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] (G : Matrix κ ι ℂ) : Matrix (ι ⊕ κ) (ι ⊕ κ) ℂ

The lower block shear with identity diagonal and off-diagonal block G.

Equations

• Complexity.ExactFourier.lowerShear G = Matrix.fromBlocks 1 0 G 1

theorem Complexity.ExactFourier.lowerShear_reindex {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] (G : Matrix κ ι ℂ) : (Matrix.reindex (Equiv.sumComm κ ι) (Equiv.sumComm κ ι)) (rectangularShear G) = lowerShear G

theorem Complexity.ExactFourier.lowerShear_unit {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (G : Matrix κ ι ℂ) : IsUnit (lowerShear G)

theorem Complexity.ExactFourier.MatrixPrice.lowerShear_price (p : MatrixPrice) {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (G : Matrix κ ι ℂ) : p.value (lowerShear G) = p.value (rectangularShear G)

theorem Complexity.ExactFourier.signedSwap_monomial {ι : Type u_1} [DecidableEq ι] : MonomialMatrix (Matrix.fromBlocks 0 1 (-1) 0)

theorem Complexity.ExactFourier.twoWay_identity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (G : Matrix ι ι ℂ) (hG : IsUnit G) : rectangularShear G * lowerShear (-G⁻¹) * rectangularShear G = Matrix.fromBlocks 0 G (-G⁻¹) 0

theorem Complexity.ExactFourier.MatrixPrice.twoWay_bound (p : MatrixPrice) {ι : Type} [Fintype ι] [DecidableEq ι] (G : Matrix ι ι ℂ) (hG : IsUnit G) : 2 * p.value G ≤ 2 * p.value (rectangularShear G) + p.value (rectangularShear G⁻¹)

Necessary pre-corner price bound: both the forward and inverse circuits are charged.