Exact Fourier circuits: positive reach

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

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

theorem Complexity.ExactFourier.PositiveGeneration.Pattern.monomial_right {α : Type} [Fintype α] [DecidableEq α] {A H : Matrix α α ℂ} {k : ℕ} (h : Pattern A k H) (M : Matrix α α ℂ) (hM : MonomialMatrix M) : Pattern A k (H * M)

theorem Complexity.ExactFourier.PositiveGeneration.Pattern.mul {α : Type} [Fintype α] [DecidableEq α] {A H K : Matrix α α ℂ} {k l : ℕ} (hH : Pattern A k H) (hK : Pattern A l K) : Pattern A (k + l) (H * K)

def Complexity.ExactFourier.PositiveGeneration.Reach {α : Type} [Fintype α] [DecidableEq α] (A H : Matrix α α ℂ) : Prop

The matrix is realized by some positive word in A and monomial matrices.

Equations

• Complexity.ExactFourier.PositiveGeneration.Reach A H = ∃ (k : ℕ), Complexity.ExactFourier.PositiveGeneration.Pattern A k H

theorem Complexity.ExactFourier.PositiveGeneration.Reach.one {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) : Reach A 1

theorem Complexity.ExactFourier.PositiveGeneration.Reach.monomial {α : Type} [Fintype α] [DecidableEq α] (A M : Matrix α α ℂ) (hM : MonomialMatrix M) : Reach A M

theorem Complexity.ExactFourier.PositiveGeneration.Reach.self {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) : Reach A A

theorem Complexity.ExactFourier.PositiveGeneration.Reach.mul {α : Type} [Fintype α] [DecidableEq α] {A H K : Matrix α α ℂ} (hH : Reach A H) (hK : Reach A K) : Reach A (H * K)

theorem Complexity.ExactFourier.PositiveGeneration.Reach.unit {α : Type} [Fintype α] [DecidableEq α] {A H : Matrix α α ℂ} (hA : IsUnit A) (hH : Reach A H) : IsUnit H

def Complexity.ExactFourier.PositiveGeneration.directions {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) : Set (Matrix α α ℂ)

Diagonal directions conjugated by matrices reachable from A.

Equations

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

def Complexity.ExactFourier.PositiveGeneration.tangentSpan {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) : Submodule ℂ (Matrix α α ℂ)

The complex linear span of all reachable conjugated diagonal directions.

Equations

• Complexity.ExactFourier.PositiveGeneration.tangentSpan A = Submodule.span ℂ (Complexity.ExactFourier.PositiveGeneration.directions A)

theorem Complexity.ExactFourier.PositiveGeneration.direction_mem {α : Type} [Fintype α] [DecidableEq α] (A s : Matrix α α ℂ) (hs : Reach A s) (d : α → ℂ) : s * Matrix.diagonal d * s⁻¹ ∈ tangentSpan A

