Rational hitting lists: certificates #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/Certificates.lean
Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.
theorem
Complexity.RationalHitting.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
Complexity.RationalHitting.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)
:
Embed the regular localization into a field containing its numerator ring.
Equations
Instances For
@[simp]
theorem
Complexity.RationalHitting.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)
:
theorem
Complexity.RationalHitting.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
Complexity.RationalHitting.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
Complexity.RationalHitting.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
instance
Complexity.RationalHitting.PencilCertificates.laurentCharZero
{E : Type u_3}
[Field E]
[CharZero E]
:
def
Complexity.RationalHitting.PencilCertificates.coefficients
{K : Type u_1}
[Field K]
[CharZero K]
{n q : ℕ}
(L : Matrix (Fin q) (Fin q) (Affine.Form n))
:
Extract the homogeneous coefficient matrices of an affine pencil.
Equations
- Complexity.RationalHitting.PencilCertificates.coefficients L i a b = (algebraMap ℚ K) (Complexity.RationalHitting.Affine.coeff (L a b) i)
Instances For
noncomputable def
Complexity.RationalHitting.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))
:
The polynomial matrix certificate for the affine pencil.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Complexity.RationalHitting.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.
Equations
Instances For
theorem
Complexity.RationalHitting.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
Complexity.RationalHitting.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
Complexity.RationalHitting.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
Complexity.RationalHitting.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)))
: