All table values have at most `B` bits

All table values have at most B bits. -/ def TwB (p R B : ℕ) : Prop := ∀ c < R, zsz (twD p R c).1 ≤ B ∧ zsz (twD p R c).2 ≤ B theorem tabBody_cost (M : MulSpec) (tw : RM) (p R Ctw : ℕ) (htw : TwSpec M tw p R Ctw) (w : IState HS) (c : ℕ) (hc : c < R) (LQ LP LM : List Item) (hq : w.G hQ = .int ((c : ℤ) + 1) :: LQ) (hp : w.G hPp = .int p :: LP) (hm : w.G hM2 = .int R :: LM) (B : ℕ) (hRB : 2 * R + 2 < 2 ^ B) (hv : TwB p R B) : (tabBody tw).cost M w ≤ Ctw + 2 * 10 ^ 9 * (B + 2) ^ 2 := by have zb : ∀ n : ℕ, n ≤ 2 * R + 2 → zsz (n : ℤ) ≤ B := fun n hn => zsz_nat_le hn hRB have hB1 : 1 ≤ B := by rcases Nat.eq_zero_or_pos B with h | h · rw [h, pow_zero] at hRB; omega · exact h have eq : (Ex.add (Ex.reg (S := HS) hQ) (.lit (-1))).eval w = c := by simp [Ex.eval, IState.top_eq hq] set w1 := w.upd hC (.int c :: w.G hC) with hw1 have r1 : (push hC (.add (.reg hQ) (.lit (-1)))).run w = w1 := by simp only [RS.run, eq, hw1] obtain ⟨-, r2, c2⟩ := htw.2 w1 c (w.G hC) LP LM (by simp [hw1]) (by simp +decide [hw1, hp]) (by simp +decide [hw1, hm]) hc set w2 := (w1.upd hVA (.int (twD p R c).1 :: w1.G hVA)).upd hVB (.int (twD p R c).2 :: w1.G hVB) with hw2 have c1 : (push hC (.add (.reg hQ) (.lit (-1)))).cost w ≤ 4 * 10 ^ 8 * (B + 2) ^ 2 := by have := cost_le_QB B (push hC (.add (.reg hQ) (.lit (-1)))) w (by simp only [QB, Ex.Bnd, Ex.eval, IState.top_eq hq] refine ⟨?, ?, ?⟩ · exact_mod_cast zb (c + 1) (by omega) · rw [zsz_neg, zsz_one]; omega · have := zb c (by omega); simpa using this) simpa [qsz, Ex.size] using this have c3 : tabPush.cost w2 ≤ 13 * 10 ^ 8 * (B + 2) ^ 2 := by have hq3 : QB B tabPush w2 := by simp +decide only [tabPush, QB, RS.run, Ex.Bnd, Ex.eval, IState.top, IState.upd_G, hw2, hw1, if_true, if_false, List.tail_cons] obtain ⟨v1, v2⟩ := hv c hc refine ⟨v2, v1, ⟨?, ?, ?⟩, v1, v2, ?⟩ · exact zb c (by omega) · exact zb c (by omega) · exact_mod_cast zb (c + c) (by omega) · exact zb c (by omega) have := cost_le_QB B _ w2 hq3 simp only [tabPush, qsz, Ex.size] at this ⊢ nlinarith rw [tabBody, RM.cost_seq', RM.cost_seq', RM.cost_rs', RM.cost_rs', RM.run_rs, r1, r2] have hX : 4 ≤ (B + 2) ^ 2 := by nlinarith [Nat.zero_le B] clear * - c1 c2 c3 hX generalize (B + 2) ^ 2 = X at * omega theorem tabGen_cost (M : MulSpec) (tw : RM) (p R Ctw : ℕ) (htw : TwSpec M tw p R Ctw) (s : IState HS) (LP LM : List Item) (hp : s.G hPp = .int p :: LP) (hm : s.G hM2 = .int R :: LM) (B : ℕ) (hRB : 2 * R + 2 < 2 ^ B) (hv : TwB p R B) : (tabGen tw).cost M s ≤ (R + 1) * (Ctw + 3 * 10 ^ 9 * (B + 2) ^ 2) := by obtain ⟨H, -⟩ := tabGen_states M tw p R Ctw htw s LP LM hp hm have e : (Ex.reg (S := HS) hM2).eval s = R := by simp [Ex.eval, IState.top_eq hm] have hRz : zsz (R : ℤ) ≤ B := zsz_nat_le (le_refl R) (by omega) have c := RM.RepStates.cost_le H B (Ctw + 2 * 10 ^ 9 * (B + 2) ^ 2) (by simp only [Ex.Bnd, IState.top_eq hm]; exact hRz) (by rw [e]; exact hRz) (by intro k hk rw [e, Int.toNat_natCast] at hk ⊢ exact tabBody_cost M tw p R Ctw htw _ (R - (k + 1)) (by omega) (s.G hQ) LP LM (by simp only [withCtr, IState.upd_G, if_true]; congr 2; push_cast [show k + 1 ≤ R by omega]; ring) (by simp +decide [withCtr, hp]) (by simp +decide [withCtr, hm]) B hRB hv) rw [e, Int.toNat_natCast] at c unfold tabGen refine le_trans c ? simp only [Ex.size] clear * - have hX : 4 ≤ (B + 2) ^ 2 := by nlinarith [Nat.zero_le B] generalize (B + 2) ^ 2 = X at * nlinarith /-! ## The scan -/ theorem scanBody_cost (w : IState HS) (k0 a b ca cb : ℤ) (hk0 : 0 ≤ k0) (Rst LA LB : List Item) (h0 : w.G 0 = .int k0 :: .int a :: .int b :: Rst) (hA : w.G hCa = .int ca :: LA) (hB : w.G hCb = .int cb :: LB) (B : ℕ) (hB1 : 2 ≤ B) (zk : zsz k0 ≤ B) (za : zsz a ≤ B) (zb : zsz b ≤ B) (zca : zsz ca ≤ B) (zcb : zsz cb ≤ B) : scanBody.cost w ≤ 27 * 3000 * (B + 2) := by have hmod := Int.emod_two_eq k0 have zm : zsz (k0.tmod 2) ≤ B := by rw [Int.tmod_eq_emod_of_nonneg hk0] rcases hmod with h | h <;> rw [h] <;> simp [zsz_zero, zsz_one] <;> omega have z2 : zsz (2 : ℤ) ≤ B := by have : zsz (2 : ℤ) = zsz ((2 : ℕ) : ℤ) := rfl rw [this]; exact zsz_nat_le (le_refl 2) (by calc 2 < 2 ^ 2 := by norm_num _ ≤ 2 ^ B := Nat.pow_le_pow_right (by norm_num) hB1) have hl : LinB B scanBody w := by have zm' : zsz (-(k0.tmod 2)) ≤ B := by rw [zsz_neg]; exact zm rw [Int.tmod_eq_emod_of_nonneg hk0] at zm zm' rcases hmod with h | h · simp +decide only [scanBody, scanPre, scanPost, LinB, RS.run, Ex.Lin, Ex.Bnd, Ex.eval, IState.top, IState.upd_G, h0, hA, hB, if_true, if_false, List.tail_cons, parE, emitP, setP, true_and, and_true, Int.tmod_eq_emod_of_nonneg hk0, h, neg_zero, lt_irrefl] rw [h] at zm zm' constructorm* _ ∧ _ <;> assumption · simp +decide only [scanBody, scanPre, scanPost, LinB, RS.run, Ex.Lin, Ex.Bnd, Ex.eval, IState.top, IState.upd_G, h0, hA, hB, if_true, if_false, List.tail_cons, parE, emitP, setP, true_and, and_true, Int.tmod_eq_emod_of_nonneg hk0, h, show (-1 : ℤ) < 0 by decide] rw [h] at zm zm' constructorm* _ ∧ _ <;> assumption have := cost_le_linB B _ w hl simpa [scanBody, scanPre, scanPost, lsz, parE, emitP, setP, Ex.size] using this theorem curF_bnd (B : ℕ) : ∀ (Z : List (List ℤ)) (cur : ℤ × ℤ), (∀ r ∈ Z, Bnd B r) → zsz cur.1 ≤ B → zsz cur.2 ≤ B → zsz (curF cur Z).1 ≤ B ∧ zsz (curF cur Z).2 ≤ B | [], cur, , h1, h2 => ⟨h1, h2⟩ | r :: Z, cur, hZ, h1, h2 => by simp only [curF] split_ifs · exact curF_bnd B Z cur (fun r' hr' => hZ r' (List.mem_cons_of_mem _ hr')) h1 h2 · apply curF_bnd B Z _ (fun r' hr' => hZ r' (List.mem_cons_of_mem _ hr')) · have := hZ r List.mem_cons_self rcases r with _ | ⟨x, _ | ⟨y, t⟩⟩ · simp [zsz_zero] · simp [zsz_zero] · exact this y (by simp) · have := hZ r List.mem_cons_self rcases r with _ | ⟨x, _ | ⟨y, _ | ⟨z, t⟩⟩⟩ · simp [zsz_zero] · simp [zsz_zero] · simp [zsz_zero] · exact this z (by simp) theorem scanLoop_cost (s : IState HS) (Z : List (List ℤ)) (hZ : ∀ r ∈ Z, Rec3 r) (Rst : List Item) (cur0 : ℤ × ℤ) (LA LB L1 : List Item) (h0 : s.G 0 = ints Z.flatten ++ Rst) (hA : s.G hCa = .int cur0.1 :: LA) (hB : s.G hCb = .int cur0.2 :: LB) (h1 : s.G 1 = .int Z.length :: L1) (B : ℕ) (hB2 : 2 ≤ B) (hZB : ∀ r ∈ Z, Bnd B r) (hc1 : zsz cur0.1 ≤ B) (hc2 : zsz cur0.2 ≤ B) (hn : zsz (Z.length : ℤ) ≤ B) : scanLoop.cost s ≤ (Z.length + 1) * 90000 * (B + 2) := by have H := scan_states s Z hZ Rst cur0 LA LB L1 h0 hA hB h1 have e : (Ex.reg (S := HS) 1).eval s = Z.length := by simp [Ex.eval, IState.top_eq h1] have c := RepStates.cost_le_lin H B (27 * 3000 * (B + 2)) trivial (by simp only [Ex.Bnd, IState.top_eq h1]; exact hn) (by intro k hk rw [e, Int.toNat_natCast] at hk ⊢ obtain ⟨k0, a, b, hr, hk0⟩ := hZ _ (List.getElem_mem hk) have hd := List.drop_eq_getElem_cons hk rw [hr] at hd have hrB := hZB _ (List.getElem_mem hk) rw [hr] at hrB obtain ⟨zc1, zc2⟩ := curF_bnd B (Z.take k) cur0 (fun r hr' => hZB r (List.mem_of_mem_take hr')) hc1 hc2 exact scanBody_cost _ k0 a b _ _ hk0 (ints (Z.drop (k + 1)).flatten ++ Rst) LA LB (by simp +decide [withCtr, scSt, hd]) (by simp +decide [withCtr, scSt]) (by simp +decide [withCtr, scSt]) B hB2 (hrB k0 (by simp)) (hrB a (by simp)) (hrB b (by simp)) zc1 zc2) rw [e, Int.toNat_natCast] at c unfold scanLoop refine le_trans c ? simp only [Ex.size] nlinarith /-! ## Sort, scan, gather