theorem Complexity.ExactFourier.PositiveGeneration.diagonal_mem {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (d : α → ℂ) : Matrix.diagonal d ∈ tangentSpan A

theorem Complexity.ExactFourier.PositiveGeneration.tangent_conj {α : Type} [Fintype α] [DecidableEq α] (A s : Matrix α α ℂ) (hs : Reach A s) {X : Matrix α α ℂ} (hX : X ∈ tangentSpan A) : s * X * s⁻¹ ∈ tangentSpan A

theorem Complexity.ExactFourier.PositiveGeneration.tangent_monomial_conj {α : Type} [Fintype α] [DecidableEq α] (A M : Matrix α α ℂ) (hM : MonomialMatrix M) (X : Matrix α α ℂ) (hX : X ∈ tangentSpan A) : M * X * M⁻¹ ∈ tangentSpan A

theorem Complexity.ExactFourier.PositiveGeneration.single_diagonal {α : Type} [DecidableEq α] (k : α) : Matrix.diagonal (Pi.single k 1) = Matrix.single k k 1

theorem Complexity.ExactFourier.PositiveGeneration.projector_apply {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (k i j : α) : (A * Matrix.single k k 1 * A⁻¹) i j = A i k * A⁻¹ k j

theorem Complexity.ExactFourier.PositiveGeneration.tangent_top {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (hA : IsUnit A) (hn : ¬MonomialMatrix A) : tangentSpan A = ⊤

noncomputable def Complexity.ExactFourier.PositiveGeneration.conjLinear {α : Type} [Fintype α] [DecidableEq α] (p : Matrix α α ℂ) : Matrix α α ℂ →ₗ[ℂ] Matrix α α ℂ

The linear map sending X to p * X * p⁻¹.

Equations

• Complexity.ExactFourier.PositiveGeneration.conjLinear p = { toFun := fun (X : Matrix α α ℂ) => p * X * p⁻¹, map_add' := ⋯, map_smul' := ⋯ }

def Complexity.ExactFourier.PositiveGeneration.diagLinear {α : Type} [DecidableEq α] : (α → ℂ) →ₗ[ℂ] Matrix α α ℂ

The complex linear map forming a diagonal matrix from its entries.

Equations

• Complexity.ExactFourier.PositiveGeneration.diagLinear = { toFun := Matrix.diagonal, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def Complexity.ExactFourier.PositiveGeneration.diagConj {α : Type} [Fintype α] [DecidableEq α] (p : Matrix α α ℂ) : Submodule ℂ (Matrix α α ℂ)

The subspace of diagonal matrices conjugated by p.

Equations

• Complexity.ExactFourier.PositiveGeneration.diagConj p = (Complexity.ExactFourier.PositiveGeneration.conjLinear p ∘ₗ Complexity.ExactFourier.PositiveGeneration.diagLinear).range

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.mem_diagConj {α : Type} [Fintype α] [DecidableEq α] (p X : Matrix α α ℂ) : X ∈ diagConj p ↔ ∃ (d : α → ℂ), p * Matrix.diagonal d * p⁻¹ = X

inductive Complexity.ExactFourier.PositiveGeneration.Chain {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) : Matrix α α ℂ → Submodule ℂ (Matrix α α ℂ) → Prop

A sequence of reachable products and the diagonal directions accumulated along it.

• nil {α : Type} [Fintype α] [DecidableEq α] {A : Matrix α α ℂ} : Chain A 1 (diagConj 1)
• snoc {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} {s : Matrix α α ℂ} : Chain A p U → Reach A s → Chain A (p * s) (U ⊔ diagConj (p * s))

theorem Complexity.ExactFourier.PositiveGeneration.Chain.reach {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (h : Chain A p U) : Reach A p

theorem Complexity.ExactFourier.PositiveGeneration.directions_after_span {α : Type} [Fintype α] [DecidableEq α] (A p : Matrix α α ℂ) (hA : IsUnit A) (hn : ¬MonomialMatrix A) (hp : IsUnit p) (U : Submodule ℂ (Matrix α α ℂ)) (h : ∀ (s : Matrix α α ℂ), Reach A s → diagConj (p * s) ≤ U) : U = ⊤

theorem Complexity.ExactFourier.PositiveGeneration.exists_full_chain {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (hA : IsUnit A) (hn : ¬MonomialMatrix A) : ∃ (p : Matrix α α ℂ), Chain A p ⊤

def Complexity.ExactFourier.PositiveGeneration.genericPoint (R : Type u_3) [CommRing R] [IsDomain R] : PrimeSpectrum R

The point of an integral domain's prime spectrum corresponding to the zero ideal.

Equations

• Complexity.ExactFourier.PositiveGeneration.genericPoint R = { asIdeal := ⊥, isPrime := ⋯ }

theorem Complexity.ExactFourier.PositiveGeneration.generic_mem_open {R : Type u_1} [CommRing R] [IsDomain R] {U : Set (PrimeSpectrum R)} (hU : IsOpen U) (hne : U.Nonempty) : genericPoint R ∈ U

theorem Complexity.ExactFourier.PositiveGeneration.constructible_generic_nhds {R : Type u_1} [CommRing R] [IsDomain R] {T : Set (PrimeSpectrum R)} (hT : Topology.IsConstructible T) : ∃ (U : Set (PrimeSpectrum R)), IsOpen U ∧ genericPoint R ∈ U ∧ ∀ x ∈ U, x ∈ T ↔ genericPoint R ∈ T

theorem Complexity.ExactFourier.PositiveGeneration.constructible_contains_basic {R : Type u_1} [CommRing R] [IsDomain R] {T : Set (PrimeSpectrum R)} (hT : Topology.IsConstructible T) (hg : genericPoint R ∈ T) : ∃ (g : R), g ≠ 0 ∧ ↑(PrimeSpectrum.basicOpen g) ⊆ T

theorem Complexity.ExactFourier.PositiveGeneration.dominant_open_image {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] (f : R →+* S) (hf : f.FinitePresentation) (hinj : Function.Injective ⇑f) (p : S) (hp : p ≠ 0) : ∃ (g : R), g ≠ 0 ∧ ↑(PrimeSpectrum.basicOpen g) ⊆ PrimeSpectrum.comap f '' ↑(PrimeSpectrum.basicOpen p)

A dominant finite-presentation map meets an actual nonempty basic open, not merely its closure. This is the open-image step in positive generation.

theorem Complexity.ExactFourier.PositiveGeneration.polynomial_hom_finitePresentation {ι κ : Type} [Finite ι] [Finite κ] (f : MvPolynomial ι ℂ →ₐ[ℂ] MvPolynomial κ ℂ) : f.FinitePresentation

theorem Complexity.ExactFourier.PositiveGeneration.maximal_avoiding {R : Type u_1} [CommRing R] [IsJacobsonRing R] (I : Ideal R) (hI : I.IsPrime) (p : R) (hp : p ∉ I) : ∃ (J : Ideal R), J.IsMaximal ∧ I ≤ J ∧ p ∉ J

theorem Complexity.ExactFourier.PositiveGeneration.polynomial_open_image {ι κ : Type} [Finite ι] [Finite κ] (f : MvPolynomial ι ℂ →ₐ[ℂ] MvPolynomial κ ℂ) (hinj : Function.Injective ⇑f) (p : MvPolynomial κ ℂ) (hp : p ≠ 0) : ∃ (g : MvPolynomial ι ℂ), g ≠ 0 ∧ ∀ (y : ι → ℂ), (MvPolynomial.aeval y) g ≠ 0 → ∃ (x : κ → ℂ), (MvPolynomial.aeval x) p ≠ 0 ∧ ∀ (i : ι), (MvPolynomial.aeval x) (f (MvPolynomial.X i)) = y i

Point-level consequence of Chevalley and the Nullstellensatz.

noncomputable def Complexity.ExactFourier.PositiveGeneration.polynomialMap {ι κ : Type} (f : MvPolynomial ι ℂ →ₐ[ℂ] MvPolynomial κ ℂ) (x : κ → ℂ) : ι → ℂ

The map on complex coordinate spaces induced by a polynomial substitution.

Equations

• Complexity.ExactFourier.PositiveGeneration.polynomialMap f x i = (MvPolynomial.aeval x) (f (MvPolynomial.X i))

theorem Complexity.ExactFourier.PositiveGeneration.eval_polynomialMap {ι κ : Type} (f : MvPolynomial ι ℂ →ₐ[ℂ] MvPolynomial κ ℂ) (x : κ → ℂ) (p : MvPolynomial ι ℂ) : (MvPolynomial.aeval (polynomialMap f x)) p = (MvPolynomial.aeval x) (f p)

theorem Complexity.ExactFourier.PositiveGeneration.injective_of_submersion {ι κ : Type} [Fintype ι] [Fintype κ] (f : MvPolynomial ι ℂ →ₐ[ℂ] MvPolynomial κ ℂ) (x : κ → ℂ) (d : (κ → ℂ) →L[ℂ] ι → ℂ) (hd : HasStrictFDerivAt (polynomialMap f) d x) (hs : (↑d).range = ⊤) : Function.Injective ⇑f

A surjective strict derivative certifies dominance, with no dimension reduction or extra algebraic hypotheses.