Magnitude bounds and polynomial-time certificates for the integer lift tables

Complexity/Computability/Circuit/Rational/Runtime/Lift/Defs.lean defines the list-level programs coeffRow, testRows, liftTable, and liftRows that materialize the integer Taylor test matrices and integer lift tables at a grid point. This file bounds the magnitude and bit length of every value those programs compute: each coefficient, each shift-and-add intermediate, each power, each partial product and term, every prefix sum, and every entry. For n + 1 matrices, M residues and grid coordinates at most H, all of them have at most Rational.liftBits n M H bits, which at the generator's parameters is Rational.PolynomialBounds.logarithmic n s + 2. Using these bounds, it certifies that coeffRows, testRows, liftTable, and liftRows are computable in polynomial time on multi-tape Turing machines.

Main definitions

• Cslib.Circuits.Rational.liftBits: the bit-length budget of the lift program.
• Cslib.Circuits.Rational.coeffEntryBound, Cslib.Circuits.Rational.coeffRowBound: encoded length bounds on intermediate coefficient rows.

Main results

• Cslib.Circuits.Rational.intBits_coeffRow_le, Cslib.Circuits.Rational.intBits_test_le, Cslib.Circuits.Rational.intBits_lift_le, Cslib.Circuits.Rational.intBits_le_of_mem_liftRows: the bit-length bounds.
• Cslib.Circuits.Rational.intBits_le_of_mem_liftRows_parameters: at the generator's parameters, every entry has at most logConstant * (n + s + 1) ^ 22 + 2 bits.
• Cslib.Circuits.Rational.length_encList_coeffRow_le: encoded length bound on intermediate coefficient rows.
• Cslib.Circuits.Rational.computableInPolyTime_coeffRow, Cslib.Circuits.Rational.computableInPolyTime_testRows, Cslib.Circuits.Rational.computableInPolyTime_liftTable, Cslib.Circuits.Rational.computableInPolyTime_liftRows, Cslib.Circuits.Rational.liftRows_polytime: polynomial-time certificates for the coefficient rows, the Taylor test matrix and the integer lift tables.

References

• 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.

Magnitude bounds

theorem Cslib.Circuits.Rational.natAbs_pow_le {z : ℤ} {H : ℕ} (hH : 1 ≤ H) (hz : z.natAbs ≤ H) {q M : ℕ} (hq : q ≤ M) : (z ^ q).natAbs ≤ H ^ M

theorem Cslib.Circuits.Rational.natAbs_getD_coeffRow_le {c : ℤ} {w : ℕ} (hw : 1 ≤ w) (hc : c.natAbs ≤ w) (k i : ℕ) : ((coeffRow c k).getD i 0).natAbs ≤ (2 * w) ^ k

The coefficients of (X + c) ^ k are at most (2 * w) ^ k in absolute value, by IntegralTest.coeff_bound.

theorem Cslib.Circuits.Rational.natAbs_shiftAdd_le {c : ℤ} {w : ℕ} (hw : 1 ≤ w) (hc : c.natAbs ≤ w) (k i : ℕ) : ((0 :: coeffRow c k).getD i 0).natAbs ≤ (2 * w) ^ (k + 1) ∧ (c * (coeffRow c k).getD i 0).natAbs ≤ (2 * w) ^ (k + 1) ∧ ((0 :: coeffRow c k).getD i 0 + c * (coeffRow c k).getD i 0).natAbs ≤ (2 * w) ^ (k + 1)

The values computed by the shift-and-add step from coeffRow c k: the shifted coefficient, the scaled coefficient and their sum.

theorem Cslib.Circuits.Rational.natAbs_rowEntry_coeffRows_le {c : ℤ} {w : ℕ} (hw : 1 ≤ w) (hc : c.natAbs ≤ w) (M k i : ℕ) : (rowEntry (coeffRows c M) k i).natAbs ≤ (2 * w) ^ M

theorem Cslib.Circuits.Rational.natAbs_coeffProduct_le {M : ℕ} {a : ℤ} {w : ℕ} (hw : 1 ≤ w) (ha : a.natAbs ≤ w) (k u v q : ℕ) : (rowEntry (coeffRows (-a) M) k u * rowEntry (coeffRows a M) v q).natAbs ≤ (2 * w) ^ (2 * M)

