Encoding-length bounds for the hitting lists

Bounds on the length of the canonical binary encoding of the generated list. The normalized matrices are U₀⁻¹ * Uₐ for integer matrices Uₐ with entries of absolute value at most 2 ^ b; by Cramer's rule each entry is a ratio of two integer determinants, and the permutation-sum bound |det A| ≤ d! * B ^ d keeps both below 2 ^ (d * d + d * b + 1). Polynomial bookkeeping in the parameters n and s then bounds the full output length by a fixed polynomial of degree 104 in n + s + 1. The bounds hold for all n and s, including n = 0; the source assumes 1 ≤ n, and covering n = 0 raises the grid-size coefficient from 24577 to 49153, so the constant outputConstant is larger than the source's.

Main definitions

• Rational.PolynomialBounds.logarithmic: an exponent bounding the integer lift entries.
• Rational.PolynomialBounds.logConstant, Rational.PolynomialBounds.bitConstant, Rational.PolynomialBounds.outputConstant: the fixed coefficients of the bounds.

Main results

• Rational.EncodingBounds.normalized_entry_ratio: Cramer's rule for normalized integer matrices.
• Rational.EncodingBounds.normalization_bit_bound: the encoding length of a normalized entry.
• Rational.EncodingBounds.output_length_le: the encoding length of a whole output.
• Rational.Generator.list_output_bound: the encoded hitting list has length at most outputConstant * (n + s + 1) ^ 104.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/EncodingBounds.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

theorem Cslib.Circuits.Rational.EncodingBounds.encodeNat_length (a : ℕ) : (encodeNat a).length = 2 * (Nat.digits 2 a).length + 1

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

theorem Cslib.Circuits.Rational.EncodingBounds.ratio_num_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).num.natAbs ≤ a.natAbs

theorem Cslib.Circuits.Rational.EncodingBounds.ratio_den_le (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).den ≤ b.natAbs

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.EncodingBounds.encodeNat_linear (a : ℕ) : (encodeNat a).length ≤ 2 * (a + 1) + 1

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.PolynomialBounds.lift_power (c m i j : ℕ) (hm : 1 ≤ m) (hij : i ≤ j) : c * m ^ i ≤ c * m ^ j

def Cslib.Circuits.Rational.PolynomialBounds.logarithmic (n s : ℕ) : ℕ

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

def Cslib.Circuits.Rational.PolynomialBounds.logConstant : ℕ

Fixed coefficient bounding the binary logarithm of integral entry magnitudes.

theorem Cslib.Circuits.Rational.PolynomialBounds.logarithmic_bound (n s : ℕ) : logarithmic n s ≤ logConstant * (n + s + 1) ^ 22

def Cslib.Circuits.Rational.PolynomialBounds.bitConstant : ℕ

Fixed coefficient in the bound on normalized rational entry encodings.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.PolynomialBounds.outputConstant : ℕ

Fixed coefficient in the bound on the complete binary output length. It differs from the source's constant: the bound also covers n = 0, which raises the grid-size coefficient of Parameters.polynomial_H from 24577 to 49153.

theorem Cslib.Circuits.Rational.PolynomialBounds.output_bits_bound (n m D L B : ℕ) (hm : 1 ≤ m) (hn : n ≤ m) (hD : D ≤ 256 * m ^ 10) (hL : L ≤ 49153 ^ 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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.Generator.list_output_bound (n s : ℕ) : (encodeOutput (list n s)).length ≤ PolynomialBounds.outputConstant * (n + s + 1) ^ 104