Rational hitting lists: taylor computation

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

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

theorem Complexity.RationalHitting.StackLanguage.range_sum_fin {A : Type} [AddCommMonoid A] (n : ℕ) (f : ℕ → A) : (List.map f (List.range n)).sum = ∑ i : Fin n, f ↑i

theorem Complexity.RationalHitting.StackLanguage.finEquiv_val {m : ℕ} [NeZero m] (i : Fin m) : ((ZMod.finEquiv m) i).val = ↑i

theorem Complexity.RationalHitting.StackLanguage.finEquiv_symm_val {m : ℕ} [NeZero m] (i : ZMod m) : ↑((ZMod.finEquiv m).symm i) = i.val

theorem Complexity.RationalHitting.StackLanguage.finEquiv_cast {m : ℕ} [NeZero m] (i : Fin m) : (ZMod.finEquiv m) i = ↑↑i

theorem Complexity.RationalHitting.StackLanguage.range_sum_zmod {A : Type} [AddCommMonoid A] (m : ℕ) [NeZero m] (f : ZMod m → A) : (List.map (fun (k : ℕ) => f ↑k) (List.range m)).sum = ∑ k : ZMod m, f k

theorem Complexity.RationalHitting.StackLanguage.zmod_val_sub {m : ℕ} [NeZero m] (a b : ZMod m) : (a - b).val = (a.val + (m - b.val) % m) % m

theorem Complexity.RationalHitting.StackLanguage.coordinate_vals (e : ℕ) (i : Fin (Generator.matrixDimension e)) : (((Generator.coordinate e).symm i).1.val, ↑((Generator.coordinate e).symm i).2) = (↑i / CyclotomicRing.degree e, ↑i % CyclotomicRing.degree e)

def Complexity.RationalHitting.StackLanguage.Runtime.taylorTerm (m : ℕ) (a t : ℤ) (i j r : ℕ) : ℤ

One integer summand in a Taylor test-matrix entry.

Equations

• Complexity.RationalHitting.StackLanguage.Runtime.taylorTerm m a t i j r = (-a) ^ (m - 1 - r - i) * ↑((m - 1 - r).choose i) * (a ^ (j - r) * ↑(j.choose r)) * t ^ r

def Complexity.RationalHitting.StackLanguage.Runtime.taylor (m : ℕ) (a t : ℤ) (i j : ℕ) : ℤ

Sum the integer Taylor test-matrix entry over its finite range.

Equations

• Complexity.RationalHitting.StackLanguage.Runtime.taylor m a t i j = (List.map (fun (r : ℕ) => Complexity.RationalHitting.StackLanguage.Runtime.taylorTerm m a t i j r) (List.range m)).sum

def Complexity.RationalHitting.StackLanguage.Runtime.padded (m N : ℕ) (a t : ℤ) (i j : ℕ) : ℤ

Set Taylor entries outside the retained column range to zero.

Equations

• Complexity.RationalHitting.StackLanguage.Runtime.padded m N a t i j = if j < N then Complexity.RationalHitting.StackLanguage.Runtime.taylor m a t i j else 0

theorem Complexity.RationalHitting.StackLanguage.Runtime.taylor_eq (m : ℕ) (a t : ℤ) (i j : Fin m) : taylor m a t ↑i ↑j = IntegralTest.full m a t i j

theorem Complexity.RationalHitting.StackLanguage.Runtime.padded_eq (m N : ℕ) (a t : ℤ) (i j : Fin m) : padded m N a t ↑i ↑j = IntegralTest.padded m N a t i j

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Runtime.TaylorArgs : Type

Encoded arguments for one Taylor matrix entry.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Runtime.taylorTerm_poly : Poly fun (a : TaylorArgs × Unary) => taylorTerm a.1.1.val a.1.2.1 a.1.2.2.1 a.1.2.2.2.1.val a.1.2.2.2.2.val a.2.val

theorem Complexity.RationalHitting.StackLanguage.Runtime.taylor_poly : Poly fun (a : TaylorArgs) => taylor a.1.val a.2.1 a.2.2.1 a.2.2.2.1.val a.2.2.2.2.val

theorem Complexity.RationalHitting.StackLanguage.Runtime.padded_poly : Poly fun (a : Unary × TaylorArgs) => padded a.2.1.val a.1.val a.2.2.1 a.2.2.2.1 a.2.2.2.2.1.val a.2.2.2.2.2.val

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Params : Type

