Rational hitting lists: generator

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

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

def Complexity.RationalHitting.Generator.matrixDimension (e : ℕ) : ℕ

Dimension after expanding the cyclotomic matrix representation over the rationals.

Equations

• Complexity.RationalHitting.Generator.matrixDimension e = Complexity.RationalHitting.CyclotomicRing.dimension e * Complexity.RationalHitting.CyclotomicRing.degree e

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

Equations

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

def Complexity.RationalHitting.Generator.grid (H : ℕ) : List (Fin 3 → Fin H)

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

Equations

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

theorem Complexity.RationalHitting.Generator.mem_grid (H : ℕ) (x : Fin 3 → Fin H) : x ∈ grid H

theorem Complexity.RationalHitting.Generator.grid_length (H : ℕ) : (grid H).length = H ^ 3

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

Equations

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

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

Expand a specialized lift as a rational matrix.

Equations

• Complexity.RationalHitting.Generator.rationalLift n N e x i = (Complexity.RationalHitting.Generator.regular e) (Complexity.RationalHitting.Generator.specializedLift n N e x i)

noncomputable def Complexity.RationalHitting.Generator.tupleAt (n N e : ℕ) (x : Fin 3 → ℕ) : Tuple n (matrixDimension e)

Normalize all variable matrices by the zeroth matrix.

Equations

• Complexity.RationalHitting.Generator.tupleAt n N e x i = (Complexity.RationalHitting.Generator.rationalLift n N e x 0)⁻¹ * Complexity.RationalHitting.Generator.rationalLift n N e x i.succ

noncomputable def Complexity.RationalHitting.Generator.atPoint (n N e : ℕ) (x : Fin 3 → ℕ) : Option (Tuple n (matrixDimension e))

The filtering step tests only Z_0, and receives no formula.

Equations

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

noncomputable def Complexity.RationalHitting.Generator.output (n N e H : ℕ) : Output n

Collect the normalized tuples emitted at all grid points.

Equations

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

theorem Complexity.RationalHitting.Generator.length_output_le (n N e H : ℕ) : (output n N e H).tuples.length ≤ H ^ 3

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.Generator.WitnessField : Type

The Hahn field containing the algebraic witnesses for the generator.

Equations

• Complexity.RationalHitting.Generator.WitnessField = HahnSeries Complexity.RationalHitting.QuantumLift.Exponents ℂ

instance Complexity.RationalHitting.Generator.witnessCharZero : CharZero WitnessField

noncomputable def Complexity.RationalHitting.Generator.witnessEmbedding (e : ℕ) : CyclotomicRing.R e →+* WitnessField

Embed the cyclotomic field into the Hahn witness field.

Equations

• Complexity.RationalHitting.Generator.witnessEmbedding e = HahnSeries.C.comp (Complexity.RationalHitting.CyclotomicRing.intoComplex e).toRingHom

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

Equations

• Complexity.RationalHitting.Generator.finPencil f = (Matrix.reindex (Fintype.equivFin f.Index) (Fintype.equivFin f.Index)) f.pencil

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.Generator.onePencil (n : ℕ) : Matrix (Fin 1) (Fin 1) (Affine.Form n)

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

Equations

• Complexity.RationalHitting.Generator.onePencil n x✝¹ x✝ = Complexity.RationalHitting.Affine.constant 1

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

Determinant polynomials whose simultaneous nonvanishing certifies a hit.

Equations

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

