The parameter frame. -/ def fK (p ℓ n : ℕ) (j : Fin HS) : List ℤ := if j = kc then [(2 : ℤ) ^ p] else if j…

The parameter frame. -/ def fK (p ℓ n : ℕ) (j : Fin HS) : List ℤ := if j = kc then [(2 : ℤ) ^ p] else if j = kr then [((2 ^ ℓ : ℕ) : ℤ)] else if j = kK then [kG (kb p ℓ) (2 ^ ℓ) ((2 : ℤ) ^ p)] else if j = kB then [(2 : ℤ) ^ kb p ℓ] else if j = kJ then [((2 : ℤ) ^ kb p ℓ) ^ (2 * 2 ^ ℓ)] else if j = kD then [(2 : ℤ) ^ (p + ℓ)] else if j = vRH then [((2 ^ n : ℕ) : ℤ)] else if j = vT then [((2 * (2 ^ n * 2 ^ ℓ) : ℕ) : ℤ)] else if j = vZ then [0] else [] /-! ## Arithmetic -/ theorem geom_aux (m : ℕ) (hm : 1 ≤ m) : ∀ r : ℕ, (m - 1) * (∑ h ∈ Finset.range r, m ^ h) + 1 = m ^ r | 0 => by simp | r + 1 => by rw [Finset.sum_range_succ, Nat.mul_add, Nat.add_right_comm, geom_aux m hm r, pow_succ] have : (m - 1) * m ^ r + m ^ r = m ^ r * m := by rcases m with _ | m · omega · simp only [Nat.add_sub_cancel]; ring omega theorem kG_eq (b r p : ℕ) (hb : 1 ≤ b) : kG b r ((2 : ℤ) ^ p) = ((2 ^ p * (2 ^ (b * r) - 1) / (2 ^ b - 1) : ℕ) : ℤ) := by have hm : 1 ≤ 2 ^ b := Nat.one_le_two_pow have hm2 : 0 < 2 ^ b - 1 := by have : 2 ≤ 2 ^ b := by calc 2 = 2 ^ 1 := by norm_num _ ≤ 2 ^ b := Nat.pow_le_pow_right (by norm_num) hb omega have g := geom_aux (2 ^ b) hm r rw [← pow_mul] at g have e : 2 ^ p * (2 ^ (b * r) - 1) / (2 ^ b - 1) = 2 ^ p * ∑ h ∈ Finset.range r, (2 ^ b) ^ h := by rw [show 2 ^ (b * r) - 1 = (2 ^ b - 1) * ∑ h ∈ Finset.range r, (2 ^ b) ^ h by omega, Nat.mul_left_comm, Nat.mul_div_cancel_left _ hm2] rw [e, kG] push_cast rw [Finset.mul_sum] /-! ## Records

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

theorem NLogN.KFV.abs_le_of_disk {r p : ℕ} {zs : List GI} {xs : List (Fin r → ℂ)} (h : RecRep r p zs xs)
    (hd : Disk xs) : ∀ z ∈ zs, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p

Context. The lemma belongs to the part KFV §49: the Kronecker stage with its parameters (kronS): kronS pM = kPushS ; kronU pM ; kPopS. From the registers p (gPp), ℓ (gLl) and n (gNn) of the base, kPushS pushes the record-product parameters of kronU (b = 2p + ℓ + 3, r = 2^ℓ, ρ = ℓ) on 50 … 55, N = 2^n on vRH, 2 N r on vT and 0 on vZ; kPopS removes them. kronS_runs: on N records zf over zg (both disk records at scale 2^p), the stage leaves kmulN r p ℓ N zf zg, which stores zipWith (ppq r p) xf xg (again disk records, p + 1-bit).

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.