Rational hitting lists: certificates

A nonzero value of a rational formula at a rational matrix substitution becomes an invertible value after a generic quantum-deformation lift into a matrix ring over a Hahn series field (Rational.formula_invertible_witness); the domain of the original tree is preserved through a localization regular at the specialization point. The affine certificate pencils of a formula then yield nonzero determinant polynomials of bounded degree (PencilCertificates.determinant_ne_zero, PencilCertificates.degree_le), which the generator evaluates on an integer grid.

Main definitions

• Cslib.Circuits.Rational.LocalSpecialization.Regular, Cslib.Circuits.Rational.LocalSpecialization.evaluate: fractions regular at a point and their evaluation.
• Cslib.Circuits.Rational.PencilCertificates.polynomial, Cslib.Circuits.Rational.PencilCertificates.determinant: the polynomial matrix certificate of an affine pencil and its determinant.

Main results

• Cslib.Circuits.Rational.QuantumLift.formula_invertible_value, Cslib.Circuits.Rational.formula_invertible_witness: a nonzero value lifts to a defined invertible value.
• Cslib.Circuits.Rational.PencilCertificates.determinant_ne_zero, Cslib.Circuits.Rational.PencilCertificates.degree_le: the certificate determinants are nonzero polynomials of bounded total degree.

References

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

def Cslib.Circuits.Rational.LocalSpecialization.denominators {P : Type u_1} {K : Type u_2} [CommRing P] [Field K] (ev : P →+* K) : Submonoid P

Elements whose specialized values are nonzero.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.LocalSpecialization.Regular {P : Type u_1} {K : Type u_2} [CommRing P] [Field K] (ev : P →+* K) : Type u_1

Localize at precisely the denominators nonzero at the chosen point.

noncomputable def Cslib.Circuits.Rational.LocalSpecialization.evaluate {P : Type u_1} {K : Type u_2} [CommRing P] [Field K] (ev : P →+* K) : Regular ev →+* K

Extend specialization to fractions regular at the chosen point.

@[simp]

theorem Cslib.Circuits.Rational.LocalSpecialization.evaluate_algebraMap {P : Type u_1} {K : Type u_2} [CommRing P] [Field K] (ev : P →+* K) (p : P) : (evaluate ev) ((algebraMap P (Regular ev)) p) = ev p

theorem Cslib.Circuits.Rational.LocalSpecialization.evaluate_reflects_units {P : Type u_1} {K : Type u_2} [CommRing P] [Field K] (ev : P →+* K) (x : Regular ev) (hx : IsUnit ((evaluate ev) x)) : IsUnit x

Only fractions whose denominator is nonzero at the point are evaluated. The entire division algebra is deliberately not given a specialization.

noncomputable def Cslib.Circuits.Rational.LocalSpecialization.intoField {P : Type u_1} {K : Type u_2} {E : Type u_3} [CommRing P] [Field K] [Field E] (ev : P →+* K) (j : P →+* E) (hj : Function.Injective ⇑j) : Regular ev →+* E

Embed the regular localization into a field containing its numerator ring.

@[simp]

theorem Cslib.Circuits.Rational.LocalSpecialization.intoField_algebraMap {P : Type u_1} {K : Type u_2} {E : Type u_3} [CommRing P] [Field K] [Field E] (ev : P →+* K) (j : P →+* E) (hj : Function.Injective ⇑j) (p : P) : (intoField ev j hj) ((algebraMap P (Regular ev)) p) = j p

theorem Cslib.Circuits.Rational.LocalSpecialization.intoField_injective {P : Type u_1} {K : Type u_2} {E : Type u_3} [CommRing P] [Field K] [Field E] (ev : P →+* K) (j : P →+* E) (hj : Function.Injective ⇑j) : Function.Injective ⇑(intoField ev j hj)

theorem Cslib.Circuits.Rational.LocalSpecialization.matrix_reflects_units {P : Type u_1} {K : Type u_2} [CommRing P] [Field K] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (ev : P →+* K) (A : Matrix ι ι (Regular ev)) (hA : IsUnit ((evaluate ev).mapMatrix A)) : IsUnit A

theorem Cslib.Circuits.Rational.QuantumLift.formula_invertible_value {K : Type u_1} [Field K] [CharZero K] {d : ℕ} [NeZero d] {n : ℕ} (χ : AddChar (ZMod d) K) (hχ : χ.IsPrimitive) (f : Formula n) (W : Fin n → Matrix (ZMod d) (ZMod d) K) (a : Matrix (ZMod d) (ZMod d) K) (ha : Formula.Eval (algebraMap ℚ (Matrix (ZMod d) (ZMod d) K)) W f a) (ha0 : a ≠ 0) : ∃ (b : Matrix (ZMod d) (ZMod d) (HahnSeries Exponents K)), Formula.Eval (algebraMap ℚ (Matrix (ZMod d) (ZMod d) (HahnSeries Exponents K))) (fun (i : Fin n) => (representation χ) (liftD χ (W i))) f b ∧ IsUnit b

The original tree remains defined after the generic deformation. A nonzero original value becomes invertible. Domain preservation uses the localization regular at (1,1), while final invertibility uses the division subring.