theorem Complexity.RationalHitting.Generator.condition_nonzero {n s N e : ℕ} (hs : 1 ≤ s) (f : Formula n) (hf : f.size ≤ 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 Complexity.RationalHitting.Generator.condition_degree {n s N e : ℕ} (hs : 1 ≤ s) (f : Formula n) (hf : f.size ≤ s) : (conditions N e f).length ≤ s + 2 ∧ ∀ p ∈ conditions N e f, p.totalDegree ≤ 3 * (2 * s + 1) * CyclotomicRing.dimension e ^ 2

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.Parameters.w (n : ℕ) : ℕ

The parameters, with ambientDimension the least power of two strictly above BΔ.

Equations

• Complexity.RationalHitting.Parameters.w n = n + 1

def Complexity.RationalHitting.Parameters.rankBound (s : ℕ) : ℕ

Rank parameter for formulas of the given size.

Equations

• Complexity.RationalHitting.Parameters.rankBound s = 2 * s + 1

def Complexity.RationalHitting.Parameters.delta (n s : ℕ) : ℕ

Dimension allowance in the rank expansion argument.

Equations

• Complexity.RationalHitting.Parameters.delta n s = 2 * Complexity.RationalHitting.Parameters.w n ^ 3 * Complexity.RationalHitting.Parameters.rankBound s

def Complexity.RationalHitting.Parameters.exponent (n s : ℕ) : ℕ

Binary logarithm used to choose the next cyclotomic dimension.

Equations

• Complexity.RationalHitting.Parameters.exponent n s = Nat.log 2 (Complexity.RationalHitting.Parameters.rankBound s * Complexity.RationalHitting.Parameters.delta n s)

def Complexity.RationalHitting.Parameters.ambientDimension (n s : ℕ) : ℕ

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

Equations

• Complexity.RationalHitting.Parameters.ambientDimension n s = 2 ^ (Complexity.RationalHitting.Parameters.exponent n s + 1)

def Complexity.RationalHitting.Parameters.truncation (n s : ℕ) : ℕ

Number of retained columns after the dimension allowance.

Equations

• Complexity.RationalHitting.Parameters.truncation n s = Complexity.RationalHitting.Parameters.ambientDimension n s - Complexity.RationalHitting.Parameters.delta n s

def Complexity.RationalHitting.Parameters.gridSize (n s : ℕ) : ℕ

Side length of the integer grid used for specialization.

Equations

• Complexity.RationalHitting.Parameters.gridSize n s = 1 + 3 * (s + 2) * Complexity.RationalHitting.Parameters.rankBound s * Complexity.RationalHitting.Parameters.ambientDimension n s ^ 3

theorem Complexity.RationalHitting.Parameters.threshold_pos (n s : ℕ) : 0 < rankBound s * delta n s

theorem Complexity.RationalHitting.Parameters.threshold_lt (n s : ℕ) : rankBound s * delta n s < ambientDimension n s

theorem Complexity.RationalHitting.Parameters.M_le (n s : ℕ) : ambientDimension n s ≤ 2 * (rankBound s * delta n s)

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

theorem Complexity.RationalHitting.Parameters.N_pos (n s : ℕ) : 1 ≤ truncation n s

theorem Complexity.RationalHitting.Parameters.M_eq (n s : ℕ) : ambientDimension n s = truncation n s + delta n s

theorem Complexity.RationalHitting.Parameters.grid_large (n s : ℕ) : (s + 2) * (3 * rankBound s * ambientDimension n s ^ 2) < gridSize n s

theorem Complexity.RationalHitting.Parameters.w_bound (n s : ℕ) : w n ≤ n + s + 1

theorem Complexity.RationalHitting.Parameters.B_bound (n s : ℕ) : rankBound s ≤ 2 * (n + s + 1)

theorem Complexity.RationalHitting.Parameters.delta_bound (n s : ℕ) : delta n s ≤ 4 * (n + s + 1) ^ 4

theorem Complexity.RationalHitting.Parameters.polynomial_M (n s : ℕ) : ambientDimension n s ≤ 16 * (n + s + 1) ^ 5

theorem Complexity.RationalHitting.Parameters.polynomial_H (n s : ℕ) (hn : 1 ≤ n) : gridSize n s ≤ 24577 * (n + s + 1) ^ 17

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

The list with all parameters fixed by the unary inputs.

Equations

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

theorem Complexity.RationalHitting.Generator.list_hits (n s : ℕ) (hs : 1 ≤ s) : Hits s (list n s)

theorem Complexity.RationalHitting.Generator.list_dimension_bound (n s : ℕ) : (list n s).dimension ≤ 256 * (n + s + 1) ^ 10

theorem Complexity.RationalHitting.Generator.list_length_bound (n s : ℕ) (hn : 1 ≤ n) : (list n s).tuples.length ≤ 24577 ^ 3 * (n + s + 1) ^ 51

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

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