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.output: the list emitted for given parameters.
• Cslib.Circuits.Rational.Parameters.truncation, Cslib.Circuits.Rational.Parameters.exponent, 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

theorem Cslib.Circuits.Rational.Generator.grid_length (H : ℕ) : (grid H).length = H ^ 3

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.length_output_le (n N e H : ℕ) : (output n N e H).tuples.length ≤ H ^ 3

theorem Cslib.Circuits.Rational.Generator.transfer {n N e : ℕ} (x : Fin 3 → ℕ) (f : Formula n) (z : (Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) (CyclotomicRing.R e))ˣ) (hz : ↑z = specializedLift n N e x 0) (v : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) (CyclotomicRing.R e)) (hf : Formula.Eval (algebraMap ℚ (Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) (CyclotomicRing.R e))) (fun (i : Fin n) => ↑z⁻¹ * specializedLift n N e x i.succ) f v) (hu : IsUnit v) : ∃ (a : Mat (matrixDimension e)), Evaluates f (tupleAt n N e x) a ∧ IsUnit a

The actual emitted rational normalization is the homomorphic image of the quotient normalization. Consequently every original inverse occurrence is kept.

theorem Cslib.Circuits.Rational.Generator.emitted {n N e H : ℕ} (x : Fin 3 → Fin H) (hz : IsUnit (specializedLift n N e (fun (i : Fin 3) => ↑(x i) + 1) 0)) : (tupleAt n N e fun (i : Fin 3) => ↑(x i) + 1) ∈ (output n N e H).tuples

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Generator.WitnessField : Type

The Hahn field containing the algebraic witnesses for the generator.

noncomputable def Cslib.Circuits.Rational.Generator.witnessEmbedding (e : ℕ) : CyclotomicRing.R e →+* WitnessField

Embed the cyclotomic field into the Hahn witness field.

noncomputable def Cslib.Circuits.Rational.Generator.finPencil {n : ℕ} (f : Formula n) : Matrix (Fin (Fintype.card f.Index)) (Fin (Fintype.card f.Index)) (Affine.Form n)

Reindex the formula's pencil by its explicit finite dimension.

theorem Cslib.Circuits.Rational.Generator.finPencil_unit {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (f : Formula n) : IsUnit ((finPencil f).map ⇑(Affine.eval c X)) ↔ IsUnit (Formula.realized c X f)

def Cslib.Circuits.Rational.Generator.onePencil (n : ℕ) : Matrix (Fin 1) (Fin 1) (Affine.Form n)

A one-by-one constant pencil used to enforce normalization.

noncomputable def Cslib.Circuits.Rational.Generator.conditions {n : ℕ} (N e : ℕ) (f : Formula n) : List (MvPolynomial (Fin 3) (CyclotomicRing.R e))

Determinant polynomials whose simultaneous nonvanishing certifies a hit.

theorem Cslib.Circuits.Rational.Generator.condition_nonzero {n s N e : ℕ} (hs : 1 ≤ s) (f : Formula n) (hf : f.nodeCount ≤ s) (hnz : Nonzero f) (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) (p : MvPolynomial (Fin 3) (CyclotomicRing.R e)) : p ∈ conditions N e f → p ≠ 0

theorem Cslib.Circuits.Rational.Generator.condition_degree {n s N e : ℕ} (hs : 1 ≤ s) (f : Formula n) (hf : f.nodeCount ≤ s) : (conditions N e f).length ≤ s + 2 ∧ ∀ p ∈ conditions N e f, p.totalDegree ≤ 3 * (2 * s + 1) * CyclotomicRing.dimension e ^ 2

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.specialized_unit {K : Type u_1} [Field K] [CharZero K] {n q M N : ℕ} [NeZero M] (χ : AddChar (ZMod M) K) (L : Matrix (Fin q) (Fin q) (Affine.Form n)) (x : Fin 3 → K) (hx : (MvPolynomial.eval x) (PencilCertificates.determinant χ N L) ≠ 0) : IsUnit (L.map (Affine.homogeneous (algebraMap ℚ (Matrix (ZMod M) (ZMod M) K)) fun (i : Fin (n + 1)) => (MvPolynomial.eval₂Hom (RingHom.id K) x).mapMatrix (PencilCertificates.lifts χ N n i)))

theorem Cslib.Circuits.Rational.Generator.onePencil_unit {K : Type u_1} [Field K] [CharZero K] {n : ℕ} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (rationalLift : Fin (n + 1) → Matrix ι ι K) (h : IsUnit ((onePencil n).map (Affine.homogeneous (algebraMap ℚ (Matrix ι ι K)) rationalLift))) : IsUnit (rationalLift 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

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

theorem Cslib.Circuits.Rational.Parameters.M_le (n s : ℕ) : ambientDimension n s ≤ 2 * (rankBound s * delta n s)

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

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

theorem Cslib.Circuits.Rational.Parameters.M_eq (n s : ℕ) : ambientDimension n s = truncation n s + delta n s

theorem Cslib.Circuits.Rational.Parameters.grid_large (n s : ℕ) : (s + 2) * (3 * rankBound s * ambientDimension n s ^ 2) < gridSize n s

theorem Cslib.Circuits.Rational.Parameters.w_bound (n s : ℕ) : w n ≤ n + s + 1

theorem Cslib.Circuits.Rational.Parameters.B_bound (n s : ℕ) : rankBound s ≤ 2 * (n + s + 1)

theorem Cslib.Circuits.Rational.Parameters.delta_bound (n s : ℕ) : delta n s ≤ 4 * (n + s + 1) ^ 4

theorem Cslib.Circuits.Rational.Parameters.polynomial_M (n s : ℕ) : ambientDimension n s ≤ 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)

theorem Cslib.Circuits.Rational.Generator.list_dimension_bound (n s : ℕ) : (list n s).dimension ≤ 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

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.