Exact Fourier circuits: boundary

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/Boundary.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.Boundary.quotientLinear (ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) : Polynomial ℂ →ₗ[ℂ] Polynomial ℂ

Division by a fixed monic polynomial as a complex linear map.

Equations

• Complexity.ExactFourier.Boundary.quotientLinear ℓ hℓ = { toFun := fun (f : Polynomial ℂ) => f /ₘ ℓ, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Complexity.ExactFourier.Boundary.quotientLinear_apply (ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (f : Polynomial ℂ) : (quotientLinear ℓ hℓ) f = f /ₘ ℓ

theorem Complexity.ExactFourier.Boundary.prefix_quotient_zero (ℓ f : Polynomial ℂ) (hℓ : ℓ.Monic) {d t b : ℕ} (ht : ℓ.natDegree = t) (hf : f.natDegree ≤ d) (hb : b + d < t) : f * Polynomial.X ^ b /ₘ ℓ = 0

Inputs strictly before the final d times do not cross the coefficient boundary.

theorem Complexity.ExactFourier.Boundary.quotient_degree_lt (ℓ f : Polynomial ℂ) (hℓ : ℓ.Monic) {d t b : ℕ} (ht : ℓ.natDegree = t) (hd : 0 < d) (hf : f.natDegree ≤ d) (hb : b < t) : (f * Polynomial.X ^ b /ₘ ℓ).natDegree < d

The quotient, with sign reversed, has strictly fewer than d coefficients.

theorem Complexity.ExactFourier.Boundary.quotient_shift_expansion (ℓ f : Polynomial ℂ) (hℓ : ℓ.Monic) {d : ℕ} (hf : f.natDegree ≤ d) (b : ℕ) : f * Polynomial.X ^ b /ₘ ℓ = ∑ j ∈ Finset.range (d + 1), f.coeff j • (Polynomial.X ^ (b + j) /ₘ ℓ)

Exact division of a shifted matrix entry. This keeps the generator coefficients on the left, ready for the ordered J_i*G_j matrix formula.

theorem Complexity.ExactFourier.Boundary.boundary_difference (ℓ f : Polynomial ℂ) (b : ℕ) : f * Polynomial.X ^ b %ₘ ℓ - f * Polynomial.X ^ b = -ℓ * (f * Polynomial.X ^ b /ₘ ℓ)

Entrywise modulus reduction differs from time truncation by minus the modulus times precisely the quotient above. No bounds on coefficients are imposed.

noncomputable def Complexity.ExactFourier.Boundary.timeMatrix {ι : Type} (t : ℕ) (G : Matrix ι ι (Polynomial ℂ)) : Matrix (Fin t × ι) (Fin t × ι) ℂ

Truncated coefficient matrix of multiplication by the polynomial matrix G.

Equations

• Complexity.ExactFourier.Boundary.timeMatrix t G a b = (G a.2 b.2 * Polynomial.X ^ ↑b.1).coeff ↑a.1

noncomputable def Complexity.ExactFourier.Boundary.modulusMatrix {ι : Type} (t : ℕ) (ℓ : Polynomial ℂ) (G : Matrix ι ι (Polynomial ℂ)) : Matrix (Fin t × ι) (Fin t × ι) ℂ

Coefficient matrix of multiplication by G followed by reduction modulo ℓ.

Equations

• Complexity.ExactFourier.Boundary.modulusMatrix t ℓ G a b = (G a.2 b.2 * Polynomial.X ^ ↑b.1 %ₘ ℓ).coeff ↑a.1

theorem Complexity.ExactFourier.Boundary.correction_prefix_zero {ι : Type} {t d : ℕ} (G : Matrix ι ι (Polynomial ℂ)) (ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (ht : ℓ.natDegree = t) (hG : ∀ (i j : ι), (G i j).natDegree ≤ d) (a b : Fin t × ι) (hb : ↑b.1 < t - d) : (modulusMatrix t ℓ G - timeMatrix t G) a b = 0

The modulus correction has no columns at times b<t-d.

noncomputable def Complexity.ExactFourier.Boundary.orderedWeight (η ℓ : Polynomial ℂ) (a b i j : ℕ) : ℂ

Scalar weights for the exact ordered generator formula. Prefix correction uses η=1. The suffix uses the first t coefficients of ℓ/u^k.

Equations

• Complexity.ExactFourier.Boundary.orderedWeight η ℓ a b i j = -(η * Polynomial.X ^ i * (Polynomial.X ^ (b + j) /ₘ ℓ)).coeff a

theorem Complexity.ExactFourier.Boundary.polynomial_ordered_expansion (η ℓ f g : Polynomial ℂ) (hℓ : ℓ.Monic) {d e : ℕ} (hg : g.natDegree ≤ d) (hf : f.natDegree ≤ e) (b : ℕ) : η * f * -(g * Polynomial.X ^ b /ₘ ℓ) = ∑ i ∈ Finset.range (e + 1), ∑ j ∈ Finset.range (d + 1), (f.coeff i * g.coeff j) • -(η * Polynomial.X ^ i * (Polynomial.X ^ (b + j) /ₘ ℓ))

noncomputable def Complexity.ExactFourier.Boundary.coefficientMatrix {ι κ : Type} (G : Matrix ι κ (Polynomial ℂ)) (j : ℕ) : Matrix ι κ ℂ

Extract one coefficient from every entry of a polynomial matrix.

Equations

• Complexity.ExactFourier.Boundary.coefficientMatrix G j u v = (G u v).coeff j

noncomputable def Complexity.ExactFourier.Boundary.weightedCorrection {ι : Type} [Fintype ι] (η ℓ : Polynomial ℂ) (J G : Matrix ι ι (Polynomial ℂ)) (b : ℕ) : Matrix ι ι (Polynomial ℂ)

Polynomial correction for a single input time b, before taking its output coefficient. Matrix multiplication is in the original order J then G.

Equations

• Complexity.ExactFourier.Boundary.weightedCorrection η ℓ J G b u v = ∑ x : ι, η * J u x * -(G x v * Polynomial.X ^ b /ₘ ℓ)

theorem Complexity.ExactFourier.Boundary.ordered_span {ι : Type} [Fintype ι] (η ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (J G : Matrix ι ι (Polynomial ℂ)) {d e : ℕ} (hG : ∀ (u v : ι), (G u v).natDegree ≤ d) (hJ : ∀ (u v : ι), (J u v).natDegree ≤ e) (a b : ℕ) : coefficientMatrix (weightedCorrection η ℓ J G b) a = ∑ i ∈ Finset.range (e + 1), ∑ j ∈ Finset.range (d + 1), orderedWeight η ℓ a b i j • (coefficientMatrix J i * coefficientMatrix G j)

Exact ordered-span part of the coefficient-boundary comparison. There is no commutation hypothesis on any pair of spatial coefficient matrices.

theorem Complexity.ExactFourier.Boundary.orderedWeight_prefix (ℓ : Polynomial ℂ) (a b i j : ℕ) : orderedWeight 1 ℓ a b i j = if i ≤ a then -(Polynomial.X ^ (b + j) /ₘ ℓ).coeff (a - i) else 0

Explicit prefix coefficient convention, including negative (a-i) indices.

theorem Complexity.ExactFourier.Boundary.prefix_row_vanishes {ι : Type} [Fintype ι] (ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (J G : Matrix ι ι (Polynomial ℂ)) {d e t a b : ℕ} (ht : ℓ.natDegree = t) (hd : 0 < d) (hG : ∀ (u v : ι), (G u v).natDegree ≤ d) (hJ : ∀ (u v : ι), (J u v).natDegree ≤ e) (hb : b < t) (ha : e + d ≤ a) : coefficientMatrix (weightedCorrection 1 ℓ J G b) a = 0

The prefix correction J*v has no coefficients at times a>=e+d.

theorem Complexity.ExactFourier.Boundary.weightedCorrection_prefix_zero {ι : Type} [Fintype ι] (η ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (J G : Matrix ι ι (Polynomial ℂ)) {d t b : ℕ} (ht : ℓ.natDegree = t) (hG : ∀ (u v : ι), (G u v).natDegree ≤ d) (hb : b + d < t) : weightedCorrection η ℓ J G b = 0

No weighted correction has an input column before the suffix.

noncomputable def Complexity.ExactFourier.Boundary.activeCorrection {ι : Type} [Fintype ι] (t d : ℕ) (η ℓ : Polynomial ℂ) (J G : Matrix ι ι (Polynomial ℂ)) : Matrix (Fin t × ι) (Fin t × ι) ℂ

The actual early--suffix formula after the scalar prefix conjugation.

Equations

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

def Complexity.ExactFourier.Boundary.ActiveTime (t d e a : ℕ) : Prop

Times in the initial or final boundary region where a correction can act.

Equations

• Complexity.ExactFourier.Boundary.ActiveTime t d e a = (a < min (t - d) (e + d) ∨ t - d ≤ a)

@[instance_reducible]

instance Complexity.ExactFourier.Boundary.instDecidableActiveTime (t d e a : ℕ) : Decidable (ActiveTime t d e a)

Equations

• Complexity.ExactFourier.Boundary.instDecidableActiveTime t d e a = id inferInstance

theorem Complexity.ExactFourier.Boundary.activeCorrection_column_support {ι : Type} [Fintype ι] (t d : ℕ) (η ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (J G : Matrix ι ι (Polynomial ℂ)) (ht : ℓ.natDegree = t) (hG : ∀ (u v : ι), (G u v).natDegree ≤ d) (a b : Fin t × ι) (hb : ↑b.1 < t - d) : activeCorrection t d η ℓ J G a b = 0

theorem Complexity.ExactFourier.Boundary.activeCorrection_row_support {ι : Type} [Fintype ι] (t d e : ℕ) (η ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (J G : Matrix ι ι (Polynomial ℂ)) (ht : ℓ.natDegree = t) (hd : 0 < d) (hG : ∀ (u v : ι), (G u v).natDegree ≤ d) (hJ : ∀ (u v : ι), (J u v).natDegree ≤ e) (a b : Fin t × ι) (ha : ¬ActiveTime t d e ↑a.1) : activeCorrection t d η ℓ J G a b = 0

theorem Complexity.ExactFourier.Boundary.supported_identity_decomposition {κ : Type} [DecidableEq κ] (S : κ → Prop) [DecidablePred S] (L : Matrix κ κ ℂ) (hrow : ∀ (i j : κ), ¬S i → L i j = 0) (hcol : ∀ (i j : κ), ¬S j → L i j = 0) : (1 + L).submatrix ⇑(Equiv.sumCompl S) ⇑(Equiv.sumCompl S) = Matrix.fromBlocks (1 + L.submatrix Subtype.val Subtype.val) 0 0 1

Simultaneous row/column permutation isolates every matrix correction supported on a single active index set, with an exact identity on its complement.

theorem Complexity.ExactFourier.Boundary.active_identity_decomposition {ι : Type} [Fintype ι] [DecidableEq ι] (t d e : ℕ) (η ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (J G : Matrix ι ι (Polynomial ℂ)) (ht : ℓ.natDegree = t) (hd : 0 < d) (hG : ∀ (u v : ι), (G u v).natDegree ≤ d) (hJ : ∀ (u v : ι), (J u v).natDegree ≤ e) : let S := fun (a : Fin t × ι) => ActiveTime t d e ↑a.1; (1 + activeCorrection t d η ℓ J G).submatrix ⇑(Equiv.sumCompl S) ⇑(Equiv.sumCompl S) = Matrix.fromBlocks (1 + (activeCorrection t d η ℓ J G).submatrix Subtype.val Subtype.val) 0 0 1

noncomputable def Complexity.ExactFourier.Boundary.seriesMatrix {ι : Type} [Fintype ι] [DecidableEq ι] : Matrix ι ι (Polynomial ℂ) →+* Matrix ι ι (PowerSeries ℂ)

Embed polynomial matrices into formal power series matrices entrywise.

Equations

• Complexity.ExactFourier.Boundary.seriesMatrix = Polynomial.coeToPowerSeries.ringHom.mapMatrix

@[simp]

theorem Complexity.ExactFourier.Boundary.seriesMatrix_apply {ι : Type} [Fintype ι] [DecidableEq ι] (G : Matrix ι ι (Polynomial ℂ)) (i j : ι) : seriesMatrix G i j = ↑(G i j)

theorem Complexity.ExactFourier.Boundary.timeMatrix_eq_trunc {ι : Type} [Fintype ι] [DecidableEq ι] (t : ℕ) (G : Matrix ι ι (Polynomial ℂ)) : timeMatrix t G = (CoefficientTime.blockTruncHom t) (seriesMatrix G)

noncomputable def Complexity.ExactFourier.Boundary.quotientColumns {ι : Type} (t : ℕ) (ℓ : Polynomial ℂ) (G : Matrix ι ι (Polynomial ℂ)) : Matrix ι (Fin t × ι) (PowerSeries ℂ)

Negated quotient columns for the discrepancy between remainder and truncation.

Equations

• Complexity.ExactFourier.Boundary.quotientColumns t ℓ G i b = ↑(-(G i b.2 * Polynomial.X ^ ↑b.1 /ₘ ℓ))

theorem Complexity.ExactFourier.Boundary.difference_eq_columns {ι : Type} (t : ℕ) (ℓ : Polynomial ℂ) (G : Matrix ι ι (Polynomial ℂ)) : modulusMatrix t ℓ G - timeMatrix t G = CoefficientTime.coefficientColumns t (↑ℓ • quotientColumns t ℓ G)

The exact remainder-minus-truncation map: minus the quotient times ℓ.

theorem Complexity.ExactFourier.Boundary.timeMatrix_inverse {ι : Type} [Fintype ι] [DecidableEq ι] (t : ℕ) (u : Polynomial ℂ) (G J : Matrix ι ι (Polynomial ℂ)) (hu : u.coeff 0 ≠ 0) (hGJ : G * J = (Matrix.scalar ι) u) : (timeMatrix t G)⁻¹ = (CoefficientTime.blockTruncHom t) ((↑u)⁻¹ • seriesMatrix J)

The polynomial adjugate/denominator identity gives the TRUE inverse, before any support reduction. This is not an inverse evaluation assumption.

theorem Complexity.ExactFourier.Boundary.inverse_mul_difference {ι : Type} [Fintype ι] [DecidableEq ι] (t : ℕ) (u ℓ : Polynomial ℂ) (G J : Matrix ι ι (Polynomial ℂ)) (hu : u.coeff 0 ≠ 0) (hGJ : G * J = (Matrix.scalar ι) u) : (timeMatrix t G)⁻¹ * (modulusMatrix t ℓ G - timeMatrix t G) = CoefficientTime.coefficientColumns t ((↑ℓ * (↑u)⁻¹) • (seriesMatrix J * quotientColumns t ℓ G))

The relative correction is the coefficient map of (ℓ/u) J v, with the quotient sign included in v.

theorem Complexity.ExactFourier.Boundary.prefix_scalar_cancels {ι κ : Type} [Fintype ι] [DecidableEq ι] (t T : ℕ) (f η : PowerSeries ℂ) (hfη : f * η = 1) (V : Matrix ι κ (PowerSeries ℂ)) (a : Fin t × ι) (b : κ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CoefficientTime.prefixScalar t T f) 1 * CoefficientTime.coefficientColumns t (η • V)) a b = if ↑a.1 < T then (PowerSeries.coeff ↑a.1) (V a.2 b) else (PowerSeries.coeff ↑a.1) (η * V a.2 b)

A prefix-only scalar convolution cancels the denominator on early rows, and literally leaves the late rows unchanged.

theorem Complexity.ExactFourier.Boundary.coeff_trunc_mul_series (t : ℕ) (η V : PowerSeries ℂ) (a : Fin t) : (PowerSeries.coeff ↑a) (↑((PowerSeries.trunc t) η) * V) = (PowerSeries.coeff ↑a) (η * V)

Coefficients below t cannot see the discarded tail of a scalar series.

theorem Complexity.ExactFourier.Boundary.weightedCorrection_series {ι : Type} [Fintype ι] [DecidableEq ι] (t : ℕ) (η ℓ : Polynomial ℂ) (J G : Matrix ι ι (Polynomial ℂ)) (i : ι) (b : Fin t × ι) : ↑(weightedCorrection η ℓ J G (↑b.1) i b.2) = ↑η * (seriesMatrix J * quotientColumns t ℓ G) i b

Converting the finite polynomial ordered generator formula to series changes neither matrix order nor the sign of the quotient.

theorem Complexity.ExactFourier.Boundary.weightedCorrection_trunc_coeff {ι : Type} [Fintype ι] [DecidableEq ι] (t : ℕ) (η : PowerSeries ℂ) (ℓ : Polynomial ℂ) (J G : Matrix ι ι (Polynomial ℂ)) (a b : Fin t × ι) : (weightedCorrection ((PowerSeries.trunc t) η) ℓ J G (↑b.1) a.2 b.2).coeff ↑a.1 = (PowerSeries.coeff ↑a.1) (η * (seriesMatrix J * quotientColumns t ℓ G) a.2 b)

The finite polynomial η used in the ordered-span certificate is exactly the first t coefficients of ℓ/u; no truncation error survives in any output row.

theorem Complexity.ExactFourier.Boundary.quotientColumns_prefix_zero {ι : Type} (t d : ℕ) (ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (ht : ℓ.natDegree = t) (G : Matrix ι ι (Polynomial ℂ)) (hG : ∀ (i j : ι), (G i j).natDegree ≤ d) (i : ι) (b : Fin t × ι) (hb : ↑b.1 < t - d) : quotientColumns t ℓ G i b = 0

Quotient columns vanish on the whole coefficient prefix, not merely on an assumed active direct summand.

theorem Complexity.ExactFourier.Boundary.inverse_difference_prefix_zero {ι : Type} [Fintype ι] [DecidableEq ι] (t d : ℕ) (u ℓ : Polynomial ℂ) (G J : Matrix ι ι (Polynomial ℂ)) (hu : u.coeff 0 ≠ 0) (hGJ : G * J = (Matrix.scalar ι) u) (hℓ : ℓ.Monic) (ht : ℓ.natDegree = t) (hG : ∀ (i j : ι), (G i j).natDegree ≤ d) (a b : Fin t × ι) (hb : ↑b.1 < t - d) : ((timeMatrix t G)⁻¹ * (modulusMatrix t ℓ G - timeMatrix t G)) a b = 0

The actual relative map I+S is fixed on its right by every prefix map.

theorem Complexity.ExactFourier.Boundary.prefix_mul_inverse_difference {ι : Type} [Fintype ι] [DecidableEq ι] (t d : ℕ) (u ℓ : Polynomial ℂ) (G J : Matrix ι ι (Polynomial ℂ)) (hu : u.coeff 0 ≠ 0) (hℓ0 : ℓ.coeff 0 ≠ 0) (hGJ : G * J = (Matrix.scalar ι) u) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CoefficientTime.prefixScalar t (t - d) (↑u * (↑ℓ)⁻¹)) 1 * ((timeMatrix t G)⁻¹ * (modulusMatrix t ℓ G - timeMatrix t G)) = activeCorrection t d ((PowerSeries.trunc t) (↑ℓ * (↑u)⁻¹)) ℓ J G

Premultiplication of the literal relative correction gives exactly the previously certified finite activeCorrection matrix.

theorem Complexity.ExactFourier.Boundary.prefix_conjugated_relative_map {ι : Type} [Fintype ι] [DecidableEq ι] (t d : ℕ) (u ℓ : Polynomial ℂ) (G J : Matrix ι ι (Polynomial ℂ)) (hu : u.coeff 0 ≠ 0) (hℓ0 : ℓ.coeff 0 ≠ 0) (hGJ : G * J = (Matrix.scalar ι) u) (hG0 : IsUnit (G.map fun (f : Polynomial ℂ) => f.coeff 0)) (hℓ : ℓ.Monic) (ht : ℓ.natDegree = t) (hG : ∀ (i j : ι), (G i j).natDegree ≤ d) : have P := Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CoefficientTime.prefixScalar t (t - d) (↑u * (↑ℓ)⁻¹)) 1; P * ((timeMatrix t G)⁻¹ * modulusMatrix t ℓ G) * P⁻¹ = 1 + activeCorrection t d ((PowerSeries.trunc t) (↑ℓ * (↑u)⁻¹)) ℓ J G