Rational hitting lists: lift computation

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

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

def Complexity.RationalHitting.StackLanguage.Runtime.signed (q z i j : ℕ) : ℤ

The signed entry of the cyclotomic multiplication representation.

Equations

• Complexity.RationalHitting.StackLanguage.Runtime.signed q z i j = if (z + j) % q = i then (-1) ^ ((z + j) / q) else 0

def Complexity.RationalHitting.StackLanguage.Runtime.liftTerm (m N q : ℕ) (a t p r : ℤ) (u v i j x y k : ℕ) : ℤ

One integer summand in the finite Fourier lift.

Equations

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

def Complexity.RationalHitting.StackLanguage.Runtime.lift (m N q : ℕ) (a t p r : ℤ) (u v i j : ℕ) : ℤ

The integer lift obtained by summing the Fourier terms.

Equations

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

def Complexity.RationalHitting.StackLanguage.Runtime.entry (m N q : ℕ) (a t p r : ℤ) (I J : ℕ) : ℤ

An entry of the complete integral regular representation.

Equations

• Complexity.RationalHitting.StackLanguage.Runtime.entry m N q a t p r I J = Complexity.RationalHitting.StackLanguage.Runtime.lift m N q a t p r (I / q) (J / q) (I % q) (J % q)

@[reducible, inline]

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

Encoded parameters for an integral Fourier lift.

Equations

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

@[reducible, inline]

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

Encoded parameters and summation indices for one lift term.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Runtime.signed_poly : Poly fun (a : (Unary × Unary) × Unary × Unary) => signed a.1.1.val a.1.2.val a.2.1.val a.2.2.val

theorem Complexity.RationalHitting.StackLanguage.Runtime.liftTerm_poly : Poly fun (a : LiftTermArgs) => liftTerm a.1.1.1.1.1.val a.1.1.1.1.2.1.val a.1.1.1.1.2.2.val a.1.1.1.2.1.1 a.1.1.1.2.1.2.1 a.1.1.1.2.1.2.2.1 a.1.1.1.2.1.2.2.2 a.1.1.1.2.2.1.val a.1.1.1.2.2.2.1.val a.1.1.1.2.2.2.2.1.val a.1.1.1.2.2.2.2.2.val a.1.1.2.val a.1.2.val a.2.val

theorem Complexity.RationalHitting.StackLanguage.Runtime.lift_poly : Poly fun (a : LiftArgs) => lift a.1.1.val a.1.2.1.val a.1.2.2.val a.2.1.1 a.2.1.2.1 a.2.1.2.2.1 a.2.1.2.2.2 a.2.2.1.val a.2.2.2.1.val a.2.2.2.2.1.val a.2.2.2.2.2.val

@[reducible, inline]

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

Encoded parameters for one entry of the integral representation.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Runtime.entry_poly : Poly fun (a : EntryArgs) => entry a.1.1.val a.1.2.1.val a.1.2.2.val a.2.1.1 a.2.1.2.1 a.2.1.2.2.1 a.2.1.2.2.2 a.2.2.1.val a.2.2.2.val

theorem Complexity.RationalHitting.StackLanguage.range_sum_zmod_val {A : Type} [AddCommMonoid A] (m : ℕ) [NeZero m] (f : ℕ → A) : (List.map f (List.range m)).sum = ∑ z : ZMod m, f z.val

theorem Complexity.RationalHitting.StackLanguage.Runtime.signed_eq (e : ℕ) (z : ZMod (CyclotomicRing.dimension e)) (i j : Fin (CyclotomicRing.degree e)) : signed (CyclotomicRing.degree e) z.val ↑i ↑j = CyclotomicRing.signedEntry e z i j

theorem Complexity.RationalHitting.StackLanguage.Runtime.integerTest_apply (N e : ℕ) (a t : ℤ) (i j : ZMod (CyclotomicRing.dimension e)) : Generator.integerTest N e a t i j = padded (CyclotomicRing.dimension e) N a t i.val j.val

theorem Complexity.RationalHitting.StackLanguage.Runtime.liftTerm_eq (N e : ℕ) (a t p r : ℤ) (u v x y k : ZMod (CyclotomicRing.dimension e)) (i j : Fin (CyclotomicRing.degree e)) : liftTerm (CyclotomicRing.dimension e) N (CyclotomicRing.degree e) a t p r u.val v.val (↑i) (↑j) x.val y.val k.val = if u = v + y then Generator.integerTest N e a t k (k - y) * CyclotomicRing.signedEntry e (-x * k + x * u) i j * p ^ x.val * r ^ y.val else 0

theorem Complexity.RationalHitting.StackLanguage.Runtime.lift_eq (N e : ℕ) (a t p r : ℤ) (u v : ZMod (CyclotomicRing.dimension e)) (i j : Fin (CyclotomicRing.degree e)) : lift (CyclotomicRing.dimension e) N (CyclotomicRing.degree e) a t p r u.val v.val ↑i ↑j = IntegralLift.entry e (Generator.integerTest N e a t) p r u v i j

theorem Complexity.RationalHitting.StackLanguage.Runtime.entry_eq (n N e : ℕ) (x : Fin 3 → ℕ) (a : Fin (n + 1)) (i j : Fin (Generator.matrixDimension e)) : entry (CyclotomicRing.dimension e) N (CyclotomicRing.degree e) ↑↑a ↑(x 0) ↑(x 1) ↑(x 2) ↑i ↑j = Generator.integralLift n N e x a i j