theorem Cslib.Circuits.Rational.natAbs_testTerm_le {M : ℕ} {a t : ℤ} {w H : ℕ} (hw : 1 ≤ w) (ha : a.natAbs ≤ w) (hH : 1 ≤ H) (ht : t.natAbs ≤ H) {q : ℕ} (hq : q ≤ M) (u v : ℕ) : (testTerm M (coeffRows (-a) M) (coeffRows a M) t u v q).natAbs ≤ (2 * w) ^ (2 * M) * H ^ M

theorem Cslib.Circuits.Rational.natAbs_testTerms_take_sum_le {M : ℕ} {a t : ℤ} {w H : ℕ} (hw : 1 ≤ w) (ha : a.natAbs ≤ w) (hH : 1 ≤ H) (ht : t.natAbs ≤ H) (u v m : ℕ) : (List.take m (testTerms M (coeffRows (-a) M) (coeffRows a M) t u v)).sum.natAbs ≤ M * ((2 * w) ^ (2 * M) * H ^ M)

Every prefix sum of the summands of a Taylor entry.

theorem Cslib.Circuits.Rational.natAbs_rowEntry_testRows_le {M : ℕ} {a t : ℤ} {w H : ℕ} (hw : 1 ≤ w) (ha : a.natAbs ≤ w) (hH : 1 ≤ H) (ht : t.natAbs ≤ H) (N u v : ℕ) : (rowEntry (testRows M N a t) u v).natAbs ≤ M * ((2 * w) ^ (2 * M) * H ^ M)

theorem Cslib.Circuits.Rational.natAbs_signedCoeff_le (Dg z i j : ℕ) : (signedCoeff Dg z i j).natAbs ≤ 1

theorem Cslib.Circuits.Rational.natAbs_liftPartial_le {Dg : ℕ} {T : List (List ℤ)} {A : ℕ} (hT : ∀ (k l : ℕ), (rowEntry T k l).natAbs ≤ A) (k l z i j : ℕ) : (rowEntry T k l * signedCoeff Dg z i j).natAbs ≤ A

The partial products of a lift term, for any indices.

theorem Cslib.Circuits.Rational.natAbs_liftPartial_pow_le {M Dg : ℕ} {T : List (List ℤ)} {p : ℤ} {A H : ℕ} (hT : ∀ (k l : ℕ), (rowEntry T k l).natAbs ≤ A) (hH : 1 ≤ H) (hp : p.natAbs ≤ H) (k l z i j : ℕ) {α : ℕ} (hα : α ≤ M) : (rowEntry T k l * signedCoeff Dg z i j * p ^ α).natAbs ≤ A * H ^ M

theorem Cslib.Circuits.Rational.natAbs_liftTerm_le {M Dg : ℕ} {T : List (List ℤ)} {p r : ℤ} {A H : ℕ} (hT : ∀ (k l : ℕ), (rowEntry T k l).natAbs ≤ A) (hH : 1 ≤ H) (hp : p.natAbs ≤ H) (hr : r.natAbs ≤ H) {α : ℕ} (hα : α < M) (u v i j κ : ℕ) : (liftTerm M Dg T p r u v i j α κ).natAbs ≤ A * H ^ (2 * M)

theorem Cslib.Circuits.Rational.natAbs_liftTerms_take_sum_le {M Dg : ℕ} {T : List (List ℤ)} {p r : ℤ} {A H : ℕ} (hT : ∀ (k l : ℕ), (rowEntry T k l).natAbs ≤ A) (hH : 1 ≤ H) (hp : p.natAbs ≤ H) (hr : r.natAbs ≤ H) {α : ℕ} (hα : α < M) (u v i j m : ℕ) : (List.take m (liftTerms M Dg T p r u v i j α)).sum.natAbs ≤ M * (A * H ^ (2 * M))

Every prefix sum of an inner sum of a lift entry.

theorem Cslib.Circuits.Rational.natAbs_liftSums_take_sum_le {M Dg : ℕ} {T : List (List ℤ)} {p r : ℤ} {A H : ℕ} (hT : ∀ (k l : ℕ), (rowEntry T k l).natAbs ≤ A) (hH : 1 ≤ H) (hp : p.natAbs ≤ H) (hr : r.natAbs ≤ H) (u v i j m : ℕ) : (List.take m (liftSums M Dg T p r u v i j)).sum.natAbs ≤ M * (M * (A * H ^ (2 * M)))

