Rational hitting lists: executable

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

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

def Complexity.RationalHitting.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.

Equations

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

@[simp]

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.ExecutableGenerator.normalizedEntry {d : ℕ} (A B : DeterminantAlgorithm.Table d) (den : ℤ) (i j : Fin d) : ℚ

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

Equations

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.ExecutableGenerator.RationalTable (n d : ℕ) : Type

A finite vector of dense rational matrix tables.

Equations

• Complexity.RationalHitting.ExecutableGenerator.RationalTable n d = Vector (Vector (Vector ℚ d) d) n

def Complexity.RationalHitting.ExecutableGenerator.tuple {n d : ℕ} (T : RationalTable n d) : Tuple n d

Read a dense rational table as a matrix substitution.

Equations

• Complexity.RationalHitting.ExecutableGenerator.tuple T a i j = ((Vector.get T a).get i).get j

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

Compute the normalized tuple entrywise using determinant ratios.

Equations

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

@[simp]

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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.

Equations

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.ExecutableGenerator.output (n N e H : ℕ) : Output n

A computable generator preserving the list and its order.

Equations

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

theorem Complexity.RationalHitting.ExecutableGenerator.output_spec (n N e H : ℕ) : output n N e H = Generator.output n N e H

def Complexity.RationalHitting.ExecutableGenerator.list (n s : ℕ) : Output n

The executable hitting list for the selected parameter values.

Equations

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

theorem Complexity.RationalHitting.ExecutableGenerator.list_spec (n s : ℕ) : list n s = Generator.list n s

def Complexity.RationalHitting.ExecutableGenerator.encoded (n s : ℕ) : List Bool

The complete binary encoding of the executable hitting list.

Equations

• Complexity.RationalHitting.ExecutableGenerator.encoded n s = Complexity.RationalHitting.encodeOutput (Complexity.RationalHitting.ExecutableGenerator.list n s)

theorem Complexity.RationalHitting.ExecutableGenerator.encoded_spec (n s : ℕ) : encoded n s = encodeOutput (Generator.list n s)

theorem Complexity.RationalHitting.ExecutableGenerator.exact_output (n s : ℕ) (hn : 1 ≤ n) (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.

def Complexity.RationalHitting.ExecutableGenerator.Implementation : Prop

A finite-state implementation with polynomial transition count.

Equations

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

theorem Complexity.RationalHitting.ExecutableGenerator.main_of_implementation (hi : Implementation) : MainStatement

The finite-state implementation and list bounds imply the main statement.