Rational hitting lists: the generator

The generator evaluates the polynomial lifts of the certificate pencils at every point of a three-dimensional integer grid, keeps the points at which the normalizing matrix is invertible, and emits the normalized rational matrix tuples. For every admissible nonzero formula with at most s nodes, the certificate determinants are nonzero polynomials of bounded degree, so some grid point avoids all their zeros; the tuple emitted there gives the formula a defined invertible value. The parameters are polynomial in the number of variables and the node-count bound.

Main definitions

• Cslib.Circuits.Rational.Generator.matrixDimension, Cslib.Circuits.Rational.Generator.regular, Cslib.Circuits.Rational.Generator.grid, Cslib.Circuits.Rational.Generator.specializedLift, Cslib.Circuits.Rational.Generator.rationalLift, Cslib.Circuits.Rational.Generator.tupleAt, Cslib.Circuits.Rational.Generator.atPoint, Cslib.Circuits.Rational.Generator.output: the regular representation, specialization grid, normalized tuple at a grid point, and list emitted for given parameters.
• Cslib.Circuits.Rational.Parameters.w, Cslib.Circuits.Rational.Parameters.rankBound, Cslib.Circuits.Rational.Parameters.delta, Cslib.Circuits.Rational.Parameters.exponent, Cslib.Circuits.Rational.Parameters.ambientDimension, Cslib.Circuits.Rational.Parameters.truncation, Cslib.Circuits.Rational.Parameters.gridSize: the parameters chosen for n variables and s nodes.
• Cslib.Circuits.Rational.Generator.list: the list with these parameters.

Main results

• Cslib.Circuits.Rational.Generator.output_hits: the emitted list hits all formulas of bounded node count, once the parameters are large enough.
• Cslib.Circuits.Rational.Generator.list_hits, Cslib.Circuits.Rational.Generator.list_dimension_bound, Cslib.Circuits.Rational.Generator.list_length_bound: the list hits, with polynomially bounded dimension and length.

References

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

def Cslib.Circuits.Rational.Generator.matrixDimension (e : ℕ) : ℕ

Dimension after expanding the cyclotomic matrix representation over the rationals.

noncomputable def Cslib.Circuits.Rational.Generator.regular (e : ℕ) : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) (CyclotomicRing.R e) →+* Mat (matrixDimension e)

Entrywise regular representation, flattening and fixed row-major reindexing.

def Cslib.Circuits.Rational.Generator.grid (H : ℕ) : List (Fin 3 → Fin H)

The fixed lexicographic three-dimensional integer grid, encoded by Fin H.

theorem Cslib.Circuits.Rational.Generator.mem_grid (H : ℕ) (x : Fin 3 → Fin H) : x ∈ grid H

Every point x : Fin 3 → Fin H belongs to grid H.

noncomputable def Cslib.Circuits.Rational.Generator.specializedLift (n N e : ℕ) (x : Fin 3 → ℕ) (i : Fin (n + 1)) : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) (CyclotomicRing.R e)

The polynomial lift is evaluated over the exact rational quotient.

noncomputable def Cslib.Circuits.Rational.Generator.rationalLift (n N e : ℕ) (x : Fin 3 → ℕ) (i : Fin (n + 1)) : Mat (matrixDimension e)

Expand a specialized lift as a rational matrix.

noncomputable def Cslib.Circuits.Rational.Generator.tupleAt (n N e : ℕ) (x : Fin 3 → ℕ) : Tuple n (matrixDimension e)

Normalize all variable matrices by the zeroth matrix.

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

The filtering step tests only the zeroth lifted matrix, and receives no formula.

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

Collect the normalized tuples emitted at all grid points.

theorem Cslib.Circuits.Rational.Generator.integer_grid {K : Type u_1} [Field K] [CharZero K] (P : List (MvPolynomial (Fin 3) K)) (hP : ∀ p ∈ P, p ≠ 0) (d H : ℕ) (hd : ∀ p ∈ P, p.totalDegree ≤ d) (hH : P.length * d < H) : ∃ (x : Fin 3 → Fin H), ∀ p ∈ P, (MvPolynomial.eval fun (i : Fin 3) => ↑(↑(x i) + 1)) p ≠ 0

