The bit environment: atoms ≤ A, degree-≤ 8 values fit in B bits. -/ structure CostEnv (A B : ℕ) : Prop…

The bit environment: atoms ≤ A, degree-≤ 8 values fit in B bits. -/ structure CostEnv (A B : ℕ) : Prop where hA : 256 ≤ A hAB : ∀ k ≤ 8, A ^ k < 2 ^ B theorem CostEnv.zsz_le {A B : ℕ} (h : CostEnv A B) {z : ℤ} (hz : |z| ≤ (A : ℤ)) : zsz z ≤ B := zsz_of_abs (k := 1) (by simpa using hz) (h.hAB 1 (by norm_num)) theorem CostEnv.zsz_nat {A B : ℕ} (h : CostEnv A B) {m : ℕ} (hm : m ≤ A) : zsz (m : ℤ) ≤ B := h.zsz_le (by rw [Nat.abs_cast]; exact_mod_cast hm) theorem CostEnv.B1 {A B : ℕ} (h : CostEnv A B) : 1 ≤ B := by have := h.hAB 1 (by norm_num) by_contra h0; push Not at h0 have : B = 0 := by omega subst this; simp at ; have := h.hA; omega theorem CostEnv.K {A B : ℕ} (h : CostEnv A B) : 100 ≤ 10 ^ 7 * (B + 2) ^ 2 := by have : 1 ≤ (B + 2) ^ 2 := Nat.one_le_pow _ _ (by omega) nlinarith theorem srcE_sm (A : ℕ) (hA : 2 ≤ A) (u : IState HS) (d' Q Mh Mf : ℕ) (h : SrcRegs u d' Q Mh Mf) (hb : d' ≤ A ∧ Q ≤ A ∧ Mh ≤ A ∧ Mf ≤ A) (r : Fin HS) (c : ℤ) (L : List Item) (hr : u.G r = .int c :: L) (hc : |c| ≤ (A : ℤ)) : exSmS A u (srcE (.add (.reg r) (.lit (-1)))) := by obtain ⟨⟨L1, h1⟩, ⟨L2, h2⟩, ⟨L3, h3⟩, ⟨L4, h4⟩⟩ := h obtain ⟨b1, b2, b3, b4⟩ := hb simp only [srcE, exSmS, IState.top_eq h1, IState.top_eq h2, IState.top_eq h3, IState.top_eq h4, IState.top_eq hr] constructorm _ ∧ _ atoms theorem CostEnv.dg {A B : ℕ} (h : CostEnv A B) (e : Ex HS) (hd : exDgS e ≤ 8) : A ^ exDgS e < 2 ^ B := h.hAB _ hd /-! ## The product loop

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

theorem NLogN.KFM.pmLoop_cost (u : IState HS) (d' Q Mh Mf i s : ℕ) (h : SrcRegs u d' Q Mh Mf)
    (LS LP : List Item) (hS : u.G mS = .int (s : ℤ) :: LS) (hP : u.G mP = .int 1 :: LP)
    (hs : 2 ≤ s) (hIx : ixO.eval u = i) (hIok : ixO.ok u)
    (hj : ∀ j < i, (j < d' → j ≤ Mh) ∧ (d' ≤ j → j - d' ≤ Mf))
    (A B : ℕ) (hE : CostEnv A B) (hb : d' ≤ A ∧ Q ≤ A ∧ Mh ≤ A ∧ Mf ≤ A) (hsA : s ≤ A)
    (hiA : i ≤ A) (c0 : ℕ) (LO : List Item) (hO : u.G mOc = .int (c0 : ℤ) :: LO) (hc0 : c0 ≤ A) :
    (RS.rep mIc ixO pmB).cost u ≤ (i + 1) * 40 * (10 ^ 7 * (B + 2) ^ 2)

Context. The lemma belongs to the part KFM S9: the cost of the source and inverse lists: Write K = 10^7 (B+2)^2. Assume every atom is at most A, with A^k < 2^B for k ≤ 8.

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.