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.component, Rectangular.coefficientMatrix: the span of a family, its members in that span, and their coordinates 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

If blockEval A X is injective with 0 < e and every A i maps V into W, then finrank F V ≤ 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.

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.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.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)

If blockMatrix A X is a unit, then blockEval A X is injective.

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.