List programs and evaluation equivalences for the integer lift tables

At every grid point the executable generator materializes the integer lift matrices Rational.Generator.integralLift, built from the integer Taylor test matrices Rational.IntegralTest.padded and the signed-monomial formula Rational.IntegralLift.entry. Those definitions are indexed by Fin and ZMod with a type-level modulus, and use Nat.choose. This file restates them as ordinary programs on natural numbers, integers and lists of rows, and proves that they compute the landed matrix definitions:

• the coefficients of (X + c) ^ k are computed by k shift-and-add steps (coeffRow), with no division;
• the Taylor test matrix is a list of rows of sums over List.range M (testRows);
• every lift entry is a double sum over List.range M of M ^ 2 terms (liftEntry, liftTable, liftRows). The original formula sums over three residues; the residue β is forced to be u - v, so that sum is dropped.

Magnitude bounds, bit-length budgets, and polynomial-time Turing machine certificates for these list programs are proved in Complexity/Computability/Circuit/Rational/Runtime/Lift.lean.

Main definitions

• Cslib.Circuits.Rational.shiftAddRow, Cslib.Circuits.Rational.coeffRow, Cslib.Circuits.Rational.coeffRows: the coefficients of (X + c) ^ k, by repeated shift-and-add.
• Cslib.Circuits.Rational.testTerm, Cslib.Circuits.Rational.testTerms, Cslib.Circuits.Rational.testEntry, Cslib.Circuits.Rational.testRows: the integer Taylor test matrix as a list of rows.
• Cslib.Circuits.Rational.signedCoeff, Cslib.Circuits.Rational.liftTerm, Cslib.Circuits.Rational.liftTerms, Cslib.Circuits.Rational.liftSums, Cslib.Circuits.Rational.liftEntry: the signed coefficient of the cyclotomic regular representation, and the terms and entries of the integer lift.
• Cslib.Circuits.Rational.liftTable, Cslib.Circuits.Rational.liftRows: one integer lift matrix, and all of them at a grid point.

Main results

• Cslib.Circuits.Rational.getD_coeffRow, Cslib.Circuits.Rational.getD_coeffRow_eq: coeffRow computes the coefficients of (X + C c) ^ k.
• Cslib.Circuits.Rational.testEntry_eq, Cslib.Circuits.Rational.testRows_eq: testRows M N a t = rowsOf (IntegralTest.padded M N a t).
• Cslib.Circuits.Rational.liftEntry_eq: the double sum computes IntegralLift.entry.
• Cslib.Circuits.Rational.liftTable_eq, Cslib.Circuits.Rational.liftRows_eq, Cslib.Circuits.Rational.liftRows_eq_inputTables: the lift tables are the rows of Generator.integralLift, and of the executable generator's inputTables.

References

