Rank of the padded test matrices

The reverse-Taylor test at a point is realised by a polynomial matrix full M a in a fresh indeterminate t; zeroing its columns of index at least N gives padded M N a. Through the embedding t ↦ X into Laurent series, the rectangular kernel theorem yields a lower bound q * N on the rank of the block matrix formed from coefficient matrices and padded tests. The padded entries are polynomials of degree at most M - 1 and commute with coefficient maps.

Main definitions

• TestPolynomial.full, TestPolynomial.padded: the full and padded reverse-Taylor test matrices over K[X].
• TestPolynomial.embed: the embedding K[X] →+* K⸨X⸩.
• PaddedRank.raw: the block matrix ∑ᵢ Aᵢ ⊗ Rᵢ, written entrywise.
• PaddedRank.extend: zero-padding of vectors from N to M columns per block.

Main results

• TestPolynomial.full_embed: the embedded full test matrix is the matrix of testMap.
• PaddedRank.rank_ge: the padded block matrix has rank at least q * N.
• PaddedRank.numeric_gap: the arithmetic gap (q - 1) * M < q * N.
• TestPolynomial.eval₂_padded: padded tests commute with coefficient ring homomorphisms.

References

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

theorem Cslib.Circuits.Rational.TestPolynomial.polynomialMap_single {K : Type u_1} [Field K] (M : ℕ) (b : Fin M) : (SmallExpansion.polynomialMap M) (Pi.single b 1) = Polynomial.X ^ ↑b

theorem Cslib.Circuits.Rational.TestPolynomial.taylorCoordinates_symm {K : Type u_1} [Field K] (M : ℕ) (a : K) : (SmallExpansion.taylorCoordinates M a).symm = SmallExpansion.taylorCoordinates M (-a)

theorem Cslib.Circuits.Rational.TestPolynomial.reverseCoordinates_symm_apply {K : Type u_1} [Field K] (M : ℕ) (x : Fin M → K) : (SmallExpansion.reverseCoordinates M).symm x = fun (j : Fin M) => x j.rev

theorem Cslib.Circuits.Rational.TestPolynomial.reverseTaylor_symm_matrix {K : Type u_1} [Field K] (M : ℕ) (a : K) (i j : Fin M) : LinearMap.toMatrix' (↑(SmallExpansion.reverseTaylorCoordinates M a).symm) i j = ((Polynomial.X + Polynomial.C (-a)) ^ ↑j.rev).coeff ↑i

noncomputable def Cslib.Circuits.Rational.TestPolynomial.full {K : Type u_1} [Field K] (M : ℕ) (a : K) : Matrix (Fin M) (Fin M) (Polynomial K)

The reverse-Taylor test matrix over the univariate polynomial ring in t. Summation over all M Taylor coordinates appends only zero terms.

noncomputable def Cslib.Circuits.Rational.TestPolynomial.padded {K : Type u_1} [Field K] (M N : ℕ) (a : K) : Matrix (Fin M) (Fin M) (Polynomial K)

The polynomial test matrix with columns above the threshold set to zero.

noncomputable def Cslib.Circuits.Rational.TestPolynomial.embed {K : Type u_1} [Field K] : Polynomial K →+* LaurentReduction.F K

The original t indeterminate embeds into the fresh Laurent indeterminate.

theorem Cslib.Circuits.Rational.TestPolynomial.embed_C {K : Type u_1} [Field K] (a : K) : embed (Polynomial.C a) = HahnSeries.C a

theorem Cslib.Circuits.Rational.TestPolynomial.embed_X_pow {K : Type u_1} [Field K] (a : ℕ) : embed (Polynomial.X ^ a) = (HahnSeries.single ↑a) 1

theorem Cslib.Circuits.Rational.TestPolynomial.full_embed {K : Type u_1} [Field K] (M : ℕ) (a : K) : embed.mapMatrix (full M a) = LinearMap.toMatrix' (SmallExpansion.testMap M a)

theorem Cslib.Circuits.Rational.TestPolynomial.full_natDegree_le {K : Type u_1} [Field K] (M : ℕ) (a : K) (i j : Fin M) : (full M a i j).natDegree ≤ M - 1

theorem Cslib.Circuits.Rational.TestPolynomial.padded_natDegree_le {K : Type u_1} [Field K] (M N : ℕ) (a : K) (i j : Fin M) : (padded M N a i j).natDegree ≤ M - 1

