The executable hitting-list generator

A computable version of Generator.list that never computes in the cyclotomic field. At each grid point it materializes the integer lift matrices as dense tables, tests singularity with the staged integer determinant, and computes each normalized entry as a ratio of two integer determinants (Cramer's rule). The resulting list, in the same order, is proved equal to the noncomputable specification.

Main definitions

• Rational.ExecutableGenerator.atPoint: the normalized tuple at one grid point, if any.
• Rational.ExecutableGenerator.output: the computable list for fixed parameters.
• Rational.ExecutableGenerator.list: the computable list for n variables and s nodes.
• Rational.ExecutableGenerator.encoded: its binary encoding.

Main results

• Rational.ExecutableGenerator.atPoint_spec: pointwise agreement with the specification.
• Rational.ExecutableGenerator.list_spec: list = Generator.list.
• Rational.ExecutableGenerator.exact_output: the dimension, encoding-length and hitting guarantees of the computed list.

References

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

def Cslib.Circuits.Rational.ExecutableGenerator.inputTables (n N e : ℕ) (x : Fin 3 → ℕ) : Vector (DeterminantAlgorithm.Table (Generator.matrixDimension e)) (n + 1)

Dense, staged integer input tables. No quotient-field element is computed.

@[simp]

theorem Cslib.Circuits.Rational.ExecutableGenerator.inputTables_denote (n N e : ℕ) (x : Fin 3 → ℕ) (a : Fin (n + 1)) : DeterminantAlgorithm.denote ((inputTables n N e x).get a) = Generator.integralLift n N e x a

def Cslib.Circuits.Rational.ExecutableGenerator.normalizedEntry {d : ℕ} (A B : DeterminantAlgorithm.Table d) (den : ℤ) (i j : Fin d) : ℚ

Cramer's numerators are computed by the staged division-free algorithm.

theorem Cslib.Circuits.Rational.ExecutableGenerator.normalizedEntry_spec {d : ℕ} (A B : DeterminantAlgorithm.Table d) (hA : (DeterminantAlgorithm.denote A).det ≠ 0) (i j : Fin d) : normalizedEntry A B (DeterminantAlgorithm.determinant A) i j = (((DeterminantAlgorithm.denote A).map ⇑(Int.castRingHom ℚ))⁻¹ * (DeterminantAlgorithm.denote B).map ⇑(Int.castRingHom ℚ)) i j

@[reducible, inline]

abbrev Cslib.Circuits.Rational.ExecutableGenerator.RationalTable (n d : ℕ) : Type

A finite vector of dense rational matrix tables.

def Cslib.Circuits.Rational.ExecutableGenerator.tuple {n d : ℕ} (T : RationalTable n d) : Tuple n d

Read a dense rational table as a matrix substitution.

def Cslib.Circuits.Rational.ExecutableGenerator.normalized {n d : ℕ} (A : Vector (DeterminantAlgorithm.Table d) (n + 1)) (den : ℤ) : RationalTable n d

Compute the normalized tuple entrywise using determinant ratios.

@[simp]

theorem Cslib.Circuits.Rational.ExecutableGenerator.tuple_normalized {n d : ℕ} (A : Vector (DeterminantAlgorithm.Table d) (n + 1)) (den : ℤ) (a : Fin n) (i j : Fin d) : tuple (normalized A den) a i j = normalizedEntry (A.get 0) (A.get a.succ) den i j

def Cslib.Circuits.Rational.ExecutableGenerator.atPoint (n N e : ℕ) (x : Fin 3 → ℕ) : Option (Tuple n (Generator.matrixDimension e))

The only singularity test; all repeated algebra is materialized in dense tables.

theorem Cslib.Circuits.Rational.ExecutableGenerator.U_det_eq_zero (n N e : ℕ) (x : Fin 3 → ℕ) : (Generator.integralLift n N e x 0).det = 0 ↔ Matrix.det (Generator.rationalLift n N e x 0) = 0

theorem Cslib.Circuits.Rational.ExecutableGenerator.atPoint_spec (n N e : ℕ) (x : Fin 3 → ℕ) : atPoint n N e x = Generator.atPoint n N e x

Exact pointwise equality, including points rejected by the original determinant test.

def Cslib.Circuits.Rational.ExecutableGenerator.output (n N e H : ℕ) : Output n

A computable generator preserving the list and its order.

theorem Cslib.Circuits.Rational.ExecutableGenerator.output_spec (n N e H : ℕ) : output n N e H = Generator.output n N e H

def Cslib.Circuits.Rational.ExecutableGenerator.list (n s : ℕ) : Output n

The executable hitting list for the selected parameter values.

theorem Cslib.Circuits.Rational.ExecutableGenerator.list_spec (n s : ℕ) : list n s = Generator.list n s

def Cslib.Circuits.Rational.ExecutableGenerator.encoded (n s : ℕ) : List Bool

The complete binary encoding of the executable hitting list.

theorem Cslib.Circuits.Rational.ExecutableGenerator.encoded_spec (n s : ℕ) : encoded n s = encodeOutput (Generator.list n s)

theorem Cslib.Circuits.Rational.ExecutableGenerator.exact_output (n s : ℕ) (hs : 1 ≤ s) : (list n s).dimension ≤ 256 * (n + s + 1) ^ 10 ∧ (encodeOutput (list n s)).length ≤ PolynomialBounds.outputConstant * (n + s + 1) ^ 104 ∧ Hits s (list n s)

The hitting property and output-size bounds for the computed list.