Rational hitting lists: padded rank

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

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

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

theorem Complexity.RationalHitting.TestPolynomial.taylor_matrix {K : Type u_1} [Field K] (M : ℕ) (a : K) (i j : Fin M) : LinearMap.toMatrix' (↑(SmallExpansion.taylorCoordinates M a)) i j = ((Polynomial.X + Polynomial.C a) ^ ↑j).coeff ↑i

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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.

Equations

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

noncomputable def Complexity.RationalHitting.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.

Equations

• Complexity.RationalHitting.TestPolynomial.padded M N a i j = if ↑j < N then Complexity.RationalHitting.TestPolynomial.full M a i j else 0

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

The original t indeterminate embeds into the fresh Laurent indeterminate.

Equations

• Complexity.RationalHitting.TestPolynomial.embed = Polynomial.eval₂RingHom HahnSeries.C ((HahnSeries.single 1) 1)

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

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

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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.

Equations

• Complexity.RationalHitting.PaddedRank.raw A R a b = ∑ i : Fin w, A i a.1 b.1 * R i a.2 b.2

theorem Complexity.RationalHitting.PaddedRank.raw_apply {K : Type v_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 Complexity.RationalHitting.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.

Equations

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

theorem Complexity.RationalHitting.PaddedRank.extend_low {K : Type v_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 Complexity.RationalHitting.PaddedRank.extend_injective {K : Type v_1} [Field K] (q M N : ℕ) (hNM : N ≤ M) : Function.Injective ⇑(extend q M N)

theorem Complexity.RationalHitting.PaddedRank.padded_mulVec_low {K : Type v_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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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)