noncomputable def Cslib.Circuits.Rational.PaddedRank.raw {K : Type u_1} [Field K] {w q M : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) (LaurentReduction.F K)) (R : Fin w → Matrix (Fin M) (Fin M) (LaurentReduction.F K)) : Matrix (Fin q × Fin M) (Fin q × Fin M) (LaurentReduction.F K)

The full block matrix formed from the coefficient and test matrices.

theorem Cslib.Circuits.Rational.PaddedRank.raw_apply {K : Type u_1} [Field K] {w q M : ℕ} (A : Fin w → Matrix (Fin q) (Fin q) (LaurentReduction.F K)) (R : Fin w → Matrix (Fin M) (Fin M) (LaurentReduction.F K)) (f : Fin q × Fin M → LaurentReduction.F K) (α : Fin q) (j : Fin M) : (raw A R).mulVec f (α, j) = ∑ i : Fin w, ∑ γ : Fin q, A i α γ * (R i).mulVec (fun (b : Fin M) => f (γ, b)) j

def Cslib.Circuits.Rational.PaddedRank.extend {K : Type u_1} [Field K] (q M N : ℕ) : (Fin q × Fin N → LaurentReduction.F K) →ₗ[LaurentReduction.F K] Fin q × Fin M → LaurentReduction.F K

Pad vectors in the truncated column space with zeros.

theorem Cslib.Circuits.Rational.PaddedRank.extend_low {K : Type u_1} [Field K] (q M N : ℕ) (f : Fin q × Fin N → LaurentReduction.F K) (α : Fin q) (j : Fin M) : N ≤ ↑j → (extend q M N) f (α, j) = 0

theorem Cslib.Circuits.Rational.PaddedRank.extend_injective {K : Type u_1} [Field K] (q M N : ℕ) (hNM : N ≤ M) : Function.Injective ⇑(extend q M N)

theorem Cslib.Circuits.Rational.PaddedRank.padded_mulVec_low {K : Type u_1} [Field K] (M N : ℕ) (a : K) (f : Fin M → LaurentReduction.F K) (hf : ∀ (j : Fin M), N ≤ ↑j → f j = 0) : (TestPolynomial.embed.mapMatrix (TestPolynomial.padded M N a)).mulVec f = (SmallExpansion.testMap M a) f

theorem Cslib.Circuits.Rational.PaddedRank.rank_ge {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)) : q * N ≤ (raw A fun (i : Fin w) => TestPolynomial.embed.mapMatrix (TestPolynomial.padded M N (points i))).rank

The padded test matrices satisfy a rectangular rank lower bound, using an invertible witness and the expansion theorem.

theorem Cslib.Circuits.Rational.PaddedRank.numeric_gap (w B M N q : ℕ) (hq : 1 ≤ q) (hqB : q ≤ B) (hMN : M = N + 2 * w ^ 3 * B) (hM : B * (2 * w ^ 3 * B) < M) : (q - 1) * M < q * N

theorem Cslib.Circuits.Rational.TestPolynomial.map_taylor_coeff {K : Type u_1} {E : Type u_2} [Field K] [Field E] (φ : K →+* E) (a : K) (j r : ℕ) : φ (((Polynomial.X + Polynomial.C a) ^ j).coeff r) = ((Polynomial.X + Polynomial.C (φ a)) ^ j).coeff r

theorem Cslib.Circuits.Rational.TestPolynomial.full_map {K : Type u_1} {E : Type u_2} [Field K] [Field E] (φ : K →+* E) (M : ℕ) (a : K) (i j : Fin M) : Polynomial.map φ (full M a i j) = full M (φ a) i j

theorem Cslib.Circuits.Rational.TestPolynomial.padded_map {K : Type u_1} {E : Type u_2} [Field K] [Field E] (φ : K →+* E) (M N : ℕ) (a : K) (i j : Fin M) : Polynomial.map φ (padded M N a i j) = padded M N (φ a) i j

theorem Cslib.Circuits.Rational.TestPolynomial.eval₂_padded {K : Type u_1} {E : Type u_2} [Field K] [Field E] (φ : K →+* E) (M N : ℕ) (a : K) (i j : Fin M) : Polynomial.eval₂ (HahnSeries.C.comp φ) ((HahnSeries.single 1) 1) (padded M N a i j) = embed (padded M N (φ a) i j)