Every prefix sum of the outer sum of a lift entry.

theorem Cslib.Circuits.Rational.natAbs_liftEntry_le {M Dg : ℕ} {T : List (List ℤ)} {p r : ℤ} {A H : ℕ} (hT : ∀ (k l : ℕ), (rowEntry T k l).natAbs ≤ A) (hH : 1 ≤ H) (hp : p.natAbs ≤ H) (hr : r.natAbs ≤ H) (u v i j : ℕ) : (liftEntry M Dg T p r u v i j).natAbs ≤ M * (M * (A * H ^ (2 * M)))

theorem Cslib.Circuits.Rational.natAbs_rowEntry_liftTable_le {M Dg : ℕ} {T : List (List ℤ)} {p r : ℤ} {A H : ℕ} (hT : ∀ (k l : ℕ), (rowEntry T k l).natAbs ≤ A) (hH : 1 ≤ H) (hp : p.natAbs ≤ H) (hr : r.natAbs ≤ H) (i j : ℕ) : (rowEntry (liftTable M Dg T p r) i j).natAbs ≤ M * (M * (A * H ^ (2 * M)))

Bit lengths

def Cslib.Circuits.Rational.liftBits (n M H : ℕ) : ℕ

The bit-length budget of the lift program, for n + 1 matrices, M residues and grid coordinates at most H. At the generator's parameters it is PolynomialBounds.logarithmic n s + 2 (liftBits_parameters).

theorem Cslib.Circuits.Rational.liftBits_parameters (n s : ℕ) : liftBits n (Parameters.ambientDimension n s) (Parameters.gridSize n s) = PolynomialBounds.logarithmic n s + 2

theorem Cslib.Circuits.Rational.liftBits_bound (n s : ℕ) : liftBits n (Parameters.ambientDimension n s) (Parameters.gridSize n s) ≤ PolynomialBounds.logConstant * (n + s + 1) ^ 22 + 2

At the generator's parameters, the bit-length budget is polynomial in n + s + 1.

theorem Cslib.Circuits.Rational.intBits_le_liftBits {n M H : ℕ} {z : ℤ} (hz : z.natAbs ≤ M ^ 3 * (2 * (n + 1)) ^ (2 * M) * H ^ (3 * M)) : intBits z ≤ liftBits n M H

Every value of magnitude at most M ^ 3 * (2 * (n + 1)) ^ (2 * M) * H ^ (3 * M) fits in the budget.

theorem Cslib.Circuits.Rational.le_liftMagnitude {M w H i j k : ℕ} (hM : 1 ≤ M) (hw : 1 ≤ w) (hH : 1 ≤ H) (hi : i ≤ 3) (hj : j ≤ 2 * M) (hk : k ≤ 3 * M) : M ^ i * (2 * w) ^ j * H ^ k ≤ M ^ 3 * (2 * w) ^ (2 * M) * H ^ (3 * M)

Each factor of the magnitude bound can be weakened.

theorem Cslib.Circuits.Rational.intBits_coeffRow_le {n M H : ℕ} (hM : 1 ≤ M) (hH : 1 ≤ H) {c : ℤ} (hc : c.natAbs ≤ n) {k : ℕ} (hk : k < M) (i : ℕ) : intBits ((coeffRow c k).getD i 0) ≤ liftBits n M H ∧ intBits ((0 :: coeffRow c k).getD i 0) ≤ liftBits n M H ∧ intBits (c * (coeffRow c k).getD i 0) ≤ liftBits n M H ∧ intBits ((0 :: coeffRow c k).getD i 0 + c * (coeffRow c k).getD i 0) ≤ liftBits n M H

The bit lengths of the coefficients of (X + c) ^ k for k < M, and of the values computed by the shift-and-add step from them.

theorem Cslib.Circuits.Rational.intBits_pow_le {n M H : ℕ} (hM : 1 ≤ M) (hH : 1 ≤ H) {z : ℤ} (hz : z.natAbs ≤ H) {q : ℕ} (hq : q ≤ M) : intBits (z ^ q) ≤ liftBits n M H