The following holds (Lean statement, in the scope of module NLogN.HCrChirpCost):

theorem NLogN.CR.chirpTail_cost (v : ℕ → ℤ × ℤ) (κ : ℕ → ℕ) (R T kb : ℕ) (hκ : ∀ x < T, κ x < R)
    (hR : 2 * R ≤ 2 ^ kb) (hTk : T ≤ 2 ^ kb) (t : IState HS) (Rest LM LT L2 : List Item)
    (h0 : t.G 0 = ints (mergeL v κ R T).flatten ++ Rest) (hm : t.G hM2 = .int R :: LM)
    (ht : t.G hTT = .int T :: LT) (h2 : t.G 2 = .int kb :: L2) (B : ℕ)
    (hv : ∀ c < R, zsz (v c).1 ≤ B ∧ zsz (v c).2 ≤ B) (hBig : 4 * R + 3 * T + 4 < 2 ^ B)
    (hkbB : kb + 2 ≤ B) :
    chirpTail.cost t ≤ 10 ^ 7 * (kb + 1) * (R + T + 1) * (B + kb + 6)

Context. The lemma belongs to the part Costs of the chirp table program (namespace NLogN.CR): QB B p s: every expression of the loop-free program p evaluated from s has all intermediate values of at most B bits; then p.cost s ≤ qsz p · 10^8 · (B + 2)^2.

Formalization Note. This is a lemma of the Lean development NLogN, a multitape-Turing-machine implementation of the Harvey–van der Hoeven $O(n\log n)$ integer multiplication algorithm, used in the proof of NLogN.FIN.theorem_1_1_nlogn : IntMul.MulTimeBound fun n => n * Real.log n. All names refer to the definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8 (namespace NLogN), built on the platform model Def_IntMul_MultitapeModel and the published reference Def_IntMul_HvdH_MachineRef. The machine layer: IState HS is a state of 64 item stacks; RM programs have a semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s relative to a multiplication spec M : MulSpec; zsz z is the bit length of $|z|$.