Rational hitting lists: rectangular

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

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

def Complexity.RationalHitting.Rectangular.blockEval {F : Type u_1} [Field F] {w q e : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F) (X : Fin w → Matrix (Fin e) (Fin e) F) : (Fin e → Fin q → F) →ₗ[F] Fin e → Fin q → F

The ordinary Kronecker evaluation, with the two vector indices curried in reverse order. This is only a coordinate convention.

Equations

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

theorem Complexity.RationalHitting.Rectangular.no_shrunk_subspace {F : Type u_1} [Field F] {w q e : ℕ} (he : 0 < e) (A : Fin w → Matrix (Fin q) (Fin q) F) (X : Fin w → Matrix (Fin e) (Fin e) F) (hX : Function.Injective ⇑(blockEval A X)) (V W : Submodule F (Fin q → F)) (hVW : ∀ (i : Fin w), Submodule.map (A i).mulVecLin V ≤ W) : Module.finrank F ↥V ≤ Module.finrank F ↥W

theorem Complexity.RationalHitting.Rectangular.blockEval_injective_of_leftInverse {F : Type u_1} [Field F] {w q e : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F) (X : Fin w → Matrix (Fin e) (Fin e) F) (J : (Fin e → Fin q → F) →ₗ[F] Fin e → Fin q → F) (hJ : J ∘ₗ blockEval A X = LinearMap.id) : Function.Injective ⇑(blockEval A X)

Full-rank blocks preserve the dimension of a common input subspace; this form avoids any unwarranted specialization of Laurent-series coefficients.

def Complexity.RationalHitting.Rectangular.componentSpace {F : Type u_1} [Field F] {P : Type u_2} [AddCommGroup P] [Module F P] {q : ℕ} (f : Fin q → P) : Submodule F P

The subspace spanned by the components of a vector.

Equations

• Complexity.RationalHitting.Rectangular.componentSpace f = Submodule.span F (Set.range f)

def Complexity.RationalHitting.Rectangular.component {F : Type u_1} [Field F] {P : Type u_2} [AddCommGroup P] [Module F P] {q : ℕ} (f : Fin q → P) (α : Fin q) : ↥(componentSpace f)

A component regarded as a vector in the component span.

Equations

• Complexity.RationalHitting.Rectangular.component f α = ⟨f α, ⋯⟩

noncomputable def Complexity.RationalHitting.Rectangular.coefficientMatrix {F : Type u_1} [Field F] {P : Type u_2} [AddCommGroup P] [Module F P] {q k : ℕ} (f : Fin q → P) (b : Module.Basis (Fin k) F ↥(componentSpace f)) : Matrix (Fin q) (Fin k) F

Coordinates of each component in a basis of their span.

Equations

• Complexity.RationalHitting.Rectangular.coefficientMatrix f b α = b.equivFun (Complexity.RationalHitting.Rectangular.component f α)

theorem Complexity.RationalHitting.Rectangular.span_component_top {F : Type u_1} [Field F] {P : Type u_2} [AddCommGroup P] [Module F P] {q : ℕ} (f : Fin q → P) : Submodule.span F (Set.range (component f)) = ⊤

theorem Complexity.RationalHitting.Rectangular.rank_coefficientMatrix {F : Type u_1} [Field F] {P : Type u_2} [AddCommGroup P] [Module F P] {q k : ℕ} (f : Fin q → P) (b : Module.Basis (Fin k) F ↥(componentSpace f)) : (coefficientMatrix f b).rank = k

theorem Complexity.RationalHitting.Rectangular.coefficientMatrix_expansion {F : Type u_1} [Field F] {P : Type u_2} [AddCommGroup P] [Module F P] {q k : ℕ} (f : Fin q → P) (b : Module.Basis (Fin k) F ↥(componentSpace f)) (α : Fin q) : ∑ j : Fin k, coefficientMatrix f b α j • ↑(b j) = f α

def Complexity.RationalHitting.Rectangular.imageCombination {F : Type u_1} [Field F] {P : Type u_2} {Q : Type u_3} [AddCommGroup P] [Module F P] [AddCommGroup Q] [Module F Q] {w k : ℕ} (T : Fin w → P →ₗ[F] Q) (u : Fin k → P) : (Fin w × Fin k → F) →ₗ[F] Q

The output map of the wk possible component images.

Equations

• Complexity.RationalHitting.Rectangular.imageCombination T u = Fintype.linearCombination F fun (ij : Fin w × Fin k) => (T ij.1) (u ij.2)

def Complexity.RationalHitting.Rectangular.concatMatrix {F : Type u_1} [Field F] {w q k : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F) (P : Matrix (Fin q) (Fin k) F) : Matrix (Fin q) (Fin w × Fin k) F

The concatenated coefficient matrix.

Equations

• Complexity.RationalHitting.Rectangular.concatMatrix A P α ij = (A ij.1 * P) α ij.2

theorem Complexity.RationalHitting.Rectangular.concat_row_relation {F : Type u_1} [Field F] {P : Type u_2} {Q : Type u_3} [AddCommGroup P] [Module F P] [AddCommGroup Q] [Module F Q] {w q k : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F) (T : Fin w → P →ₗ[F] Q) (f : Fin q → P) (b : Module.Basis (Fin k) F ↥(componentSpace f)) (hker : ∀ (α : Fin q), ∑ i : Fin w, ∑ γ : Fin q, A i α γ • (T i) (f γ) = 0) (α : Fin q) : (concatMatrix A (coefficientMatrix f b)).row α ∈ (imageCombination T fun (j : Fin k) => ↑(b j)).ker

