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.taylorCoordinates_symm {K : Type u_1} [Field K] (M : ℕ) (a : K) : (SmallExpansion.taylorCoordinates M a).symm = SmallExpansion.taylorCoordinates M (-a)

The inverse of taylorCoordinates M a is 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

(reverseCoordinates M).symm reverses the index j to 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

The (i, j) matrix entry of (reverseTaylorCoordinates M a).symm is the degree-i coefficient of (X + C (-a)) ^ j.rev.

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.full_embed {K : Type u_1} [Field K] (M : ℕ) (a : K) : embed.mapMatrix (full M a) = LinearMap.toMatrix' (SmallExpansion.testMap M a)

Mapping embed over full M a gives the matrix of testMap M a.

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

Every entry of padded M N a has polynomial degree at most 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

Matrix-vector multiplication by raw A R expands blockwise over i and γ.

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_injective {K : Type u_1} [Field K] (q M N : ℕ) (hNM : N ≤ M) : Function.Injective ⇑(extend q M N)

Zero-padding from N to M columns is injective when N ≤ M.

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

When 1 ≤ q ≤ B, M = N + 2 * w ^ 3 * B, and B * (2 * w ^ 3 * B) < M, the rank threshold satisfies (q - 1) * M < q * N.

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)

Evaluating padded M N a i j along HahnSeries.C.comp φ at HahnSeries.single 1 1 equals embed (padded M N (φ a) i j).