Documentation

Complexity.Computability.PolyTime.Int.Jet

Truncated univariate integer Taylor jet subtraction, congruences, and fold combinators #

Builds on Cslib.truncZJet, Cslib.polyAdd, and Cslib.mulZJet from Complexity/Computability/PolyTime/ParityFactorEval.lean to provide truncated length-J addition, subtraction, scalar subtraction, Polynomial.X ^ J divisibility congruences, foldl product invariants, encIntBin bit-length bounds, and a plain ComputableInPolyTime product-fold combinator in ℤ[z] / (z ^ J).

All operations (Cslib.IntJet.add, Cslib.IntJet.sub, Cslib.IntJet.subConst, together with Cslib.truncZJet and Cslib.mulZJet) are total on arbitrary List ℤ inputs: missing entries read as 0 via List.getD _ 0, entries at indices ≥ J are truncated modulo z ^ J, and every output has exact length J.

Main definitions and results #

Cslib.IntJet.add, Cslib.IntJet.sub, Cslib.IntJet.subConst: truncated length-J addition (via Cslib.truncZJet and Cslib.polyAdd) and subtraction on List ℤ.
Cslib.IntJet.X_pow_dvd_truncZJet, Cslib.IntJet.X_pow_dvd_add, Cslib.IntJet.X_pow_dvd_sub, Cslib.IntJet.X_pow_dvd_subConst, Cslib.IntJet.X_pow_dvd_mulZJet, Cslib.IntJet.X_pow_dvd_foldl_mulZJet: congruences modulo Polynomial.X ^ J over ℤ[X].
Cslib.IntJet.coeffNorm1_mulZJet_le, Cslib.IntJet.coeffNorm1_foldl_mulZJet_le, Cslib.IntJet.length_encIntBin_getD_le_coeffNorm1, Cslib.IntJet.computableInPolyTime_foldl_mulZJet: Polynomial.coeffNorm1, encIntBin, and plain Turing.MultiTapeTM.ComputableInPolyTime bounds and @[fun_prop] rules.

References #

OpenAI, The Exponential Time Hypothesis is False, Appendix B.1, B.4 (pp. 48–51).

def Cslib.IntJet.add (J : ℕ) (a b : List ℤ) :

Pointwise addition of two integer jets modulo z ^ J (exact length J), reusing Cslib.truncZJet and Cslib.polyAdd.

Instances For

def Cslib.IntJet.sub (J : ℕ) (a b : List ℤ) :

Pointwise subtraction of two integer jets, zero-padded via getD _ 0 to exact length J.

Instances For

def Cslib.IntJet.subConst (J : ℕ) (c : ℤ) (a : List ℤ) :

Subtract an integer jet a from a scalar constant c modulo z ^ J (exact length J).

Instances For

@[simp]

theorem Cslib.IntJet.length_add (J : ℕ) (a b : List ℤ) :

(add J a b).length = J

@[simp]

theorem Cslib.IntJet.length_sub (J : ℕ) (a b : List ℤ) :

(sub J a b).length = J

@[simp]

theorem Cslib.IntJet.length_subConst (J : ℕ) (c : ℤ) (a : List ℤ) :

(subConst J c a).length = J

theorem Cslib.IntJet.length_foldl_mulZJet {α : Type u_1} (J : ℕ) (stepJet : α → List ℤ) (l : List α) {acc : List ℤ} (hacc : acc.length = J) :

(List.foldl (fun (s : List ℤ) (x : α) => mulZJet J s (stepJet x)) acc l).length = J

Folding Cslib.mulZJet J preserves exact length J whenever acc.length = J.

theorem Cslib.IntJet.X_pow_dvd_truncZJet (J : ℕ) (a : List ℤ) :

Polynomial.X ^ J ∣ Polynomial.ofCoeffList (truncZJet J a) - Polynomial.ofCoeffList a

Cslib.truncZJet J a is congruent to Polynomial.ofCoeffList a modulo X ^ J.

theorem Cslib.IntJet.X_pow_dvd_truncZJet_singleton (J : ℕ) (c : ℤ) :

Polynomial.X ^ J ∣ Polynomial.ofCoeffList (truncZJet J [c]) - Polynomial.C c

Cslib.truncZJet J [c] is congruent to Polynomial.C c modulo X ^ J.

