State errors of the recurrence, unit u = 2^{-Δ}: after k steps ‖h_k - H C^k‖ ≤ (4k+1)u and ‖g_k - G H^k…

State errors of the recurrence, unit u = 2^{-Δ}: after k steps ‖h_k - H C^k‖ ≤ (4k+1)u and ‖g_k - G H^k C^{k(k-1)/2}‖ ≤ 4k²u.

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

theorem NLogN.KFM.cst_err (Δ : ℕ) (c h g : GI) (C H G : ℂ) (hC : ‖C‖ ≤ 1) (hH : ‖H‖ ≤ 1)
    (hG : ‖G‖ ≤ 1) (hc : ‖vP Δ c - C‖ ≤ (2 : ℝ)⁻¹ ^ Δ) (hh : ‖vP Δ h - H‖ ≤ (2 : ℝ)⁻¹ ^ Δ)
    (hg : ‖vP Δ g - G‖ ≤ 0) :
    ∀ k : ℕ, (4 * (k : ℝ) ^ 2 + 1) * (2 : ℝ)⁻¹ ^ Δ ≤ 1 →
      ‖vP Δ (cst Δ c h g k).1 - H * C ^ k‖ ≤ (4 * k + 1) * (2 : ℝ)⁻¹ ^ Δ ∧
      ‖vP Δ (cst Δ c h g k).2 - G * H ^ k * C ^ (k * (k - 1) / 2)‖ ≤ 4 * (k : ℝ) ^ 2 * (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.