Unary parameters for variable count, truncation, dimension, degree, and grid size.

Equations

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

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Params.n (p : Params) : ℕ

Number of input variables in the encoded parameter record.

Equations

• p.n = p.1.val

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Params.truncation (p : Params) : ℕ

Truncation threshold in the encoded parameter record.

Equations

• p.truncation = p.2.1.val

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Params.m (p : Params) : ℕ

Cyclotomic matrix dimension in the encoded parameter record.

Equations

• p.m = p.2.2.1.val

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Params.q (p : Params) : ℕ

Cyclotomic degree in the encoded parameter record.

Equations

• p.q = p.2.2.2.1.val

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Params.gridSize (p : Params) : ℕ

Grid side length in the encoded parameter record.

Equations

• p.gridSize = p.2.2.2.2.val

def Complexity.RationalHitting.StackLanguage.Params.of (n s : ℕ) : Params

Construct the encoded generator parameters from variable count and formula size.

Equations

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

def Complexity.RationalHitting.StackLanguage.Params.rankBound (a : Unary) : Unary

Compute the rank bound as a unary value.

Equations

• Complexity.RationalHitting.StackLanguage.Params.rankBound a = { val := Complexity.RationalHitting.Parameters.rankBound a.val }

def Complexity.RationalHitting.StackLanguage.Params.delta (a : Unary × Unary) : Unary

Compute the rank expansion allowance as a unary value.

Equations

• Complexity.RationalHitting.StackLanguage.Params.delta a = { val := Complexity.RationalHitting.Parameters.delta a.1.val a.2.val }

def Complexity.RationalHitting.StackLanguage.Params.threshold (a : Unary × Unary) : Unary

The unary threshold determining the next power-of-two dimension.

Equations

• Complexity.RationalHitting.StackLanguage.Params.threshold a = Complexity.RationalHitting.StackLanguage.Params.rankBound a.2 * Complexity.RationalHitting.StackLanguage.Params.delta a

def Complexity.RationalHitting.StackLanguage.Params.exponent (a : Unary × Unary) : Unary

Compute the cyclotomic exponent as a unary value.

Equations

• Complexity.RationalHitting.StackLanguage.Params.exponent a = { val := Complexity.RationalHitting.Parameters.exponent a.1.val a.2.val }

def Complexity.RationalHitting.StackLanguage.Params.ambientDimension (a : Unary × Unary) : Unary

Compute the ambient dimension as a unary value.

Equations

• Complexity.RationalHitting.StackLanguage.Params.ambientDimension a = { val := Complexity.RationalHitting.Parameters.ambientDimension a.1.val a.2.val }

def Complexity.RationalHitting.StackLanguage.Params.truncationUnary (a : Unary × Unary) : Unary

Compute the truncation threshold as a unary value.

Equations

• Complexity.RationalHitting.StackLanguage.Params.truncationUnary a = { val := Complexity.RationalHitting.Parameters.truncation a.1.val a.2.val }

def Complexity.RationalHitting.StackLanguage.Params.gridSizeUnary (a : Unary × Unary) : Unary

Compute the grid side length as a unary value.

Equations

• Complexity.RationalHitting.StackLanguage.Params.gridSizeUnary a = { val := Complexity.RationalHitting.Parameters.gridSize a.1.val a.2.val }

def Complexity.RationalHitting.StackLanguage.Params.degree (a : Unary × Unary) : Unary

Compute the cyclotomic degree as a unary value.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Poly.paramB : Poly Params.rankBound

theorem Complexity.RationalHitting.StackLanguage.Poly.paramDelta : Poly Params.delta

theorem Complexity.RationalHitting.StackLanguage.Poly.paramThreshold : Poly Params.threshold

theorem Complexity.RationalHitting.StackLanguage.Poly.paramExponent : Poly Params.exponent

theorem Complexity.RationalHitting.StackLanguage.Poly.paramM : Poly Params.ambientDimension

theorem Complexity.RationalHitting.StackLanguage.Poly.paramN : Poly Params.truncationUnary

theorem Complexity.RationalHitting.StackLanguage.Poly.paramH : Poly Params.gridSizeUnary

theorem Complexity.RationalHitting.StackLanguage.Poly.paramDegree : Poly Params.degree

theorem Complexity.RationalHitting.StackLanguage.Poly.params : Poly fun (a : Unary × Unary) => Params.of a.1.val a.2.val