theorem Cslib.IntJet.X_pow_dvd_add (J : ℕ) (a b : List ℤ) :

Polynomial.X ^ J ∣ Polynomial.ofCoeffList (add J a b) - (Polynomial.ofCoeffList a + Polynomial.ofCoeffList b)

theorem Cslib.IntJet.X_pow_dvd_sub (J : ℕ) (a b : List ℤ) :

Polynomial.X ^ J ∣ Polynomial.ofCoeffList (sub J a b) - (Polynomial.ofCoeffList a - Polynomial.ofCoeffList b)

theorem Cslib.IntJet.X_pow_dvd_subConst (J : ℕ) (c : ℤ) (a : List ℤ) :

Polynomial.X ^ J ∣ Polynomial.ofCoeffList (subConst J c a) - (Polynomial.C c - Polynomial.ofCoeffList a)

theorem Cslib.IntJet.X_pow_dvd_mulZJet (J : ℕ) (a b : List ℤ) :

Polynomial.X ^ J ∣ Polynomial.ofCoeffList (mulZJet J a b) - Polynomial.ofCoeffList a * Polynomial.ofCoeffList b

Cslib.mulZJet J a b is congruent to ofCoeffList a * ofCoeffList b modulo X ^ J.

theorem Cslib.IntJet.X_pow_dvd_foldl_mulZJet {α : Type u_1} (J : ℕ) (l : List α) (stepJet : α → List ℤ) (stepPoly : α → Polynomial ℤ) (hstep : ∀ x ∈ l, Polynomial.X ^ J ∣ Polynomial.ofCoeffList (stepJet x) - stepPoly x) (acc : List ℤ) (accPoly : Polynomial ℤ) (hacc : Polynomial.X ^ J ∣ Polynomial.ofCoeffList acc - accPoly) :

Polynomial.X ^ J ∣ Polynomial.ofCoeffList (List.foldl (fun (s : List ℤ) (x : α) => mulZJet J s (stepJet x)) acc l) - accPoly * (List.map stepPoly l).prod

Folding Cslib.mulZJet J over l preserves congruence modulo X ^ J.

theorem Cslib.IntJet.natAbs_getD_le_coeffNorm1 (a : List ℤ) (k : ℕ) :

(a.getD k 0).natAbs ≤ (Polynomial.ofCoeffList a).coeffNorm1

theorem Cslib.IntJet.length_encIntBin_getD_le_coeffNorm1 (a : List ℤ) (k : ℕ) :

(Turing.MultiTapeTM.encIntBin (a.getD k 0)).length ≤ (Polynomial.ofCoeffList a).coeffNorm1.size + 1

Every entry a.getD k 0 has encIntBin bit-length at most coeffNorm1.size + 1.

theorem Cslib.IntJet.coeffNorm1_truncZJet_le (J : ℕ) (a : List ℤ) :

(Polynomial.ofCoeffList (truncZJet J a)).coeffNorm1 ≤ (Polynomial.ofCoeffList a).coeffNorm1

theorem Cslib.IntJet.coeffNorm1_truncZJet_singleton_le (J : ℕ) (c : ℤ) :

(Polynomial.ofCoeffList (truncZJet J [c])).coeffNorm1 ≤ c.natAbs

theorem Cslib.IntJet.coeffNorm1_add_le (J : ℕ) (a b : List ℤ) :

(Polynomial.ofCoeffList (add J a b)).coeffNorm1 ≤ (Polynomial.ofCoeffList a).coeffNorm1 + (Polynomial.ofCoeffList b).coeffNorm1

theorem Cslib.IntJet.coeffNorm1_sub_le (J : ℕ) (a b : List ℤ) :

(Polynomial.ofCoeffList (sub J a b)).coeffNorm1 ≤ (Polynomial.ofCoeffList a).coeffNorm1 + (Polynomial.ofCoeffList b).coeffNorm1

theorem Cslib.IntJet.coeffNorm1_subConst_le (J : ℕ) (c : ℤ) (a : List ℤ) :

(Polynomial.ofCoeffList (subConst J c a)).coeffNorm1 ≤ c.natAbs + (Polynomial.ofCoeffList a).coeffNorm1

theorem Cslib.IntJet.coeffNorm1_mulZJet_le (J : ℕ) (a b : List ℤ) :