The bit lengths of the powers z ^ q for q ≤ M; computing a power by repeated multiplication passes only through smaller powers.

theorem Cslib.Circuits.Rational.intBits_test_le {n M H : ℕ} (hM : 1 ≤ M) (hH : 1 ≤ H) {a t : ℤ} (ha : a.natAbs ≤ n) (ht : t.natAbs ≤ H) (N k u v q m : ℕ) (hq : q < M) : intBits (rowEntry (coeffRows (-a) M) k u * rowEntry (coeffRows a M) v q) ≤ liftBits n M H ∧ intBits (testTerm M (coeffRows (-a) M) (coeffRows a M) t u v q) ≤ liftBits n M H ∧ intBits (List.take m (testTerms M (coeffRows (-a) M) (coeffRows a M) t u v)).sum ≤ liftBits n M H ∧ intBits (rowEntry (testRows M N a t) u v) ≤ liftBits n M H

The bit lengths of the values computed for the Taylor test matrix testRows M N a t: the products of coefficients, the terms, every prefix sum of the terms of an entry, and the entries.

theorem Cslib.Circuits.Rational.intBits_lift_le {n M H : ℕ} (hM : 1 ≤ M) (hH : 1 ≤ H) {a t p r : ℤ} (ha : a.natAbs ≤ n) (ht : t.natAbs ≤ H) (hp : p.natAbs ≤ H) (hr : r.natAbs ≤ H) (N Dg u v i j k l z m : ℕ) {α κ : ℕ} (hα : α < M) : intBits (rowEntry (testRows M N a t) k l * signedCoeff Dg z i j) ≤ liftBits n M H ∧ intBits (rowEntry (testRows M N a t) k l * signedCoeff Dg z i j * p ^ α) ≤ liftBits n M H ∧ intBits (liftTerm M Dg (testRows M N a t) p r u v i j α κ) ≤ liftBits n M H ∧ intBits (List.take m (liftTerms M Dg (testRows M N a t) p r u v i j α)).sum ≤ liftBits n M H ∧ intBits (List.take m (liftSums M Dg (testRows M N a t) p r u v i j)).sum ≤ liftBits n M H ∧ intBits (liftEntry M Dg (testRows M N a t) p r u v i j) ≤ liftBits n M H ∧ intBits (rowEntry (liftTable M Dg (testRows M N a t) p r) k l) ≤ liftBits n M H

The bit lengths of the values computed for the integer lift with the Taylor test matrix testRows M N a t: the partial products and the terms, every prefix sum of an inner sum and of the outer sum, the entries and the entries of the lift table.

theorem Cslib.Circuits.Rational.intBits_le_of_mem_liftRows {n M H : ℕ} (hM : 1 ≤ M) (hH : 1 ≤ H) {N Dg t p r : ℕ} (ht : t ≤ H) (hp : p ≤ H) (hr : r ≤ H) {table : List (List ℤ)} (htable : table ∈ liftRows n N M Dg t p r) {row : List ℤ} (hrow : row ∈ table) {z : ℤ} (hz : z ∈ row) : intBits z ≤ liftBits n M H

Every entry of every integer lift table at a grid point with coordinates at most H has at most liftBits n M H bits.

theorem Cslib.Circuits.Rational.intBits_le_of_mem_liftRows_parameters {n s t p r : ℕ} (ht : t ≤ Parameters.gridSize n s) (hp : p ≤ Parameters.gridSize n s) (hr : r ≤ Parameters.gridSize n s) {table : List (List ℤ)} (htable : table ∈ liftRows n (Parameters.truncation n s) (Parameters.ambientDimension n s) (CyclotomicRing.degree (Parameters.exponent n s)) t p r) {row : List ℤ} (hrow : row ∈ table) {z : ℤ} (hz : z ∈ row) : intBits z ≤ PolynomialBounds.logConstant * (n + s + 1) ^ 22 + 2

At the generator's parameters, every entry of every integer lift table at a grid point has at most logConstant * (n + s + 1) ^ 22 + 2 bits.

Polynomial-time certificates

def Cslib.Circuits.Rational.coeffEntryBound (L k : ℕ) : ℕ

