Sizes of the small values. -/ theorem zszQ {b : ℕ} {z : ℤ} (h : |z| ≤ 2 ^ (b + 1)) : zsz z ≤ 8 * b + 8 :=…

Sizes of the small values. -/ theorem zszQ {b : ℕ} {z : ℤ} (h : |z| ≤ 2 ^ (b + 1)) : zsz z ≤ 8 * b + 8 := KFL.zsz_le_of_abs (lt_of_le_of_lt h (pow_lt_pow_right₀ (by norm_num) (by omega))) theorem gam_le {n : ℕ} (hn : n0 ≤ n) : 8 * dP n * αP n ^ 2 ≤ bP n := by obtain ⟨-, -, -, -, -, -, -, -, -, -, -, -, -, -, -, -, hγ, -⟩ := params_ok hn unfold γP at hγ have : ((8 * dP n * αP n ^ 2 : ℕ) : ℝ) ≤ (bP n : ℝ) := by push_cast; linarith exact_mod_cast this theorem alpha_pos {n : ℕ} (hn : n0 ≤ n) : 1 ≤ αP n := by obtain ⟨-, -, hb, hd, -, -, -, -, -, -, -, -, -, -, -, h12, -⟩ := params_ok hn by_contra h0 have : αP n = 0 := by omega rw [this] at h12 have : (1 : ℝ) ≤ dP n := by exact_mod_cast hd have : (8192 : ℝ) ≤ bP n := by exact_mod_cast hb norm_num at h12 nlinarith theorem b_pow {n : ℕ} (hn : n0 ≤ n) : 8 * bP n + 100 ≤ 2 ^ bP n := by have hb := (setup_facts hn).1 have := cube_lt_pow (bP n) (by omega) have : bP n ≤ bP n ^ 3 := Nat.le_self_pow (by norm_num) _ omega set_option maxHeartbeats 4000000 in theorem parQ_bnd {n : ℕ} (hn : n0 ≤ n) (S : ℕ) (hS : S < 2 ^ bP n) (t : IState HS) (h : QRegs t n S) : PBnd (8 * bP n + 8) Lq t := by obtain ⟨hb8, hd1, hdb, -⟩ := setup_facts hn obtain ⟨hT1, -, hLb, -⟩ := L_facts hn have hn2 := n_le hn have hγ := gam_le hn have hbp := b_pow hn have hα0 := alpha_pos hn have hα1 : αP n ^ 2 ≤ bP n := by nlinarith set M := (n + bP n - 1) / bP n with hM have hn1 : 3 ≤ n := n0_ge3 hn have hMn : M ≤ n := by rw [hM]; apply Nat.div_le_of_le_mul have : n + bP n ≤ bP n * n := by nlinarith omega obtain ⟨LL, hLL⟩ := h.hL obtain ⟨LN, hNN⟩ := h.hN obtain ⟨LB, hBB⟩ := h.hB obtain ⟨LD, hDD⟩ := h.hD obtain ⟨LA, hAA⟩ := h.hA obtain ⟨LS, hSS⟩ := h.hS have hMq : ((n : ℤ) + ((bP n : ℤ) + -1)) / (bP n : ℤ) = (M : ℤ) := by rw [show (n : ℤ) + ((bP n : ℤ) + -1) = ((n + bP n - 1 : ℕ) : ℤ) by omega, hM]; norm_cast have eγ : 2 * (dP n : ℤ) * ((αP n : ℤ) * (αP n : ℤ)) = ((2 * dP n * αP n ^ 2 : ℕ) : ℤ) := by push_cast; ring have zP : (2 : ℤ) ^ (bP n + 1) = 2 * 2 ^ bP n := by rw [pow_succ]; ring have zb : (8 * (bP n : ℤ) + 100) ≤ 2 ^ bP n := by exact_mod_cast hbp have zn : (n : ℤ) ≤ 2 ^ bP n := by exact_mod_cast hn2 have zS : (S : ℤ) < 2 ^ bP n := by exact_mod_cast hS have zM : (M : ℤ) ≤ n := by exact_mod_cast hMn have zγ : ((2 * dP n * αP n ^ 2 : ℕ) : ℤ) ≤ bP n := by push_cast; push_cast at hγ; nlinarith have zα : (αP n : ℤ) * αP n ≤ bP n := by have : ((αP n ^ 2 : ℕ) : ℤ) ≤ bP n := by exact_mod_cast hα1 push_cast at this; nlinarith have zd : (2 : ℤ) * dP n ≤ bP n := by have : dP n ≤ dP n * αP n ^ 2 := Nat.le_mul_of_pos_right _ (by positivity) have : 2 * dP n ≤ bP n := by nlinarith exact_mod_cast this have zL : (LP n : ℤ) < bP n := by exact_mod_cast hLb simp (config := {decide := true}) [Lq, PBnd, Ex.Bnd, Ex.eval, IState.top, IState.upd_G, hLL, hNN, hBB, hDD, hAA, hSS, hMq, eγ] constructorm* _ ∧ _ all_goals first | omega | (apply zszQ; rw [abs_le, zP]; constructor <;> nlinarith) | (push_cast at zγ ⊢; nlinarith) | skip /-! ## parS -/ set_option maxHeartbeats 4000000 in theorem parS_cost {n : ℕ} (hn : n0 ≤ n) (t : IState HS) (LD LB : List Item) (hD : t.G zD = .int (dP n : ℤ) :: LD) (hB : t.G zB = .int (bP n : ℤ) :: LB) (h : SrcRegs t (dpN n) (srcQ (dP n) (rP n)) (srcM (dP n) (rP n) (rP n / 2)) (srcM (dP n) (rP n) (rP n))) : parS.cost t ≤ 100 * (10 ^ 7 * (16 * bP n + 17 + 2) ^ 2) * (dP n + 2) := by obtain ⟨hb, hd1, hdb, -⟩ := setup_facts hn have hE := costEnv_n (bP n) (by omega) set B := 16 * bP n + 17 with hBd set A := 2 ^ (2 * bP n + 2) with hA set K := 10 ^ 7 * (B + 2) ^ 2 with hK obtain ⟨a1, a2, a3, a4, a5, -⟩ := src_atoms hn have hbA : 2 ^ bP n * 2 ^ bP n * 4 = A := by rw [hA, pow_add, two_mul, pow_add]; norm_num have hb2 : bP n < 2 ^ bP n := Nat.lt_two_pow_self have h1 : 1 ≤ 2 ^ bP n := Nat.one_le_two_pow have hsA : 2 ^ bP n ≤ A := by nlinarith have hdA : dP n + 1 ≤ A := by nlinarith have hbB : bP n + 1 ≤ B := by omega -- 1 set t1 := t.upd mOc (.int ((dP n : ℤ) + 1) :: t.G mOc) with ht1 have e1 : (RS.push mOc (.add (.reg zD) (.lit 1))).run t = t1 := by simp only [RS.run, Ex.eval, IState.top_eq hD, ht1] have c1 := RS.pushCost_le (.add (.reg zD) (.lit 1) : Ex HS) t B (by simp only [Ex.Bnd, Ex.eval, IState.top_eq hD] refine ⟨hE.zsz_nat (by omega), hE.zsz_le (by norm_num; omega), ?_⟩ exact hE.zsz_le (by rw [abs_le]; constructor <;> push_cast <;> omega)) have s1 : (Ex.add (.reg zD) (.lit 1) : Ex HS).size + 1 ≤ 5 := by decide -- 2 have t1B : t1.G zB = .int (bP n : ℤ) :: LB := by simp +decide [t1, hB] set t2 := t1.upd mS (.int ((2 : ℤ) ^ bP n) :: t1.G mS) with ht2 have e2 : (RS.push mS (.pow2 (.reg zB))).run t1 = t2 := by simp only [RS.run, Ex.eval, IState.top_eq t1B, Int.toNat_natCast, ht2] have c2 := RS.pushCost_le (.pow2 (.reg zB) : Ex HS) t1 B (by simp only [Ex.Bnd, Ex.eval, IState.top_eq t1B, Int.toNat_natCast] exact ⟨hE.zsz_nat (by omega), hbB⟩) have s2 : (Ex.pow2 (.reg zB) : Ex HS).size + 1 ≤ 5 := by decide -- 3 set t3 := t2.upd mP (.int 1 :: t2.G mP) with ht3 have e3 : (RS.push mP (.lit 1)).run t2 = t3 := by simp only [RS.run, Ex.eval, ht3] have c3 := RS.pushCost_le (.lit 1 : Ex HS) t2 B (by simp only [Ex.Bnd]; exact hE.zsz_le (by norm_num; omega)) have s3 : (Ex.lit 1 : Ex HS).size + 1 ≤ 5 := by decide -- 4 the loop have h3 : SrcRegs t3 (dpN n) (srcQ (dP n) (rP n)) (srcM (dP n) (rP n) (rP n / 2)) (srcM (dP n) (rP n) (rP n)) := ((h.upd mOc (by decide) _).upd mS (by decide) _).upd mP (by decide) _ have h3O : t3.G mOc = .int ((dP n : ℤ) + 1) :: t.G mOc := by simp +decide [t3, t2, t1] have h3O' : t3.G mOc = .int ((dP n + 1 : ℕ) : ℤ) :: t.G mOc := by rw [h3O]; push_cast; rfl have hpow : 2 ≤ 2 ^ bP n := by calc 2 = 2 ^ 1 := by norm_num _ ≤ 2 ^ bP n := Nat.pow_le_pow_right (by norm_num) (by omega) have hIx : ixO.eval t3 = (dP n : ℤ) := by simp only [ixO, Ex.eval, IState.top_eq h3O]; ring have hS3 : t3.G mS = .int ((2 ^ bP n : ℕ) : ℤ) :: t1.G mS := by simp +decide [t3, t2] have hP3 : t3.G mP = .int 1 :: t2.G mP := by simp +decide [t3] have hj : ∀ j < dP n, (j < dpN n → j ≤ srcM (dP n) (rP n) (rP n / 2)) ∧ (dpN n ≤ j → j - dpN n ≤ srcM (dP n) (rP n) (rP n)) := fun j hj => ⟨(src_facts hn j hj).1, (src_facts hn j hj).2.1⟩ have c4 := pmLoop_cost t3 _ _ _ _ (dP n) (2 ^ bP n) h3 (t1.G mS) (t2.G mP) hS3 hP3 hpow hIx ⟨IState.isInt_of h3O, trivial⟩ hj A B hE ⟨a1, a2, a3, a4⟩ hsA (by omega) (dP n + 1) (t.G mOc) h3O' hdA obtain ⟨-, r4⟩ := prodLoop_run t3 _ _ _ _ (dP n) (2 ^ bP n) h3 (t1.G mS) (t2.G mP) hS3 hP3 hpow hIx ⟨IState.isInt_of h3O, trivial⟩ hj set S' := (∏ j ∈ Finset.range (dP n), srcV (dpN n) (srcQ (dP n) (rP n)) (srcM (dP n) (rP n) (rP n / 2)) (srcM (dP n) (rP n) (rP n)) j) % 2 ^ bP n with hS' have hS'l : S' < 2 ^ bP n := Nat.mod_lt _ (by omega) set t4 := t3.upd mP (.int (S' : ℤ) :: t2.G mP) with ht4 -- 5 have h4P : t4.G mP = .int (S' : ℤ) :: t2.G mP := by simp [t4] have c5 := RS.pushCost_le (.reg mP : Ex HS) t4 B (by simp only [Ex.Bnd, IState.top_eq h4P]; exact hE.zsz_nat (by omega)) have s5 : (Ex.reg mP : Ex HS).size + 1 ≤ 5 := by decide set t5 := t4.upd rS (.int (S' : ℤ) :: t4.G rS) with ht5 have e5 : (RS.push rS (.reg mP)).run t4 = t5 := by simp only [RS.run, Ex.eval, IState.top_eq h4P, ht5] -- pops have h5P : t5.G mP = .int (S' : ℤ) :: t2.G mP := by simp +decide [t5, h4P] set t6 := t5.upd mP (t2.G mP) with ht6 have e6 : (RS.pop mP).run t5 = t6 := by simp only [RS.run, h5P, List.tail_cons, ht6] have h6S : t6.G mS = .int ((2 : ℤ) ^ bP n) :: t1.G mS := by simp +decide [t6, t5, t4, t3, t2] set t7 := t6.upd mS (t1.G mS) with ht7 have e7 : (RS.pop mS).run t6 = t7 := by simp only [RS.run, h6S, List.tail_cons, ht7] have h7O : t7.G mOc = .int ((dP n : ℤ) + 1) :: t.G mOc := by simp +decide [t7, t6, t5, t4, t3, t2, t1] have p6 : (RS.pop mP).cost t5 ≤ 2 * B + 2 := by show 2 * zsz (t5.top mP) + 2 ≤ _; rw [IState.top_eq h5P]; have := hE.zsz_nat (m := S') (by omega) omega have p7 : (RS.pop mS).cost t6 ≤ 2 * B + 2 := by show 2 * zsz (t6.top mS) + 2 ≤ _; rw [IState.top_eq h6S] have := hE.zsz_le (z := (2 : ℤ) ^ bP n) (by rw [abs_of_nonneg (by positivity)]; exact_mod_cast hsA) omega have p8 : (RS.pop mOc).cost t7 ≤ 2 * B + 2 := by show 2 * zsz (t7.top mOc) + 2 ≤ _; rw [IState.top_eq h7O] have := hE.zsz_le (z := (dP n : ℤ) + 1) (by rw [abs_le]; constructor <;> push_cast <;> omega) omega rw [parS, rsCost_seq, e1, rsCost_seq, e2, rsCost_seq, e3, rsCost_seq, r4, rsCost_seq, e5, rsCost_seq, e6, rsCost_seq, e7] have hK1 : 2 * B + 2 ≤ K := by have : B + 2 ≤ (B + 2) ^ 2 := Nat.le_self_pow (by norm_num) _ omega have c1' : (Ex.add (.reg zD) (.lit 1) : Ex HS).cost t + (2 * moveCost (zsz ((Ex.add (.reg zD) (.lit 1) : Ex HS).eval t)) + 19) ≤ 5 * K := by calc _ ≤ _ := c1 _ ≤ 5 * K := by rw [hK, ← mul_assoc]; exact Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ s1) have c2' : (Ex.pow2 (.reg zB) : Ex HS).cost t1 + (2 * moveCost (zsz ((Ex.pow2 (.reg zB) : Ex HS).eval t1)) + 19) ≤ 5 * K := by calc _ ≤ _ := c2 _ ≤ 5 * K := by rw [hK, ← mul_assoc]; exact Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ s2) have c3' : (Ex.lit 1 : Ex HS).cost t2 + (2 * moveCost (zsz ((Ex.lit 1 : Ex HS).eval t2)) + 19) ≤ 5 * K := by calc _ ≤ _ := c3 _ ≤ 5 * K := by rw [hK, ← mul_assoc]; exact Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ s3) have c5' : (Ex.reg mP : Ex HS).cost t4 + (2 * moveCost (zsz ((Ex.reg mP : Ex HS).eval t4)) + 19) ≤ 5 * K := by calc _ ≤ _ := c5 _ ≤ 5 * K := by rw [hK, ← mul_assoc]; exact Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ s5) simp only [rsCost_push] rw [← hK] at c4 have : (dP n + 1) * 40 * K ≤ 40 * K * (dP n + 2) := by nlinarith nlinarith /-! ## The whole setup

The following holds (Lean statement, in the scope of module Solutions.KFMSetC):

theorem NLogN.KFM.setup_cost (x y : List Bool) (hn : IntMul.OpenAI.Glue.n0 ≤ x.length) :
    cStart x.length + 12 * 10 ^ 15 * (bP x.length + 1) ^ 4 +
        parS.cost (setupSt x.length (stA x y)) +
        parQ.cost ((setupSt x.length (stA x y)).upd NLogN.KFM.rS (.int (sCmp x.length : ℤ) ::
          (setupSt x.length (stA x y)).G NLogN.KFM.rS)) + (3 + 2 * shlCost x.length) ≤
      10 ^ 17 * ((bP x.length + 1) ^ 6 + x.length + 1)

Context. The lemma belongs to the part KFM SetC: the cost of the parameter pushes.

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.