Rational hitting lists: deformation

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

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

noncomputable def Complexity.RationalHitting.QuantumLift.polynomialLift {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) K) : Matrix (ZMod d) (ZMod d) (MvPolynomial (Fin 2) K)

The two-parameter polynomial lift.

Equations

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

theorem Complexity.RationalHitting.QuantumLift.polynomialLift_embed {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) K) : PolynomialHahn.embed.mapMatrix (polynomialLift χ R) = (representation χ) (liftD χ R)

theorem Complexity.RationalHitting.QuantumLift.polynomialLift_specialize {K : Type u_1} [Field K] [CharZero K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (hχ : χ.IsPrimitive) (R : Matrix (ZMod d) (ZMod d) K) : (MvPolynomial.aeval fun (x : Fin 2) => 1).mapMatrix (polynomialLift χ R) = R

noncomputable def Complexity.RationalHitting.QuantumLift.blockPolynomial {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) {m : Type u_2} (A : Matrix m m (Matrix (ZMod d) (ZMod d) K)) : Matrix (m × ZMod d) (m × ZMod d) (MvPolynomial (Fin 2) K)

Flatten a block matrix after applying the polynomial lift to each block.

Equations

• Complexity.RationalHitting.QuantumLift.blockPolynomial χ A i j = Complexity.RationalHitting.QuantumLift.polynomialLift χ (A i.1 j.1) i.2 j.2

def Complexity.RationalHitting.QuantumLift.blockOriginal {K : Type u_1} {d : ℕ} {m : Type u_2} (A : Matrix m m (Matrix (ZMod d) (ZMod d) K)) : Matrix (m × ZMod d) (m × ZMod d) K

Flatten the original block matrix over the coefficient field.

Equations

• Complexity.RationalHitting.QuantumLift.blockOriginal A i j = A i.1 j.1 i.2 j.2

theorem Complexity.RationalHitting.QuantumLift.blockPolynomial_embed {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) {m : Type u_2} [Fintype m] [DecidableEq m] (A : Matrix m m (Matrix (ZMod d) (ZMod d) K)) : PolynomialHahn.embed.mapMatrix (blockPolynomial χ A) = (BlockDivision.blockEmbedding (representation χ)) fun (i j : m) => liftD χ (A i j)

theorem Complexity.RationalHitting.QuantumLift.blockPolynomial_specialize {K : Type u_1} [Field K] [CharZero K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) {m : Type u_2} [Fintype m] [DecidableEq m] (hχ : χ.IsPrimitive) (A : Matrix m m (Matrix (ZMod d) (ZMod d) K)) : (MvPolynomial.aeval fun (x : Fin 2) => 1).mapMatrix (blockPolynomial χ A) = blockOriginal A

theorem Complexity.RationalHitting.QuantumLift.blockPolynomial_det_ne_zero {K : Type u_1} [Field K] [CharZero K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) {m : Type u_2} [Fintype m] [DecidableEq m] (hχ : χ.IsPrimitive) (A : Matrix m m (Matrix (ZMod d) (ZMod d) K)) (hm : 1 ≤ Fintype.card m) (hA : (Fintype.card m - 1) * d < (blockOriginal A).rank) : (blockPolynomial χ A).det ≠ 0

The rank gap forces the determinant of the actual polynomial lift to be nonzero. The Hahn division ring is only a proof device; the resulting polynomial is the original finite Fourier lift, not a new generator.

noncomputable def Complexity.RationalHitting.ThreeLift.coeffP {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) (Polynomial K)) (a b : ZMod d) : Polynomial K

Coefficient polynomials for the exact cyclic-diagonal Fourier transform.

Equations

• Complexity.RationalHitting.ThreeLift.coeffP χ R a b = Polynomial.C (↑d)⁻¹ * ∑ j : ZMod d, Polynomial.C (χ (-a * j)) * R j (j - b)

noncomputable def Complexity.RationalHitting.ThreeLift.uni {K : Type u_1} [Field K] : Polynomial K →+* MvPolynomial (Fin 3) K

Embed the univariate parameter as the first of three polynomial variables.

Equations

• Complexity.RationalHitting.ThreeLift.uni = Polynomial.eval₂RingHom MvPolynomial.C (MvPolynomial.X 0)

noncomputable def Complexity.RationalHitting.ThreeLift.lift {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) (Polynomial K)) : Matrix (ZMod d) (ZMod d) (MvPolynomial (Fin 3) K)

The three-parameter polynomial lift, before specialization.

Equations

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

noncomputable def Complexity.RationalHitting.ThreeLift.specialize {K : Type u_1} {E : Type u_2} [Field K] [Field E] (φ : K →+* E) (t : E) : MvPolynomial (Fin 3) K →+* MvPolynomial (Fin 2) E

Embed t into a coefficient field, leaving p,r polynomial indeterminates.