theorem Cslib.Circuits.Rational.Generator.output_hits {n s N e H : ℕ} (hs : 1 ≤ s) (hN : 1 ≤ N) (hMN : CyclotomicRing.dimension e = N + 2 * (n + 1) ^ 3 * (2 * s + 1)) (hM : (2 * s + 1) * (2 * (n + 1) ^ 3 * (2 * s + 1)) < CyclotomicRing.dimension e) (hH : (s + 2) * (3 * (2 * s + 1) * CyclotomicRing.dimension e ^ 2) < H) : Hits s (output n N e H)

The finite formula-independent list hits every admissible nonzero formula at a defined and invertible original-tree value.

def Cslib.Circuits.Rational.Parameters.w (n : ℕ) : ℕ

The number n + 1 of matrices in a lifted tuple: one per variable, and the normalizing matrix.

def Cslib.Circuits.Rational.Parameters.rankBound (s : ℕ) : ℕ

Rank parameter for formulas of the given node count.

def Cslib.Circuits.Rational.Parameters.delta (n s : ℕ) : ℕ

Dimension allowance in the rank expansion argument.

def Cslib.Circuits.Rational.Parameters.exponent (n s : ℕ) : ℕ

Binary logarithm used to choose the next cyclotomic dimension.

def Cslib.Circuits.Rational.Parameters.ambientDimension (n s : ℕ) : ℕ

The least power of two strictly above the rank expansion threshold.

def Cslib.Circuits.Rational.Parameters.truncation (n s : ℕ) : ℕ

Number of retained columns after the dimension allowance.

def Cslib.Circuits.Rational.Parameters.gridSize (n s : ℕ) : ℕ

Side length of the integer grid used for specialization.

theorem Cslib.Circuits.Rational.Parameters.threshold_pos (n s : ℕ) : 0 < rankBound s * delta n s

The rank-expansion threshold rankBound s * delta n s is positive.

theorem Cslib.Circuits.Rational.Parameters.M_minimal (n s k : ℕ) (hk : rankBound s * delta n s < 2 ^ k) : ambientDimension n s ≤ 2 ^ k

ambientDimension n s is at most any power of two strictly above rankBound s * delta n s.

theorem Cslib.Circuits.Rational.Parameters.N_pos (n s : ℕ) : 1 ≤ truncation n s

The truncation parameter truncation n s is at least 1.

theorem Cslib.Circuits.Rational.Parameters.polynomial_M (n s : ℕ) : ambientDimension n s ≤ 16 * (n + s + 1) ^ 5

ambientDimension n s is at most 16 * (n + s + 1) ^ 5.

theorem Cslib.Circuits.Rational.Parameters.polynomial_H (n s : ℕ) : gridSize n s ≤ 49153 * (n + s + 1) ^ 17

The grid side length is polynomial in n + s + 1, for every n, including n = 0: the factor s + 2 is bounded by 2 * (n + s + 1).

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

The list with all parameters fixed by n and s.

theorem Cslib.Circuits.Rational.Generator.list_hits (n s : ℕ) (hs : 1 ≤ s) : Hits s (list n s)

When 1 ≤ s, list n s hits all admissible nonzero formulas of node count at most s.

theorem Cslib.Circuits.Rational.Generator.list_dimension_bound (n s : ℕ) : (list n s).dimension ≤ 256 * (n + s + 1) ^ 10

The matrix dimension of list n s is at most 256 * (n + s + 1) ^ 10.

theorem Cslib.Circuits.Rational.Generator.list_length_bound (n s : ℕ) : (list n s).tuples.length ≤ 49153 ^ 3 * (n + s + 1) ^ 51

The number of tuples in list n s is at most 49153 ^ 3 * (n + s + 1) ^ 51.

theorem Cslib.Circuits.Rational.Generator.algebraic_generator : ∃ (G : (n : ℕ) → ℕ → Output n), ∀ (n s : ℕ), 1 ≤ s → (G n s).dimension ≤ 256 * (n + s + 1) ^ 10 ∧ (G n s).tuples.length ≤ 49153 ^ 3 * (n + s + 1) ^ 51 ∧ Hits s (G n s)

The algebraic hitting property and the polynomial list-cardinality bound.