theorem Complexity.RationalHitting.Rectangular.rank_concat_lt {F : Type u_1} [Field F] {P : Type u_2} {Q : Type u_3} [AddCommGroup P] [Module F P] [AddCommGroup Q] [Module F Q] {w q k : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F) (T : Fin w → P →ₗ[F] Q) (f : Fin q → P) (b : Module.Basis (Fin k) F ↥(componentSpace f)) (hker : ∀ (α : Fin q), ∑ i : Fin w, ∑ γ : Fin q, A i α γ • (T i) (f γ) = 0) (hex : (w - 1) * k < Module.finrank F ↥(imageCombination T fun (j : Fin k) => ↑(b j)).range) (hw : 1 ≤ w) : (concatMatrix A (coefficientMatrix f b)).rank < k

theorem Complexity.RationalHitting.Rectangular.coefficient_image_le_concat {F : Type u_1} [Field F] {w q k : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F) (P : Matrix (Fin q) (Fin k) F) (i : Fin w) : Submodule.map (A i).mulVecLin (Submodule.span F (Set.range P.col)) ≤ Submodule.span F (Set.range (concatMatrix A P).col)

theorem Complexity.RationalHitting.Rectangular.component_image_le_range {F : Type u_1} [Field F] {P : Type u_2} {Q : Type u_3} [AddCommGroup P] [Module F P] [AddCommGroup Q] [Module F Q] {w q k : ℕ} (T : Fin w → P →ₗ[F] Q) (f : Fin q → P) (b : Module.Basis (Fin k) F ↥(componentSpace f)) (i : Fin w) : Submodule.map (T i) (componentSpace f) ≤ (imageCombination T fun (j : Fin k) => ↑(b j)).range

theorem Complexity.RationalHitting.Rectangular.kernel_impossible {F : Type u_1} [Field F] {P : Type u_2} {Q : Type u_3} [AddCommGroup P] [Module F P] [AddCommGroup Q] [Module F Q] {w q k e : ℕ} (hw : 1 ≤ w) (he : 0 < e) (A : Fin w → Matrix (Fin q) (Fin q) F) (T : Fin w → P →ₗ[F] Q) (X : Fin w → Matrix (Fin e) (Fin e) F) (hX : Function.Injective ⇑(blockEval A X)) (f : Fin q → P) (b : Module.Basis (Fin k) F ↥(componentSpace f)) (hker : ∀ (α : Fin q), ∑ i : Fin w, ∑ γ : Fin q, A i α γ • (T i) (f γ) = 0) (hex : (w - 1) * k < Module.finrank F ↥(imageCombination T fun (j : Fin k) => ↑(b j)).range) : False

A kernel vector with sufficiently expansive component span contradicts any invertible block evaluation of the same coefficient matrices.

def Complexity.RationalHitting.Rectangular.blockMatrix {F : Type u_1} [Field F] {w q e : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F) (X : Fin w → Matrix (Fin e) (Fin e) F) : Matrix (Fin q × Fin e) (Fin q × Fin e) F

The block matrix obtained as a sum of Kronecker products.

Equations

• Complexity.RationalHitting.Rectangular.blockMatrix A X = ∑ i : Fin w, Matrix.kroneckerMap (fun (x1 x2 : F) => x1 * x2) (A i) (X i)

theorem Complexity.RationalHitting.Rectangular.blockMatrix_mulVec {F : Type u_1} [Field F] {w q e : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F) (X : Fin w → Matrix (Fin e) (Fin e) F) (v : Fin e → Fin q → F) (α : Fin q) (β : Fin e) : (blockMatrix A X).mulVec (fun (j : Fin q × Fin e) => v j.2 j.1) (α, β) = (blockEval A X) v β α

theorem Complexity.RationalHitting.Rectangular.blockEval_injective_of_isUnit {F : Type u_1} [Field F] {w q e : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) F) (X : Fin w → Matrix (Fin e) (Fin e) F) (h : IsUnit (blockMatrix A X)) : Function.Injective ⇑(blockEval A X)

theorem Complexity.RationalHitting.RectangularExpansion.rectangular_kernel_zero {K : Type u_1} [Field K] [CharZero K] (w B M N q e : ℕ) (hw : 1 ≤ w) (hN : 1 ≤ N) (hMN : M = N + 2 * w ^ 3 * B) (hq : q ≤ B) (he : 0 < e) (points : Fin w → K) (hp : Function.Injective points) (A : Fin w → Matrix (Fin q) (Fin q) (LaurentReduction.F K)) (X : Fin w → Matrix (Fin e) (Fin e) (LaurentReduction.F K)) (hX : Function.Injective ⇑(Rectangular.blockEval A X)) (f : Fin q → Fin M → LaurentReduction.F K) (hf : ∀ (α : Fin q) (j : Fin M), N ≤ ↑j → f α j = 0) (hker : ∀ (α : Fin q), ∑ i : Fin w, ∑ γ : Fin q, A i α γ • (SmallExpansion.testMap M (points i)) (f γ) = 0) : f = 0

The rectangular Taylor tests have no nonzero kernel component family when the same coefficients have an invertible matrix witness.