theorem Cslib.Circuits.Rational.formula_invertible_witness {n d : ℕ} (hd : 0 < d) (f : Formula n) (W : Fin n → Matrix (Fin d) (Fin d) ℚ) (a : Matrix (Fin d) (Fin d) ℚ) (ha : Formula.Eval (algebraMap ℚ (Matrix (Fin d) (Fin d) ℚ)) W f a) (ha0 : a ≠ 0) : ∃ (X : Fin n → Matrix (Fin d) (Fin d) (HahnSeries QuantumLift.Exponents ℂ)) (v : Matrix (Fin d) (Fin d) (HahnSeries QuantumLift.Exponents ℂ)), Formula.Eval (algebraMap ℚ (Matrix (Fin d) (Fin d) (HahnSeries QuantumLift.Exponents ℂ))) X f v ∧ IsUnit v

A nonzero value of a formula at a rational matrix substitution becomes a defined invertible value at some substitution of matrices over the Hahn series field QuantumLift.Exponents ℂ.

def Cslib.Circuits.Rational.PencilCertificates.coefficients {K : Type u_1} [Field K] [CharZero K] {n q : ℕ} (L : Matrix (Fin q) (Fin q) (Affine.Form n)) : Fin (n + 1) → Matrix (Fin q) (Fin q) K

Extract the homogeneous coefficient matrices of an affine pencil.

noncomputable def Cslib.Circuits.Rational.PencilCertificates.lifts {K : Type u_1} [Field K] {M : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (N n : ℕ) : Fin (n + 1) → Matrix (ZMod M) (ZMod M) (MvPolynomial (Fin 3) K)

Polynomial lifts for each homogeneous coordinate at the test points.

noncomputable def Cslib.Circuits.Rational.PencilCertificates.polynomial {K : Type u_1} [Field K] [CharZero K] {n q M : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (N : ℕ) (L : Matrix (Fin q) (Fin q) (Affine.Form n)) : Matrix (Fin q × ZMod M) (Fin q × ZMod M) (MvPolynomial (Fin 3) K)

The polynomial matrix certificate for the affine pencil.

noncomputable def Cslib.Circuits.Rational.PencilCertificates.determinant {K : Type u_1} [Field K] [CharZero K] {n q M : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (N : ℕ) (L : Matrix (Fin q) (Fin q) (Affine.Form n)) : MvPolynomial (Fin 3) K

The determinant polynomial certifying invertibility of the lifted pencil.

theorem Cslib.Circuits.Rational.PencilCertificates.polynomial_apply {K : Type u_1} [Field K] [CharZero K] {n q M N : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (L : Matrix (Fin q) (Fin q) (Affine.Form n)) (a b : Fin q × ZMod M) : polynomial χ N L a b = ∑ i : Fin (n + 1), MvPolynomial.C ((algebraMap ℚ K) (Affine.coeff (L a.1 b.1) i)) * lifts χ N n i a.2 b.2

theorem Cslib.Circuits.Rational.PencilCertificates.specialized {K : Type u_1} [Field K] [CharZero K] {n q M N : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (L : Matrix (Fin q) (Fin q) (Affine.Form n)) (x : Fin 3 → K) : (MvPolynomial.eval₂Hom (RingHom.id K) x).mapMatrix (polynomial χ N L) = (Matrix.compRingEquiv (Fin q) (ZMod M) K) (L.map (Affine.homogeneous (algebraMap ℚ (Matrix (ZMod M) (ZMod M) K)) fun (i : Fin (n + 1)) => (MvPolynomial.eval₂Hom (RingHom.id K) x).mapMatrix (lifts χ N n i)))

theorem Cslib.Circuits.Rational.PencilCertificates.block_eq {K : Type u_1} {E : Type u_2} [Field K] [CharZero K] [Field E] [CharZero E] {n q : ℕ} (φ : K →+* E) (L : Matrix (Fin q) (Fin q) (Affine.Form n)) {d : ℕ} (X : Fin n → Matrix (Fin d) (Fin d) E) : (Rectangular.blockMatrix (fun (i : Fin (n + 1)) => φ.mapMatrix (coefficients L i)) fun (i : Fin (n + 1)) => Fin.cases 1 X i) = (Matrix.compRingEquiv (Fin q) (Fin d) E) (L.map ⇑(Affine.eval (algebraMap ℚ (Matrix (Fin d) (Fin d) E)) X))

theorem Cslib.Circuits.Rational.PencilCertificates.determinant_ne_zero {K : Type u_1} {E : Type u_2} [Field K] [CharZero K] [Field E] [CharZero E] {n q M N : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (hχ : χ.IsPrimitive) (φ : K →+* E) (L : Matrix (Fin q) (Fin q) (Affine.Form n)) (B d : ℕ) (hq : 1 ≤ q) (hqB : q ≤ B) (hN : 1 ≤ N) (hMN : M = N + 2 * (n + 1) ^ 3 * B) (hM : B * (2 * (n + 1) ^ 3 * B) < M) (hd : 0 < d) (X : Fin n → Matrix (Fin d) (Fin d) (LaurentReduction.F E)) (hX : IsUnit (L.map ⇑(Affine.eval (algebraMap ℚ (Matrix (Fin d) (Fin d) (LaurentReduction.F E))) X))) : determinant χ N L ≠ 0

theorem Cslib.Circuits.Rational.PencilCertificates.degree_le {K : Type u_1} [Field K] [CharZero K] {n q M N : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (L : Matrix (Fin q) (Fin q) (Affine.Form n)) : (determinant χ N L).totalDegree ≤ 3 * q * M ^ 2