Documentation

Complexity.Computability.Circuit.Rational.EncodingBounds

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 #

Main results #

References #

source
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.

source
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

For d × d integer matrices A (with A.det ≠ 0) and B whose entries have absolute value at most 2 ^ b, the binary encoding of each entry of A⁻¹ * B has length at most 4 * (d * d + d * b + 1) + 3.

source
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

If every entry of every matrix tuple in H has encoded length at most B, then the encoded output encodeOutput H has length at most 2 * (H.dimension + 1) + 1 + 2 * (H.tuples.length + 1) + 1 plus H.tuples.length * n * H.dimension ^ 2 * B.

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

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

Instances For
    source
    def Cslib.Circuits.Rational.PolynomialBounds.logConstant :
    ℕ

    Fixed coefficient bounding the binary logarithm of integral entry magnitudes.

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

      The entry-magnitude exponent logarithmic n s is at most logConstant * (n + s + 1) ^ 22.

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

      Fixed coefficient in the bound on normalized rational entry encodings.

      Instances For
        source
        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.

        Instances For
          source
          theorem Cslib.Circuits.Rational.Generator.list_output_bound (n s : ℕ) :
          (encodeOutput (list n s)).length ≤ PolynomialBounds.outputConstant * (n + s + 1) ^ 104

          The binary encoding of the hitting list list n s has length at most PolynomialBounds.outputConstant * (n + s + 1) ^ 104.