Rational hitting lists: encoding bounds

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/EncodingBounds.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

theorem Complexity.RationalHitting.EncodingBounds.encodeNat_length (a : ℕ) : (encodeNat a).length = 2 * (Nat.digits 2 a).length + 1

theorem Complexity.RationalHitting.EncodingBounds.encodeNat_le (a L : ℕ) (ha : a < 2 ^ L) : (encodeNat a).length ≤ 2 * L + 1

theorem Complexity.RationalHitting.EncodingBounds.ratio_num_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).num.natAbs ≤ a.natAbs

theorem Complexity.RationalHitting.EncodingBounds.ratio_den_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).den ≤ b.natAbs

theorem Complexity.RationalHitting.EncodingBounds.encodeRat_ratio_le (a b : ℤ) (hb : b ≠ 0) (L : ℕ) (ha : a.natAbs < 2 ^ L) (hb' : b.natAbs < 2 ^ L) : (encodeRat (Rat.divInt a b)).length ≤ 4 * L + 3

theorem Complexity.RationalHitting.EncodingBounds.determinant_bound {d : ℕ} (A : Matrix (Fin d) (Fin d) ℤ) (B : ℕ) (hA : ∀ (i j : Fin d), |A i j| ≤ ↑B) : |A.det| ≤ ↑d.factorial * ↑B ^ d

theorem Complexity.RationalHitting.EncodingBounds.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 : Fin d) => B k j).det A.det

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

theorem Complexity.RationalHitting.EncodingBounds.nat_le_two_pow (n : ℕ) : n ≤ 2 ^ n

theorem Complexity.RationalHitting.EncodingBounds.determinant_pow_bound {d b : ℕ} (A : Matrix (Fin d) (Fin d) ℤ) (hA : ∀ (i j : Fin d), |A i j| ≤ 2 ^ b) : |A.det| < 2 ^ (d * d + d * b + 1)

theorem Complexity.RationalHitting.EncodingBounds.normalization_bit_bound {d b : ℕ} (A B : Matrix (Fin d) (Fin d) ℤ) (hA : A.det ≠ 0) (hAb : ∀ (i j : Fin d), |A i j| ≤ 2 ^ b) (hBb : ∀ (i j : Fin d), |B i j| ≤ 2 ^ b) (i j : Fin d) : (encodeRat (((A.map ⇑(Int.castRingHom ℚ))⁻¹ * B.map ⇑(Int.castRingHom ℚ)) i j)).length ≤ 4 * (d * d + d * b + 1) + 3

theorem Complexity.RationalHitting.EncodingBounds.flatMap_length_le {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β) (B : ℕ) (h : ∀ a ∈ l, (f a).length ≤ B) : (List.flatMap f l).length ≤ l.length * B

theorem Complexity.RationalHitting.EncodingBounds.tuple_length_le {n d B : ℕ} (X : Tuple n d) (h : ∀ (a : Fin n) (i j : Fin d), (encodeRat (X a i j)).length ≤ B) : (encodeTuple X).length ≤ n * d * d * B

theorem Complexity.RationalHitting.EncodingBounds.encodeNat_linear (a : ℕ) : (encodeNat a).length ≤ 2 * (a + 1) + 1

theorem Complexity.RationalHitting.EncodingBounds.output_length_le {n B : ℕ} (H : Output n) (hb : ∀ X ∈ H.tuples, ∀ (a : Fin n) (i j : Fin H.dimension), (encodeRat (X a i j)).length ≤ B) : (encodeOutput H).length ≤ 2 * (H.dimension + 1) + 1 + 2 * (H.tuples.length + 1) + 1 + H.tuples.length * n * H.dimension * H.dimension * B

theorem Complexity.RationalHitting.PolynomialBounds.mul_monomials (a b m i j : ℕ) : a * m ^ i * (b * m ^ j) = a * b * m ^ (i + j)

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

theorem Complexity.RationalHitting.PolynomialBounds.lift_power (c m i j : ℕ) (hm : 1 ≤ m) (hij : i ≤ j) : c * m ^ i ≤ c * m ^ j

theorem Complexity.RationalHitting.PolynomialBounds.one_le_pow (m k : ℕ) (hm : 1 ≤ m) : 1 ≤ m ^ k