Upper bound on the bit length of any entry of coeffRow c i for i ≤ k, where L is the encoded length of c.

def Cslib.Circuits.Rational.coeffRowBound (L k : ℕ) : ℕ

Upper bound on the encoded length of coeffRow c i for i ≤ k, where L is the encoded length of c.

theorem Cslib.Circuits.Rational.length_encList_coeffRow_le (c : ℤ) {i k : ℕ} (hik : i ≤ k) : ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) (coeffRow c i)).length ≤ coeffRowBound (Turing.MultiTapeTM.encIntBin c).length k

Every intermediate coefficient row up to stage k has encoded length bounded by coeffRowBound.

theorem Cslib.Circuits.Rational.unary_decide_eq {α : Type} {encIn : α ↪ List Bool} {a b : α → ℕ} (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn Turing.MultiTapeTM.encUnary) (hb : Turing.MultiTapeTM.ComputableInPolyTime b encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => decide (a x = b x)) encIn Turing.MultiTapeTM.encBool

theorem Cslib.Circuits.Rational.computableInPolyTime_shiftAddRow {α : Type} {encIn : α ↪ List Bool} {c : α → ℤ} {l : α → List ℤ} (hc : Turing.MultiTapeTM.ComputableInPolyTime c encIn Turing.MultiTapeTM.encIntBin) (hl : Turing.MultiTapeTM.ComputableInPolyTime l encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => shiftAddRow (c x) (l x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

One shift-and-add step of the coefficient recurrence is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_coeffRow {α : Type} {encIn : α ↪ List Bool} {c : α → ℤ} {k : α → ℕ} (hc : Turing.MultiTapeTM.ComputableInPolyTime c encIn Turing.MultiTapeTM.encIntBin) (hk : Turing.MultiTapeTM.ComputableInPolyTime k encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => coeffRow (c x) (k x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Computing the coefficient row coeffRow c k is polynomial-time for a binary integer c and a unary degree k.

theorem Cslib.Circuits.Rational.computableInPolyTime_coeffRows {α : Type} {encIn : α ↪ List Bool} {c : α → ℤ} {M : α → ℕ} (hc : Turing.MultiTapeTM.ComputableInPolyTime c encIn Turing.MultiTapeTM.encIntBin) (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => coeffRows (c x) (M x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Computing the table of coefficient rows coeffRows c M is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_testTerm {α : Type} {encIn : α ↪ List Bool} {M u v q : α → ℕ} {minus plus : α → List (List ℤ)} {t : α → ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hminus : Turing.MultiTapeTM.ComputableInPolyTime minus encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hplus : Turing.MultiTapeTM.ComputableInPolyTime plus encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encIntBin) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn Turing.MultiTapeTM.encUnary) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn Turing.MultiTapeTM.encUnary) (hq : Turing.MultiTapeTM.ComputableInPolyTime q encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => testTerm (M x) (minus x) (plus x) (t x) (u x) (v x) (q x)) encIn Turing.MultiTapeTM.encIntBin

Computing one summand of a Taylor test matrix entry is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_testTerms {α : Type} {encIn : α ↪ List Bool} {M u v : α → ℕ} {minus plus : α → List (List ℤ)} {t : α → ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hminus : Turing.MultiTapeTM.ComputableInPolyTime minus encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hplus : Turing.MultiTapeTM.ComputableInPolyTime plus encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encIntBin) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn Turing.MultiTapeTM.encUnary) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => testTerms (M x) (minus x) (plus x) (t x) (u x) (v x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Computing the list of summands of a Taylor test matrix entry is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_testEntry {α : Type} {encIn : α ↪ List Bool} {M N u v : α → ℕ} {minus plus : α → List (List ℤ)} {t : α → ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hN : Turing.MultiTapeTM.ComputableInPolyTime N encIn Turing.MultiTapeTM.encUnary) (hminus : Turing.MultiTapeTM.ComputableInPolyTime minus encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hplus : Turing.MultiTapeTM.ComputableInPolyTime plus encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encIntBin) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn Turing.MultiTapeTM.encUnary) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => testEntry (M x) (N x) (minus x) (plus x) (t x) (u x) (v x)) encIn Turing.MultiTapeTM.encIntBin

Computing one entry of the integer Taylor test matrix is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_testRows {α : Type} {encIn : α ↪ List Bool} {M N : α → ℕ} {a t : α → ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hN : Turing.MultiTapeTM.ComputableInPolyTime N encIn Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn Turing.MultiTapeTM.encIntBin) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encIntBin) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => testRows (M x) (N x) (a x) (t x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Computing the integer Taylor test matrix testRows M N a t is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_signedCoeff {α : Type} {encIn : α ↪ List Bool} {Dg z i j : α → ℕ} (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (hz : Turing.MultiTapeTM.ComputableInPolyTime z encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => signedCoeff (Dg x) (z x) (i x) (j x)) encIn Turing.MultiTapeTM.encIntBin

Computing the signed cyclotomic regular-representation coefficient is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_liftTerm {α : Type} {encIn : α ↪ List Bool} {M Dg u v i j a k : α → ℕ} {T : α → List (List ℤ)} {p r : α → ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (hT : Turing.MultiTapeTM.ComputableInPolyTime T encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encIntBin) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encIntBin) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn Turing.MultiTapeTM.encUnary) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => liftTerm (M x) (Dg x) (T x) (p x) (r x) (u x) (v x) (i x) (j x) (a x) (k x)) encIn Turing.MultiTapeTM.encIntBin

Computing one summand of an integer lift entry is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_liftTerms {α : Type} {encIn : α ↪ List Bool} {M Dg u v i j a : α → ℕ} {T : α → List (List ℤ)} {p r : α → ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (hT : Turing.MultiTapeTM.ComputableInPolyTime T encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encIntBin) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encIntBin) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn Turing.MultiTapeTM.encUnary) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => liftTerms (M x) (Dg x) (T x) (p x) (r x) (u x) (v x) (i x) (j x) (a x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Computing the inner list of summands of an integer lift entry is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_liftSums {α : Type} {encIn : α ↪ List Bool} {M Dg u v i j : α → ℕ} {T : α → List (List ℤ)} {p r : α → ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (hT : Turing.MultiTapeTM.ComputableInPolyTime T encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encIntBin) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encIntBin) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn Turing.MultiTapeTM.encUnary) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => liftSums (M x) (Dg x) (T x) (p x) (r x) (u x) (v x) (i x) (j x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Computing the list of inner sums of an integer lift entry is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_liftEntry {α : Type} {encIn : α ↪ List Bool} {M Dg u v i j : α → ℕ} {T : α → List (List ℤ)} {p r : α → ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (hT : Turing.MultiTapeTM.ComputableInPolyTime T encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encIntBin) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encIntBin) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn Turing.MultiTapeTM.encUnary) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn Turing.MultiTapeTM.encUnary) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => liftEntry (M x) (Dg x) (T x) (p x) (r x) (u x) (v x) (i x) (j x)) encIn Turing.MultiTapeTM.encIntBin

Computing one entry of the integer lift matrix is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_liftTable {α : Type} {encIn : α ↪ List Bool} {M Dg : α → ℕ} {T : α → List (List ℤ)} {p r : α → ℤ} (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (hT : Turing.MultiTapeTM.ComputableInPolyTime T encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encIntBin) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encIntBin) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => liftTable (M x) (Dg x) (T x) (p x) (r x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Computing the integer lift matrix liftTable M Dg T p r is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_liftRows {α : Type} {encIn : α ↪ List Bool} {n N M Dg t p r : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hN : Turing.MultiTapeTM.ComputableInPolyTime N encIn Turing.MultiTapeTM.encUnary) (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encUnary) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => liftRows (n x) (N x) (M x) (Dg x) (t x) (p x) (r x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))

Computing all n + 1 integer lift tables liftRows n N M Dg t p r at a grid point is polynomial-time from unary parameters and coordinates.

theorem Cslib.Circuits.Rational.liftRows_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : ℕ × ℕ × ℕ × ℕ × ℕ × ℕ × ℕ) => liftRows q.1 q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2.1 q.2.2.2.2.2.1 q.2.2.2.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)))))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))

Standalone polynomial-time certificate for liftRows on a 7-tuple of unary naturals.