Rectangular kernels of block evaluations

Block evaluations of ∑ᵢ Aᵢ ⊗ Xᵢ, built from coefficient matrices Aᵢ and square witness matrices Xᵢ. If such an evaluation is injective, the matrices Aᵢ cannot map a subspace into a smaller one. Combined with small-subspace expansion, this shows that the reverse-Taylor tests have no nonzero kernel family of bounded support whenever the same coefficients admit an invertible block witness.

Main definitions

• Rectangular.blockEval: the block evaluation map on Fin e → Fin q → F.
• Rectangular.blockMatrix: the corresponding sum of Kronecker products.
• Rectangular.componentSpace, Rectangular.coefficientMatrix: the span of a family and the coordinates of its members in a basis of that span.
• Rectangular.imageCombination, Rectangular.concatMatrix: the combined images under several maps, and the concatenated coefficient matrix.

Main results

• Rectangular.no_shrunk_subspace: an injective block evaluation forbids shrinking subspaces.
• Rectangular.kernel_impossible: an expanding kernel family contradicts injectivity.
• Rectangular.blockEval_injective_of_isUnit: an invertible block matrix gives an injective block evaluation.
• RectangularExpansion.rectangular_kernel_zero: the reverse-Taylor tests have trivial bounded-support kernel families.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/Rectangular.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

def Cslib.Circuits.Rational.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.

theorem Cslib.Circuits.Rational.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

def Cslib.Circuits.Rational.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.

def Cslib.Circuits.Rational.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.

noncomputable def Cslib.Circuits.Rational.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.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 combined output map of the w * k component images.

def Cslib.Circuits.Rational.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.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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.