From 99d9e0d69372a439fe89c955398c74361686e888 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:28:05 -0400 Subject: [PATCH 1/4] feat(PolyTime): arithmetic in (Z/2^p)[U]/(f) on coefficient lists Addition, multiplication by U and shift-and-add multiplication modulo 2^p and a monic f given by its lower coefficients, proved correct in AdjoinRoot (f mod 2^p) and certified polynomial-time with p in unary and coordinates in binary. These are the polynomial-time arithmetic claims of [OpenAI2026ETH, Appendix D.4.1] for addition and multiplication (l = 1). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../PolyTime/GaloisRingArithmetic.lean | 446 ++++++++++++++++++ ComplexityTests/GaloisRingArithmetic.lean | 59 +++ 3 files changed, 506 insertions(+) create mode 100644 Complexity/Computability/PolyTime/GaloisRingArithmetic.lean create mode 100644 ComplexityTests/GaloisRingArithmetic.lean diff --git a/Complexity.lean b/Complexity.lean index fdd3b220c..566b83dcb 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1985,6 +1985,7 @@ public import Complexity.Computability.PolyTime.CNF.SparsePolyCompile public import Complexity.Computability.PolyTime.CSP.ToCNF public import Complexity.Computability.PolyTime.CommonCountingAccum public import Complexity.Computability.PolyTime.FineGrained.ParameterCheck +public import Complexity.Computability.PolyTime.GaloisRingArithmetic public import Complexity.Computability.PolyTime.GreedyLabelSchedule public import Complexity.Computability.PolyTime.GreedySlotScore public import Complexity.Computability.PolyTime.Int.ExactDiv diff --git a/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean new file mode 100644 index 000000000..b46df6766 --- /dev/null +++ b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean @@ -0,0 +1,446 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Data.ZMod.Basic +public import Mathlib.RingTheory.AdjoinRoot +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Fold +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryDivision +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeLoops +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Data.List.GetD +import Mathlib.Data.Nat.Size + +/-! +# Arithmetic modulo `2 ^ p` and a monic polynomial, on coefficient lists + +The coefficient rings of the contraction algorithm of [OpenAI2026ETH] (Appendix D.4.1, p. 57) are +`A_p = (ℤ / 2 ^ p)[U] / (f)` for a monic `f ∈ ℤ[U]` of degree `e`. An element is represented in the +basis `1, U, …, U ^ (e - 1)` by its list of coordinates, each an integer residue modulo `2 ^ p`. +The monic polynomial is given by the list `fl` of its coefficients below the leading one +(`GaloisRingArith.monicOf`), so `e` is the length of `fl`. With `f` irreducible modulo `2`, `A_p` is +the Galois ring `(ℤ / 2 ^ p)[U] / (f)`; nothing here needs irreducibility. + +The value of a coefficient list `c` is `∑ i < e, c i U ^ i` in `A_p` (`GaloisRingArith.val`). + +* **Addition** (`GaloisRingArith.add`) adds coordinates modulo `2 ^ p`. +* **Multiplication by `U`** (`GaloisRingArith.mulX`) shifts the coordinates up and subtracts the top + coordinate times `f`, reducing `U ^ e = -∑ i < e, fl i U ^ i`. +* **Multiplication** (`GaloisRingArith.mul`) is shift-and-add: `c d = ∑ i < e, c i (U ^ i d)`, + accumulating `c i` times the current `U ^ i d` and multiplying it by `U`, `e` times. + +Each operation is correct (`GaloisRingArith.val_add`, `GaloisRingArith.val_mulX`, +`GaloisRingArith.val_mul`) and polynomial-time, with the precision `p` in unary and the +coordinates and the coefficients of `f` in binary (`GaloisRingArith.computableInPolyTime_add`, +`GaloisRingArith.computableInPolyTime_mul`). Their outputs are reduced, with `e` coordinates below +`2 ^ p` (`GaloisRingArith.length_mul`, `GaloisRingArith.lt_of_mem_mul`). These are the +polynomial-time arithmetic claims of Appendix D.4.1 for addition and multiplication, in the case +`ℓ = 1` of the source, where `A = O` has no `V`-coordinates. Inversion of units, which the source +does by Newton lifting, is not covered here. + +## Main definitions + +* `Cslib.GaloisRingArith.monicOf`: the monic polynomial with given lower coefficients. +* `Cslib.GaloisRingArith.val`: the value of a coefficient list. +* `Cslib.GaloisRingArith.add`, `Cslib.GaloisRingArith.mulX`, `Cslib.GaloisRingArith.mul`: addition, + multiplication by `U` and multiplication. + +## Main results + +* `Cslib.GaloisRingArith.val_add`, `Cslib.GaloisRingArith.val_mulX`, + `Cslib.GaloisRingArith.val_mul`: correctness. +* `Cslib.GaloisRingArith.computableInPolyTime_add`, + `Cslib.GaloisRingArith.computableInPolyTime_mulX`, + `Cslib.GaloisRingArith.computableInPolyTime_mul`: polynomial time. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.4.1 (p. 57). +-/ + +@[expose] public section + +namespace Cslib.GaloisRingArith + +open Polynomial Finset + +/-- The monic polynomial `U ^ e + ∑ i < e, fl i U ^ i` of degree `e = fl.length`. -/ +noncomputable def monicOf (fl : List ℕ) : ℤ[X] := + X ^ fl.length + ∑ i ∈ range fl.length, C (fl.getD i 0 : ℤ) * X ^ i + +/-- `monicOf fl` is monic, of degree `fl.length`. -/ +theorem monic_monicOf (fl : List ℕ) : (monicOf fl).Monic := by + unfold monicOf + apply monic_X_pow_add + refine (degree_sum_le _ _).trans_lt ?_ + rw [Finset.sup_lt_iff (WithBot.bot_lt_coe _)] + intro i hi + exact (degree_C_mul_X_pow_le _ _).trans_lt (WithBot.coe_lt_coe.mpr (mem_range.mp hi)) + +/-- The ring `A_p = (ℤ / 2 ^ p)[U] / (f)` for `f = monicOf fl`. -/ +abbrev Ring (p : ℕ) (fl : List ℕ) : Type := + AdjoinRoot ((monicOf fl).map (Int.castRingHom (ZMod (2 ^ p)))) + +/-- The value `∑ i < e, c i U ^ i` of a coefficient list in `A_p`, with `e = fl.length`. +Coordinates past `e` are ignored and missing ones are zero. -/ +noncomputable def val (p : ℕ) (fl c : List ℕ) : Ring p fl := + ∑ i ∈ range fl.length, ((c.getD i 0 : ℕ) : Ring p fl) * AdjoinRoot.root _ ^ i + +/-- Coordinatewise sum modulo `2 ^ p`. -/ +def add (p : ℕ) (fl c d : List ℕ) : List ℕ := + (List.range fl.length).map fun i => (c.getD i 0 + d.getD i 0) % 2 ^ p + +/-- Add `k` times `d` to `c`, coordinatewise modulo `2 ^ p`. -/ +def addSmul (p : ℕ) (fl c : List ℕ) (k : ℕ) (d : List ℕ) : List ℕ := + (List.range fl.length).map fun i => (c.getD i 0 + k * d.getD i 0) % 2 ^ p + +/-- Multiplication by `U`: shift the coordinates up and subtract the top coordinate times the +lower coefficients of `f`, modulo `2 ^ p`. -/ +def mulX (p : ℕ) (fl c : List ℕ) : List ℕ := + (List.range fl.length).map fun i => + ((0 :: c).getD i 0 + (2 ^ p - c.getD (fl.length - 1) 0 * fl.getD i 0 % 2 ^ p)) % 2 ^ p + +/-- The zero element, with `e` coordinates. -/ +def zero (fl : List ℕ) : List ℕ := (List.range fl.length).map fun _ => 0 + +/-- One step of shift-and-add multiplication by `c`: from `(U ^ i d, ∑ j < i, c j U ^ j d)`, +add `c i U ^ i d` to the accumulator and multiply the current power by `U`. -/ +def mulStep (p : ℕ) (fl c : List ℕ) (s : List ℕ × List ℕ) (i : ℕ) : List ℕ × List ℕ := + (mulX p fl s.1, addSmul p fl s.2 (c.getD i 0) s.1) + +/-- **Multiplication** by shift-and-add. -/ +def mul (p : ℕ) (fl c d : List ℕ) : List ℕ := + ((List.range fl.length).foldl (mulStep p fl c) (d, zero fl)).2 + +/-! ### Correctness -/ + +section Correctness + +variable {p : ℕ} {fl : List ℕ} + +theorem natCast_two_pow : ((2 ^ p : ℕ) : Ring p fl) = 0 := by + rw [← map_natCast (algebraMap (ZMod (2 ^ p)) (Ring p fl)), ZMod.natCast_self, map_zero] + +theorem natCast_mod_two_pow (x : ℕ) : ((x % 2 ^ p : ℕ) : Ring p fl) = (x : Ring p fl) := by + conv_rhs => rw [← Nat.mod_add_div x (2 ^ p)] + rw [Nat.cast_add, Nat.cast_mul, natCast_two_pow, zero_mul, add_zero] + +/-- The root satisfies `U ^ e = -∑ i < e, fl i U ^ i`. -/ +theorem root_pow_length : + (AdjoinRoot.root _ : Ring p fl) ^ fl.length = + -∑ i ∈ range fl.length, ((fl.getD i 0 : ℕ) : Ring p fl) * AdjoinRoot.root _ ^ i := by + have hmap : (monicOf fl).map (Int.castRingHom (ZMod (2 ^ p))) = X ^ fl.length + + ∑ i ∈ range fl.length, C ((fl.getD i 0 : ℕ) : ZMod (2 ^ p)) * X ^ i := by + simp [monicOf, Polynomial.map_sum] + have h := AdjoinRoot.eval₂_root ((monicOf fl).map (Int.castRingHom (ZMod (2 ^ p)))) + conv at h => lhs; arg 3; rw [hmap] + simp only [eval₂_add, eval₂_finsetSum, eval₂_mul, eval₂_natCast, eval₂_X_pow, + map_natCast] at h + exact eq_neg_of_add_eq_zero_left h + +@[simp] theorem val_zero : val p fl (zero fl) = 0 := by + refine sum_eq_zero fun i hi => ?_ + rw [zero, List.getD_eq_getElem _ _ (by simpa using hi)] + simp + +/-- **Addition is correct.** -/ +theorem val_add (c d : List ℕ) : val p fl (add p fl c d) = val p fl c + val p fl d := by + rw [val, val, val, ← sum_add_distrib] + refine sum_congr rfl fun i hi => ?_ + rw [add, List.getD_eq_getElem _ _ (by simpa using hi)] + simp only [List.getElem_map, List.getElem_range, natCast_mod_two_pow, Nat.cast_add, add_mul] + +/-- **Adding a multiple is correct.** -/ +theorem val_addSmul (c : List ℕ) (k : ℕ) (d : List ℕ) : + val p fl (addSmul p fl c k d) = val p fl c + (k : Ring p fl) * val p fl d := by + rw [val, val, val, mul_sum, ← sum_add_distrib] + refine sum_congr rfl fun i hi => ?_ + rw [addSmul, List.getD_eq_getElem _ _ (by simpa using hi)] + simp only [List.getElem_map, List.getElem_range, natCast_mod_two_pow, Nat.cast_add, + Nat.cast_mul] + ring + +/-- Shifting coordinates and subtracting the top one times the lower coefficients of `f` is +multiplication by a root of `f`, in any commutative ring. -/ +private theorem shift_sub_mul_sum {R : Type*} [CommRing R] (r : R) (cs fs : ℕ → R) (e : ℕ) + (hroot : r ^ (e + 1) = -∑ i ∈ range (e + 1), fs i * r ^ i) : + ∑ i ∈ range (e + 1), ((if i = 0 then 0 else cs (i - 1)) - cs e * fs i) * r ^ i = + r * ∑ i ∈ range (e + 1), cs i * r ^ i := by + simp only [sub_mul, sum_sub_distrib] + rw [sum_range_succ' (fun i => (if i = 0 then 0 else cs (i - 1)) * r ^ i)] + simp only [Nat.add_sub_cancel, Nat.succ_ne_zero, ite_false, ite_true, zero_mul, add_zero] + rw [mul_sum, sum_range_succ (fun i => r * (cs i * r ^ i)), + show r * (cs e * r ^ e) = cs e * r ^ (e + 1) by ring, hroot, mul_neg, mul_sum, + ← sub_eq_add_neg] + congr 1 + · exact sum_congr rfl fun i _ => by ring + · exact sum_congr rfl fun i _ => by ring + +/-- **Multiplication by `U` is correct.** -/ +theorem val_mulX (c : List ℕ) : + val p fl (mulX p fl c) = AdjoinRoot.root _ * val p fl c := by + -- Each coordinate is the shifted coordinate minus the top coordinate times `fl i`. + have hcoord (i : ℕ) (hi : i < fl.length) : (((mulX p fl c).getD i 0 : ℕ) : Ring p fl) = + (if i = 0 then 0 else (c.getD (i - 1) 0 : Ring p fl)) - + (c.getD (fl.length - 1) 0 : Ring p fl) * (fl.getD i 0 : Ring p fl) := by + rw [mulX, List.getD_eq_getElem _ _ (by simpa using hi)] + simp only [List.getElem_map, List.getElem_range, natCast_mod_two_pow, Nat.cast_add] + rw [Nat.cast_sub (Nat.mod_lt _ (Nat.two_pow_pos p)).le, natCast_two_pow, natCast_mod_two_pow, + Nat.cast_mul] + rcases i with _ | i <;> simp [sub_eq_add_neg] + rcases Nat.eq_zero_or_pos fl.length with he | he + · simp [val, he] + obtain ⟨e, he'⟩ := Nat.exists_eq_add_of_lt he + rw [Nat.zero_add] at he' + have hroot := root_pow_length (p := p) (fl := fl) + rw [val, val, sum_congr rfl fun i hi => by rw [hcoord i (mem_range.mp hi)]] + rw [he', Nat.add_sub_cancel] at * + exact shift_sub_mul_sum _ (fun i => (c.getD i 0 : Ring p fl)) (fun i => (fl.getD i 0 : Ring p fl)) + e hroot + +/-- **Multiplication is correct.** -/ +theorem val_mul (c d : List ℕ) : val p fl (mul p fl c d) = val p fl c * val p fl d := by + -- After `j` steps the state is `(U ^ j d, ∑ i < j, c i U ^ i d)`. + have hinv (j : ℕ) : + val p fl ((List.range j).foldl (mulStep p fl c) (d, zero fl)).1 = + AdjoinRoot.root _ ^ j * val p fl d ∧ + val p fl ((List.range j).foldl (mulStep p fl c) (d, zero fl)).2 = + (∑ i ∈ range j, ((c.getD i 0 : ℕ) : Ring p fl) * AdjoinRoot.root _ ^ i) * val p fl d := by + induction j with + | zero => simp + | succ j ih => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, mulStep] + refine ⟨?_, ?_⟩ + · rw [val_mulX, ih.1, pow_succ]; ring + · rw [val_addSmul, ih.1, ih.2, sum_range_succ]; ring + rw [mul, (hinv fl.length).2] + rfl + +end Correctness + +/-! ### Reduced outputs -/ + +@[simp] theorem length_add (p : ℕ) (fl c d : List ℕ) : (add p fl c d).length = fl.length := by + simp [add] + +@[simp] theorem length_addSmul (p : ℕ) (fl c : List ℕ) (k : ℕ) (d : List ℕ) : + (addSmul p fl c k d).length = fl.length := by + simp [addSmul] + +@[simp] theorem length_mulX (p : ℕ) (fl c : List ℕ) : (mulX p fl c).length = fl.length := by + simp [mulX] + +@[simp] theorem length_zero (fl : List ℕ) : (zero fl).length = fl.length := by simp [zero] + +theorem lt_of_mem_add {p : ℕ} {fl c d : List ℕ} {x : ℕ} (hx : x ∈ add p fl c d) : x < 2 ^ p := by + obtain ⟨i, -, rfl⟩ := List.mem_map.mp hx + exact Nat.mod_lt _ (Nat.two_pow_pos p) + +theorem lt_of_mem_addSmul {p : ℕ} {fl c : List ℕ} {k : ℕ} {d : List ℕ} {x : ℕ} + (hx : x ∈ addSmul p fl c k d) : x < 2 ^ p := by + obtain ⟨i, -, rfl⟩ := List.mem_map.mp hx + exact Nat.mod_lt _ (Nat.two_pow_pos p) + +theorem lt_of_mem_mulX {p : ℕ} {fl c : List ℕ} {x : ℕ} (hx : x ∈ mulX p fl c) : x < 2 ^ p := by + obtain ⟨i, -, rfl⟩ := List.mem_map.mp hx + exact Nat.mod_lt _ (Nat.two_pow_pos p) + +theorem length_mul (p : ℕ) (fl c d : List ℕ) : (mul p fl c d).length = fl.length := by + rcases Nat.eq_zero_or_pos fl.length with he | he + · simp [mul, he, zero] + obtain ⟨e, he'⟩ := Nat.exists_eq_add_of_lt he + rw [mul, Nat.zero_add] at * + rw [he', List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, mulStep, + length_addSmul, he'] + +theorem lt_of_mem_mul {p : ℕ} {fl c d : List ℕ} {x : ℕ} (hx : x ∈ mul p fl c d) : x < 2 ^ p := by + rcases Nat.eq_zero_or_pos fl.length with he | he + · simp [mul, he, zero] at hx + obtain ⟨e, he'⟩ := Nat.exists_eq_add_of_lt he + rw [Nat.zero_add] at he' + rw [mul, he', List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, + mulStep] at hx + exact lt_of_mem_addSmul hx + +/-! ### Polynomial time -/ + +section PolyTime + +open Turing.MultiTapeTM + +variable {α : Type} {encIn : α ↪ List Bool} + +/-- Reduction modulo `2 ^ p`, with `p` in unary. -/ +@[fun_prop] +theorem computableInPolyTime_mod_two_pow {x p : α → ℕ} + (hx : ComputableInPolyTime x encIn encNat) (hp : ComputableInPolyTime p encIn encUnary) : + ComputableInPolyTime (fun a => x a % 2 ^ p a) encIn encNat := + ComputableInPolyTime.binary_mod.comp (hx.prod (ComputableInPolyTime.binary_two_pow.comp hp)) + +/-- A coordinate, at a unary index. -/ +theorem computableInPolyTime_getD {c : α → List ℕ} {i : α → ℕ} + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hi : ComputableInPolyTime i encIn encUnary) : + ComputableInPolyTime (fun a => (c a).getD (i a) 0) encIn encNat := + (ComputableInPolyTime.listGetD (encA := encNat) 0).comp (hc.prod hi) + +/-- Tabulating `e` coordinates, for a unary `e`. -/ +theorem computableInPolyTime_tabulate {n : α → ℕ} {g : α → ℕ → ℕ} + (hn : ComputableInPolyTime n encIn encUnary) + (hg : ComputableInPolyTime (fun q : α × ℕ => g q.1 q.2) (encPair encIn encUnary) encNat) : + ComputableInPolyTime (fun x => (List.range (n x)).map (g x)) encIn (encList encNat) := + ComputableInPolyTime.mapWithInput (ComputableInPolyTime.range.comp hn) hg + +private theorem length_polyTime {fl : α → List ℕ} + (hfl : ComputableInPolyTime fl encIn (encList encNat)) : + ComputableInPolyTime (fun x => (fl x).length) encIn encUnary := + (ComputableInPolyTime.length_list encNat).comp hfl + +/-- **Addition is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_add {p : α → ℕ} {fl c d : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hd : ComputableInPolyTime d encIn (encList encNat)) : + ComputableInPolyTime (fun x => add (p x) (fl x) (c x) (d x)) encIn (encList encNat) := by + have h1 := ComputableInPolyTime.fst encIn encUnary + have h2 := ComputableInPolyTime.snd encIn encUnary + exact computableInPolyTime_tabulate (length_polyTime hfl) + (computableInPolyTime_mod_two_pow (ComputableInPolyTime.binary_add.comp + ((computableInPolyTime_getD (hc.comp h1) h2).prod + (computableInPolyTime_getD (hd.comp h1) h2))) (hp.comp h1)) + +/-- **Adding a multiple is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_addSmul {p k : α → ℕ} {fl c d : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hk : ComputableInPolyTime k encIn encNat) + (hd : ComputableInPolyTime d encIn (encList encNat)) : + ComputableInPolyTime (fun x => addSmul (p x) (fl x) (c x) (k x) (d x)) encIn + (encList encNat) := by + have h1 := ComputableInPolyTime.fst encIn encUnary + have h2 := ComputableInPolyTime.snd encIn encUnary + exact computableInPolyTime_tabulate (length_polyTime hfl) + (computableInPolyTime_mod_two_pow (ComputableInPolyTime.binary_add.comp + ((computableInPolyTime_getD (hc.comp h1) h2).prod + (ComputableInPolyTime.binary_mul' (hk.comp h1) + (computableInPolyTime_getD (hd.comp h1) h2)))) (hp.comp h1)) + +/-- **Multiplication by `U` is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_mulX {p : α → ℕ} {fl c : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) : + ComputableInPolyTime (fun x => mulX (p x) (fl x) (c x)) encIn (encList encNat) := by + have h1 := ComputableInPolyTime.fst encIn encUnary + have h2 := ComputableInPolyTime.snd encIn encUnary + have hshift := computableInPolyTime_getD + (ComputableInPolyTime.cons' (ComputableInPolyTime.const 0) (hc.comp h1)) h2 + have htop := computableInPolyTime_getD (hc.comp h1) + (ComputableInPolyTime.unary_sub' (length_polyTime (hfl.comp h1)) + (ComputableInPolyTime.const 1)) + have hsub := computableInPolyTime_mod_two_pow + (ComputableInPolyTime.binary_mul' htop (computableInPolyTime_getD (hfl.comp h1) h2)) + (hp.comp h1) + exact computableInPolyTime_tabulate (length_polyTime hfl) + (computableInPolyTime_mod_two_pow (ComputableInPolyTime.binary_add.comp (hshift.prod + (ComputableInPolyTime.binary_sub' (ComputableInPolyTime.binary_two_pow.comp (hp.comp h1)) + hsub))) (hp.comp h1)) + +/-- A reduced coefficient list, with `e` coordinates below `2 ^ p`, is at most +`e (2 p + 1)` long in binary. -/ +theorem length_encList_le {p e : ℕ} {c : List ℕ} (hlen : c.length = e) + (hlt : ∀ x ∈ c, x < 2 ^ p) : (encList encNat c).length ≤ e * (2 * p + 1) := by + rw [length_encList] + calc (c.map fun x => 2 * (encNat x).length + 1).sum + ≤ (c.map fun x => 2 * (encNat x).length + 1).length • (2 * p + 1) := + List.sum_le_length_nsmul _ _ fun n hn => by + obtain ⟨x, hx, rfl⟩ := List.mem_map.mp hn + have : (encNat x).length ≤ p := by + change x.bits.length ≤ p + rw [Nat.size_eq_bits_len] at * + exact (Nat.size_eq_bits_len x ▸ Nat.size_le.mpr (hlt x hx)) + omega + _ = e * (2 * p + 1) := by rw [List.length_map, hlen, smul_eq_mul] + +/-- **Multiplication is polynomial-time**, with the precision in unary. Every intermediate pair is +reduced after its first step, so its length is bounded by the precision and the degree. -/ +@[fun_prop] +theorem computableInPolyTime_mul {p : α → ℕ} {fl c d : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hd : ComputableInPolyTime d encIn (encList encNat)) : + ComputableInPolyTime (fun x => mul (p x) (fl x) (c x) (d x)) encIn (encList encNat) := by + let encS := encPair (encList encNat) (encList encNat) + have hinit : ComputableInPolyTime (fun x => (d x, zero (fl x))) encIn encS := + hd.prod (computableInPolyTime_tabulate (g := fun _ _ => 0) (length_polyTime hfl) + (ComputableInPolyTime.const 0)) + have hrange : ComputableInPolyTime (fun x => List.range (fl x).length) encIn + (encList encUnary) := + ComputableInPolyTime.range.comp (length_polyTime hfl) + -- The step, on the input, the state and the unary index. + have hstep : ComputableInPolyTime + (fun q : (α × (List ℕ × List ℕ)) × ℕ => mulStep (p q.1.1) (fl q.1.1) (c q.1.1) q.1.2 q.2) + (encPair (encPair encIn encS) encUnary) encS := by + have hq := ComputableInPolyTime.fst (encPair encIn encS) encUnary + have hx := (ComputableInPolyTime.fst encIn encS).comp hq + have hs := (ComputableInPolyTime.snd encIn encS).comp hq + have hi := ComputableInPolyTime.snd (encPair encIn encS) encUnary + have hcur := (ComputableInPolyTime.fst (encList encNat) (encList encNat)).comp hs + have hacc := (ComputableInPolyTime.snd (encList encNat) (encList encNat)).comp hs + exact (computableInPolyTime_mulX (hp.comp hx) (hfl.comp hx) hcur).prod + (computableInPolyTime_addSmul (hp.comp hx) (hfl.comp hx) hacc + (computableInPolyTime_getD (hc.comp hx) hi) hcur) + -- Every step's output is reduced, hence of bounded length. + have hgrowth : PolyBounded (fun x => (encIn x).length) + (fun x => 3 * ((fl x).length * (2 * p x + 1)) + 1) := by + have hpl := (ComputableInPolyTime.polyBounded_length hp) + have hfll := (ComputableInPolyTime.polyBounded_length hfl) + refine (((PolyBounded.const 3).mul (hfll.mul (((PolyBounded.const 2).mul hpl).add + (PolyBounded.const 1)))).add (PolyBounded.const 1)).mono fun x => ?_ + have h1 : p x ≤ (encUnary (p x)).length := by simp + have h2 : (fl x).length ≤ (encList encNat (fl x)).length := by + rw [length_encList] + calc (fl x).length = ((fl x).map fun _ => 1).sum := by simp + _ ≤ ((fl x).map fun a => 2 * (encNat a).length + 1).sum := + List.sum_le_sum fun a _ => by omega + have := Nat.mul_le_mul h2 (Nat.add_le_add_right (Nat.mul_le_mul_left 2 h1) 1) + omega + have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encUnary) (encL := encList encUnary) + (step := fun x s i => mulStep (p x) (fl x) (c x) s i) hinit + ⟨hrange, hstep, inferInstance, inferInstance⟩ ⟨hgrowth, fun x s i _ => ?_⟩ + · exact (ComputableInPolyTime.snd (encList encNat) (encList encNat)).comp hfold + · have hcur := length_encList_le (length_mulX (p x) (fl x) s.1) fun _ h => lt_of_mem_mulX h + have hacc := length_encList_le (length_addSmul (p x) (fl x) s.2 ((c x).getD i 0) s.1) + fun _ h => lt_of_mem_addSmul h + simp only [mulStep, encS, length_encPair] + omega + +end PolyTime + +end Cslib.GaloisRingArith diff --git a/ComplexityTests/GaloisRingArithmetic.lean b/ComplexityTests/GaloisRingArithmetic.lean new file mode 100644 index 000000000..566fca586 --- /dev/null +++ b/ComplexityTests/GaloisRingArithmetic.lean @@ -0,0 +1,59 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.PolyTime.GaloisRingArithmetic + +/-! # Arithmetic in `(ℤ / 2 ^ p)[U] / (f)` on coefficient lists + +Concrete products in the Galois ring `(ℤ / 8)[U] / (U ^ 2 + U + 1)` (`p = 3`, `fl = [1, 1]`), the +correctness statements, and the polynomial-time certificates in closed form, with the precision +in unary and the coordinates in binary. -/ + +namespace ComplexityTests.GaloisRingArithmetic + +open Cslib.GaloisRingArith Turing.MultiTapeTM + +-- `U * U = U ^ 2 = -1 - U`, that is `7 + 7 U` modulo `8`. +example : mulX 3 [1, 1] [0, 1] = [7, 7] := by decide + +-- `(1 + 2 U) (3 + U) = 3 + 7 U + 2 U ^ 2 = 1 + 5 U` modulo `8` and `U ^ 2 + U + 1`. +example : mul 3 [1, 1] [1, 2] [3, 1] = [1, 5] := by decide + +-- Addition reduces each coordinate: `(7 + 5 U) + (3 + 6 U) = 2 + 3 U` modulo `8`. +example : add 3 [1, 1] [7, 5] [3, 6] = [2, 3] := by decide + +-- `U` has order `3` here: `U ^ 3 = 1`. +example : mul 3 [1, 1] [0, 1] (mul 3 [1, 1] [0, 1] [0, 1]) = [1, 0] := by decide + +-- Unreduced inputs are reduced: missing coordinates are zero, extra ones ignored. +example : mul 3 [1, 1] [9] [3, 1, 4] = [3, 1] := by decide + +-- Degree three, `f = U ^ 3 + U + 1`, modulo `16`: `U ^ 2 * U = U ^ 3 = -1 - U`. +example : mulX 4 [1, 1, 0] [0, 0, 1] = [15, 15, 0] := by decide + +/-- The defining polynomial is monic. -/ +example : (monicOf [1, 1]).Monic := monic_monicOf _ + +/-- Multiplication is correct in the ring itself. -/ +example (c d : List ℕ) : val 3 [1, 1] (mul 3 [1, 1] c d) = val 3 [1, 1] c * val 3 [1, 1] d := + val_mul c d + +/-- **Multiplication in polynomial time**, on the ring description `(p, fl)` with `p` in unary +and the two coefficient lists in binary. -/ +example : ComputableInPolyTime + (fun q : (ℕ × List ℕ) × (List ℕ × List ℕ) => mul q.1.1 q.1.2 q.2.1 q.2.2) + (encPair (encPair encUnary (encList encNat)) (encPair (encList encNat) (encList encNat))) + (encList encNat) := by + fun_prop + +/-- **Addition in polynomial time**, in the same encoding. -/ +example : ComputableInPolyTime + (fun q : (ℕ × List ℕ) × (List ℕ × List ℕ) => add q.1.1 q.1.2 q.2.1 q.2.2) + (encPair (encPair encUnary (encList encNat)) (encPair (encList encNat) (encList encNat))) + (encList encNat) := by + fun_prop + +end ComplexityTests.GaloisRingArithmetic From b9caee50441cd14c22ce4d3f0285c1f20bed8e32 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:36:29 -0400 Subject: [PATCH 2/4] feat(PolyTime): unit and powers in (Z/2^p)[U]/(f) Powers c^k by k multiplications, with k in unary (the mode exponents of [OpenAI2026ETH, Appendix D.4.6] are below the precision). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../PolyTime/GaloisRingArithmetic.lean | 93 ++++++++++++++++++- ComplexityTests/GaloisRingArithmetic.lean | 17 ++++ 2 files changed, 106 insertions(+), 4 deletions(-) diff --git a/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean index b46df6766..8a9bfcd2a 100644 --- a/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean +++ b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean @@ -47,6 +47,9 @@ The value of a coefficient list `c` is `∑ i < e, c i U ^ i` in `A_p` (`GaloisR coordinate times `f`, reducing `U ^ e = -∑ i < e, fl i U ^ i`. * **Multiplication** (`GaloisRingArith.mul`) is shift-and-add: `c d = ∑ i < e, c i (U ^ i d)`, accumulating `c i` times the current `U ^ i d` and multiplying it by `U`, `e` times. +* **Powers** (`GaloisRingArith.pow`) `c ^ k` take `k` multiplications from `GaloisRingArith.one`, + with `k` in unary. In the source the exponents of the mode substitutions are below the + precision (Appendix D.4.6, p. 63), so they are polynomial. Each operation is correct (`GaloisRingArith.val_add`, `GaloisRingArith.val_mulX`, `GaloisRingArith.val_mul`) and polynomial-time, with the precision `p` in unary and the @@ -61,16 +64,19 @@ does by Newton lifting, is not covered here. * `Cslib.GaloisRingArith.monicOf`: the monic polynomial with given lower coefficients. * `Cslib.GaloisRingArith.val`: the value of a coefficient list. -* `Cslib.GaloisRingArith.add`, `Cslib.GaloisRingArith.mulX`, `Cslib.GaloisRingArith.mul`: addition, - multiplication by `U` and multiplication. +* `Cslib.GaloisRingArith.add`, `Cslib.GaloisRingArith.mulX`, `Cslib.GaloisRingArith.mul`, + `Cslib.GaloisRingArith.one`, `Cslib.GaloisRingArith.pow`: addition, multiplication by `U`, + multiplication, the unit and powers. ## Main results * `Cslib.GaloisRingArith.val_add`, `Cslib.GaloisRingArith.val_mulX`, - `Cslib.GaloisRingArith.val_mul`: correctness. + `Cslib.GaloisRingArith.val_mul`, `Cslib.GaloisRingArith.val_one`, + `Cslib.GaloisRingArith.val_pow`: correctness. * `Cslib.GaloisRingArith.computableInPolyTime_add`, `Cslib.GaloisRingArith.computableInPolyTime_mulX`, - `Cslib.GaloisRingArith.computableInPolyTime_mul`: polynomial time. + `Cslib.GaloisRingArith.computableInPolyTime_mul`, + `Cslib.GaloisRingArith.computableInPolyTime_pow`: polynomial time. ## References @@ -131,6 +137,13 @@ def mulStep (p : ℕ) (fl c : List ℕ) (s : List ℕ × List ℕ) (i : ℕ) : L def mul (p : ℕ) (fl c d : List ℕ) : List ℕ := ((List.range fl.length).foldl (mulStep p fl c) (d, zero fl)).2 +/-- The unit element `1`, with `e` coordinates. -/ +def one (fl : List ℕ) : List ℕ := (List.range fl.length).map fun i => if i = 0 then 1 else 0 + +/-- **Powers** `c ^ k`, by `k` multiplications; the exponent is read in unary. -/ +def pow (p : ℕ) (fl c : List ℕ) (k : ℕ) : List ℕ := + (List.range k).foldl (fun acc _ => mul p fl acc c) (one fl) + /-! ### Correctness -/ section Correctness @@ -235,6 +248,34 @@ theorem val_mul (c d : List ℕ) : val p fl (mul p fl c d) = val p fl c * val p rw [mul, (hinv fl.length).2] rfl +/-- **The unit is correct.** -/ +@[simp] theorem val_one : val p fl (one fl) = 1 := by + rcases Nat.eq_zero_or_pos fl.length with he | he + · -- The defining polynomial is `1`, so the ring is trivial. + have h1 : (monicOf fl).map (Int.castRingHom (ZMod (2 ^ p))) = 1 := by + simp [monicOf, he] + have h : (1 : Ring p fl) = 0 := by + rw [← map_one (AdjoinRoot.mk ((monicOf fl).map (Int.castRingHom (ZMod (2 ^ p))))), + AdjoinRoot.mk_eq_zero, h1] + simp [val, he, h] + · obtain ⟨e, he'⟩ := Nat.exists_eq_add_of_lt he + rw [Nat.zero_add] at he' + rw [val, he', sum_range_succ'] + simp only [one, he'] + rw [sum_eq_zero fun i hi => by + rw [List.getD_eq_getElem _ _ (by simp at hi ⊢; omega)] + simp] + rw [List.getD_eq_getElem _ _ (by simp)] + simp + +/-- **Powers are correct.** -/ +theorem val_pow (c : List ℕ) (k : ℕ) : val p fl (pow p fl c k) = val p fl c ^ k := by + rw [pow] + induction k with + | zero => simp + | succ k ih => rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, + val_mul, ih, pow_succ] + end Correctness /-! ### Reduced outputs -/ @@ -441,6 +482,50 @@ theorem computableInPolyTime_mul {p : α → ℕ} {fl c d : α → List ℕ} simp only [mulStep, encS, length_encPair] omega +/-- **Powers are polynomial-time**, with the precision and the exponent in unary. -/ +@[fun_prop] +theorem computableInPolyTime_pow {p k : α → ℕ} {fl c : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hk : ComputableInPolyTime k encIn encUnary) : + ComputableInPolyTime (fun x => pow (p x) (fl x) (c x) (k x)) encIn (encList encNat) := by + have hone : ComputableInPolyTime (fun x => one (fl x)) encIn (encList encNat) := by + have h2 := ComputableInPolyTime.snd encIn encUnary + refine computableInPolyTime_tabulate (g := fun _ i => if i = 0 then 1 else 0) + (length_polyTime hfl) ?_ + refine (ComputableInPolyTime.ite (encMid := encNat) (c := fun q : α × ℕ => q.2 == 0) + ((ComputableInPolyTime.beq (h2) (ComputableInPolyTime.const 0))) + (ComputableInPolyTime.const 1) (ComputableInPolyTime.const 0)).of_enc_eq fun q => ?_ + by_cases h : q.2 = 0 <;> simp [h] + have hstep : ComputableInPolyTime (fun q : (α × List ℕ) × ℕ => mul (p q.1.1) (fl q.1.1) q.1.2 + (c q.1.1)) (encPair (encPair encIn (encList encNat)) encUnary) (encList encNat) := by + have hq := ComputableInPolyTime.fst (encPair encIn (encList encNat)) encUnary + have hx := (ComputableInPolyTime.fst encIn (encList encNat)).comp hq + have hacc := (ComputableInPolyTime.snd encIn (encList encNat)).comp hq + exact computableInPolyTime_mul (hp.comp hx) (hfl.comp hx) hacc (hc.comp hx) + have hgrowth : PolyBounded (fun x => (encIn x).length) + (fun x => (fl x).length * (2 * p x + 1)) := by + have hpl := (ComputableInPolyTime.polyBounded_length hp) + have hfll := (ComputableInPolyTime.polyBounded_length hfl) + refine (hfll.mul (((PolyBounded.const 2).mul hpl).add (PolyBounded.const 1))).mono + fun x => ?_ + have h1 : p x ≤ (encUnary (p x)).length := by simp + have h2 : (fl x).length ≤ (encList encNat (fl x)).length := by + rw [length_encList] + calc (fl x).length = ((fl x).map fun _ => 1).sum := by simp + _ ≤ ((fl x).map fun a => 2 * (encNat a).length + 1).sum := + List.sum_le_sum fun a _ => by omega + exact Nat.mul_le_mul h2 (Nat.add_le_add_right (Nat.mul_le_mul_left 2 h1) 1) + have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encUnary) (encL := encList encUnary) + (step := fun x acc _ => mul (p x) (fl x) acc (c x)) hone + ⟨ComputableInPolyTime.range.comp hk, hstep, inferInstance, inferInstance⟩ + ⟨hgrowth, fun x acc _ _ => ?_⟩ + · exact hfold + · have := length_encList_le (length_mul (p x) (fl x) acc (c x)) fun _ h => lt_of_mem_mul h + omega + end PolyTime end Cslib.GaloisRingArith diff --git a/ComplexityTests/GaloisRingArithmetic.lean b/ComplexityTests/GaloisRingArithmetic.lean index 566fca586..f0e7710ba 100644 --- a/ComplexityTests/GaloisRingArithmetic.lean +++ b/ComplexityTests/GaloisRingArithmetic.lean @@ -34,6 +34,16 @@ example : mul 3 [1, 1] [9] [3, 1, 4] = [3, 1] := by decide -- Degree three, `f = U ^ 3 + U + 1`, modulo `16`: `U ^ 2 * U = U ^ 3 = -1 - U`. example : mulX 4 [1, 1, 0] [0, 0, 1] = [15, 15, 0] := by decide +-- The unit, and `U ^ 3 = 1` as a power. +example : one [1, 1] = [1, 0] ∧ pow 3 [1, 1] [0, 1] 3 = [1, 0] := by decide + +-- `(1 + U) ^ 2 = 1 + 2 U + U ^ 2 = U`. +example : pow 3 [1, 1] [1, 1] 2 = [0, 1] := by decide + +/-- Powers are correct. -/ +example (c : List ℕ) (k : ℕ) : val 3 [1, 1] (pow 3 [1, 1] c k) = val 3 [1, 1] c ^ k := + val_pow c k + /-- The defining polynomial is monic. -/ example : (monicOf [1, 1]).Monic := monic_monicOf _ @@ -56,4 +66,11 @@ example : ComputableInPolyTime (encList encNat) := by fun_prop +/-- **Powers in polynomial time**, with the exponent in unary. -/ +example : ComputableInPolyTime + (fun q : (ℕ × List ℕ) × (List ℕ × ℕ) => pow q.1.1 q.1.2 q.2.1 q.2.2) + (encPair (encPair encUnary (encList encNat)) (encPair (encList encNat) encUnary)) + (encList encNat) := by + fun_prop + end ComplexityTests.GaloisRingArithmetic From dc4824e4e3a12d05ae3527e90eb88b985f9c6525 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:41:30 -0400 Subject: [PATCH 3/4] feat(PolyTime): negation, subtraction and Newton inversion in (Z/2^p)[U]/(f) The seed x^(2^e - 2) by e - 1 squarings, then p Newton steps y(2 - xy); correct whenever the seed inverts x modulo 2, which holds for units of a Galois ring. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../PolyTime/GaloisRingArithmetic.lean | 287 +++++++++++++++--- ComplexityTests/GaloisRingArithmetic.lean | 20 ++ 2 files changed, 266 insertions(+), 41 deletions(-) diff --git a/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean index 8a9bfcd2a..123a3cfdb 100644 --- a/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean +++ b/Complexity/Computability/PolyTime/GaloisRingArithmetic.lean @@ -50,6 +50,12 @@ The value of a coefficient list `c` is `∑ i < e, c i U ^ i` in `A_p` (`GaloisR * **Powers** (`GaloisRingArith.pow`) `c ^ k` take `k` multiplications from `GaloisRingArith.one`, with `k` in unary. In the source the exponents of the mode substitutions are below the precision (Appendix D.4.6, p. 63), so they are polynomial. +* **Inversion** (`GaloisRingArith.inv`) starts from the seed `x ^ (2 ^ e - 2)`, a product of `e - 1` + repeated squares (`GaloisRingArith.seed`), and takes `p` Newton steps `y ↦ y (2 - x y)`, each + squaring the defect `x y - 1` (`GaloisRingArith.val_mul_newton`). When the seed inverts `x` + modulo `2`, the result is the inverse (`GaloisRingArith.val_mul_inv`). In a Galois ring, with + `f` irreducible modulo `2`, this holds for every unit, since the residue field has `2 ^ e` + elements; that bridge is not made here. Each operation is correct (`GaloisRingArith.val_add`, `GaloisRingArith.val_mulX`, `GaloisRingArith.val_mul`) and polynomial-time, with the precision `p` in unary and the @@ -57,26 +63,32 @@ coordinates and the coefficients of `f` in binary (`GaloisRingArith.computableIn `GaloisRingArith.computableInPolyTime_mul`). Their outputs are reduced, with `e` coordinates below `2 ^ p` (`GaloisRingArith.length_mul`, `GaloisRingArith.lt_of_mem_mul`). These are the polynomial-time arithmetic claims of Appendix D.4.1 for addition and multiplication, in the case -`ℓ = 1` of the source, where `A = O` has no `V`-coordinates. Inversion of units, which the source -does by Newton lifting, is not covered here. +`ℓ = 1` of the source, where `A = O` has no `V`-coordinates, together with the inversion of units +by inversion modulo two and Newton lifting that the source names (Appendix D.4.1, p. 58). ## Main definitions * `Cslib.GaloisRingArith.monicOf`: the monic polynomial with given lower coefficients. * `Cslib.GaloisRingArith.val`: the value of a coefficient list. * `Cslib.GaloisRingArith.add`, `Cslib.GaloisRingArith.mulX`, `Cslib.GaloisRingArith.mul`, - `Cslib.GaloisRingArith.one`, `Cslib.GaloisRingArith.pow`: addition, multiplication by `U`, - multiplication, the unit and powers. + `Cslib.GaloisRingArith.one`, `Cslib.GaloisRingArith.pow`, `Cslib.GaloisRingArith.neg`, + `Cslib.GaloisRingArith.sub`: addition, multiplication by `U`, multiplication, the unit, powers, + negation and subtraction. +* `Cslib.GaloisRingArith.seed`, `Cslib.GaloisRingArith.newton`, `Cslib.GaloisRingArith.inv`: + inversion. ## Main results * `Cslib.GaloisRingArith.val_add`, `Cslib.GaloisRingArith.val_mulX`, `Cslib.GaloisRingArith.val_mul`, `Cslib.GaloisRingArith.val_one`, - `Cslib.GaloisRingArith.val_pow`: correctness. + `Cslib.GaloisRingArith.val_pow`, `Cslib.GaloisRingArith.val_neg`, + `Cslib.GaloisRingArith.val_sub`, `Cslib.GaloisRingArith.val_seed`, + `Cslib.GaloisRingArith.val_mul_inv`: correctness. * `Cslib.GaloisRingArith.computableInPolyTime_add`, `Cslib.GaloisRingArith.computableInPolyTime_mulX`, `Cslib.GaloisRingArith.computableInPolyTime_mul`, - `Cslib.GaloisRingArith.computableInPolyTime_pow`: polynomial time. + `Cslib.GaloisRingArith.computableInPolyTime_pow`, + `Cslib.GaloisRingArith.computableInPolyTime_inv`: polynomial time. ## References @@ -144,6 +156,33 @@ def one (fl : List ℕ) : List ℕ := (List.range fl.length).map fun i => if i = def pow (p : ℕ) (fl c : List ℕ) (k : ℕ) : List ℕ := (List.range k).foldl (fun acc _ => mul p fl acc c) (one fl) +/-- Negation, coordinatewise modulo `2 ^ p`. -/ +def neg (p : ℕ) (fl c : List ℕ) : List ℕ := + (List.range fl.length).map fun i => (2 ^ p - c.getD i 0 % 2 ^ p) % 2 ^ p + +/-- Subtraction. -/ +def sub (p : ℕ) (fl c d : List ℕ) : List ℕ := add p fl c (neg p fl d) + +/-- One step of the seed of inversion: from `(x ^ 2 ^ j, x ^ (2 ^ (j + 1) - 2))`, square the power +and multiply it in. -/ +def seedStep (p : ℕ) (fl : List ℕ) (s : List ℕ × List ℕ) : List ℕ × List ℕ := + (mul p fl s.1 s.1, mul p fl s.2 (mul p fl s.1 s.1)) + +/-- The seed `x ^ (2 ^ e - 2) = x ^ 2 x ^ 4 ⋯ x ^ (2 ^ (e - 1))` of inversion, by `e - 1` +squarings. In a Galois ring it inverts `x` modulo `2`, since the residue field has `2 ^ e` +elements. -/ +def seed (p : ℕ) (fl x : List ℕ) : List ℕ := + ((List.range (fl.length - 1)).foldl (fun s _ => seedStep p fl s) (x, one fl)).2 + +/-- One Newton step `y (2 - x y)` towards the inverse of `x`. -/ +def newton (p : ℕ) (fl x y : List ℕ) : List ℕ := + mul p fl y (sub p fl (add p fl (one fl) (one fl)) (mul p fl x y)) + +/-- **Inversion**: `p` Newton steps from the seed. It is the inverse of `x` whenever the seed +inverts `x` modulo `2` (`val_mul_inv`), in particular for every unit of a Galois ring. -/ +def inv (p : ℕ) (fl x : List ℕ) : List ℕ := + (List.range p).foldl (fun y _ => newton p fl x y) (seed p fl x) + /-! ### Correctness -/ section Correctness @@ -276,6 +315,78 @@ theorem val_pow (c : List ℕ) (k : ℕ) : val p fl (pow p fl c k) = val p fl c | succ k ih => rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, val_mul, ih, pow_succ] +/-- **Negation is correct.** -/ +theorem val_neg (c : List ℕ) : val p fl (neg p fl c) = -val p fl c := by + rw [val, val, ← sum_neg_distrib] + refine sum_congr rfl fun i hi => ?_ + rw [neg, List.getD_eq_getElem _ _ (by simpa using hi)] + simp only [List.getElem_map, List.getElem_range, natCast_mod_two_pow] + rw [Nat.cast_sub (Nat.mod_lt _ (Nat.two_pow_pos p)).le, natCast_two_pow, natCast_mod_two_pow] + ring + +/-- **Subtraction is correct.** -/ +theorem val_sub (c d : List ℕ) : val p fl (sub p fl c d) = val p fl c - val p fl d := by + rw [sub, val_add, val_neg, sub_eq_add_neg] + +/-- **The seed is the power `x ^ (2 ^ e - 2)`.** -/ +theorem val_seed (x : List ℕ) : val p fl (seed p fl x) = val p fl x ^ (2 ^ fl.length - 2) := by + have hinv (j : ℕ) : + val p fl ((List.range j).foldl (fun s _ => seedStep p fl s) (x, one fl)).1 = + val p fl x ^ 2 ^ j ∧ + val p fl ((List.range j).foldl (fun s _ => seedStep p fl s) (x, one fl)).2 = + val p fl x ^ (2 ^ (j + 1) - 2) := by + induction j with + | zero => simp + | succ j ih => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, seedStep] + refine ⟨?_, ?_⟩ + · rw [val_mul, ih.1, ← pow_add, ← two_mul, ← pow_succ'] + · rw [val_mul, val_mul, ih.1, ih.2, ← pow_add, ← pow_add] + congr 1 + have : 2 ≤ 2 ^ (j + 1) := by + calc 2 = 2 ^ 1 := rfl + _ ≤ 2 ^ (j + 1) := Nat.pow_le_pow_right (by norm_num) (by omega) + rw [pow_succ 2 (j + 1)] + omega + rw [seed, (hinv _).2] + rcases Nat.eq_zero_or_pos fl.length with he | he + · simp [he] + · rw [Nat.sub_add_cancel he] + +/-- **Newton's step squares the defect**: if `x y = 1 + 2 ^ m w` then +`x (y (2 - x y)) = 1 + 2 ^ (2 m) (-w ^ 2)`. -/ +theorem val_mul_newton (x y : List ℕ) {m : ℕ} {w : Ring p fl} + (h : val p fl x * val p fl y = 1 + 2 ^ m * w) : + val p fl x * val p fl (newton p fl x y) = 1 + 2 ^ (2 * m) * -w ^ 2 := by + rw [newton, val_mul, val_sub, val_add, val_mul, val_one] + have : val p fl x * (val p fl y * (1 + 1 - val p fl x * val p fl y)) = + (val p fl x * val p fl y) * (2 - val p fl x * val p fl y) := by ring + rw [this, h, show (2 : Ring p fl) ^ (2 * m) = 2 ^ m * 2 ^ m by rw [two_mul, pow_add]] + ring + +/-- **Inversion is correct** when the seed inverts `x` modulo `2`. -/ +theorem val_mul_inv (x : List ℕ) {w : Ring p fl} + (h : val p fl x * val p fl x ^ (2 ^ fl.length - 2) = 1 + 2 * w) : + val p fl x * val p fl (inv p fl x) = 1 := by + have hstep (k : ℕ) : ∃ w' : Ring p fl, val p fl x * + val p fl ((List.range k).foldl (fun y _ => newton p fl x y) (seed p fl x)) = + 1 + 2 ^ 2 ^ k * w' := by + induction k with + | zero => exact ⟨w, by rw [List.range_zero, List.foldl_nil, val_seed, h, pow_zero, pow_one]⟩ + | succ k ih => + obtain ⟨w', hw'⟩ := ih + refine ⟨-w' ^ 2, ?_⟩ + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, + val_mul_newton _ _ hw', show 2 ^ (k + 1) = 2 * 2 ^ k by ring] + obtain ⟨w', hw'⟩ := hstep p + rw [inv, hw'] + have hp : (2 : Ring p fl) ^ 2 ^ p = 0 := by + have h2p : (2 : Ring p fl) ^ p = 0 := by + rw [show (2 : Ring p fl) ^ p = ((2 ^ p : ℕ) : Ring p fl) by push_cast; rfl, + natCast_two_pow] + exact pow_eq_zero_of_le Nat.lt_two_pow_self.le h2p + rw [hp, zero_mul, add_zero] + end Correctness /-! ### Reduced outputs -/ @@ -427,6 +538,38 @@ theorem length_encList_le {p e : ℕ} {c : List ℕ} (hlen : c.length = e) omega _ = e * (2 * p + 1) := by rw [List.length_map, hlen, smul_eq_mul] +/-- The unit is polynomial-time. -/ +@[fun_prop] +theorem computableInPolyTime_one {fl : α → List ℕ} + (hfl : ComputableInPolyTime fl encIn (encList encNat)) : + ComputableInPolyTime (fun x => one (fl x)) encIn (encList encNat) := by + have h2 := ComputableInPolyTime.snd encIn encUnary + refine computableInPolyTime_tabulate (g := fun _ i => if i = 0 then 1 else 0) + (length_polyTime hfl) ?_ + refine (ComputableInPolyTime.ite (encMid := encNat) (c := fun q : α × ℕ => q.2 == 0) + ((ComputableInPolyTime.beq (h2) (ComputableInPolyTime.const 0))) + (ComputableInPolyTime.const 1) (ComputableInPolyTime.const 0)).of_enc_eq fun q => ?_ + by_cases h : q.2 = 0 <;> simp [h] + +/-- The length bound shared by the folds below: a pair of reduced lists. -/ +private theorem polyBounded_reduced {p : α → ℕ} {fl : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) : + PolyBounded (fun x => (encIn x).length) + (fun x => 3 * ((fl x).length * (2 * p x + 1)) + 1) := by + have hpl := (ComputableInPolyTime.polyBounded_length hp) + have hfll := (ComputableInPolyTime.polyBounded_length hfl) + refine (((PolyBounded.const 3).mul (hfll.mul (((PolyBounded.const 2).mul hpl).add + (PolyBounded.const 1)))).add (PolyBounded.const 1)).mono fun x => ?_ + have h1 : p x ≤ (encUnary (p x)).length := by simp + have h2 : (fl x).length ≤ (encList encNat (fl x)).length := by + rw [length_encList] + calc (fl x).length = ((fl x).map fun _ => 1).sum := by simp + _ ≤ ((fl x).map fun a => 2 * (encNat a).length + 1).sum := + List.sum_le_sum fun a _ => by omega + have := Nat.mul_le_mul h2 (Nat.add_le_add_right (Nat.mul_le_mul_left 2 h1) 1) + omega + /-- **Multiplication is polynomial-time**, with the precision in unary. Every intermediate pair is reduced after its first step, so its length is bounded by the precision and the degree. -/ @[fun_prop] @@ -457,20 +600,7 @@ theorem computableInPolyTime_mul {p : α → ℕ} {fl c d : α → List ℕ} (computableInPolyTime_addSmul (hp.comp hx) (hfl.comp hx) hacc (computableInPolyTime_getD (hc.comp hx) hi) hcur) -- Every step's output is reduced, hence of bounded length. - have hgrowth : PolyBounded (fun x => (encIn x).length) - (fun x => 3 * ((fl x).length * (2 * p x + 1)) + 1) := by - have hpl := (ComputableInPolyTime.polyBounded_length hp) - have hfll := (ComputableInPolyTime.polyBounded_length hfl) - refine (((PolyBounded.const 3).mul (hfll.mul (((PolyBounded.const 2).mul hpl).add - (PolyBounded.const 1)))).add (PolyBounded.const 1)).mono fun x => ?_ - have h1 : p x ≤ (encUnary (p x)).length := by simp - have h2 : (fl x).length ≤ (encList encNat (fl x)).length := by - rw [length_encList] - calc (fl x).length = ((fl x).map fun _ => 1).sum := by simp - _ ≤ ((fl x).map fun a => 2 * (encNat a).length + 1).sum := - List.sum_le_sum fun a _ => by omega - have := Nat.mul_le_mul h2 (Nat.add_le_add_right (Nat.mul_le_mul_left 2 h1) 1) - omega + have hgrowth := polyBounded_reduced hp hfl have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth (encA := encUnary) (encL := encList encUnary) (step := fun x s i => mulStep (p x) (fl x) (c x) s i) hinit @@ -490,33 +620,14 @@ theorem computableInPolyTime_pow {p k : α → ℕ} {fl c : α → List ℕ} (hc : ComputableInPolyTime c encIn (encList encNat)) (hk : ComputableInPolyTime k encIn encUnary) : ComputableInPolyTime (fun x => pow (p x) (fl x) (c x) (k x)) encIn (encList encNat) := by - have hone : ComputableInPolyTime (fun x => one (fl x)) encIn (encList encNat) := by - have h2 := ComputableInPolyTime.snd encIn encUnary - refine computableInPolyTime_tabulate (g := fun _ i => if i = 0 then 1 else 0) - (length_polyTime hfl) ?_ - refine (ComputableInPolyTime.ite (encMid := encNat) (c := fun q : α × ℕ => q.2 == 0) - ((ComputableInPolyTime.beq (h2) (ComputableInPolyTime.const 0))) - (ComputableInPolyTime.const 1) (ComputableInPolyTime.const 0)).of_enc_eq fun q => ?_ - by_cases h : q.2 = 0 <;> simp [h] + have hone := computableInPolyTime_one hfl have hstep : ComputableInPolyTime (fun q : (α × List ℕ) × ℕ => mul (p q.1.1) (fl q.1.1) q.1.2 (c q.1.1)) (encPair (encPair encIn (encList encNat)) encUnary) (encList encNat) := by have hq := ComputableInPolyTime.fst (encPair encIn (encList encNat)) encUnary have hx := (ComputableInPolyTime.fst encIn (encList encNat)).comp hq have hacc := (ComputableInPolyTime.snd encIn (encList encNat)).comp hq exact computableInPolyTime_mul (hp.comp hx) (hfl.comp hx) hacc (hc.comp hx) - have hgrowth : PolyBounded (fun x => (encIn x).length) - (fun x => (fl x).length * (2 * p x + 1)) := by - have hpl := (ComputableInPolyTime.polyBounded_length hp) - have hfll := (ComputableInPolyTime.polyBounded_length hfl) - refine (hfll.mul (((PolyBounded.const 2).mul hpl).add (PolyBounded.const 1))).mono - fun x => ?_ - have h1 : p x ≤ (encUnary (p x)).length := by simp - have h2 : (fl x).length ≤ (encList encNat (fl x)).length := by - rw [length_encList] - calc (fl x).length = ((fl x).map fun _ => 1).sum := by simp - _ ≤ ((fl x).map fun a => 2 * (encNat a).length + 1).sum := - List.sum_le_sum fun a _ => by omega - exact Nat.mul_le_mul h2 (Nat.add_le_add_right (Nat.mul_le_mul_left 2 h1) 1) + have hgrowth := polyBounded_reduced hp hfl have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth (encA := encUnary) (encL := encList encUnary) (step := fun x acc _ => mul (p x) (fl x) acc (c x)) hone @@ -526,6 +637,100 @@ theorem computableInPolyTime_pow {p k : α → ℕ} {fl c : α → List ℕ} · have := length_encList_le (length_mul (p x) (fl x) acc (c x)) fun _ h => lt_of_mem_mul h omega +/-- **Negation is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_neg {p : α → ℕ} {fl c : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) : + ComputableInPolyTime (fun x => neg (p x) (fl x) (c x)) encIn (encList encNat) := by + have h1 := ComputableInPolyTime.fst encIn encUnary + have h2 := ComputableInPolyTime.snd encIn encUnary + exact computableInPolyTime_tabulate (length_polyTime hfl) + (computableInPolyTime_mod_two_pow (ComputableInPolyTime.binary_sub' + (ComputableInPolyTime.binary_two_pow.comp (hp.comp h1)) + (computableInPolyTime_mod_two_pow (computableInPolyTime_getD (hc.comp h1) h2) + (hp.comp h1))) (hp.comp h1)) + +/-- **Subtraction is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_sub {p : α → ℕ} {fl c d : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hd : ComputableInPolyTime d encIn (encList encNat)) : + ComputableInPolyTime (fun x => sub (p x) (fl x) (c x) (d x)) encIn (encList encNat) := + computableInPolyTime_add hp hfl hc (computableInPolyTime_neg hp hfl hd) + +/-- **A Newton step is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_newton {p : α → ℕ} {fl x y : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hx : ComputableInPolyTime x encIn (encList encNat)) + (hy : ComputableInPolyTime y encIn (encList encNat)) : + ComputableInPolyTime (fun a => newton (p a) (fl a) (x a) (y a)) encIn (encList encNat) := + computableInPolyTime_mul hp hfl hy (computableInPolyTime_sub hp hfl + (computableInPolyTime_add hp hfl (computableInPolyTime_one hfl) + (computableInPolyTime_one hfl)) (computableInPolyTime_mul hp hfl hx hy)) + +/-- **The seed of inversion is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_seed {p : α → ℕ} {fl x : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hx : ComputableInPolyTime x encIn (encList encNat)) : + ComputableInPolyTime (fun a => seed (p a) (fl a) (x a)) encIn (encList encNat) := by + let encS := encPair (encList encNat) (encList encNat) + have hstep : ComputableInPolyTime + (fun q : (α × (List ℕ × List ℕ)) × ℕ => seedStep (p q.1.1) (fl q.1.1) q.1.2) + (encPair (encPair encIn encS) encUnary) encS := by + have hq := ComputableInPolyTime.fst (encPair encIn encS) encUnary + have ha := (ComputableInPolyTime.fst encIn encS).comp hq + have hs := (ComputableInPolyTime.snd encIn encS).comp hq + have h1 := (ComputableInPolyTime.fst (encList encNat) (encList encNat)).comp hs + have h2 := (ComputableInPolyTime.snd (encList encNat) (encList encNat)).comp hs + have hsq := computableInPolyTime_mul (hp.comp ha) (hfl.comp ha) h1 h1 + exact hsq.prod (computableInPolyTime_mul (hp.comp ha) (hfl.comp ha) h2 hsq) + have hfold := ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encUnary) (encL := encList encUnary) + (step := fun a s _ => seedStep (p a) (fl a) s) + (hx.prod (computableInPolyTime_one hfl)) + ⟨ComputableInPolyTime.range.comp (ComputableInPolyTime.unary_sub' (length_polyTime hfl) + (ComputableInPolyTime.const 1)), hstep, inferInstance, inferInstance⟩ + ⟨polyBounded_reduced hp hfl, fun a s _ _ => ?_⟩ + · exact (ComputableInPolyTime.snd (encList encNat) (encList encNat)).comp hfold + · have h1 := length_encList_le (length_mul (p a) (fl a) s.1 s.1) fun _ h => lt_of_mem_mul h + have h2 := length_encList_le (length_mul (p a) (fl a) s.2 (mul (p a) (fl a) s.1 s.1)) + fun _ h => lt_of_mem_mul h + simp only [seedStep, length_encPair] + omega + +/-- **Inversion is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_inv {p : α → ℕ} {fl x : α → List ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hx : ComputableInPolyTime x encIn (encList encNat)) : + ComputableInPolyTime (fun a => inv (p a) (fl a) (x a)) encIn (encList encNat) := by + have hstep : ComputableInPolyTime + (fun q : (α × List ℕ) × ℕ => newton (p q.1.1) (fl q.1.1) (x q.1.1) q.1.2) + (encPair (encPair encIn (encList encNat)) encUnary) (encList encNat) := by + have hq := ComputableInPolyTime.fst (encPair encIn (encList encNat)) encUnary + have ha := (ComputableInPolyTime.fst encIn (encList encNat)).comp hq + have hy := (ComputableInPolyTime.snd encIn (encList encNat)).comp hq + exact computableInPolyTime_newton (hp.comp ha) (hfl.comp ha) (hx.comp ha) hy + exact ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encUnary) (encL := encList encUnary) + (step := fun a y _ => newton (p a) (fl a) (x a) y) (computableInPolyTime_seed hp hfl hx) + ⟨ComputableInPolyTime.range.comp hp, hstep, inferInstance, inferInstance⟩ + ⟨polyBounded_reduced hp hfl, fun a y _ _ => by + have := length_encList_le (length_mul (p a) (fl a) y + (sub (p a) (fl a) (add (p a) (fl a) (one (fl a)) (one (fl a))) (mul (p a) (fl a) (x a) y))) + fun _ h => lt_of_mem_mul h + simp only [newton] + omega⟩ + end PolyTime end Cslib.GaloisRingArith diff --git a/ComplexityTests/GaloisRingArithmetic.lean b/ComplexityTests/GaloisRingArithmetic.lean index f0e7710ba..c3f7705e2 100644 --- a/ComplexityTests/GaloisRingArithmetic.lean +++ b/ComplexityTests/GaloisRingArithmetic.lean @@ -44,6 +44,20 @@ example : pow 3 [1, 1] [1, 1] 2 = [0, 1] := by decide example (c : List ℕ) (k : ℕ) : val 3 [1, 1] (pow 3 [1, 1] c k) = val 3 [1, 1] c ^ k := val_pow c k +-- Inversion of units: `U⁻¹ = U ^ 2 = 7 + 7 U`, and `(1 + 2 U)⁻¹`, `(3 + 5 U)⁻¹` are inverses. +example : inv 3 [1, 1] [0, 1] = [7, 7] := by decide +example : mul 3 [1, 1] [1, 2] (inv 3 [1, 1] [1, 2]) = [1, 0] := by decide +example : mul 3 [1, 1] [3, 5] (inv 3 [1, 1] [3, 5]) = [1, 0] := by decide + +-- `2` is not a unit, and inversion does not invert it. +example : mul 3 [1, 1] [2, 0] (inv 3 [1, 1] [2, 0]) ≠ [1, 0] := by decide + +/-- Inversion is correct when the seed inverts modulo `2`. -/ +example (x : List ℕ) {w : Ring 3 [1, 1]} + (h : val 3 [1, 1] x * val 3 [1, 1] x ^ (2 ^ 2 - 2) = 1 + 2 * w) : + val 3 [1, 1] x * val 3 [1, 1] (inv 3 [1, 1] x) = 1 := + val_mul_inv x h + /-- The defining polynomial is monic. -/ example : (monicOf [1, 1]).Monic := monic_monicOf _ @@ -73,4 +87,10 @@ example : ComputableInPolyTime (encList encNat) := by fun_prop +/-- **Inversion in polynomial time.** -/ +example : ComputableInPolyTime + (fun q : (ℕ × List ℕ) × List ℕ => inv q.1.1 q.1.2 q.2) + (encPair (encPair encUnary (encList encNat)) (encList encNat)) (encList encNat) := by + fun_prop + end ComplexityTests.GaloisRingArithmetic From 5bea2c18e98885ca91912b0cb285c04d22e7b250 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:59:31 -0400 Subject: [PATCH 4/4] feat(PolyTime): polynomials over (Z/2^p)[U]/(f) and Lagrange interpolation Addition, scaling, multiplication by z - v and Horner evaluation of coefficient-list polynomials, and Lagrange interpolation with Newton inverses of the denominators, proved to take the given values and certified polynomial-time with the precision in unary. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../PolyTime/GaloisRingInterpolation.lean | 594 ++++++++++++++++++ ComplexityTests/GaloisRingInterpolation.lean | 55 ++ 3 files changed, 650 insertions(+) create mode 100644 Complexity/Computability/PolyTime/GaloisRingInterpolation.lean create mode 100644 ComplexityTests/GaloisRingInterpolation.lean diff --git a/Complexity.lean b/Complexity.lean index 566b83dcb..a79124c54 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1986,6 +1986,7 @@ public import Complexity.Computability.PolyTime.CSP.ToCNF public import Complexity.Computability.PolyTime.CommonCountingAccum public import Complexity.Computability.PolyTime.FineGrained.ParameterCheck public import Complexity.Computability.PolyTime.GaloisRingArithmetic +public import Complexity.Computability.PolyTime.GaloisRingInterpolation public import Complexity.Computability.PolyTime.GreedyLabelSchedule public import Complexity.Computability.PolyTime.GreedySlotScore public import Complexity.Computability.PolyTime.Int.ExactDiv diff --git a/Complexity/Computability/PolyTime/GaloisRingInterpolation.lean b/Complexity/Computability/PolyTime/GaloisRingInterpolation.lean new file mode 100644 index 000000000..d0d12173f --- /dev/null +++ b/Complexity/Computability/PolyTime/GaloisRingInterpolation.lean @@ -0,0 +1,594 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.PolyTime.GaloisRingArithmetic +public import Mathlib.Algebra.Polynomial.BigOperators +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeLoops +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Data.List.GetD +import Mathlib.Data.Nat.Size + +/-! +# Polynomials over `(ℤ / 2 ^ p)[U] / (f)` and Lagrange interpolation, on coefficient lists + +Polynomials in `z` over the coefficient ring `A_p = (ℤ / 2 ^ p)[U] / (f)` of +`Complexity/Computability/PolyTime/GaloisRingArithmetic.lean` are lists of coefficients, +constant first, each a coefficient list of `A_p` (`GaloisRingArith.pval`). + +* **Addition** (`GaloisRingArith.padd`), **scaling** (`GaloisRingArith.psmul`) and + **multiplication by `z - v`** (`GaloisRingArith.pmulLinear`). +* **Evaluation** (`GaloisRingArith.peval`) by Horner's rule. +* **Lagrange interpolation** (`GaloisRingArith.interp`) at nodes `v₀, …, v_{n-1}`: the sum of + `y_i (∏_{j ≠ i} (v_i - v_j))⁻¹ ∏_{j ≠ i} (z - v_j)`, with the inverses of + `GaloisRingArith.inv`. When those inverses are correct, for instance at nodes with unit + differences in a Galois ring, the result takes the value `y_i` at `v_i` + (`GaloisRingArith.eval_pval_interp`). It has at most `n + 1` coefficients and degree below `n` + (`GaloisRingArith.pval_interp`); at nodes with unit differences, a polynomial of degree below + `n` is determined by its values there. + +Every operation is polynomial-time, with the precision in unary +(`GaloisRingArith.computableInPolyTime_interp` and the rules before it). + +This is the interpolation step of the contraction algorithm of [OpenAI2026ETH] +(Appendix D.4.4, p. 61), which recovers `F (t + α z)` modulo `2 ^ p_t` from its values at +`M (2 L - 1) + 1` binary-coordinate lifts. + +## Main definitions + +* `Cslib.GaloisRingArith.pval`: the polynomial of a list of coefficient lists. +* `Cslib.GaloisRingArith.padd`, `Cslib.GaloisRingArith.psmul`, `Cslib.GaloisRingArith.pmulLinear`, + `Cslib.GaloisRingArith.peval`: polynomial arithmetic. +* `Cslib.GaloisRingArith.interp`: Lagrange interpolation. + +## Main results + +* `Cslib.GaloisRingArith.pval_padd`, `Cslib.GaloisRingArith.pval_psmul`, + `Cslib.GaloisRingArith.pval_pmulLinear`, `Cslib.GaloisRingArith.peval_eq`: correctness. +* `Cslib.GaloisRingArith.eval_pval_interp`: interpolation takes the given values. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.4.4 (p. 61). +-/ + +@[expose] public section + +namespace Cslib.GaloisRingArith + +open Polynomial Finset + +variable {p : ℕ} {fl : List ℕ} + +/-- The polynomial `∑ k, P_k z ^ k` over `A_p` of a list of coefficient lists. -/ +noncomputable def pval (p : ℕ) (fl : List ℕ) (P : List (List ℕ)) : (Ring p fl)[X] := + ∑ k ∈ range P.length, C (val p fl (P.getD k [])) * X ^ k + +/-- The empty coefficient list has value zero. -/ +@[simp] theorem val_nil : val p fl [] = 0 := by simp [val] + +/-- Coefficientwise sum, of length the longer length. -/ +def padd (p : ℕ) (fl : List ℕ) (P Q : List (List ℕ)) : List (List ℕ) := + (List.range (max P.length Q.length)).map fun k => add p fl (P.getD k []) (Q.getD k []) + +/-- Scaling by an element of `A_p`. -/ +def psmul (p : ℕ) (fl c : List ℕ) (P : List (List ℕ)) : List (List ℕ) := + P.map fun a => mul p fl c a + +/-- Multiplication by `z - v`. -/ +def pmulLinear (p : ℕ) (fl v : List ℕ) (P : List (List ℕ)) : List (List ℕ) := + (List.range (P.length + 1)).map fun k => + sub p fl (([] :: P).getD k []) (mul p fl v (P.getD k [])) + +/-- Evaluation at `z` by Horner's rule. -/ +def peval (p : ℕ) (fl : List ℕ) (P : List (List ℕ)) (z : List ℕ) : List ℕ := + P.foldr (fun a acc => add p fl a (mul p fl z acc)) (zero fl) + +/-- Extending a polynomial by zero coefficients does not change it. -/ +theorem pval_eq_sum_of_le (P : List (List ℕ)) {n : ℕ} (h : P.length ≤ n) : + pval p fl P = ∑ k ∈ range n, C (val p fl (P.getD k [])) * X ^ k := by + rw [pval, ← sum_range_add_sum_Ico _ h] + rw [sum_eq_zero (s := Ico _ _) fun k hk => by + rw [List.getD_eq_default _ _ (by simp at hk; omega), val_nil, C_0, zero_mul], add_zero] + +/-- **Addition is correct.** -/ +theorem pval_padd (P Q : List (List ℕ)) : + pval p fl (padd p fl P Q) = pval p fl P + pval p fl Q := by + rw [pval_eq_sum_of_le P (le_max_left P.length Q.length), + pval_eq_sum_of_le Q (le_max_right P.length Q.length), ← sum_add_distrib, pval] + simp only [padd, List.length_map, List.length_range] + refine sum_congr rfl fun k hk => ?_ + rw [List.getD_eq_getElem _ _ (by simpa using hk)] + simp [val_add, add_mul] + +/-- **Scaling is correct.** -/ +theorem pval_psmul (c : List ℕ) (P : List (List ℕ)) : + pval p fl (psmul p fl c P) = C (val p fl c) * pval p fl P := by + rw [pval, pval, mul_sum] + simp only [psmul, List.length_map] + refine sum_congr rfl fun k hk => ?_ + rw [List.getD_eq_getElem _ _ (by simpa using hk), List.getD_eq_getElem _ _ (by simpa using hk)] + simp [val_mul, mul_assoc] + +/-- **Multiplication by `z - v` is correct.** -/ +theorem pval_pmulLinear (v : List ℕ) (P : List (List ℕ)) : + pval p fl (pmulLinear p fl v P) = (X - C (val p fl v)) * pval p fl P := by + have hcoeff (k : ℕ) (hk : k < P.length + 1) : + val p fl ((pmulLinear p fl v P).getD k []) = + val p fl (([] :: P).getD k []) - val p fl v * val p fl (P.getD k []) := by + rw [pmulLinear, List.getD_eq_getElem _ _ (by simpa using hk)] + simp [val_sub, val_mul] + rw [pval, show (pmulLinear p fl v P).length = P.length + 1 by simp [pmulLinear], + sum_congr rfl fun k hk => by rw [hcoeff k (mem_range.mp hk)]] + rw [sub_mul, pval, mul_sum, mul_sum] + simp only [map_sub, map_mul, sub_mul, sum_sub_distrib] + congr 1 + · rw [sum_range_succ'] + simp only [List.getD_cons_zero, val_nil, C_0, zero_mul, add_zero, List.getD_cons_succ] + refine sum_congr rfl fun k _ => by ring + · rw [sum_range_succ, List.getD_eq_default _ _ le_rfl, val_nil, C_0, mul_zero, zero_mul, + add_zero] + refine sum_congr rfl fun k _ => by ring + +/-- **Evaluation is correct.** -/ +theorem peval_eq (P : List (List ℕ)) (z : List ℕ) : + val p fl (peval p fl P z) = (pval p fl P).eval (val p fl z) := by + induction P with + | nil => simp [peval, pval] + | cons a P ih => + rw [peval, List.foldr_cons, ← peval, val_add, val_mul, ih] + simp only [pval, List.length_cons, sum_range_succ', List.getD_cons_succ, List.getD_cons_zero, + eval_add, eval_finsetSum, eval_mul, eval_C, eval_pow, eval_X, pow_zero, mul_one, pow_succ, + mul_sum] + rw [add_comm] + congr 1 + refine sum_congr rfl fun k _ => by ring + +/-! ### Lagrange interpolation -/ + +/-- The numerator `∏_{j < n, j ≠ i} (z - v_j)` of the `i`-th Lagrange basis polynomial. -/ +def basisNum (p : ℕ) (fl : List ℕ) (v : List (List ℕ)) (i : ℕ) : List (List ℕ) := + (List.range v.length).foldl + (fun P j => if j = i then P else pmulLinear p fl (v.getD j []) P) [one fl] + +/-- The denominator `∏_{j < n, j ≠ i} (v_i - v_j)` of the `i`-th Lagrange basis polynomial. -/ +def basisDen (p : ℕ) (fl : List ℕ) (v : List (List ℕ)) (i : ℕ) : List ℕ := + (List.range v.length).foldl + (fun d j => if j = i then d else mul p fl d (sub p fl (v.getD i []) (v.getD j []))) (one fl) + +/-- **Lagrange interpolation** of the values `y` at the nodes `v`. -/ +def interp (p : ℕ) (fl : List ℕ) (v : List (List ℕ)) (y : List (List ℕ)) : List (List ℕ) := + (List.range v.length).foldl (fun P i => + padd p fl P (psmul p fl (mul p fl (y.getD i []) (inv p fl (basisDen p fl v i))) + (basisNum p fl v i))) [] + +theorem pval_basisNum (v : List (List ℕ)) (i : ℕ) : + pval p fl (basisNum p fl v i) = + ∏ j ∈ (range v.length).erase i, (X - C (val p fl (v.getD j []))) := by + have h (m : ℕ) (hm : m ≤ v.length) : pval p fl ((List.range m).foldl + (fun P j => if j = i then P else pmulLinear p fl (v.getD j []) P) [one fl]) = + ∏ j ∈ (range m).erase i, (X - C (val p fl (v.getD j []))) := by + induction m with + | zero => simp [pval] + | succ m ih => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, range_add_one] + by_cases hmi : m = i + · subst hmi + simp only [↓reduceIte] + rw [ih (by omega), erase_insert (by simp), Finset.erase_eq_of_notMem (by simp)] + · simp only [hmi, ↓reduceIte] + rw [pval_pmulLinear, ih (by omega), erase_insert_of_ne hmi, prod_insert (by simp)] + exact h _ le_rfl + +theorem val_basisDen (v : List (List ℕ)) (i : ℕ) : + val p fl (basisDen p fl v i) = + ∏ j ∈ (range v.length).erase i, (val p fl (v.getD i []) - val p fl (v.getD j [])) := by + have h (m : ℕ) : val p fl ((List.range m).foldl + (fun d j => if j = i then d else mul p fl d (sub p fl (v.getD i []) (v.getD j []))) + (one fl)) = ∏ j ∈ (range m).erase i, (val p fl (v.getD i []) - val p fl (v.getD j [])) := by + induction m with + | zero => simp + | succ m ih => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, range_add_one] + by_cases hmi : m = i + · subst hmi + simp only [↓reduceIte] + rw [ih, erase_insert (by simp), Finset.erase_eq_of_notMem (by simp)] + · simp only [hmi, ↓reduceIte] + rw [val_mul, val_sub, ih, erase_insert_of_ne hmi, prod_insert (by simp), mul_comm] + exact h _ + +/-- **Interpolation is the Lagrange formula**, with the computed inverses of the denominators. -/ +theorem pval_interp (v y : List (List ℕ)) : + pval p fl (interp p fl v y) = ∑ i ∈ range v.length, + C (val p fl (y.getD i []) * val p fl (inv p fl (basisDen p fl v i))) * + ∏ j ∈ (range v.length).erase i, (X - C (val p fl (v.getD j []))) := by + have h (m : ℕ) (hm : m ≤ v.length) : pval p fl ((List.range m).foldl (fun P i => + padd p fl P (psmul p fl (mul p fl (y.getD i []) (inv p fl (basisDen p fl v i))) + (basisNum p fl v i))) []) = ∑ i ∈ range m, + C (val p fl (y.getD i []) * val p fl (inv p fl (basisDen p fl v i))) * + ∏ j ∈ (range v.length).erase i, (X - C (val p fl (v.getD j []))) := by + induction m with + | zero => simp [pval] + | succ m ih => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil, sum_range_succ, + pval_padd, ih (by omega), pval_psmul, val_mul, pval_basisNum] + exact h _ le_rfl + +/-- **Interpolation takes the given values** at the nodes, given correct inverses of the +denominators. -/ +theorem eval_pval_interp (v y : List (List ℕ)) + (hinv : ∀ i < v.length, val p fl (basisDen p fl v i) * + val p fl (inv p fl (basisDen p fl v i)) = 1) {k : ℕ} (hk : k < v.length) : + (pval p fl (interp p fl v y)).eval (val p fl (v.getD k [])) = val p fl (y.getD k []) := by + rw [pval_interp v y, eval_finsetSum, sum_eq_single k] + · rw [eval_mul, eval_C, eval_prod] + simp only [eval_sub, eval_X, eval_C] + rw [← val_basisDen, mul_assoc, mul_comm (val p fl (inv p fl _)), hinv k hk, mul_one] + · intro i hi hik + rw [eval_mul, eval_prod, prod_eq_zero (i := k) (mem_erase.mpr ⟨Ne.symm hik, mem_range.mpr hk⟩) + (by simp), mul_zero] + · intro hk' + exact absurd (mem_range.mpr hk) hk' + +/-! ### Sizes -/ + +/-- A coefficient list is *small* when it has `e` coordinates below `2 ^ (p + 1)`: reduced +coordinates and the unit both are. -/ +def Small (p : ℕ) (fl c : List ℕ) : Prop := c.length = fl.length ∧ ∀ a ∈ c, a < 2 ^ (p + 1) + +theorem small_of_lt {c : List ℕ} (hlen : c.length = fl.length) (hlt : ∀ a ∈ c, a < 2 ^ p) : + Small p fl c := + ⟨hlen, fun a ha => (hlt a ha).trans (Nat.pow_lt_pow_right (by norm_num) (by omega))⟩ + +theorem small_add (c d : List ℕ) : Small p fl (add p fl c d) := + small_of_lt (length_add p fl c d) fun _ h => lt_of_mem_add h + +theorem small_mul (c d : List ℕ) : Small p fl (mul p fl c d) := + small_of_lt (length_mul p fl c d) fun _ h => lt_of_mem_mul h + +theorem small_sub (c d : List ℕ) : Small p fl (sub p fl c d) := small_add _ _ + +theorem small_one : Small p fl (one fl) := by + refine ⟨by simp [one], fun a ha => ?_⟩ + simp only [one, List.mem_map, List.mem_range] at ha + obtain ⟨i, -, rfl⟩ := ha + have : 1 < 2 ^ (p + 1) := Nat.one_lt_two_pow (by omega) + split <;> omega + +theorem length_encList_le_of_small {c : List ℕ} (h : Small p fl c) : + (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat c).length ≤ + fl.length * (2 * (p + 1) + 1) := + length_encList_le h.1 h.2 + +/-- A list of small coefficient lists of length at most `n` is at most +`n (2 e (2 p + 3) + 1)` long. -/ +theorem length_encPoly_le {P : List (List ℕ)} {n : ℕ} (hlen : P.length ≤ n) + (h : ∀ c ∈ P, Small p fl c) : + (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) P).length ≤ + n * (2 * (fl.length * (2 * (p + 1) + 1)) + 1) := by + rw [Turing.MultiTapeTM.length_encList] + calc (P.map fun c => 2 * (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat c).length + 1).sum + ≤ (P.map fun c => 2 * (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat c).length + + 1).length • (2 * (fl.length * (2 * (p + 1) + 1)) + 1) := + List.sum_le_length_nsmul _ _ fun m hm => by + obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hm + have := length_encList_le_of_small (h c hc) + omega + _ ≤ n * (2 * (fl.length * (2 * (p + 1) + 1)) + 1) := by + rw [List.length_map, smul_eq_mul] + exact Nat.mul_le_mul_right _ hlen + +@[simp] theorem length_padd (P Q : List (List ℕ)) : + (padd p fl P Q).length = max P.length Q.length := by simp [padd] + +@[simp] theorem length_psmul (c : List ℕ) (P : List (List ℕ)) : + (psmul p fl c P).length = P.length := by simp [psmul] + +@[simp] theorem length_pmulLinear (v : List ℕ) (P : List (List ℕ)) : + (pmulLinear p fl v P).length = P.length + 1 := by simp [pmulLinear] + +theorem small_of_mem_padd {P Q : List (List ℕ)} {c : List ℕ} (h : c ∈ padd p fl P Q) : + Small p fl c := by + obtain ⟨k, -, rfl⟩ := List.mem_map.mp h + exact small_add _ _ + +theorem small_of_mem_psmul {c' : List ℕ} {P : List (List ℕ)} {c : List ℕ} + (h : c ∈ psmul p fl c' P) : Small p fl c := by + obtain ⟨a, -, rfl⟩ := List.mem_map.mp h + exact small_mul _ _ + +theorem small_of_mem_pmulLinear {v : List ℕ} {P : List (List ℕ)} {c : List ℕ} + (h : c ∈ pmulLinear p fl v P) : Small p fl c := by + obtain ⟨k, -, rfl⟩ := List.mem_map.mp h + exact small_sub _ _ + +theorem length_basisNum_le (v : List (List ℕ)) (i : ℕ) : + (basisNum p fl v i).length ≤ v.length + 1 := by + have h (m : ℕ) : ((List.range m).foldl + (fun P j => if j = i then P else pmulLinear p fl (v.getD j []) P) [one fl]).length ≤ + m + 1 := by + induction m with + | zero => simp + | succ m ih => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil] + split + · omega + · rw [length_pmulLinear]; omega + exact h _ + +theorem small_of_mem_basisNum {v : List (List ℕ)} {i : ℕ} {c : List ℕ} + (h : c ∈ basisNum p fl v i) : Small p fl c := by + have key (m : ℕ) : ∀ c ∈ (List.range m).foldl + (fun P j => if j = i then P else pmulLinear p fl (v.getD j []) P) [one fl], Small p fl c := by + induction m with + | zero => simp [small_one] + | succ m ih => + rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil] + split + · exact ih + · exact fun c hc => small_of_mem_pmulLinear hc + exact key _ c h + +/-! ### Polynomial time -/ + +section PolyTime + +open Turing.MultiTapeTM + +variable {α : Type} {encIn : α ↪ List Bool} + +private theorem lengthPolyTime {β : Type} {encB : β ↪ List Bool} {l : α → List β} + (hl : ComputableInPolyTime l encIn (encList encB)) : + ComputableInPolyTime (fun x => (l x).length) encIn encUnary := + (ComputableInPolyTime.length_list encB).comp hl + +private theorem getDPolyTime {P : α → List (List ℕ)} {k : α → ℕ} + (hP : ComputableInPolyTime P encIn (encList (encList encNat))) + (hk : ComputableInPolyTime k encIn encUnary) : + ComputableInPolyTime (fun x => (P x).getD (k x) []) encIn (encList encNat) := + (ComputableInPolyTime.listGetD (encA := encList encNat) []).comp (hP.prod hk) + +/-- **Addition of polynomials is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_padd {p : α → ℕ} {fl : α → List ℕ} {P Q : α → List (List ℕ)} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hP : ComputableInPolyTime P encIn (encList (encList encNat))) + (hQ : ComputableInPolyTime Q encIn (encList (encList encNat))) : + ComputableInPolyTime (fun x => padd (p x) (fl x) (P x) (Q x)) encIn + (encList (encList encNat)) := by + have h1 := ComputableInPolyTime.fst encIn encUnary + have h2 := ComputableInPolyTime.snd encIn encUnary + have hmax : ComputableInPolyTime (fun x => max (P x).length (Q x).length) encIn encUnary := + (ComputableInPolyTime.unary_add' (lengthPolyTime hP) + (ComputableInPolyTime.unary_sub' (lengthPolyTime hQ) (lengthPolyTime hP))).of_enc_eq + fun x => by congr 1; omega + exact ComputableInPolyTime.mapWithInput (ComputableInPolyTime.range.comp hmax) + (computableInPolyTime_add (hp.comp h1) (hfl.comp h1) (getDPolyTime (hP.comp h1) h2) + (getDPolyTime (hQ.comp h1) h2)) + +/-- **Scaling a polynomial is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_psmul {p : α → ℕ} {fl c : α → List ℕ} {P : α → List (List ℕ)} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hc : ComputableInPolyTime c encIn (encList encNat)) + (hP : ComputableInPolyTime P encIn (encList (encList encNat))) : + ComputableInPolyTime (fun x => psmul (p x) (fl x) (c x) (P x)) encIn + (encList (encList encNat)) := by + have h1 := ComputableInPolyTime.fst encIn (encList encNat) + have h2 := ComputableInPolyTime.snd encIn (encList encNat) + exact ComputableInPolyTime.mapWithInput hP + (computableInPolyTime_mul (hp.comp h1) (hfl.comp h1) (hc.comp h1) h2) + +/-- **Multiplication by `z - v` is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_pmulLinear {p : α → ℕ} {fl v : α → List ℕ} + {P : α → List (List ℕ)} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hv : ComputableInPolyTime v encIn (encList encNat)) + (hP : ComputableInPolyTime P encIn (encList (encList encNat))) : + ComputableInPolyTime (fun x => pmulLinear (p x) (fl x) (v x) (P x)) encIn + (encList (encList encNat)) := by + have h1 := ComputableInPolyTime.fst encIn encUnary + have h2 := ComputableInPolyTime.snd encIn encUnary + exact ComputableInPolyTime.mapWithInput (ComputableInPolyTime.range.comp + (ComputableInPolyTime.unary_add' (lengthPolyTime hP) (ComputableInPolyTime.const 1))) + (computableInPolyTime_sub (hp.comp h1) (hfl.comp h1) + (getDPolyTime (ComputableInPolyTime.cons' (ComputableInPolyTime.const []) + (hP.comp h1)) h2) + (computableInPolyTime_mul (hp.comp h1) (hfl.comp h1) (hv.comp h1) + (getDPolyTime (hP.comp h1) h2))) + +private theorem polyBounded_small {p : α → ℕ} {fl : α → List ℕ} {n : α → ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hn : PolyBounded (fun x => (encIn x).length) n) : + PolyBounded (fun x => (encIn x).length) + (fun x => n x * (2 * ((fl x).length * (2 * (p x + 1) + 1)) + 1)) := by + have hpl : PolyBounded (fun x => (encIn x).length) p := by + simpa using (ComputableInPolyTime.polyBounded_length hp) + have hfll : PolyBounded (fun x => (encIn x).length) fun x => (fl x).length := + (lengthPolyTime hfl).polyBounded_length.mono fun x => by simp + exact hn.mul (((PolyBounded.const 2).mul (hfll.mul (((PolyBounded.const 2).mul + (hpl.add (PolyBounded.const 1))).add (PolyBounded.const 1)))).add (PolyBounded.const 1)) + +/-- **Evaluation is polynomial-time**, with the precision in unary. -/ +@[fun_prop] +theorem computableInPolyTime_peval {p : α → ℕ} {fl z : α → List ℕ} {P : α → List (List ℕ)} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hP : ComputableInPolyTime P encIn (encList (encList encNat))) + (hz : ComputableInPolyTime z encIn (encList encNat)) : + ComputableInPolyTime (fun x => peval (p x) (fl x) (P x) (z x)) encIn (encList encNat) := by + simp only [peval, List.foldr_eq_foldl_reverse] + have hstep : ComputableInPolyTime + (fun q : (α × List ℕ) × List ℕ => add (p q.1.1) (fl q.1.1) q.2 (mul (p q.1.1) (fl q.1.1) + (z q.1.1) q.1.2)) (encPair (encPair encIn (encList encNat)) (encList encNat)) + (encList encNat) := by + have hq := ComputableInPolyTime.fst (encPair encIn (encList encNat)) (encList encNat) + have ha := (ComputableInPolyTime.fst encIn (encList encNat)).comp hq + have hacc := (ComputableInPolyTime.snd encIn (encList encNat)).comp hq + have hc := ComputableInPolyTime.snd (encPair encIn (encList encNat)) (encList encNat) + exact computableInPolyTime_add (hp.comp ha) (hfl.comp ha) hc + (computableInPolyTime_mul (hp.comp ha) (hfl.comp ha) (hz.comp ha) hacc) + have hzero : ComputableInPolyTime (fun x => zero (fl x)) encIn (encList encNat) := + computableInPolyTime_tabulate (g := fun _ _ => 0) (lengthPolyTime hfl) + (ComputableInPolyTime.const 0) + exact ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encList encNat) (encL := encList (encList encNat)) + (step := fun x acc a => add (p x) (fl x) a (mul (p x) (fl x) (z x) acc)) hzero + ⟨ComputableInPolyTime.listReverseWithInput hP, hstep, inferInstance, inferInstance⟩ + ⟨(polyBounded_small hp hfl (PolyBounded.const 1)), fun x acc a _ => by + have := length_encList_le_of_small (small_add (p := p x) (fl := fl x) a + (mul (p x) (fl x) (z x) acc)) + omega⟩ + +/-- **Lagrange numerators are polynomial-time**, with the precision and the index in unary. -/ +@[fun_prop] +theorem computableInPolyTime_basisNum {p : α → ℕ} {fl : α → List ℕ} {v : α → List (List ℕ)} + {i : α → ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hv : ComputableInPolyTime v encIn (encList (encList encNat))) + (hi : ComputableInPolyTime i encIn encUnary) : + ComputableInPolyTime (fun x => basisNum (p x) (fl x) (v x) (i x)) encIn + (encList (encList encNat)) := by + let encS := encList (encList encNat) + have hstep : ComputableInPolyTime + (fun q : (α × List (List ℕ)) × ℕ => if q.2 = i q.1.1 then q.1.2 + else pmulLinear (p q.1.1) (fl q.1.1) ((v q.1.1).getD q.2 []) q.1.2) + (encPair (encPair encIn encS) encUnary) encS := by + have hq := ComputableInPolyTime.fst (encPair encIn encS) encUnary + have ha := (ComputableInPolyTime.fst encIn encS).comp hq + have hP := (ComputableInPolyTime.snd encIn encS).comp hq + have hj := ComputableInPolyTime.snd (encPair encIn encS) encUnary + refine (ComputableInPolyTime.ite (ComputableInPolyTime.beq hj (hi.comp ha)) hP + (computableInPolyTime_pmulLinear (hp.comp ha) (hfl.comp ha) (getDPolyTime (hv.comp ha) hj) + hP)).of_enc_eq fun q => ?_ + by_cases h : q.2 = i q.1.1 <;> simp [h] + have hfold := ComputableInPolyTime.foldlWith_spec (encA := encUnary) + (encL := encList encUnary) (par := fun x => x) + (step := fun x P j => if j = i x then P else pmulLinear (p x) (fl x) ((v x).getD j []) P) + ComputableInPolyTime.id' (ComputableInPolyTime.range.comp (lengthPolyTime hv)) + (ComputableInPolyTime.cons' (computableInPolyTime_one hfl) (ComputableInPolyTime.const [])) + hstep (fun x consumed P => P.length ≤ consumed.length + 1 ∧ ∀ c ∈ P, Small (p x) (fl x) c) + (fun x => ⟨by simp, by simp [small_one]⟩) + (fun x consumed P j _ hP => by + refine ⟨?_, ?_⟩ + · simp only [List.length_append, List.length_singleton] + split + · omega + · rw [length_pmulLinear]; omega + · split + · exact hP.2 + · exact fun c hc => small_of_mem_pmulLinear hc) + (polyBounded_small hp hfl ((lengthPolyTime hv).polyBounded_length.add (PolyBounded.const 1))) + (fun x consumed P hpre hP => by + have hlen : consumed.length ≤ (v x).length := by + simpa using hpre.length_le + refine (length_encPoly_le (n := (v x).length + 1) (by omega) hP.2).trans ?_ + simp [encUnary_apply]) + exact hfold.1 + +/-- **Lagrange denominators are polynomial-time**, with the precision and the index in unary. -/ +@[fun_prop] +theorem computableInPolyTime_basisDen {p : α → ℕ} {fl : α → List ℕ} {v : α → List (List ℕ)} + {i : α → ℕ} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hv : ComputableInPolyTime v encIn (encList (encList encNat))) + (hi : ComputableInPolyTime i encIn encUnary) : + ComputableInPolyTime (fun x => basisDen (p x) (fl x) (v x) (i x)) encIn (encList encNat) := by + have hstep : ComputableInPolyTime + (fun q : (α × List ℕ) × ℕ => if q.2 = i q.1.1 then q.1.2 + else mul (p q.1.1) (fl q.1.1) q.1.2 (sub (p q.1.1) (fl q.1.1) ((v q.1.1).getD (i q.1.1) []) + ((v q.1.1).getD q.2 []))) + (encPair (encPair encIn (encList encNat)) encUnary) (encList encNat) := by + have hq := ComputableInPolyTime.fst (encPair encIn (encList encNat)) encUnary + have ha := (ComputableInPolyTime.fst encIn (encList encNat)).comp hq + have hd := (ComputableInPolyTime.snd encIn (encList encNat)).comp hq + have hj := ComputableInPolyTime.snd (encPair encIn (encList encNat)) encUnary + refine (ComputableInPolyTime.ite (ComputableInPolyTime.beq hj (hi.comp ha)) hd + (computableInPolyTime_mul (hp.comp ha) (hfl.comp ha) hd + (computableInPolyTime_sub (hp.comp ha) (hfl.comp ha) + (getDPolyTime (hv.comp ha) (hi.comp ha)) (getDPolyTime (hv.comp ha) hj)))).of_enc_eq + fun q => ?_ + by_cases h : q.2 = i q.1.1 <;> simp [h] + exact ComputableInPolyTime.foldlWithInput_of_bounded_growth + (encA := encUnary) (encL := encList encUnary) + (step := fun x d j => if j = i x then d + else mul (p x) (fl x) d (sub (p x) (fl x) ((v x).getD (i x) []) ((v x).getD j []))) + (computableInPolyTime_one hfl) + ⟨ComputableInPolyTime.range.comp (lengthPolyTime hv), hstep, inferInstance, inferInstance⟩ + ⟨polyBounded_small hp hfl (PolyBounded.const 1), fun x d j _ => by + split + · omega + · have := length_encList_le_of_small (small_mul (p := p x) (fl := fl x) d + (sub (p x) (fl x) ((v x).getD (i x) []) ((v x).getD j []))) + omega⟩ + +/-- **Lagrange interpolation is polynomial-time**, with the precision in unary and the nodes and +values as lists of coefficient lists. -/ +@[fun_prop] +theorem computableInPolyTime_interp {p : α → ℕ} {fl : α → List ℕ} {v y : α → List (List ℕ)} + (hp : ComputableInPolyTime p encIn encUnary) + (hfl : ComputableInPolyTime fl encIn (encList encNat)) + (hv : ComputableInPolyTime v encIn (encList (encList encNat))) + (hy : ComputableInPolyTime y encIn (encList (encList encNat))) : + ComputableInPolyTime (fun x => interp (p x) (fl x) (v x) (y x)) encIn + (encList (encList encNat)) := by + let encS := encList (encList encNat) + have hstep : ComputableInPolyTime + (fun q : (α × List (List ℕ)) × ℕ => padd (p q.1.1) (fl q.1.1) q.1.2 + (psmul (p q.1.1) (fl q.1.1) (mul (p q.1.1) (fl q.1.1) ((y q.1.1).getD q.2 []) + (inv (p q.1.1) (fl q.1.1) (basisDen (p q.1.1) (fl q.1.1) (v q.1.1) q.2))) + (basisNum (p q.1.1) (fl q.1.1) (v q.1.1) q.2))) + (encPair (encPair encIn encS) encUnary) encS := by + have hq := ComputableInPolyTime.fst (encPair encIn encS) encUnary + have ha := (ComputableInPolyTime.fst encIn encS).comp hq + have hP := (ComputableInPolyTime.snd encIn encS).comp hq + have hj := ComputableInPolyTime.snd (encPair encIn encS) encUnary + have hp' := hp.comp ha + have hfl' := hfl.comp ha + exact computableInPolyTime_padd hp' hfl' hP (computableInPolyTime_psmul hp' hfl' + (computableInPolyTime_mul hp' hfl' (getDPolyTime (hy.comp ha) hj) + (computableInPolyTime_inv hp' hfl' + (computableInPolyTime_basisDen hp' hfl' (hv.comp ha) hj))) + (computableInPolyTime_basisNum hp' hfl' (hv.comp ha) hj)) + have hfold := ComputableInPolyTime.foldlWith_spec (encA := encUnary) + (encL := encList encUnary) (par := fun x => x) + (step := fun x P i => padd (p x) (fl x) P + (psmul (p x) (fl x) (mul (p x) (fl x) ((y x).getD i []) (inv (p x) (fl x) + (basisDen (p x) (fl x) (v x) i))) (basisNum (p x) (fl x) (v x) i))) + ComputableInPolyTime.id' (ComputableInPolyTime.range.comp (lengthPolyTime hv)) + (ComputableInPolyTime.const []) hstep + (fun x _ P => P.length ≤ (v x).length + 1 ∧ ∀ c ∈ P, Small (p x) (fl x) c) + (fun x => ⟨by simp, by simp⟩) + (fun x consumed P j _ hP => by + refine ⟨?_, fun c hc => small_of_mem_padd hc⟩ + rw [length_padd, length_psmul] + exact max_le hP.1 (length_basisNum_le _ _)) + (polyBounded_small hp hfl ((lengthPolyTime hv).polyBounded_length.add (PolyBounded.const 1))) + (fun x consumed P _ hP => by + refine (length_encPoly_le hP.1 hP.2).trans ?_ + simp [encUnary_apply]) + exact hfold.1 + +end PolyTime + +end Cslib.GaloisRingArith diff --git a/ComplexityTests/GaloisRingInterpolation.lean b/ComplexityTests/GaloisRingInterpolation.lean new file mode 100644 index 000000000..00e715206 --- /dev/null +++ b/ComplexityTests/GaloisRingInterpolation.lean @@ -0,0 +1,55 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.PolyTime.GaloisRingInterpolation + +/-! # Polynomials over `(ℤ / 2 ^ p)[U] / (f)` and Lagrange interpolation + +Concrete evaluation and interpolation in the Galois ring `(ℤ / 8)[U] / (U ^ 2 + U + 1)`, at the +nodes `0, 1, U`, whose differences `1, U, U - 1` are units; the correctness statements; and the +polynomial-time certificate of interpolation in closed form. -/ + +namespace ComplexityTests.GaloisRingInterpolation + +open Cslib.GaloisRingArith Turing.MultiTapeTM + +/-- The nodes `0, 1, U`. -/ +def nodes : List (List ℕ) := [[0, 0], [1, 0], [0, 1]] + +/-- The values `1, 2, 3 + U`. -/ +def values : List (List ℕ) := [[1, 0], [2, 0], [3, 1]] + +-- Horner evaluation of `1 + U z + z ^ 2` at `z = U`: `1 + U ^ 2 + U ^ 2 = 1 + 2 U ^ 2 = 7 + 6 U`. +example : peval 3 [1, 1] [[1, 0], [0, 1], [1, 0]] [0, 1] = [7, 6] := by decide + +-- `(z - U) (z - 1) = U - (1 + U) z + z ^ 2`, that is `[U, -1 - U, 1]`. +example : pmulLinear 3 [1, 1] [0, 1] [[7, 0], [1, 0]] = [[0, 1], [7, 7], [1, 0]] := by decide + +-- The interpolating polynomial takes the values `1, 2, 3 + U` at `0, 1, U`. +example : (nodes.map fun z => peval 3 [1, 1] (interp 3 [1, 1] nodes values) z) = values := by + decide + +-- It has three coefficients. +example : (interp 3 [1, 1] nodes values).length = 3 := by decide + +/-- Interpolation takes the given values, given correct inverses of the denominators. -/ +example (v y : List (List ℕ)) + (hinv : ∀ i < v.length, val 3 [1, 1] (basisDen 3 [1, 1] v i) * + val 3 [1, 1] (inv 3 [1, 1] (basisDen 3 [1, 1] v i)) = 1) {k : ℕ} (hk : k < v.length) : + (pval 3 [1, 1] (interp 3 [1, 1] v y)).eval (val 3 [1, 1] (v.getD k [])) = + val 3 [1, 1] (y.getD k []) := + eval_pval_interp v y hinv hk + +/-- **Interpolation in polynomial time**, on the ring description `(p, fl)` with `p` in unary, +the nodes and the values. -/ +example : ComputableInPolyTime + (fun q : (ℕ × List ℕ) × (List (List ℕ) × List (List ℕ)) => interp q.1.1 q.1.2 q.2.1 q.2.2) + (encPair (encPair encUnary (encList encNat)) + (encPair (encList (encList encNat)) (encList (encList encNat)))) + (encList (encList encNat)) := by + fun_prop + +end ComplexityTests.GaloisRingInterpolation