Run twRS as IL code and move the root onto X (re on top). -/ def twC (n k j : ℕ) (X : Fin HS) : IStmt HS P…

Run twRS as IL code and move the root onto X (re on top). -/ def twC (n k j : ℕ) (X : Fin HS) : IStmt HS P := .seq (RS.code (twRS n k j)) (.seq (.op (.mv 52 X)) (.op (.mv 51 X))) def cTw (n k j : ℕ) : ℕ := twiddleCost n (zsz (j : ℤ)) (zsz (k : ℤ)) + 7 * 10 ^ 7 * (zsz (n : ℤ) + zsz (k : ℤ) + zsz (j : ℤ) + 2) ^ 2 + 220 * (n + 4) theorem twC_runs (n k j : ℕ) (hk : 0 < k) (X : Fin HS) (h51 : X ≠ 51) (h52 : X ≠ 52) (s : IState HS) : IRuns I iprog (twC n k j X) s (s.upd X (.int (HvdH.twiddle n k j).1 :: .int (HvdH.twiddle n k j).2 :: s.G X)) (cTw n k j) := by obtain ⟨o, r, c⟩ := twRS_spec n k j s have h1 := RS.code_runs (I := I) (iprog := iprog) (twRS n k j) s o rw [r] at h1 set s1 := (s.upd 51 (.int (HvdH.twiddle n k j).1 :: s.G 51)).upd 52 (.int (HvdH.twiddle n k j).2 :: s.G 52) with hs1 have m1 := IRuns.mv (I := I) (iprog := iprog) (s := s1) (i := 52) (j := X) (a := (HvdH.twiddle n k j).2) (L := s.G 52) h52.symm (by simp +decide [hs1]) set s2 := (s1.upd 52 (s.G 52)).upd X (.int (HvdH.twiddle n k j).2 :: s1.G X) with hs2 have m2 := IRuns.mv (I := I) (iprog := iprog) (s := s2) (i := 51) (j := X) (a := (HvdH.twiddle n k j).1) (L := s.G 51) h51.symm (by simp +decide [hs2, hs1, h52.symm, h51.symm]) have hb := zsz_of_near n (HvdH.twiddle n k j) _ (norm_exp_phase (2 * Real.pi * j / k) _ (by push_cast; ring)) ((vP_twiddle n k j hk).trans (pow_le_one₀ (by norm_num) (by norm_num))) refine (h1.seq (m1.seq m2)).mono' ?_ ?_ · simp only [hs2, hs1] clear h1 m1 m2 st_eq · unfold cTw have := moveIntCost_le (zsz (HvdH.twiddle n k j).1); have := moveIntCost_le (zsz (HvdH.twiddle n k j).2) omega /-! ## Size bounds along the recurrence

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

theorem NLogN.KFM.cst_bnd (Δ n : ℕ) (c h : GI) (C H : ℂ) (hC : ‖C‖ ≤ 1) (hH : ‖H‖ ≤ 1)
    (hc : ‖vP Δ c - C‖ ≤ (2 : ℝ)⁻¹ ^ Δ) (hh : ‖vP Δ h - H‖ ≤ (2 : ℝ)⁻¹ ^ Δ)
    (hu : (4 * (n : ℝ) ^ 2 + 1) * (2 : ℝ)⁻¹ ^ Δ ≤ 1) :
    ∀ k ≤ n, GBnd (Δ + 2) (cst Δ c h (oneP Δ) k).1 ∧ GBnd (Δ + 2) (cst Δ c h (oneP Δ) k).2

Context. The lemma belongs to the part KFM 9c: the per-axis root-table program (chirpL recurrence in IL).

Formalization Note. This lemma belongs to the item-language (IL) layer of the integer-multiplication-kappa campaign: tape-level programs (register programs over 64 item stacks of the NLogN multitape framework, definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8) that implement the data-movement primitives of the OpenAI preprint Integer multiplication below $n\log n$ (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine $O(1)$-per-element costs, Gaussian record primitives, Proposition 14 pieces) with exact list denotations from the array-model bundles IntMul_Kappa_K_Defs* and explicit cost bounds. All names refer to the definition bundles up to IntMul_Kappa_K_Defs22.