The source transform (round six, `ftil_phase6`)

The source transform.

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

theorem IntMul.Kappa.R6.ftil_phase6 (hp₃ : ∀ j, iprog (g₃ j) = (IL.kTableP tab ext₃ j).ren id g₃)
    (hp₄ : ∀ j, iprog (g₄ j) = (IL.kTableP tab ext₄ j).ren id g₄)
    {Q : Q6} (hQ : QOk Q) {D : ℕ} (hD : Q.d = D + 1)
    [instS : ∀ i, NeZero (Q.sB D i)] [instT : ∀ i, NeZero (Q.tB D i)]
    (M : AxisMaps6 Q.α (Q.sB D) (Q.tB D))
    {eA eB : Fin (7 + P₃)} {dSL : Fin HS} {C₀ : ℝ} {A : ℕ} (hdL : dSL ≠ 0)
    (hL : lineG6 Isym (IL.kTableP tab ext₃) eA eB dSL C₀ A Q D M)
    {eC : Fin (7 + P₄)} {dSC : Fin HS} {C₁ : ℝ} {A₁ : ℕ} (hdC : dSC ≠ 0)
    {θt θit at' bt : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ} {ζ : ℂ}
    (hζ : ζ ^ Q.tB D (Fin.last D) = -1)
    (hθ : Phases Q.p (twX (Q.tB D) ζ) θt)
    (hθi : Phases Q.p (fun j => (twX (Q.tB D) ζ j)⁻¹) θit)
    (ha : Phases Q.p (fun j => (starRingEnd ℂ) (chirp (Q.sB D) (Q.tB D) j)) at')
    (hb' : Phases Q.p (chirp (Q.sB D) (Q.tB D)) bt) (hbg : Grid Q.p bt)
    (hC : chirpG6 Isym (IL.kTableP tab ext₄) eC dSC C₁ A₁ Q D θt θit at' bt)
    (BL BC : ℕ) (hBL : ∀ x ∈ Q.dLn, zsz x ≤ BL) (hBC : ∀ x ∈ Q.dCh, zsz x ≤ BC)
    (t : IState HS) (hR : Q.Base t) (zs : List GI)
    (u : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ) (R0 : List Item)
    (h0 : t.G 0 = ints (gflat zs) ++ R0)
    (hu : RepPad Q.p (Q.sB D) (Q.tB D) zs u) (hu1 : ‖u‖ ≤ 1 / 2) :
    ∃ (zs' : List GI) (U : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ) (c : ℕ),
      IRuns Isym iprog (ftilP6 g₃ g₄ eA eB eC dSL dSC) t (t.upd 0 (ints (gflat zs') ++ R0)) c ∧
      RepPad Q.p (Q.sB D) (Q.tB D) zs' U ∧
      GB (Q.p + 2 + (2 * (D + 1) * Q.α ^ 2 + 1)) zs' ∧
      ‖U - Rperm (Q.sB D) (Q.tB D) (dftM (Q.sB D) u)‖ ≤ Q.Es * hp Q.p ∧
      (c : ℝ) ≤ kCall6 Q 2 4 BL C₀ A + kCall6 Q 2 5 BC C₁ A₁ + kCall6 Q 2 4 BL C₀ A +
        kShl6 Q D

Context. Round-six machine: the source transform and one input

The frozen KFMChain / KFMBig4 / KFMBig5 / KFMBig6 at the round-six parameters:

• lemma20_6, source_call6, w_small6: Lemma 20 and one source transform with the exact per-axis maps AxisMaps6 (only A, B, hA, hB, hid are used);
• ftil_phase6: A-lines; chirp; B₀-lines; ×2^γ;
• Ix6, BigCtx6: the fixed data and the context of one size;
• digW_runs6, inP_phase6: one input.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).