• The index bridges and the forms of signedCoeff, testTerm and the lift sum are adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (files lean/OAI/Computability/RationalHitting/TaylorComputation.lean and LiftComputation.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

Index bridges

theorem Cslib.Circuits.Rational.val_finEquiv {m : ℕ} [NeZero m] (i : Fin m) : ((ZMod.finEquiv m) i).val = ↑i

theorem Cslib.Circuits.Rational.val_finEquiv_symm {m : ℕ} [NeZero m] (z : ZMod m) : ↑((ZMod.finEquiv m).symm z) = z.val

theorem Cslib.Circuits.Rational.sum_range_eq_sum_fin {A : Type u_1} [AddCommMonoid A] (m : ℕ) (f : ℕ → A) : (List.map f (List.range m)).sum = ∑ i : Fin m, f ↑i

A sum over List.range m is a sum over Fin m.

theorem Cslib.Circuits.Rational.sum_range_eq_sum_zmod {A : Type u_1} [AddCommMonoid A] (m : ℕ) [NeZero m] (f : ℕ → A) : (List.map f (List.range m)).sum = ∑ z : ZMod m, f z.val

A sum over List.range m is a sum over the residues modulo m.

theorem Cslib.Circuits.Rational.val_sub_eq_mod {m : ℕ} [NeZero m] (u v : ZMod m) : (u - v).val = (u.val + m - v.val) % m

Residue subtraction on values, without truncated subtraction below zero.

theorem Cslib.Circuits.Rational.val_neg_mul_add_mul_eq_mod {m : ℕ} [NeZero m] (a u k : ZMod m) : (-a * k + a * u).val = a.val * (u.val + m - k.val) % m

The residue -a * k + a * u of the lift formula, on values.

theorem Cslib.Circuits.Rational.val_coordinate_symm_fst (e : ℕ) (i : Fin (Generator.matrixDimension e)) : ((Generator.coordinate e).symm i).1.val = ↑i / CyclotomicRing.degree e

The residue of the row-major block coordinate is the quotient by the degree.

theorem Cslib.Circuits.Rational.val_coordinate_symm_snd (e : ℕ) (i : Fin (Generator.matrixDimension e)) : ↑((Generator.coordinate e).symm i).2 = ↑i % CyclotomicRing.degree e

The position inside the block of the row-major block coordinate is the remainder.

Lists of rows

theorem Cslib.Circuits.Rational.tabulateRows_eq_rowsOf {d : ℕ} (g : ℕ → ℕ → ℤ) (A : Matrix (Fin d) (Fin d) ℤ) (h : ∀ (i j : Fin d), g ↑i ↑j = A i j) : tabulateRows d g = rowsOf A

A tabulated list of rows is the list of rows of a matrix it agrees with.

theorem Cslib.Circuits.Rational.natAbs_le_of_mem_rows {rows : List (List ℤ)} {C : ℕ} (h : ∀ (i j : ℕ), (rowEntry rows i j).natAbs ≤ C) {row : List ℤ} (hrow : row ∈ rows) {z : ℤ} (hz : z ∈ row) : z.natAbs ≤ C

Every stored entry is bounded once every indexed entry is.

Coefficient rows

def Cslib.Circuits.Rational.shiftAddRow (c : ℤ) (l : List ℤ) : List ℤ

Multiply a polynomial by X + c. The polynomial is given by its list of coefficients, constant coefficient first; coefficient i of the product is l[i - 1] + c * l[i].

def Cslib.Circuits.Rational.coeffRow (c : ℤ) (k : ℕ) : List ℤ

The coefficients of (X + c) ^ k, constant coefficient first, computed by k shift-and-add steps from [1].

def Cslib.Circuits.Rational.coeffRows (c : ℤ) (M : ℕ) : List (List ℤ)

The coefficient rows coeffRow c k for k < M.

@[simp]

theorem Cslib.Circuits.Rational.length_shiftAddRow (c : ℤ) (l : List ℤ) : (shiftAddRow c l).length = l.length + 1

theorem Cslib.Circuits.Rational.getD_shiftAddRow (c : ℤ) (l : List ℤ) (i : ℕ) : (shiftAddRow c l).getD i 0 = (0 :: l).getD i 0 + c * l.getD i 0

@[simp]

theorem Cslib.Circuits.Rational.coeffRow_zero (c : ℤ) : coeffRow c 0 = [1]

theorem Cslib.Circuits.Rational.coeffRow_succ (c : ℤ) (k : ℕ) : coeffRow c (k + 1) = shiftAddRow c (coeffRow c k)

@[simp]

theorem Cslib.Circuits.Rational.length_coeffRow (c : ℤ) (k : ℕ) : (coeffRow c k).length = k + 1

theorem Cslib.Circuits.Rational.getD_coeffRow (c : ℤ) (k i : ℕ) : (coeffRow c k).getD i 0 = ((Polynomial.X + Polynomial.C c) ^ k).coeff i

coeffRow computes the coefficients of (X + C c) ^ k.

theorem Cslib.Circuits.Rational.getD_coeffRow_eq (c : ℤ) (k i : ℕ) : (coeffRow c k).getD i 0 = c ^ (k - i) * ↑(k.choose i)

The closed form of the coefficient rows, as in IntegralTest.full.

theorem Cslib.Circuits.Rational.rowEntry_coeffRows (c : ℤ) (M k i : ℕ) : rowEntry (coeffRows c M) k i = if k < M then (coeffRow c k).getD i 0 else 0

The integer Taylor test matrix

def Cslib.Circuits.Rational.testTerm (M : ℕ) (minus plus : List (List ℤ)) (t : ℤ) (u v q : ℕ) : ℤ

The summand q of entry (u, v) of the integer Taylor test matrix: coefficient u of (X - a) ^ (M - 1 - q) times coefficient q of (X + a) ^ v times t ^ q, read from the coefficient rows minus and plus.

def Cslib.Circuits.Rational.testTerms (M : ℕ) (minus plus : List (List ℤ)) (t : ℤ) (u v : ℕ) : List ℤ

The summands of entry (u, v) of the integer Taylor test matrix.

def Cslib.Circuits.Rational.testEntry (M N : ℕ) (minus plus : List (List ℤ)) (t : ℤ) (u v : ℕ) : ℤ

Entry (u, v) of the integer Taylor test matrix; the columns from N on are zero.

def Cslib.Circuits.Rational.testRows (M N : ℕ) (a t : ℤ) : List (List ℤ)

The integer Taylor test matrix IntegralTest.padded M N a t as a list of rows.

theorem Cslib.Circuits.Rational.testEntry_eq (M N : ℕ) (a t : ℤ) (u v : Fin M) : testEntry M N (coeffRows (-a) M) (coeffRows a M) t ↑u ↑v = IntegralTest.padded M N a t u v

theorem Cslib.Circuits.Rational.rowEntry_testRows (M N : ℕ) (a t : ℤ) (u v : Fin M) : rowEntry (testRows M N a t) ↑u ↑v = IntegralTest.padded M N a t u v

theorem Cslib.Circuits.Rational.testRows_eq (M N : ℕ) (a t : ℤ) : testRows M N a t = rowsOf (IntegralTest.padded M N a t)

The list program computes the integer Taylor test matrix.

theorem Cslib.Circuits.Rational.rowEntry_testRows_integerTest (N e : ℕ) (a t : ℤ) (u v : ZMod (CyclotomicRing.dimension e)) : rowEntry (testRows (CyclotomicRing.dimension e) N a t) u.val v.val = Generator.integerTest N e a t u v

The Taylor rows, read at residues, are the residue-indexed Generator.integerTest.

@[simp]

theorem Cslib.Circuits.Rational.length_testRows (M N : ℕ) (a t : ℤ) : (testRows M N a t).length = M

The integer lift

def Cslib.Circuits.Rational.signedCoeff (Dg z i j : ℕ) : ℤ

The signed coefficient of the cyclotomic regular representation on natural numbers: CyclotomicRing.signedEntry with the residue replaced by its value.

def Cslib.Circuits.Rational.liftTerm (M Dg : ℕ) (T : List (List ℤ)) (p r : ℤ) (u v i j α κ : ℕ) : ℤ

The term (α, κ) of entry ((u, i), (v, j)) of the integer lift with test matrix T, with M residues and cyclotomic degree Dg. The residue β of IntegralLift.entry is forced to be u - v, which is (u + M - v) % M; κ - β and α * (u - κ) are computed likewise.

def Cslib.Circuits.Rational.liftTerms (M Dg : ℕ) (T : List (List ℤ)) (p r : ℤ) (u v i j α : ℕ) : List ℤ

The terms κ < M of the inner sum, for the residue α.

def Cslib.Circuits.Rational.liftSums (M Dg : ℕ) (T : List (List ℤ)) (p r : ℤ) (u v i j : ℕ) : List ℤ

The inner sums α < M of an integer lift entry.

def Cslib.Circuits.Rational.liftEntry (M Dg : ℕ) (T : List (List ℤ)) (p r : ℤ) (u v i j : ℕ) : ℤ

Entry ((u, i), (v, j)) of the integer lift: a double sum of M ^ 2 terms.

def Cslib.Circuits.Rational.liftTable (M Dg : ℕ) (T : List (List ℤ)) (p r : ℤ) : List (List ℤ)

The integer lift matrix with test matrix T, in the row-major block order: index i is the pair (i / Dg, i % Dg).

def Cslib.Circuits.Rational.liftRows (n N M Dg t p r : ℕ) : List (List (List ℤ))

The n + 1 integer lift matrices at the grid point (t, p, r), with truncation N, M residues and cyclotomic degree Dg.

theorem Cslib.Circuits.Rational.signedCoeff_eq (e : ℕ) (z : ZMod (CyclotomicRing.dimension e)) (i j : Fin (CyclotomicRing.degree e)) : signedCoeff (CyclotomicRing.degree e) z.val ↑i ↑j = CyclotomicRing.signedEntry e z i j

theorem Cslib.Circuits.Rational.liftEntry_eq (e : ℕ) {T : List (List ℤ)} {T' : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) ℤ} (hT : ∀ (k l : ZMod (CyclotomicRing.dimension e)), rowEntry T k.val l.val = T' k l) (p r : ℤ) (u v : ZMod (CyclotomicRing.dimension e)) (i j : Fin (CyclotomicRing.degree e)) : liftEntry (CyclotomicRing.dimension e) (CyclotomicRing.degree e) T p r u.val v.val ↑i ↑j = IntegralLift.entry e T' p r u v i j

The double sum computes the integer lift formula, for any list of rows that agrees with the test matrix at residues.

theorem Cslib.Circuits.Rational.liftEntry_testRows (N e : ℕ) (a t p r : ℤ) (u v : ZMod (CyclotomicRing.dimension e)) (i j : Fin (CyclotomicRing.degree e)) : liftEntry (CyclotomicRing.dimension e) (CyclotomicRing.degree e) (testRows (CyclotomicRing.dimension e) N 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

The integer lift entry of Generator.integralLift, on the residues of the test rows.

theorem Cslib.Circuits.Rational.liftEntry_coordinate (n N e : ℕ) (x : Fin 3 → ℕ) (a : Fin (n + 1)) (i j : Fin (Generator.matrixDimension e)) : liftEntry (CyclotomicRing.dimension e) (CyclotomicRing.degree e) (testRows (CyclotomicRing.dimension e) N ↑↑a ↑(x 0)) (↑(x 1)) (↑(x 2)) (↑i / CyclotomicRing.degree e) (↑j / CyclotomicRing.degree e) (↑i % CyclotomicRing.degree e) (↑j % CyclotomicRing.degree e) = Generator.integralLift n N e x a i j

The entries of a lift table are the entries of Generator.integralLift.

theorem Cslib.Circuits.Rational.liftTable_eq (n N e : ℕ) (x : Fin 3 → ℕ) (a : Fin (n + 1)) : liftTable (CyclotomicRing.dimension e) (CyclotomicRing.degree e) (testRows (CyclotomicRing.dimension e) N ↑↑a ↑(x 0)) ↑(x 1) ↑(x 2) = rowsOf (Generator.integralLift n N e x a)

The list program computes Generator.integralLift.

theorem Cslib.Circuits.Rational.rowEntry_liftTable (n N e : ℕ) (x : Fin 3 → ℕ) (a : Fin (n + 1)) (i j : Fin (Generator.matrixDimension e)) : rowEntry (liftTable (CyclotomicRing.dimension e) (CyclotomicRing.degree e) (testRows (CyclotomicRing.dimension e) N ↑↑a ↑(x 0)) ↑(x 1) ↑(x 2)) ↑i ↑j = Generator.integralLift n N e x a i j

theorem Cslib.Circuits.Rational.liftRows_eq (n N e : ℕ) (x : Fin 3 → ℕ) : liftRows n N (CyclotomicRing.dimension e) (CyclotomicRing.degree e) (x 0) (x 1) (x 2) = List.map (fun (a : Fin (n + 1)) => rowsOf (Generator.integralLift n N e x a)) (List.finRange (n + 1))

The list program computes all integer lift matrices at a grid point.

theorem Cslib.Circuits.Rational.liftRows_eq_inputTables (n N e : ℕ) (x : Fin 3 → ℕ) : liftRows n N (CyclotomicRing.dimension e) (CyclotomicRing.degree e) (x 0) (x 1) (x 2) = List.map (fun (A : DeterminantAlgorithm.Table (Generator.matrixDimension e)) => rowsOf (DeterminantAlgorithm.denote A)) (ExecutableGenerator.inputTables n N e x).toList

The list program computes the executable generator's dense input tables.

@[simp]

theorem Cslib.Circuits.Rational.length_liftTable (M Dg : ℕ) (T : List (List ℤ)) (p r : ℤ) : (liftTable M Dg T p r).length = M * Dg

@[simp]

theorem Cslib.Circuits.Rational.length_liftRows (n N M Dg t p r : ℕ) : (liftRows n N M Dg t p r).length = n + 1