Theme/Packed.lean — FrcCore

1import FrcCore.Nat23/-!4# The packed arithmetic of the kernel-decided witnesses — rows as one natural number, no axioms56The first file of the operator theme (6 November 2026). A kernel-decided witness on a cycle of `p` sites or on an7`n × n` matrix over the coefficient field costs the kernel one reduction step per field operation, and the kernel keeps8every intermediate term: the powers of the translation on the 173-cycle, evaluated on lists of field elements, exhausted9six gigabytes (`reports/core-proofs-20261105/execution.md`). Here a row of residues is packed into one natural number with10slots of `W = 48` bits, `pack [a₀, a₁, …] = a₀ + B a₁ + B² a₂ + …` with `B = 2^W`; the product of two packed rows is one11multiplication of natural numbers, which the kernel performs in one step on its big-number representation; the acyclic12convolution of the rows is read off the product's slots, and the cyclic one by adding the high half of the slots to the13low half, one addition more; the residues modulo `p` are taken on unpacking, slot by slot. A product that costs the kernel14`n²` field multiplications on lists costs it about `4n` operations on packed rows, and the memory follows.1516The file states the arithmetic on lists (`aconv`, the acyclic convolution; `cfold`, the cyclic fold; `combo`, a linear17combination of rows — the convolution of a cycle and the rows of a matrix product), the same arithmetic on packed numbers18(`packFold`, `unpack`), and proves them equal: `pack` is linear (`pack_smul`, `pack_addL`), turns the acyclic convolution19into the product (`pack_aconv`) and the cyclic fold into the fold of the number (`packFold_pack`), and `unpack` inverts20`pack` on bounded rows (`unpack_pack`) — the slot bound is the one hypothesis, and the bound of a convolution of residues21is computed (`aconv_bound`, `cfold_bound`). The division algorithm for `/` is proved from the definition of `Nat.div`, as22the base theme proves it for `%`, so that nothing here needs the standard library's division lemmas. No axioms.23-/2425namespace FRC.Dirac.Packed2627/-! ## The division algorithm for `/`, from the definition of `Nat.div` -/28section div2930theorem div_go_fuel {y : Nat} (hy : 0 < y) : ∀ (f1 f2 x : Nat) (h1 : x < f1) (h2 : x < f2),31    Nat.div.go y hy f1 x h1 = Nat.div.go y hy f2 x h2 := by32  intro f133  induction f1 with34  | zero => intro f2 x h1; exact absurd h1 (Nat.not_lt_zero x)35  | succ f1 ih =>36    intro f2 x h1 h237    cases f2 with38    | zero => exact absurd h2 (Nat.not_lt_zero x)39    | succ f2 =>40      show (if h : y ≤ x then Nat.div.go y hy f1 (x - y) _ + 1 else 0)41          = (if h : y ≤ x then Nat.div.go y hy f2 (x - y) _ + 1 else 0)42      exact match Nat.decLe y x with43        | .isTrue h => by rw [dite_eq_left h, dite_eq_left h, ih f2 (x - y) _ _]44        | .isFalse h => by rw [dite_eq_right h, dite_eq_right h]4546theorem div_eq' (x y : Nat) (hy : 0 < y) : x / y = if y ≤ x then (x - y) / y + 1 else 0 := by47  show Nat.div x y = _48  unfold Nat.div49  rw [dite_eq_left hy]50  show (if h : y ≤ x then Nat.div.go y hy x (x - y) _ + 1 else 0) = _51  exact match Nat.decLe y x with52    | .isTrue h => by53        rw [dite_eq_left h, ite_eq_left h]54        show _ = Nat.div (x - y) y + 155        unfold Nat.div56        rw [dite_eq_left hy, div_go_fuel hy x (x - y + 1) (x - y) _ _]57    | .isFalse h => by rw [dite_eq_right h, ite_eq_right h]5859/-- The division algorithm: `x = y (x / y) + x % y`. -/60theorem div_add_mod' (y : Nat) (hy : 0 < y) : ∀ x : Nat, x = y * (x / y) + x % y := by61  intro x62  induction x using Nat.strongRecOn with63  | _ x ih =>64    exact match Nat.decLe y x with65      | .isTrue h => by66          rw [div_eq' x y hy, ite_eq_left h, FRC.Nat.mod_eq_sub_mod hy h, Nat.mul_succ, Nat.add_assoc,67            Nat.add_comm y, ← Nat.add_assoc, ← ih (x - y) (Nat.sub_lt (Nat.lt_of_lt_of_le hy h) hy),68            FRC.Nat.sub_add_cancel h]69      | .isFalse h => by70          rw [div_eq' x y hy, ite_eq_right h, FRC.Nat.mod_eq_of_lt (Nat.lt_of_not_le h), Nat.mul_zero, Nat.zero_add]7172/-- The quotient is determined: `x = y q + r` with `r < y` gives `x / y = q`. -/73theorem div_unique {y x q r : Nat} (hr : r < y) (h : x = y * q + r) : x / y = q :=74  FRC.Nat.quot_unique (Nat.mod_lt x (FRC.Nat.pos_of_lt hr)) hr (by rw [← div_add_mod' y (FRC.Nat.pos_of_lt hr) x, ← h])7576theorem div_eq_of_lt {x y : Nat} (h : x < y) : x / y = 0 :=77  div_unique h (by rw [Nat.mul_zero, Nat.zero_add])7879/-- `(r + y q) / y = q` and `(r + y q) % y = r` for `r < y`. -/80theorem add_mul_div {y q r : Nat} (hr : r < y) : (r + y * q) / y = q :=81  div_unique hr (Nat.add_comm _ _)8283theorem add_mul_mod {y q r : Nat} (hr : r < y) : (r + y * q) % y = r :=84  FRC.Nat.mod_unique hr (Nat.add_comm _ _)8586end div8788/-! ## The slots -/8990/-- The slot width, in bits, and the base `B = 2^W`: a slot holds every residue sum the witnesses form (the bound91`cfold_bound`: `2 n p³ < B` on every standard shell, `2 · 1549⁴ < 2⁴⁸`). -/92def W : Nat := 4893def B : Nat := 2 ^ W9495theorem B_pos : 0 < B := Nat.pow_pos (by decide)9697/-- A row packed into one natural number: `pack [a₀, a₁, …] = a₀ + B (a₁ + B (…))`. -/98def pack : List Nat → Nat99  | [] => 0100  | x :: l => x + B * pack l101102/-- The `k` slots of a natural number, each reduced modulo `p`. -/103def unpack (p : Nat) : Nat → Nat → List Nat104  | 0, _ => []105  | k + 1, P => P % B % p :: unpack p k (P / B)106107/-- The entries of a row are below `B`. -/108def Bounded : List Nat → Prop109  | [] => True110  | x :: l => x < B ∧ Bounded l111112/-- `pack` inverts `unpack` on bounded rows, up to the residues: the slots are the entries modulo `p`. -/113theorem unpack_pack (p : Nat) : ∀ l : List Nat, Bounded l → unpack p l.length (pack l) = l.map (· % p)114  | [], _ => rfl115  | x :: l, ⟨hx, hl⟩ => by116    show (x + B * pack l) % B % p :: unpack p l.length ((x + B * pack l) / B) = x % p :: l.map (· % p)117    rw [add_mul_mod hx, add_mul_div hx, unpack_pack p l hl]118119theorem pack_lt : ∀ l : List Nat, Bounded l → pack l < B ^ l.length120  | [], _ => Nat.lt_succ_self 0121  | x :: l, ⟨hx, hl⟩ => by122    show x + B * pack l < B ^ (l.length + 1)123    have h1 : pack l + 1 ≤ B ^ l.length := pack_lt l hl124    calc x + B * pack l < B + B * pack l := Nat.add_lt_add_right hx _125      _ = B * (pack l + 1) := by rw [Nat.mul_succ, Nat.add_comm]126      _ ≤ B * B ^ l.length := Nat.mul_le_mul_left B h1127      _ = B ^ (l.length + 1) := by rw [FRC.Nat.pow_succ', Nat.mul_comm]128129/-! ## Linearity: scalar multiples, sums and the acyclic convolution -/130131/-- `c · l`, entrywise. -/132def smul (c : Nat) (l : List Nat) : List Nat := l.map (c * ·)133134/-- `u + v`, entrywise, the shorter row padded with zeros. -/135def addL : List Nat → List Nat → List Nat136  | [], v => v137  | u, [] => u138  | x :: u, y :: v => (x + y) :: addL u v139140/-- The acyclic convolution (the product of the rows as polynomials): `(x :: a) * b = x b + (0 :: a * b)`. -/141def aconv : List Nat → List Nat → List Nat142  | [], _ => []143  | x :: a, b => addL (smul x b) (0 :: aconv a b)144145theorem pack_smul (c : Nat) : ∀ l : List Nat, pack (smul c l) = c * pack l146  | [] => by show 0 = c * 0; rw [Nat.mul_zero]147  | x :: l => by148    show c * x + B * pack (smul c l) = c * (x + B * pack l)149    rw [pack_smul c l, Nat.mul_add, FRC.Nat.mul_left_comm]150151theorem pack_addL : ∀ u v : List Nat, pack (addL u v) = pack u + pack v152  | [], v => by show pack v = 0 + pack v; rw [Nat.zero_add]153  | x :: u, [] => by show pack (x :: u) = pack (x :: u) + 0; rw [Nat.add_zero]154  | x :: u, y :: v => by155    show x + y + B * pack (addL u v) = x + B * pack u + (y + B * pack v)156    rw [pack_addL u v, Nat.mul_add, Nat.add_assoc, Nat.add_assoc, Nat.add_left_comm y]157158/-- The product of the packed rows is the packed acyclic convolution. -/159theorem pack_aconv : ∀ a b : List Nat, pack (aconv a b) = pack a * pack b160  | [], b => by show 0 = 0 * pack b; rw [Nat.zero_mul]161  | x :: a, b => by162    show pack (addL (smul x b) (0 :: aconv a b)) = (x + B * pack a) * pack b163    rw [pack_addL, pack_smul]164    show x * pack b + (0 + B * pack (aconv a b)) = _165    rw [Nat.zero_add, pack_aconv a b, Nat.add_mul, Nat.mul_assoc]166167/-! ## The cyclic fold -/168169/-- The cyclic fold of a row of `2n − 1` (or `2n`) entries to `n`: the high half added to the low half, the170convolution on the cycle of `n` sites from the acyclic one. -/171def cfold (n : Nat) (c : List Nat) : List Nat := addL (c.take n) (c.drop n)172173/-- The same on a packed row: the high slots are `P / Bⁿ`, the low ones `P % Bⁿ`. -/174def packFold (n P : Nat) : Nat := P % B ^ n + P / B ^ n175176theorem pack_take_drop : ∀ (n : Nat) (c : List Nat), pack c = pack (c.take n) + B ^ n * pack (c.drop n)177  | 0, c => by show pack c = 0 + 1 * pack c; rw [Nat.zero_add, Nat.one_mul]178  | n + 1, [] => by show 0 = 0 + B ^ (n + 1) * 0; rw [Nat.mul_zero]179  | n + 1, x :: c => by180    show x + B * pack c = x + B * pack (c.take n) + B ^ (n + 1) * pack (c.drop n)181    rw [pack_take_drop n c, Nat.mul_add, Nat.add_assoc, FRC.Nat.pow_succ', Nat.mul_comm (B ^ n) B, Nat.mul_assoc]182183theorem bounded_take : ∀ (n : Nat) (c : List Nat), Bounded c → Bounded (c.take n)184  | 0, _, _ => trivial185  | _ + 1, [], _ => trivial186  | n + 1, _ :: c, ⟨hx, hc⟩ => ⟨hx, bounded_take n c hc⟩187188theorem length_take_le : ∀ (n : Nat) (c : List Nat), (c.take n).length ≤ n189  | 0, _ => Nat.le_refl 0190  | _ + 1, [] => Nat.zero_le _191  | n + 1, _ :: c => Nat.succ_le_succ (length_take_le n c)192193theorem pow_le_pow_of_le {m n : Nat} (h : m ≤ n) : B ^ m ≤ B ^ n := by194  obtain ⟨k, rfl⟩ : ∃ k, n = m + k := ⟨n - m, by rw [Nat.add_comm, FRC.Nat.sub_add_cancel h]⟩195  rw [FRC.Nat.pow_add]196  exact Nat.le_mul_of_pos_right _ (Nat.pow_pos B_pos)197198/-- The fold of the packed row is the packed fold, for a bounded row. -/199theorem packFold_pack (n : Nat) (c : List Nat) (hc : Bounded c) : packFold n (pack c) = pack (cfold n c) := by200  have hlt : pack (c.take n) < B ^ n :=201    Nat.lt_of_lt_of_le (pack_lt _ (bounded_take n c hc)) (pow_le_pow_of_le (length_take_le n c))202  show pack c % B ^ n + pack c / B ^ n = pack (addL (c.take n) (c.drop n))203  rw [pack_addL, pack_take_drop n c, add_mul_mod hlt, add_mul_div hlt]204205/-! ## The combination of rows (the rows of a matrix product) -/206207/-- `Σ_k c_k · r_k`: a row of the product of a matrix with the rows `r` is the combination of the rows by the entries. -/208def combo : List Nat → List (List Nat) → List Nat209  | [], _ => []210  | _, [] => []211  | c :: cs, r :: rs => addL (smul c r) (combo cs rs)212213/-- The same on packed rows. -/214def packCombo : List Nat → List Nat → Nat215  | [], _ => 0216  | _, [] => 0217  | c :: cs, P :: Ps => c * P + packCombo cs Ps218219theorem pack_combo : ∀ (cs : List Nat) (rs : List (List Nat)), pack (combo cs rs) = packCombo cs (rs.map pack)220  | [], _ => rfl221  | _ :: _, [] => rfl222  | c :: cs, r :: rs => by223    show pack (addL (smul c r) (combo cs rs)) = c * pack r + packCombo cs (rs.map pack)224    rw [pack_addL, pack_smul, pack_combo cs rs]225226/-! ## The bounds -/227228/-- The entries of a row are below `m`. -/229def Below (m : Nat) : List Nat → Prop230  | [] => True231  | x :: l => x < m ∧ Below m l232233theorem below_mono {m m' : Nat} (h : m ≤ m') : ∀ l, Below m l → Below m' l234  | [], _ => trivial235  | _ :: l, ⟨hx, hl⟩ => ⟨Nat.lt_of_lt_of_le hx h, below_mono h l hl⟩236237/-- The entries of `u + v` are below `m + m'` when those of `u` are below `m` and those of `v` below `m'`238(`0 < m`, `0 < m'` for the padded tails). -/239theorem below_addL {m m' : Nat} (hm : 0 < m) (hm' : 0 < m') :240    ∀ u v, Below m u → Below m' v → Below (m + m') (addL u v)241  | [], v, _, hv => below_mono (Nat.le_add_left m' m) v hv242  | _ :: _, [], hu, _ => below_mono (Nat.le_add_right m m') _ hu243  | _ :: u, _ :: v, ⟨hx, hu⟩, ⟨hy, hv⟩ => ⟨Nat.add_lt_add hx hy, below_addL hm hm' u v hu hv⟩244245theorem below_smul {c m m' : Nat} (hc : c < m) : ∀ l, Below m' l → Below (m * m') (smul c l)246  | [], _ => trivial247  | _ :: l, ⟨hx, hl⟩ => ⟨Nat.mul_lt_mul_of_lt_of_lt hc hx, below_smul hc l hl⟩248249theorem below_zero_cons {m : Nat} (hm : 0 < m) {l : List Nat} (h : Below m l) : Below m (0 :: l) := ⟨hm, h⟩250251/-- The acyclic convolution of two rows of residues below `p`, the first of `k` entries, has entries below `k p²`. -/252theorem aconv_bound {p : Nat} (hp : 0 < p) : ∀ (a b : List Nat), Below p a → Below p b →253    Below (a.length * (p * p) + 1) (aconv a b)254  | [], _, _, _ => trivial255  | x :: a, b, ⟨hx, ha⟩, hb => by256    show Below ((a.length + 1) * (p * p) + 1) (addL (smul x b) (0 :: aconv a b))257    have h1 : Below (p * p) (smul x b) := below_smul hx b hb258    have h2 : Below (a.length * (p * p) + 1) (0 :: aconv a b) :=259      below_zero_cons (Nat.succ_pos _) (aconv_bound hp a b ha hb)260    have := below_addL (Nat.mul_pos hp hp) (Nat.succ_pos _) _ _ h1 h2261    rw [Nat.succ_mul, Nat.add_comm (a.length * (p * p)) (p * p), Nat.add_assoc]262    exact this263264theorem below_take {m : Nat} : ∀ (n : Nat) (c : List Nat), Below m c → Below m (c.take n)265  | 0, _, _ => trivial266  | _ + 1, [], _ => trivial267  | n + 1, _ :: c, ⟨hx, hc⟩ => ⟨hx, below_take n c hc⟩268269theorem below_drop {m : Nat} : ∀ (n : Nat) (c : List Nat), Below m c → Below m (c.drop n)270  | 0, _, h => h271  | _ + 1, [], _ => trivial272  | n + 1, _ :: c, ⟨_, hc⟩ => below_drop n c hc273274/-- The cyclic fold of a row with entries below `m` has entries below `2m`. -/275theorem cfold_bound {m : Nat} (hm : 0 < m) (n : Nat) (c : List Nat) (h : Below m c) : Below (m + m) (cfold n c) :=276  below_addL hm hm _ _ (below_take n c h) (below_drop n c h)277278theorem bounded_of_below {m : Nat} (hm : m ≤ B) : ∀ l, Below m l → Bounded l279  | [], _ => trivial280  | _ :: l, ⟨hx, hl⟩ => ⟨Nat.lt_of_lt_of_le hx hm, bounded_of_below hm l hl⟩281282/-! ## The cyclic convolution of residues: the list form, the packed form, and their equality -/283284/-- The cyclic convolution of two rows of residues on the cycle of `n` sites, reduced modulo `p`: the list form. -/285def cycList (p n : Nat) (a b : List Nat) : List Nat := (cfold n (aconv a b)).map (· % p)286287/-- The packed form: one product, one fold, `n` slots. -/288def cycPacked (p n : Nat) (A C : Nat) : List Nat := unpack p n (packFold n (A * C))289290theorem length_addL_left : ∀ u v : List Nat, v.length ≤ u.length → (addL u v).length = u.length291  | [], [], _ => rfl292  | [], _ :: _, h => absurd h (Nat.not_succ_le_zero _)293  | _ :: _, [], _ => rfl294  | _ :: u, _ :: v, h => by295    show (addL u v).length + 1 = u.length + 1296    rw [length_addL_left u v (Nat.le_of_succ_le_succ h)]297298theorem length_addL_right : ∀ u v : List Nat, u.length ≤ v.length → (addL u v).length = v.length299  | [], _, _ => rfl300  | _ :: _, [], h => absurd h (Nat.not_succ_le_zero _)301  | _ :: u, _ :: v, h => by302    show (addL u v).length + 1 = v.length + 1303    rw [length_addL_right u v (Nat.le_of_succ_le_succ h)]304305theorem length_smul (c : Nat) : ∀ l : List Nat, (smul c l).length = l.length306  | [] => rfl307  | _ :: l => by show (smul c l).length + 1 = l.length + 1; rw [length_smul c l]308309/-- `|a * b| + 1 = |a| + |b|` for nonempty rows. -/310theorem length_aconv : ∀ a b : List Nat, 0 < a.length → 0 < b.length → (aconv a b).length + 1 = a.length + b.length311  | [], _, h, _ => absurd h (Nat.lt_irrefl 0)312  | [x], b, _, hb => by313    show (addL (smul x b) (0 :: aconv [] b)).length + 1 = 1 + b.length314    rw [length_addL_left _ _ (by rw [length_smul]; exact hb), length_smul, Nat.add_comm]315  | x :: y :: a, b, _, hb => by316    show (addL (smul x b) (0 :: aconv (y :: a) b)).length + 1 = a.length + 1 + 1 + b.length317    have ih := length_aconv (y :: a) b (Nat.succ_pos _) hb318    have hle : (smul x b).length ≤ (0 :: aconv (y :: a) b).length := by319      show (smul x b).length ≤ (aconv (y :: a) b).length + 1320      rw [length_smul, ih]; exact Nat.le_add_left _ _321    rw [length_addL_right _ _ hle]322    show (aconv (y :: a) b).length + 1 + 1 = a.length + 1 + 1 + b.length323    rw [ih]; show a.length + 1 + b.length + 1 = _; rw [Nat.add_right_comm]324325theorem length_take_of_le : ∀ (n : Nat) (c : List Nat), n ≤ c.length → (c.take n).length = n326  | 0, _, _ => rfl327  | _ + 1, [], h => absurd h (Nat.not_succ_le_zero _)328  | n + 1, _ :: c, h => by show (c.take n).length + 1 = n + 1; rw [length_take_of_le n c (Nat.le_of_succ_le_succ h)]329330theorem length_drop : ∀ (n : Nat) (c : List Nat), (c.drop n).length = c.length - n331  | 0, _ => rfl332  | n + 1, [] => by show 0 = 0 - (n + 1); rw [Nat.zero_sub]333  | n + 1, _ :: c => by show (c.drop n).length = c.length + 1 - (n + 1); rw [length_drop n c, Nat.succ_sub_succ]334335/-- The fold of a row of `2n − 1` entries has `n` entries. -/336theorem length_cfold (n : Nat) (c : List Nat) (hc : c.length + 1 = n + n) : (cfold n c).length = n := by337  have hn : n ≤ c.length := by338    have : n + 1 ≤ c.length + 1 := by339      rw [hc]340      cases n with341      | zero => exact absurd hc (by rw [Nat.add_zero]; exact Nat.succ_ne_zero _)342      | succ n => exact Nat.succ_le_succ (Nat.le_add_right (n + 1) n)343    exact Nat.le_of_succ_le_succ this344  have hd : (c.drop n).length ≤ (c.take n).length := by345    rw [length_drop, length_take_of_le n c hn]346    have e : c.length = n + (n - 1) := by347      cases n with348      | zero => exact absurd hc (by rw [Nat.add_zero]; exact Nat.succ_ne_zero _)349      | succ n =>350        have : c.length + 1 = n + 1 + (n + 1 - 1) + 1 := by rw [hc, Nat.add_sub_cancel]; rfl351        exact Nat.succ.inj this352    rw [e, FRC.Nat.add_sub_cancel_left]353    exact Nat.sub_le n 1354  show (addL (c.take n) (c.drop n)).length = n355  rw [length_addL_left _ _ hd, length_take_of_le n c hn]356357/-- The packed cyclic convolution of rows of residues below `p`, each of `n` entries, is the list form, when358`2 n p² ≤ B`: the one bound of the method. -/359theorem cycPacked_eq (p n : Nat) (hp : 0 < p) (hn : 0 < n) (a b : List Nat) (ha : Below p a) (hb : Below p b)360    (la : a.length = n) (lb : b.length = n) (hB : 2 * (n * (p * p) + 1) ≤ B) :361    cycPacked p n (pack a) (pack b) = cycList p n a b := by362  have hc : Below (n * (p * p) + 1) (aconv a b) := la ▸ aconv_bound hp a b ha hb363  have hf : Below (n * (p * p) + 1 + (n * (p * p) + 1)) (cfold n (aconv a b)) :=364    cfold_bound (Nat.succ_pos _) n _ hc365  have hB' : n * (p * p) + 1 + (n * (p * p) + 1) ≤ B := by rw [← Nat.two_mul]; exact hB366  have hbnd : Bounded (cfold n (aconv a b)) := bounded_of_below hB' _ hf367  have hbndc : Bounded (aconv a b) :=368    bounded_of_below (Nat.le_trans (Nat.le_add_right _ _) hB') _ hc369  have hlen : (cfold n (aconv a b)).length = n :=370    length_cfold n _ (by rw [length_aconv a b (la ▸ hn) (lb ▸ hn), la, lb])371  show unpack p n (packFold n (pack a * pack b)) = (cfold n (aconv a b)).map (· % p)372  rw [← pack_aconv, packFold_pack n _ hbndc, ← unpack_pack p _ hbnd, hlen]373374/-! ## Rows over the quadratic extension: pairs of rows of residues -/375376/-- The cyclic convolution over `K = 𝔽_p(√ν)` on the cycle of `n` sites, the list form: with `a = a₁ + a₂ w` and377`b = b₁ + b₂ w` (rows of residues), `ab = (a₁b₁ + ν a₂b₂) + (a₁b₂ + a₂b₁) w`. -/378def cycExtList (p ν n : Nat) (a b : List Nat × List Nat) : List Nat × List Nat :=379  ((cfold n (addL (aconv a.1 b.1) (smul ν (aconv a.2 b.2)))).map (· % p),380   (cfold n (addL (aconv a.1 b.2) (aconv a.2 b.1))).map (· % p))381382/-- The packed form: four products of natural numbers, two folds, `2n` slots. -/383def cycExtPacked (p ν n : Nat) (A C : Nat × Nat) : List Nat × List Nat :=384  (unpack p n (packFold n (A.1 * C.1 + ν * (A.2 * C.2))), unpack p n (packFold n (A.1 * C.2 + A.2 * C.1)))385386/-- A pair of rows of residues below `p`, each of `n` entries. -/387def Row (p n : Nat) (a : List Nat × List Nat) : Prop :=388  Below p a.1 ∧ Below p a.2 ∧ a.1.length = n ∧ a.2.length = n389390theorem length_aconv' {n : Nat} (hn : 0 < n) {a b : List Nat} (la : a.length = n) (lb : b.length = n) :391    (aconv a b).length + 1 = n + n := by rw [length_aconv a b (la ▸ hn) (lb ▸ hn), la, lb]392393theorem length_smul_aconv {n : Nat} (hn : 0 < n) (c : Nat) {a b : List Nat} (la : a.length = n) (lb : b.length = n) :394    (smul c (aconv a b)).length + 1 = n + n := by rw [length_smul, length_aconv' hn la lb]395396theorem length_addL_eq {u v : List Nat} {k : Nat} (hu : u.length = k) (hv : v.length = k) : (addL u v).length = k := by397  rw [length_addL_left u v (by rw [hu, hv]; exact Nat.le_refl k), hu]398399theorem length_addL_eq' {u v : List Nat} {m : Nat} (hu : u.length + 1 = m) (hv : v.length + 1 = m) :400    (addL u v).length + 1 = m := by401  have e : v.length = u.length := Nat.succ.inj (hv.trans hu.symm)402  rw [length_addL_left u v (e ▸ Nat.le_refl _), hu]403404/-- The bound of a term `aconv` or `ν · aconv`: below `p (n p² + 1)`. -/405theorem below_aconv_term {p ν n : Nat} (hp : 0 < p) (hν : ν < p) {a b : List Nat} (ha : Below p a) (hb : Below p b)406    (la : a.length = n) : Below (p * (n * (p * p) + 1)) (smul ν (aconv a b)) :=407  below_smul hν _ (la ▸ aconv_bound hp a b ha hb)408409theorem below_aconv_one {p n : Nat} (hp : 0 < p) {a b : List Nat} (ha : Below p a) (hb : Below p b)410    (la : a.length = n) : Below (p * (n * (p * p) + 1)) (aconv a b) :=411  below_mono (Nat.le_mul_of_pos_left _ hp) _ (la ▸ aconv_bound hp a b ha hb)412413/-- The packed cyclic convolution over `K` of two rows is the list form, when `4 p (n p² + 1) ≤ B`: the one bound of414the method on the extension. -/415theorem cycExtPacked_eq (p ν n : Nat) (hp : 0 < p) (hν : ν < p) (hn : 0 < n) (a b : List Nat × List Nat)416    (ha : Row p n a) (hb : Row p n b) (hB : 4 * (p * (n * (p * p) + 1)) ≤ B) :417    cycExtPacked p ν n (pack a.1, pack a.2) (pack b.1, pack b.2) = cycExtList p ν n a b := by418  obtain ⟨ha1, ha2, la1, la2⟩ := ha419  obtain ⟨hb1, hb2, lb1, lb2⟩ := hb420  have hm : 0 < p * (n * (p * p) + 1) := Nat.mul_pos hp (Nat.succ_pos _)421  have h2 : p * (n * (p * p) + 1) + p * (n * (p * p) + 1) + (p * (n * (p * p) + 1) + p * (n * (p * p) + 1)) ≤ B := by422    have e : 4 * (p * (n * (p * p) + 1)) =423        p * (n * (p * p) + 1) + p * (n * (p * p) + 1) + (p * (n * (p * p) + 1) + p * (n * (p * p) + 1)) := by424      rw [show (4 : Nat) = 2 + 2 from rfl, Nat.add_mul, Nat.two_mul]425    rw [← e]; exact hB426  have hhalf : p * (n * (p * p) + 1) + p * (n * (p * p) + 1) ≤ B :=427    Nat.le_trans (Nat.le_add_right _ _) h2428  -- the real part429  have hre : Below (p * (n * (p * p) + 1) + p * (n * (p * p) + 1))430      (addL (aconv a.1 b.1) (smul ν (aconv a.2 b.2))) :=431    below_addL hm hm _ _ (below_aconv_one hp ha1 hb1 la1) (below_aconv_term hp hν ha2 hb2 la2)432  have lre : (addL (aconv a.1 b.1) (smul ν (aconv a.2 b.2))).length + 1 = n + n :=433    length_addL_eq' (length_aconv' hn la1 lb1) (length_smul_aconv hn ν la2 lb2)434  have him : Below (p * (n * (p * p) + 1) + p * (n * (p * p) + 1)) (addL (aconv a.1 b.2) (aconv a.2 b.1)) :=435    below_addL hm hm _ _ (below_aconv_one hp ha1 hb2 la1) (below_aconv_one hp ha2 hb1 la2)436  have lim : (addL (aconv a.1 b.2) (aconv a.2 b.1)).length + 1 = n + n :=437    length_addL_eq' (length_aconv' hn la1 lb2) (length_aconv' hn la2 lb1)438  show (unpack p n (packFold n (pack a.1 * pack b.1 + ν * (pack a.2 * pack b.2))),439      unpack p n (packFold n (pack a.1 * pack b.2 + pack a.2 * pack b.1))) =440    ((cfold n (addL (aconv a.1 b.1) (smul ν (aconv a.2 b.2)))).map (· % p),441     (cfold n (addL (aconv a.1 b.2) (aconv a.2 b.1))).map (· % p))442  rw [← pack_aconv, ← pack_aconv, ← pack_aconv, ← pack_aconv, ← pack_smul, ← pack_addL, ← pack_addL,443    packFold_pack n _ (bounded_of_below hhalf _ hre), packFold_pack n _ (bounded_of_below hhalf _ him),444    ← unpack_pack p _ (bounded_of_below h2 _ (cfold_bound (Nat.add_pos_left hm _) n _ hre)), length_cfold n _ lre,445    ← unpack_pack p _ (bounded_of_below h2 _ (cfold_bound (Nat.add_pos_left hm _) n _ him)), length_cfold n _ lim]446447/-! ## The rows kept packed: the slot-wise reduction by halving -/448449/-- The slot-wise reduction modulo `p` of a packed row of at most sixteen slots, written out: the kernel evaluates450these sixteen quotients and residues without unfolding a recursion (`leaf16_eq`: it is `pack (unpack p 16 P)`). -/451def leaf16 (p P : Nat) : Nat :=452  let P1 := P / B453  let P2 := P1 / B454  let P3 := P2 / B455  let P4 := P3 / B456  let P5 := P4 / B457  let P6 := P5 / B458  let P7 := P6 / B459  let P8 := P7 / B460  let P9 := P8 / B461  let P10 := P9 / B462  let P11 := P10 / B463  let P12 := P11 / B464  let P13 := P12 / B465  let P14 := P13 / B466  let P15 := P14 / B467  P % B % p + B * (P1 % B % p + B * (P2 % B % p + B * (P3 % B % p + B * (P4 % B % p + B * (P5 % B % p + B * (P6 % B % p + B * (P7 % B % p + B * (P8 % B % p + B * (P9 % B % p + B * (P10 % B % p + B * (P11 % B % p + B * (P12 % B % p + B * (P13 % B % p + B * (P14 % B % p + B * (P15 % B % p + B * 0)))))))))))))))468469theorem leaf16_eq (p P : Nat) : leaf16 p P = pack (unpack p 16 P) := rfl470471/-- The slot-wise reduction modulo `p` of a packed row of at most `16 · 2^k` slots, by halving down to the leaves of472sixteen slots: the low and the high halves reduced and reassembled. A row stays packed between the products this473way; the slot-by-slot chain of `unpack` and `pack` would hold `n` growing numbers at a time, and the kernel, which474keeps every reduction step, would hold them all. -/475def repack (p : Nat) : Nat → Nat → Nat476  | 0, P => leaf16 p P477  | k + 1, P => repack p k (P % B ^ (16 * 2 ^ k)) + B ^ (16 * 2 ^ k) * repack p k (P / B ^ (16 * 2 ^ k))478479theorem bounded_drop : ∀ (n : Nat) (c : List Nat), Bounded c → Bounded (c.drop n)480  | 0, _, h => h481  | _ + 1, [], _ => trivial482  | n + 1, _ :: c, ⟨_, hc⟩ => bounded_drop n c hc483484theorem map_take (f : Nat → Nat) : ∀ (n : Nat) (l : List Nat), (l.take n).map f = (l.map f).take n485  | 0, _ => rfl486  | _ + 1, [] => rfl487  | n + 1, x :: l => by show f x :: (l.take n).map f = f x :: (l.map f).take n; rw [map_take f n l]488489theorem map_drop (f : Nat → Nat) : ∀ (n : Nat) (l : List Nat), (l.drop n).map f = (l.map f).drop n490  | 0, _ => rfl491  | _ + 1, [] => rfl492  | n + 1, _ :: l => map_drop f n l493494theorem pack_unpack_zero (p : Nat) : ∀ k : Nat, pack (unpack p k 0) = 0495  | 0 => rfl496  | k + 1 => by497    show 0 % B % p + B * pack (unpack p k (0 / B)) = 0498    rw [Nat.zero_mod, Nat.zero_mod, div_eq_of_lt B_pos, pack_unpack_zero p k, Nat.mul_zero]499500/-- `unpack_pack` with spare slots: the slots past the row are zero and do not change the packed value. -/501theorem pack_unpack_pack (p : Nat) : ∀ (l : List Nat) (k : Nat), Bounded l → l.length ≤ k →502    pack (unpack p k (pack l)) = pack (l.map (· % p))503  | [], k, _, _ => pack_unpack_zero p k504  | _ :: _, 0, _, h => absurd h (Nat.not_succ_le_zero _)505  | x :: l, k + 1, ⟨hx, hl⟩, h => by506    show (x + B * pack l) % B % p + B * pack (unpack p k ((x + B * pack l) / B)) = x % p + B * pack (l.map (· % p))507    rw [add_mul_mod hx, add_mul_div hx, pack_unpack_pack p l k hl (Nat.le_of_succ_le_succ h)]508509/-- `repack` is the packed slot-wise reduction: on a bounded row of at most `16 · 2^k` entries, the packed row of510the residues. -/511theorem repack_pack (p : Nat) : ∀ (k : Nat) (l : List Nat), Bounded l → l.length ≤ 16 * 2 ^ k →512    repack p k (pack l) = pack (l.map (· % p))513  | 0, l, hl, hlen => by514    show leaf16 p (pack l) = _515    rw [leaf16_eq]; exact pack_unpack_pack p l 16 hl hlen516  | k + 1, l, hl, hlen => by517    have hm : pack (l.take (16 * 2 ^ k)) < B ^ (16 * 2 ^ k) :=518      Nat.lt_of_lt_of_le (pack_lt _ (bounded_take _ l hl)) (pow_le_pow_of_le (length_take_le _ l))519    have h2 : (l.drop (16 * 2 ^ k)).length ≤ 16 * 2 ^ k := by520      rw [length_drop]521      rw [Nat.pow_succ, ← Nat.mul_assoc, Nat.mul_two] at hlen522      exact Nat.le_trans (Nat.sub_le_sub_right hlen _) (by rw [FRC.Nat.add_sub_cancel]; exact Nat.le_refl _)523    show repack p k (pack l % B ^ (16 * 2 ^ k)) + B ^ (16 * 2 ^ k) * repack p k (pack l / B ^ (16 * 2 ^ k)) =524      pack (l.map (· % p))525    rw [pack_take_drop (16 * 2 ^ k) l, add_mul_mod hm, add_mul_div hm,526      repack_pack p k _ (bounded_take _ l hl) (length_take_le _ l), repack_pack p k _ (bounded_drop _ l hl) h2,527      pack_take_drop (16 * 2 ^ k) (l.map (· % p)), map_take, map_drop]528529/-- The product on the cycle of two packed real rows (rows of residues), the result reduced slot-wise on530`16 · 2^k ≥ n` slots: one product, one fold, one reduction. -/531def rmul (p n k : Nat) (A C : Nat) : Nat := repack p k (packFold n (A * C))532533/-- `rmul` is the packed `cycList`, under the bound of `cycPacked_eq` and `n ≤ 16 · 2^k`. -/534theorem rmul_eq (p n k : Nat) (hp : 0 < p) (hn : 0 < n) (a b : List Nat) (ha : Below p a) (hb : Below p b)535    (la : a.length = n) (lb : b.length = n) (hB : 2 * (n * (p * p) + 1) ≤ B) (hk : n ≤ 16 * 2 ^ k) :536    rmul p n k (pack a) (pack b) = pack (cycList p n a b) := by537  have hc : Below (n * (p * p) + 1) (aconv a b) := la ▸ aconv_bound hp a b ha hb538  have hf : Below (n * (p * p) + 1 + (n * (p * p) + 1)) (cfold n (aconv a b)) :=539    cfold_bound (Nat.succ_pos _) n _ hc540  have hB' : n * (p * p) + 1 + (n * (p * p) + 1) ≤ B := by rw [← Nat.two_mul]; exact hB541  have hbndc : Bounded (aconv a b) :=542    bounded_of_below (Nat.le_trans (Nat.le_add_right _ _) hB') _ hc543  have hlen : (cfold n (aconv a b)).length = n :=544    length_cfold n _ (by rw [length_aconv a b (la ▸ hn) (lb ▸ hn), la, lb])545  show repack p k (packFold n (pack a * pack b)) = pack ((cfold n (aconv a b)).map (· % p))546  rw [← pack_aconv, packFold_pack n _ hbndc]547  exact repack_pack p k _ (bounded_of_below hB' _ hf) (by rw [hlen]; exact hk)548549/-- The product on the cycle over `K` of two packed rows, the result reduced slot-wise on `16 · 2^k ≥ n` slots: four550products, two folds, two reductions, and the rows stay packed. -/551def pmul (p ν n k : Nat) (A C : Nat × Nat) : Nat × Nat :=552  (repack p k (packFold n (A.1 * C.1 + ν * (A.2 * C.2))), repack p k (packFold n (A.1 * C.2 + A.2 * C.1)))553554/-- `pmul` is the packed `cycExtList`, under the bound of `cycExtPacked_eq` and `n ≤ 16 · 2^k`. -/555theorem pmul_eq (p ν n k : Nat) (hp : 0 < p) (hν : ν < p) (hn : 0 < n) (a b : List Nat × List Nat)556    (ha : Row p n a) (hb : Row p n b) (hB : 4 * (p * (n * (p * p) + 1)) ≤ B) (hk : n ≤ 16 * 2 ^ k) :557    pmul p ν n k (pack a.1, pack a.2) (pack b.1, pack b.2) =558      (pack (cycExtList p ν n a b).1, pack (cycExtList p ν n a b).2) := by559  obtain ⟨ha1, ha2, la1, la2⟩ := ha560  obtain ⟨hb1, hb2, lb1, lb2⟩ := hb561  have hm : 0 < p * (n * (p * p) + 1) := Nat.mul_pos hp (Nat.succ_pos _)562  have h2 : p * (n * (p * p) + 1) + p * (n * (p * p) + 1) + (p * (n * (p * p) + 1) + p * (n * (p * p) + 1)) ≤ B := by563    have e : 4 * (p * (n * (p * p) + 1)) =564        p * (n * (p * p) + 1) + p * (n * (p * p) + 1) + (p * (n * (p * p) + 1) + p * (n * (p * p) + 1)) := by565      rw [show (4 : Nat) = 2 + 2 from rfl, Nat.add_mul, Nat.two_mul]566    rw [← e]; exact hB567  have hhalf : p * (n * (p * p) + 1) + p * (n * (p * p) + 1) ≤ B :=568    Nat.le_trans (Nat.le_add_right _ _) h2569  have hre : Below (p * (n * (p * p) + 1) + p * (n * (p * p) + 1))570      (addL (aconv a.1 b.1) (smul ν (aconv a.2 b.2))) :=571    below_addL hm hm _ _ (below_aconv_one hp ha1 hb1 la1) (below_aconv_term hp hν ha2 hb2 la2)572  have lre : (addL (aconv a.1 b.1) (smul ν (aconv a.2 b.2))).length + 1 = n + n :=573    length_addL_eq' (length_aconv' hn la1 lb1) (length_smul_aconv hn ν la2 lb2)574  have him : Below (p * (n * (p * p) + 1) + p * (n * (p * p) + 1)) (addL (aconv a.1 b.2) (aconv a.2 b.1)) :=575    below_addL hm hm _ _ (below_aconv_one hp ha1 hb2 la1) (below_aconv_one hp ha2 hb1 la2)576  have lim : (addL (aconv a.1 b.2) (aconv a.2 b.1)).length + 1 = n + n :=577    length_addL_eq' (length_aconv' hn la1 lb2) (length_aconv' hn la2 lb1)578  show (repack p k (packFold n (pack a.1 * pack b.1 + ν * (pack a.2 * pack b.2))),579      repack p k (packFold n (pack a.1 * pack b.2 + pack a.2 * pack b.1))) =580    (pack ((cfold n (addL (aconv a.1 b.1) (smul ν (aconv a.2 b.2)))).map (· % p)),581     pack ((cfold n (addL (aconv a.1 b.2) (aconv a.2 b.1))).map (· % p)))582  rw [← pack_aconv, ← pack_aconv, ← pack_aconv, ← pack_aconv, ← pack_smul, ← pack_addL, ← pack_addL,583    packFold_pack n _ (bounded_of_below hhalf _ hre), packFold_pack n _ (bounded_of_below hhalf _ him),584    repack_pack p k _ (bounded_of_below h2 _ (cfold_bound (Nat.add_pos_left hm _) n _ hre))585      (by rw [length_cfold n _ lre]; exact hk),586    repack_pack p k _ (bounded_of_below h2 _ (cfold_bound (Nat.add_pos_left hm _) n _ him))587      (by rw [length_cfold n _ lim]; exact hk)]588589/-- The sum of two packed rows, reduced slot-wise. -/590def padd (p k : Nat) (A C : Nat) : Nat := repack p k (A + C)591592theorem padd_eq (p k : Nat) (hp : 0 < p) (a b : List Nat) (ha : Below p a) (hb : Below p b) (la : a.length ≤ 16 * 2 ^ k)593    (hab : b.length ≤ a.length) (hB : p + p ≤ B) : padd p k (pack a) (pack b) = pack ((addL a b).map (· % p)) := by594  show repack p k (pack a + pack b) = _595  rw [← pack_addL]596  exact repack_pack p k _ (bounded_of_below hB _ (below_addL hp hp a b ha hb))597    (by rw [length_addL_left a b hab]; exact la)598599/-- The number of halvings that cover `n` slots: the least `k` with `n ≤ 2^k`, by halving `n` (its own fuel), and600the halvings above the leaves of sixteen slots, `16 · 2^(slots n) ≥ n`. -/601def slotsAux : Nat → Nat → Nat602  | 0, _ => 0603  | f + 1, n => if n ≤ 1 then 0 else slotsAux f ((n + 1) / 2) + 1604def slots (n : Nat) : Nat := slotsAux ((n + 15) / 16) ((n + 15) / 16)605606theorem le_two_pow_slotsAux : ∀ (f n : Nat), n ≤ f → n ≤ 2 ^ slotsAux f n607  | 0, n, h => Nat.le_trans h (Nat.zero_le _)608  | f + 1, n, h => by609    show n ≤ 2 ^ (if n ≤ 1 then 0 else slotsAux f ((n + 1) / 2) + 1)610    match Nat.decLe n 1 with611    | .isTrue h1 => rw [ite_eq_left h1]; exact h1612    | .isFalse h1 =>613      rw [ite_eq_right h1]614      have hn : 1 < n := Nat.lt_of_not_le h1615      have e := div_add_mod' 2 (by decide) (n + 1)616      have hq : 2 * ((n + 1) / 2) ≤ n + 1 := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_eq e.symm)617      have h2 : 2 * ((n + 1) / 2) < 2 * n :=618        Nat.lt_of_le_of_lt hq (by rw [Nat.two_mul]; exact Nat.add_lt_add_left hn n)619      have hlt : (n + 1) / 2 < n :=620        Nat.lt_of_not_le fun hle => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le h2 (Nat.mul_le_mul_left 2 hle))621      have ih := le_two_pow_slotsAux f ((n + 1) / 2) (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hlt h))622      have hdiv : n ≤ 2 * ((n + 1) / 2) := by623        have hr : (n + 1) % 2 ≤ 1 := Nat.le_of_lt_succ (Nat.mod_lt _ (by decide))624        have : n + 1 ≤ 2 * ((n + 1) / 2) + 1 := Nat.le_trans (Nat.le_of_eq e) (Nat.add_le_add_left hr _)625        exact Nat.le_of_succ_le_succ this626      rw [Nat.pow_succ, Nat.mul_comm]627      exact Nat.le_trans hdiv (Nat.mul_le_mul_left 2 ih)628629theorem le_two_pow_slots (n : Nat) : n ≤ 16 * 2 ^ slots n := by630  have e := div_add_mod' 16 (by decide) (n + 15)631  have hr : (n + 15) % 16 ≤ 15 := Nat.le_of_lt_succ (Nat.mod_lt _ (by decide))632  have h1 : n ≤ 16 * ((n + 15) / 16) :=633    Nat.le_of_add_le_add_right (Nat.le_trans (Nat.le_of_eq e) (Nat.add_le_add_left hr _))634  exact Nat.le_trans h1 (Nat.mul_le_mul_left 16 (le_two_pow_slotsAux _ _ (Nat.le_refl _)))635636/-! ## Matrices over the extension: the rows of a product as combinations of rows -/637638/-- The product of two matrices over `K` given as pairs of matrices of residues (the real and the `w` parts, rows as639lists): the row `i` of `AB` is the combination of the rows of `B` by the entries of the row `i` of `A`, the list form. -/640def mulExtList (p ν : Nat) (A B : List (List Nat) × List (List Nat)) : List (List Nat) × List (List Nat) :=641  (List.zipWith (fun ar ai => (addL (combo ar B.1) (smul ν (combo ai B.2))).map (· % p)) A.1 A.2,642   List.zipWith (fun ar ai => (addL (combo ar B.2) (combo ai B.1)).map (· % p)) A.1 A.2)643644/-- The packed form: the rows of `B` packed once, each row of the product as sums of scalar multiples of them. -/645def mulExtPacked (p ν n : Nat) (A : List (List Nat) × List (List Nat)) (P : List Nat × List Nat) :646    List (List Nat) × List (List Nat) :=647  (List.zipWith (fun ar ai => unpack p n (packCombo ar P.1 + ν * packCombo ai P.2)) A.1 A.2,648   List.zipWith (fun ar ai => unpack p n (packCombo ar P.2 + packCombo ai P.1)) A.1 A.2)649650/-- A matrix of residues below `p`: every row below `p`, of `n` entries. -/651def Mtx (p n : Nat) : List (List Nat) → Prop652  | [] => True653  | r :: rs => Below p r ∧ r.length = n ∧ Mtx p n rs654655theorem length_combo {p n : Nat} : ∀ (cs : List Nat) (rs : List (List Nat)), 0 < cs.length → Mtx p n rs →656    cs.length ≤ rs.length → (combo cs rs).length = n657  | [], _, h, _, _ => absurd h (Nat.lt_irrefl 0)658  | _ :: _, [], _, _, hl => absurd hl (Nat.not_succ_le_zero _)659  | [c], r :: _, _, ⟨_, hr, _⟩, _ => by660    show (addL (smul c r) []).length = n661    rw [length_addL_left _ _ (Nat.zero_le _), length_smul, hr]662  | c :: c' :: cs, r :: rs, _, ⟨_, hr, hrs⟩, hl => by663    show (addL (smul c r) (combo (c' :: cs) rs)).length = n664    have ih := length_combo (c' :: cs) rs (Nat.succ_pos _) hrs (Nat.le_of_succ_le_succ hl)665    rw [length_addL_left _ _ (by rw [ih, length_smul, hr]; exact Nat.le_refl n), length_smul, hr]666667/-- The combination of rows of residues below `p` by `k` coefficients below `p` has entries below `k p² + 1`. -/668theorem combo_bound {p n : Nat} (hp : 0 < p) : ∀ (cs : List Nat) (rs : List (List Nat)), Below p cs → Mtx p n rs →669    Below (cs.length * (p * p) + 1) (combo cs rs)670  | [], _, _, _ => trivial671  | _ :: _, [], _, _ => trivial672  | c :: cs, r :: rs, ⟨hc, hcs⟩, ⟨hr, _, hrs⟩ => by673    show Below ((cs.length + 1) * (p * p) + 1) (addL (smul c r) (combo cs rs))674    have := below_addL (Nat.mul_pos hp hp) (Nat.succ_pos _) _ _ (below_smul hc r hr) (combo_bound hp cs rs hcs hrs)675    rw [Nat.succ_mul, Nat.add_comm (cs.length * (p * p)) (p * p), Nat.add_assoc]676    exact this677678theorem map_pack_length : ∀ rs : List (List Nat), (rs.map pack).length = rs.length679  | [] => rfl680  | _ :: rs => by show (rs.map pack).length + 1 = rs.length + 1; rw [map_pack_length rs]681682/-- One row of the product: the packed combination is the list combination. -/683theorem row_eq (p ν n : Nat) (hp : 0 < p) (hν : ν < p) (hn : 0 < n) (ar ai : List Nat) (M : List (List Nat) × List (List Nat))684    (har : Below p ar) (hai : Below p ai) (lar : ar.length = n) (lai : ai.length = n)685    (hM1 : Mtx p n M.1) (hM2 : Mtx p n M.2) (lM1 : M.1.length = n) (lM2 : M.2.length = n)686    (hB : p * (n * (p * p) + 1) + p * (n * (p * p) + 1) ≤ B) :687    unpack p n (packCombo ar (M.1.map pack) + ν * packCombo ai (M.2.map pack)) =688      (addL (combo ar M.1) (smul ν (combo ai M.2))).map (· % p) ∧689    unpack p n (packCombo ar (M.2.map pack) + packCombo ai (M.1.map pack)) =690      (addL (combo ar M.2) (combo ai M.1)).map (· % p) := by691  have hm : 0 < p * (n * (p * p) + 1) := Nat.mul_pos hp (Nat.succ_pos _)692  have c1 : Below (p * (n * (p * p) + 1)) (combo ar M.1) :=693    below_mono (Nat.le_mul_of_pos_left _ hp) _ (lar ▸ combo_bound hp ar M.1 har hM1)694  have c2 : Below (p * (n * (p * p) + 1)) (smul ν (combo ai M.2)) :=695    below_smul hν _ (lai ▸ combo_bound hp ai M.2 hai hM2)696  have c3 : Below (p * (n * (p * p) + 1)) (combo ar M.2) :=697    below_mono (Nat.le_mul_of_pos_left _ hp) _ (lar ▸ combo_bound hp ar M.2 har hM2)698  have c4 : Below (p * (n * (p * p) + 1)) (combo ai M.1) :=699    below_mono (Nat.le_mul_of_pos_left _ hp) _ (lai ▸ combo_bound hp ai M.1 hai hM1)700  have l1 : (combo ar M.1).length = n := length_combo ar M.1 (lar ▸ hn) hM1 (by rw [lar, lM1]; exact Nat.le_refl n)701  have l2 : (combo ai M.2).length = n := length_combo ai M.2 (lai ▸ hn) hM2 (by rw [lai, lM2]; exact Nat.le_refl n)702  have l3 : (combo ar M.2).length = n := length_combo ar M.2 (lar ▸ hn) hM2 (by rw [lar, lM2]; exact Nat.le_refl n)703  have l4 : (combo ai M.1).length = n := length_combo ai M.1 (lai ▸ hn) hM1 (by rw [lai, lM1]; exact Nat.le_refl n)704  constructor705  · rw [← pack_combo, ← pack_combo, ← pack_smul, ← pack_addL,706      ← unpack_pack p _ (bounded_of_below hB _ (below_addL hm hm _ _ c1 c2)),707      length_addL_eq l1 (by rw [length_smul, l2])]708  · rw [← pack_combo, ← pack_combo, ← pack_addL,709      ← unpack_pack p _ (bounded_of_below hB _ (below_addL hm hm _ _ c3 c4)), length_addL_eq l3 l4]710711/-- The packed product of two matrices over `K` is the list form, when `2 p (n p² + 1) ≤ B`. -/712theorem mulExtPacked_eq (p ν n : Nat) (hp : 0 < p) (hν : ν < p) (hn : 0 < n)713    (A M : List (List Nat) × List (List Nat)) (hA1 : Mtx p n A.1) (hA2 : Mtx p n A.2)714    (hM1 : Mtx p n M.1) (hM2 : Mtx p n M.2) (lM1 : M.1.length = n) (lM2 : M.2.length = n)715    (hB : p * (n * (p * p) + 1) + p * (n * (p * p) + 1) ≤ B) :716    mulExtPacked p ν n A (M.1.map pack, M.2.map pack) = mulExtList p ν A M := by717  obtain ⟨A1, A2⟩ := A718  unfold mulExtPacked mulExtList719  induction A1 generalizing A2 with720  | nil => cases A2 <;> rfl721  | cons ar A1 ih =>722    cases A2 with723    | nil => rfl724    | cons ai A2 =>725      obtain ⟨har, lar, hA1'⟩ := hA1726      obtain ⟨hai, lai, hA2'⟩ := hA2727      have h := row_eq p ν n hp hν hn ar ai M har hai lar lai hM1 hM2 lM1 lM2 hB728      have ih' := ih A2 hA1' hA2'729      show (unpack p n (packCombo ar (M.1.map pack) + ν * packCombo ai (M.2.map pack)) :: List.zipWith _ A1 A2,730          unpack p n (packCombo ar (M.2.map pack) + packCombo ai (M.1.map pack)) :: List.zipWith _ A1 A2) =731        ((addL (combo ar M.1) (smul ν (combo ai M.2))).map (· % p) :: List.zipWith _ A1 A2,732          (addL (combo ar M.2) (combo ai M.1)).map (· % p) :: List.zipWith _ A1 A2)733      rw [h.1, h.2, (Prod.mk.inj ih').1, (Prod.mk.inj ih').2]734735end FRC.Dirac.Packed736