(Polynomial.ofCoeffList (mulZJet J a b)).coeffNorm1 ≤ (Polynomial.ofCoeffList a).coeffNorm1 * (Polynomial.ofCoeffList b).coeffNorm1

Submultiplicativity of Polynomial.coeffNorm1 under Cslib.mulZJet J.

theorem Cslib.IntJet.coeffNorm1_foldl_mulZJet_le {α : Type u_1} (J : ℕ) (l : List α) (stepJet : α → List ℤ) (bound : α → ℕ) (hstep : ∀ x ∈ l, (Polynomial.ofCoeffList (stepJet x)).coeffNorm1 ≤ bound x) (acc : List ℤ) :

(Polynomial.ofCoeffList (List.foldl (fun (s : List ℤ) (x : α) => mulZJet J s (stepJet x)) acc l)).coeffNorm1 ≤ (Polynomial.ofCoeffList acc).coeffNorm1 * (List.map bound l).prod

Submultiplicative Polynomial.coeffNorm1 bound across foldl of Cslib.mulZJet J.

theorem Cslib.IntJet.size_coeffNorm1_le_length_encList (a : List ℤ) :

(Polynomial.ofCoeffList a).coeffNorm1.size ≤ 2 * ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) a).length

Bit-size of (ofCoeffList a).coeffNorm1 is bounded linearly in (encList encIntBin a).length.

theorem Cslib.IntJet.length_encList_encIntBin_le_of_coeffNorm1 (a : List ℤ) :

((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) a).length ≤ a.length * (2 * (Polynomial.ofCoeffList a).coeffNorm1.size + 3)

Encoded length of a : List ℤ is bounded by a.length * (2 * coeffNorm1.size + 3).

theorem Cslib.IntJet.computableInPolyTime_add' {γ : Type} {encIn : γ ↪ List Bool} {J : γ → ℕ} {a b : γ → List ℤ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hb : Turing.MultiTapeTM.ComputableInPolyTime b encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => add (J x) (a x) (b x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

theorem Cslib.IntJet.computableInPolyTime_sub' {γ : Type} {encIn : γ ↪ List Bool} {J : γ → ℕ} {a b : γ → List ℤ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hb : Turing.MultiTapeTM.ComputableInPolyTime b encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => sub (J x) (a x) (b x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

theorem Cslib.IntJet.computableInPolyTime_subConst' {γ : Type} {encIn : γ ↪ List Bool} {J : γ → ℕ} {c : γ → ℤ} {a : γ → List ℤ} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hc : Turing.MultiTapeTM.ComputableInPolyTime c encIn Turing.MultiTapeTM.encIntBin) (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => subConst (J x) (c x) (a x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

theorem Cslib.IntJet.computableInPolyTime_subConst :

Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℤ) × List ℤ) => subConst p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encIntBin) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

theorem Cslib.IntJet.computableInPolyTime_foldl_mulZJet {γ α : Type} {encIn : γ ↪ List Bool} (encA : α ↪ List Bool) {J : γ → ℕ} {δ : γ → ℤ} {xs : γ → List α} (factor : ℕ → ℤ → α → List ℤ) (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hδ : Turing.MultiTapeTM.ComputableInPolyTime δ encIn Turing.MultiTapeTM.encIntBin) (hxs : Turing.MultiTapeTM.ComputableInPolyTime xs encIn (Turing.MultiTapeTM.encList encA)) (hfac : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : ((ℕ × ℤ) × List ℤ) × α) => factor q.1.1.1 q.1.1.2 q.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encIntBin) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) encA) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) {K : γ → ℕ} (hK : Turing.MultiTapeTM.PolyBounded (fun (x : γ) => (encIn x).length) K) (hsz : ∀ (x : γ), ∀ a ∈ xs x, (Polynomial.ofCoeffList (factor (J x) (δ x) a)).coeffNorm1.size ≤ K x) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => List.foldl (fun (acc : List ℤ) (a : α) => mulZJet (J x) acc (factor (J x) (δ x) a)) (truncZJet (J x) [1]) (xs x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Plain polynomial-time combinator for folding Cslib.mulZJet over xs from Cslib.truncZJet J [1], given a polynomial bound K on the bit-sizes of the step factors' ℓ₁ norms.