Polynomial deformation of the quantum lift

The finite Fourier (quantum) lift of a d × d matrix, written with the Weyl basis, is turned into an honest polynomial matrix: the Fourier frequencies become exponents of two commuting indeterminates. Evaluating at (1, 1) recovers the original matrix, while embedding into Hahn series recovers the division-ring representation of QuantumMatrices. The rank gap of BlockDivision then shows that the determinant of the polynomial lift of a block matrix of large rank is a nonzero polynomial. A third indeterminate carries the Taylor parameter of the padded test matrices, giving the three-variable pencil polynomial whose determinant the generator must avoid.

Main definitions

• Rational.QuantumLift.polynomialLift: the two-parameter polynomial Fourier lift.
• Rational.QuantumLift.blockPolynomial, Rational.QuantumLift.blockOriginal: the flattened lifted and original block matrices.
• Rational.ThreeLift.lift: the three-parameter lift of a matrix of univariate polynomials.
• Rational.ThreeLift.specialize: specialization of the first parameter into a field.
• Rational.ThreeLift.linear: the three-parameter lift as a K-linear map.
• Rational.PencilDeformation.polynomial: the three-variable pencil matrix.

Main results

• Rational.QuantumLift.blockPolynomial_det_ne_zero: large rank forces a nonzero determinant of the polynomial lift.
• Rational.PencilDeformation.det_ne_zero: the three-variable pencil determinant is nonzero.
• Rational.PencilDeformation.entry_degree: its entries have total degree at most 3 * M.

References

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

noncomputable def Cslib.Circuits.Rational.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.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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.

def Cslib.Circuits.Rational.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.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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.

noncomputable def Cslib.Circuits.Rational.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.

noncomputable def Cslib.Circuits.Rational.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.

noncomputable def Cslib.Circuits.Rational.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.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.ThreeLift.weyl_map {K : Type u_1} {E : Type u_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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.ThreeLift.uni_totalDegree_le {K : Type u_1} [Field K] (p : Polynomial K) : (uni p).totalDegree ≤ p.natDegree

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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.

noncomputable def Cslib.Circuits.Rational.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.

noncomputable def Cslib.Circuits.Rational.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.

theorem Cslib.Circuits.Rational.PencilDeformation.specialize {K : Type u_1} {E : Type u_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 Cslib.Circuits.Rational.PencilDeformation.raw_specialize {K : Type u_1} {E : Type u_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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.PencilDeformation.polyBlocks_degree {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) (α β : Fin q) (i j : ZMod M) : (polyBlocks A points α β i j).natDegree ≤ M - 1

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.ThreeLift.lift_zero {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : lift χ 0 = 0

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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.

theorem Cslib.Circuits.Rational.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)