Equations

• Complexity.RationalHitting.ThreeLift.specialize φ t = MvPolynomial.eval₂Hom (MvPolynomial.C.comp φ) fun (i : Fin (2 + 1)) => Fin.cases (MvPolynomial.C t) MvPolynomial.X i

theorem Complexity.RationalHitting.ThreeLift.specialize_uni {K : Type u_1} {E : Type u_2} [Field K] [Field E] (φ : K →+* E) (t : E) (p : Polynomial K) : (specialize φ t) (uni p) = MvPolynomial.C (Polynomial.eval₂ φ t p)

theorem Complexity.RationalHitting.ThreeLift.coeffP_eval {K : Type u_1} {E : Type u_2} [Field K] [Field E] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (φ : K →+* E) (t : E) (R : Matrix (ZMod d) (ZMod d) (Polynomial K)) (a b : ZMod d) : Polynomial.eval₂ φ t (coeffP χ R a b) = QuantumMatrices.fourierCoeff ((↑φ).compAddChar χ) ((Polynomial.eval₂RingHom φ t).mapMatrix R) a b

theorem Complexity.RationalHitting.ThreeLift.weyl_map {K : Type v_1} {E : Type v_2} [Field K] [Field E] {d : ℕ} (χ : AddChar (ZMod d) K) (φ : K →+* E) (a b i j : ZMod d) : φ (QuantumMatrices.weyl χ a b i j) = QuantumMatrices.weyl ((↑φ).compAddChar χ) a b i j

theorem Complexity.RationalHitting.ThreeLift.specialize_lift {K : Type u_1} {E : Type u_2} [Field K] [Field E] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (φ : K →+* E) (t : E) (R : Matrix (ZMod d) (ZMod d) (Polynomial K)) : (specialize φ t).mapMatrix (lift χ R) = QuantumLift.polynomialLift ((↑φ).compAddChar χ) ((Polynomial.eval₂RingHom φ t).mapMatrix R)

theorem Complexity.RationalHitting.ThreeLift.uni_totalDegree_le {K : Type u_1} [Field K] (p : Polynomial K) : (uni p).totalDegree ≤ p.natDegree

theorem Complexity.RationalHitting.ThreeLift.coeffP_natDegree_le {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) (Polynomial K)) (D : ℕ) (hR : ∀ (i j : ZMod d), (R i j).natDegree ≤ D) (a b : ZMod d) : (coeffP χ R a b).natDegree ≤ D

theorem Complexity.RationalHitting.ThreeLift.lift_totalDegree_le {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) (Polynomial K)) (D : ℕ) (hR : ∀ (i j : ZMod d), (R i j).natDegree ≤ D) (i j : ZMod d) : (lift χ R i j).totalDegree ≤ D + 2 * (d - 1)

noncomputable def Complexity.RationalHitting.PencilDeformation.test {K : Type u_1} [Field K] (M N : ℕ) [NeZero M] (a : K) : Matrix (ZMod M) (ZMod M) (Polynomial K)

The truncated polynomial test matrix, reindexed by cyclic indices.

Equations

• Complexity.RationalHitting.PencilDeformation.test M N a = (Matrix.reindex (ZMod.finEquiv M).toEquiv (ZMod.finEquiv M).toEquiv) (Complexity.RationalHitting.TestPolynomial.padded M N a)

noncomputable def Complexity.RationalHitting.PencilDeformation.polyBlocks {K : Type u_1} [Field K] {w q M N : ℕ} [NeZero M] (A : Fin w → Matrix (Fin q) (Fin q) K) (points : Fin w → K) : Matrix (Fin q) (Fin q) (Matrix (ZMod M) (ZMod M) (Polynomial K))

Combine coefficient matrices with polynomial test blocks.

Equations

• Complexity.RationalHitting.PencilDeformation.polyBlocks A points α β = ∑ i : Fin w, A i α β • Complexity.RationalHitting.PencilDeformation.test M N (points i)

