The lines on the canonical layout

The lines on the canonical layout.

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

theorem NLogN.KFL.linesI_spec :
    ∃ T q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∃ Ks : ℝ, 0 ≤ Ks ∧
      ∀ (K ρ f : ℕ), 1 ≤ K → ρ < K → 1 ≤ f →
      ∀ (g : Geo), g.Pos → g.Q = 2 ^ (f * K) →
      ∀ (Bb : ℕ), 2 ≤ Bb → 4 * 2 ^ (f * K) < 2 ^ Bb → zsz (g.V : ℤ) ≤ Bb →
      ∀ (ls : List Line), (∀ l ∈ ls, LineOK l) →
      ∀ (I : List Sym) (t : IState HS) (zs : List ℤ) (R : List Item),
      Bits zs → t.G 0 = ints zs ++ R → zs.length = g.V →
      ∃ c : ℕ, IRuns I l12prog (linesI q K ρ f g ls) t
          (t.upd 0 (ints (rixT g (fun c => ls.foldr (fun l c => lineP K ρ f l c) c) zs) ++ R)) c ∧
        (c : ℝ) ≤ 1 + ls.length * (2 * Ks * ((g.V : ℝ) + 1) * ((f * K : ℕ) : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50)
          + cRotG K f g Bb)

Context. The lemma belongs to the part KFL §7: the eight packed lines (22) on the canonical layout: On the 8-axis geometry sh8 = [N0,Q,N1,Q,N2,Q,N3,B] (Q = 2^{fK}; slots x, y, z = axes 1, 3, 5) a tgtZ line is one rotStep (rotation of slot z by amt l x y), a tgtY line is swap(3,5); rotStep; swap(3,5) (Lemma 12 swaps). linesI_spec: running the lines ls in order gives rixT g (ls.foldr (lineP K ρ f)); for ls = lines this is rixT g (FSc K ρ f) (KFLMath: FSc is the pull map of S0). Cost: per line ≤ 2 K_s (V+1) (fK)^τ + cRot.

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_Defs18.