def Complexity.RationalHitting.PolynomialBounds.logarithmic (n s : ℕ) : ℕ

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

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RationalHitting.PolynomialBounds.logConstant : ℕ

Fixed coefficient bounding the binary logarithm of integral entry magnitudes.

Equations

• Complexity.RationalHitting.PolynomialBounds.logConstant = 64 + 64 + 3 * 16 * 24577

theorem Complexity.RationalHitting.PolynomialBounds.logarithmic_bound (n s : ℕ) (hn : 1 ≤ n) : logarithmic n s ≤ logConstant * (n + s + 1) ^ 22

def Complexity.RationalHitting.PolynomialBounds.bitConstant : ℕ

Fixed coefficient in the bound on normalized rational entry encodings.

Equations

• Complexity.RationalHitting.PolynomialBounds.bitConstant = 4 * (256 * 256 + 256 * Complexity.RationalHitting.PolynomialBounds.logConstant + 1) + 3

theorem Complexity.RationalHitting.PolynomialBounds.normalized_bits_bound (m D b : ℕ) (hm : 1 ≤ m) (hD : D ≤ 256 * m ^ 10) (hb : b ≤ logConstant * m ^ 22) : 4 * (D * D + D * b + 1) + 3 ≤ bitConstant * m ^ 32

def Complexity.RationalHitting.PolynomialBounds.outputConstant : ℕ

Fixed coefficient in the bound on the complete binary output length.

Equations

• Complexity.RationalHitting.PolynomialBounds.outputConstant = 2 * 256 + 3 + (2 * 24577 ^ 3 + 3) + 24577 ^ 3 * 256 * 256 * Complexity.RationalHitting.PolynomialBounds.bitConstant

theorem Complexity.RationalHitting.PolynomialBounds.output_bits_bound (n m D L B : ℕ) (hm : 1 ≤ m) (hn : n ≤ m) (hD : D ≤ 256 * m ^ 10) (hL : L ≤ 24577 ^ 3 * m ^ 51) (hB : B ≤ bitConstant * m ^ 32) : 2 * (D + 1) + 1 + 2 * (L + 1) + 1 + L * n * D * D * B ≤ outputConstant * m ^ 104

theorem Complexity.RationalHitting.Generator.U_power_bound (n N e H : ℕ) (x : Fin 3 → ℕ) (hH : 1 ≤ H) (hx : ∀ (l : Fin 3), x l ≤ H) (a : Fin (n + 1)) (i j : Fin (matrixDimension e)) : |integralLift n N e x a i j| ≤ 2 ^ (4 * CyclotomicRing.dimension e + 4 * CyclotomicRing.dimension e * (n + 1) + 3 * CyclotomicRing.dimension e * H)

theorem Complexity.RationalHitting.Generator.tupleAt_bit_bound (n N e H : ℕ) (x : Fin 3 → ℕ) (hH : 1 ≤ H) (hx : ∀ (l : Fin 3), x l ≤ H) (hz : Matrix.det (rationalLift n N e x 0) ≠ 0) (a : Fin n) (i j : Fin (matrixDimension e)) : (encodeRat (tupleAt n N e x a i j)).length ≤ 4 * (matrixDimension e * matrixDimension e + matrixDimension e * (4 * CyclotomicRing.dimension e + 4 * CyclotomicRing.dimension e * (n + 1) + 3 * CyclotomicRing.dimension e * H) + 1) + 3

theorem Complexity.RationalHitting.Generator.output_entry_bit_bound (n N e H : ℕ) (hH : 1 ≤ H) (X : Tuple n (matrixDimension e)) (hX : X ∈ (output n N e H).tuples) (a : Fin n) (i j : Fin (matrixDimension e)) : (encodeRat (X a i j)).length ≤ 4 * (matrixDimension e * matrixDimension e + matrixDimension e * (4 * CyclotomicRing.dimension e + 4 * CyclotomicRing.dimension e * (n + 1) + 3 * CyclotomicRing.dimension e * H) + 1) + 3

theorem Complexity.RationalHitting.Generator.list_output_bound (n s : ℕ) (hn : 1 ≤ n) : (encodeOutput (list n s)).length ≤ PolynomialBounds.outputConstant * (n + s + 1) ^ 104