noncomputable def Complexity.RationalHitting.PencilDeformation.polynomial {K : Type u_1} [Field K] {w q M N : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (A : Fin w → Matrix (Fin q) (Fin q) K) (points : Fin w → K) : Matrix (Fin q × ZMod M) (Fin q × ZMod M) (MvPolynomial (Fin 3) K)

The polynomial matrix obtained by applying the three-parameter lift.

Equations

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

theorem Complexity.RationalHitting.PencilDeformation.specialize {K : Type v_1} {E : Type v_2} [Field K] [Field E] {w q M N : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (φ : K →+* E) (t : E) (A : Fin w → Matrix (Fin q) (Fin q) K) (points : Fin w → K) : (ThreeLift.specialize φ t).mapMatrix (polynomial χ A points) = QuantumLift.blockPolynomial ((↑φ).compAddChar χ) fun (α β : Fin q) => (Polynomial.eval₂RingHom φ t).mapMatrix (polyBlocks A points α β)

theorem Complexity.RationalHitting.PencilDeformation.raw_specialize {K : Type v_1} {E : Type v_2} [Field K] [Field E] {w q M N : ℕ} [NeZero M] (φ : K →+* E) (A : Fin w → Matrix (Fin q) (Fin q) K) (points : Fin w → K) : (QuantumLift.blockOriginal fun (α β : Fin q) => (Polynomial.eval₂RingHom (HahnSeries.C.comp φ) ((HahnSeries.single 1) 1)).mapMatrix (polyBlocks A points α β)) = (Matrix.reindex ((Equiv.refl (Fin q)).prodCongr (ZMod.finEquiv M).toEquiv) ((Equiv.refl (Fin q)).prodCongr (ZMod.finEquiv M).toEquiv)) (PaddedRank.raw (fun (i : Fin w) => (HahnSeries.C.comp φ).mapMatrix (A i)) fun (i : Fin w) => TestPolynomial.embed.mapMatrix (TestPolynomial.padded M N (φ (points i))))

theorem Complexity.RationalHitting.PencilDeformation.det_ne_zero {K : Type u_1} {E : Type u_2} [Field K] [Field E] [CharZero E] {w q M N : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (hχ : χ.IsPrimitive) (φ : K →+* E) (points : Fin w → K) (hp : Function.Injective points) (A : Fin w → Matrix (Fin q) (Fin q) K) (B e : ℕ) (hw : 1 ≤ w) (hq : 1 ≤ q) (hqB : q ≤ B) (hN : 1 ≤ N) (hMN : M = N + 2 * w ^ 3 * B) (hM : B * (2 * w ^ 3 * B) < M) (he : 0 < e) (X : Fin w → Matrix (Fin e) (Fin e) (LaurentReduction.F E)) (hX : Function.Injective ⇑(Rectangular.blockEval (fun (i : Fin w) => (HahnSeries.C.comp φ).mapMatrix (A i)) X)) : (polynomial χ A points).det ≠ 0

The three-variable determinant is nonzero. The witness can lie over an extension field and is never an input to the generator.

theorem Complexity.RationalHitting.PencilDeformation.polyBlocks_degree {K : Type v_1} [Field K] {w q M N : ℕ} [NeZero M] (A : Fin w → Matrix (Fin q) (Fin q) K) (points : Fin w → K) (α β : Fin q) (i j : ZMod M) : (polyBlocks A points α β i j).natDegree ≤ M - 1

theorem Complexity.RationalHitting.PencilDeformation.entry_degree {K : Type u_1} [Field K] {w q M N : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (A : Fin w → Matrix (Fin q) (Fin q) K) (points : Fin w → K) (a b : Fin q × ZMod M) : (polynomial χ A points a b).totalDegree ≤ 3 * M

theorem Complexity.RationalHitting.ThreeLift.coeffP_zero {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b : ZMod d) : coeffP χ 0 a b = 0

theorem Complexity.RationalHitting.ThreeLift.coeffP_add {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R S : Matrix (ZMod d) (ZMod d) (Polynomial K)) (a b : ZMod d) : coeffP χ (R + S) a b = coeffP χ R a b + coeffP χ S a b

theorem Complexity.RationalHitting.ThreeLift.coeffP_smul {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (c : K) (R : Matrix (ZMod d) (ZMod d) (Polynomial K)) (a b : ZMod d) : coeffP χ (c • R) a b = Polynomial.C c * coeffP χ R a b

theorem Complexity.RationalHitting.ThreeLift.lift_zero {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : lift χ 0 = 0

theorem Complexity.RationalHitting.ThreeLift.lift_add {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R S : Matrix (ZMod d) (ZMod d) (Polynomial K)) : lift χ (R + S) = lift χ R + lift χ S

theorem Complexity.RationalHitting.ThreeLift.lift_smul {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (c : K) (R : Matrix (ZMod d) (ZMod d) (Polynomial K)) : lift χ (c • R) = c • lift χ R

noncomputable def Complexity.RationalHitting.ThreeLift.linear {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : Matrix (ZMod d) (ZMod d) (Polynomial K) →ₗ[K] Matrix (ZMod d) (ZMod d) (MvPolynomial (Fin 3) K)

The original matrix pencil evaluated on the supplied blocks.

Equations

• Complexity.RationalHitting.ThreeLift.linear χ = { toFun := Complexity.RationalHitting.ThreeLift.lift χ, map_add' := ⋯, map_smul' := ⋯ }

theorem Complexity.RationalHitting.ThreeLift.lift_sum {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) {ι : Type u_2} (S : Finset ι) (R : ι → Matrix (ZMod d) (ZMod d) (Polynomial K)) : lift χ (∑ i ∈ S, R i) = ∑ i ∈ S, lift χ (R i)