OAI/Computability/RationalHitting/EncodingBounds.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

A staged division-free determinant computation for integer matrices. Explicit dense tables prevent recursive matrix-entry recomputation.

  1. lemma OAI.RationalHitting.EncodingBounds.encodeNat_length line 9
  2. lemma OAI.RationalHitting.EncodingBounds.encodeNat_le line 13
  3. lemma OAI.RationalHitting.EncodingBounds.ratio_num_le line 17
  4. lemma OAI.RationalHitting.EncodingBounds.ratio_den_le line 22
  5. lemma OAI.RationalHitting.EncodingBounds.encodeRat_ratio_le line 25
  6. lemma OAI.RationalHitting.EncodingBounds.determinant_bound line 33
  7. lemma OAI.RationalHitting.EncodingBounds.normalized_entry_ratio line 53

    Source documentation

    Cramer's rule used by the generator, without any assumption on arithmetic algorithms.

    lemma normalized_entry_ratio {d : ℕ} (A B : Matrix (Fin d) (Fin d) ℤ) (hA : A.det ≠ 0)
    (i j : Fin d) :
    ((A.map (Int.castRingHom ℚ))⁻¹ * B.map (Int.castRingHom ℚ)) i j =
      Rat.divInt ((A.updateCol i (fun k => B k j)).det) A.det := by
…
  8. lemma OAI.RationalHitting.EncodingBounds.nat_le_two_pow line 82
  9. lemma OAI.RationalHitting.EncodingBounds.determinant_pow_bound line 90
  10. lemma OAI.RationalHitting.EncodingBounds.normalization_bit_bound line 105
  11. lemma OAI.RationalHitting.EncodingBounds.flatMap_length_le line 126
  12. lemma OAI.RationalHitting.EncodingBounds.tuple_length_le line 137
  13. lemma OAI.RationalHitting.EncodingBounds.encodeNat_linear line 152
  14. lemma OAI.RationalHitting.EncodingBounds.output_length_le line 159
  15. lemma OAI.RationalHitting.PolynomialBounds.mul_monomials line 177

    Source documentation

    Coefficient/exponent bookkeeping, with no symbolic expansion of large powers.

    lemma mul_monomials (a b m i j : ℕ) : (a*m^i)*(b*m^j) = (a*b)*m^(i+j) := by
…
  16. lemma OAI.RationalHitting.PolynomialBounds.lift_power line 181
  17. lemma OAI.RationalHitting.PolynomialBounds.one_le_pow line 184
  18. def OAI.RationalHitting.PolynomialBounds.logarithmic line 188

    Source documentation

    Exponent bounding all denominator-cleared matrix entries by a power of 2.

    def logarithmic (n s : ℕ) : ℕ :=
…
  19. def OAI.RationalHitting.PolynomialBounds.logConstant line 191
  20. theorem OAI.RationalHitting.PolynomialBounds.logarithmic_bound line 193
  21. def OAI.RationalHitting.PolynomialBounds.bitConstant line 220
  22. theorem OAI.RationalHitting.PolynomialBounds.normalized_bits_bound line 222
  23. def OAI.RationalHitting.PolynomialBounds.outputConstant line 237
  24. theorem OAI.RationalHitting.PolynomialBounds.output_bits_bound line 239
  25. lemma OAI.RationalHitting.Generator.U_power_bound line 271
  26. lemma OAI.RationalHitting.Generator.tupleAt_bit_bound line 288
  27. lemma OAI.RationalHitting.Generator.output_entry_bit_bound line 297
  28. lemma OAI.RationalHitting.Generator.list_output_bound line 310