OAI/Computability/RationalHitting/Deformation.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RationalHitting.QuantumLift.polynomialLift line 15

   Source documentation

   The two-parameter polynomial lift.

   def polynomialLift (R : Matrix (ZMod d) (ZMod d) K) :
       Matrix (ZMod d) (ZMod d) (MvPolynomial (Fin 2) K) := fun i j =>
   …

2. lemma OAI.RationalHitting.QuantumLift.polynomialLift_embed line 21
3. lemma OAI.RationalHitting.QuantumLift.polynomialLift_specialize line 37
4. def OAI.RationalHitting.QuantumLift.blockPolynomial line 48
5. def OAI.RationalHitting.QuantumLift.blockOriginal line 52
6. lemma OAI.RationalHitting.QuantumLift.blockPolynomial_embed line 55
7. lemma OAI.RationalHitting.QuantumLift.blockPolynomial_specialize line 61
8. theorem OAI.RationalHitting.QuantumLift.blockPolynomial_det_ne_zero line 71

   Source documentation

   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.

   theorem blockPolynomial_det_ne_zero (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 := by
   …

   Mentions: OAI.RationalHitting.QuantumLift.blockOriginal, OAI.RationalHitting.QuantumLift.blockPolynomial

9. def OAI.RationalHitting.ThreeLift.coeffP line 102

   Source documentation

   Coefficient polynomials for the exact cyclic-diagonal Fourier transform.

   def coeffP (R : Matrix (ZMod d) (ZMod d) K[X]) (a b : ZMod d) : K[X] :=
   …

10. def OAI.RationalHitting.ThreeLift.uni line 105
11. def OAI.RationalHitting.ThreeLift.lift line 109

    Source documentation

    The three-parameter polynomial lift, before specialization.

    def lift (R : Matrix (ZMod d) (ZMod d) K[X]) :
        Matrix (ZMod d) (ZMod d) (MvPolynomial (Fin 3) K) := fun i j =>
    …

12. def OAI.RationalHitting.ThreeLift.specialize line 116

    Source documentation

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

    def specialize (φ : K →+* E) (t : E) :
        MvPolynomial (Fin 3) K →+* MvPolynomial (Fin 2) E :=
    …

13. lemma OAI.RationalHitting.ThreeLift.specialize_uni line 120
14. lemma OAI.RationalHitting.ThreeLift.coeffP_eval line 130
15. lemma OAI.RationalHitting.ThreeLift.weyl_map line 136
16. lemma OAI.RationalHitting.ThreeLift.specialize_lift line 141
17. lemma OAI.RationalHitting.ThreeLift.uni_totalDegree_le line 157
18. lemma OAI.RationalHitting.ThreeLift.coeffP_natDegree_le line 169
19. lemma OAI.RationalHitting.ThreeLift.lift_totalDegree_le line 177
20. def OAI.RationalHitting.PencilDeformation.test line 204
21. def OAI.RationalHitting.PencilDeformation.polyBlocks line 207
22. def OAI.RationalHitting.PencilDeformation.polynomial line 211
23. lemma OAI.RationalHitting.PencilDeformation.specialize line 216
24. lemma OAI.RationalHitting.PencilDeformation.raw_specialize line 226
25. theorem OAI.RationalHitting.PencilDeformation.det_ne_zero line 254

    Source documentation

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

    theorem det_ne_zero (χ : 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) (F E))
        (hX : Function.Injective (Rectangular.blockEval
          (fun i => ((HahnSeries.C : E →+* F E).comp φ).mapMatrix (A i)) X)) :
        (polynomial (N := N) χ A points).det ≠ 0 := by
    …

    Mentions: OAI.RationalHitting.Rectangular.blockEval, OAI.RationalHitting.PencilDeformation.polynomial

26. lemma OAI.RationalHitting.PencilDeformation.polyBlocks_degree line 284
27. lemma OAI.RationalHitting.PencilDeformation.entry_degree line 294
28. lemma OAI.RationalHitting.ThreeLift.coeffP_zero line 313
29. lemma OAI.RationalHitting.ThreeLift.coeffP_add line 314
30. lemma OAI.RationalHitting.ThreeLift.coeffP_smul line 317
31. lemma OAI.RationalHitting.ThreeLift.lift_zero line 324
32. lemma OAI.RationalHitting.ThreeLift.lift_add line 327
33. lemma OAI.RationalHitting.ThreeLift.lift_smul line 331
34. def OAI.RationalHitting.ThreeLift.linear line 342
35. lemma OAI.RationalHitting.ThreeLift.lift_sum line 348