OAI/Computability/RationalHitting/Certificates.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.LocalSpecialization.denominators line 11
  2. abbrev OAI.RationalHitting.LocalSpecialization.Regular line 20
  3. def OAI.RationalHitting.LocalSpecialization.evaluate line 22
  4. lemma OAI.RationalHitting.LocalSpecialization.evaluate_algebraMap line 25
  5. lemma OAI.RationalHitting.LocalSpecialization.evaluate_reflects_units line 30

    Source documentation

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

    lemma evaluate_reflects_units (ev : P →+* K) (x : Regular ev)
    (hx : IsUnit (evaluate ev x)) : IsUnit x := by
…

    Mentions: OAI.RationalHitting.LocalSpecialization.Regular, OAI.RationalHitting.LocalSpecialization.evaluate

  6. def OAI.RationalHitting.LocalSpecialization.intoField line 40
  7. lemma OAI.RationalHitting.LocalSpecialization.intoField_algebraMap line 47
  8. lemma OAI.RationalHitting.LocalSpecialization.intoField_injective line 51
  9. lemma OAI.RationalHitting.LocalSpecialization.matrix_reflects_units line 62
  10. theorem OAI.RationalHitting.QuantumLift.formula_invertible_value line 81

    Source documentation

    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 formula_invertible_value (hχ : χ.IsPrimitive) (f : Formula n)
    (W : Fin n → Matrix (ZMod d) (ZMod d) K) (a : Matrix (ZMod d) (ZMod d) K)
    (ha : f.Eval (algebraMap ℚ _) W a) (ha0 : a ≠ 0) :
    ∃ b : Matrix (ZMod d) (ZMod d) (HahnSeries Exponents K),
      f.Eval (algebraMap ℚ _) (fun i => representation χ (liftD χ (W i))) b ∧ IsUnit b := by
…

    Mentions: OAI.RationalHitting.Formula, OAI.RationalHitting.QuantumLift.Exponents, OAI.RationalHitting.QuantumLift.representation, OAI.RationalHitting.QuantumLift.liftD

  11. theorem OAI.RationalHitting.formula_invertible_witness line 150
  12. instance OAI.RationalHitting.PencilCertificates.laurentCharZero line 185
  13. def OAI.RationalHitting.PencilCertificates.coefficients line 191
  14. def OAI.RationalHitting.PencilCertificates.lifts line 195
  15. def OAI.RationalHitting.PencilCertificates.polynomial line 199
  16. def OAI.RationalHitting.PencilCertificates.determinant line 203
  17. lemma OAI.RationalHitting.PencilCertificates.polynomial_apply line 206
  18. lemma OAI.RationalHitting.PencilCertificates.specialized line 215
  19. lemma OAI.RationalHitting.PencilCertificates.block_eq line 226
  20. lemma OAI.RationalHitting.PencilCertificates.determinant_ne_zero line 241
  21. lemma OAI.RationalHitting.PencilCertificates.degree_le line 256