The common frame (`fx_frame`)

Proved

J6Seg.Ax.fx_frame

by xuanji · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

The common frame: the set-up, a FineBody6-style call, the tear-down.

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

theorem J6Seg.Ax.fx_frame (w f a y : ℕ) (hF0 : dF ≠ 0) (hFA : dF ≠ dA) (hA0 : dA ≠ 0)
    (hSet : SetupS Isym tbl stUp stDn ![dF] dA desc ![descFine w f a y] Cs)
    {e : Fin Pp} {g : List GI → List GI} {Ce : ℝ}
    (he : ∀ (s : IState HS) (F : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
      (∀ j, j ≠ 0 → j ≠ dF → F j = []) → F dF = descFine w f a y → F 0 = gflat zs ++ l →
      zs.length = a * (2 ^ f * y) → GB w zs →
      ∃ c : ℕ, IRuns Isym tbl (.call e) (encK s F)
        (encK s (Function.update F 0 (gflat (g zs) ++ l))) c ∧ (c : ℝ) ≤ Ce) :
    PassOK Isym tbl (fxSt stUp stDn e) dA desc
      (fun L => L.length = a * (2 ^ f * y) ∧ GB w L) g (2 * Cs + Ce)

Context. A-line axis program (AxisUA6), part 2: a fine exposure as a PassOK step

fxSt stUp stDn e = stUp; call e; stDn: the set-up pushes the fine descriptor descFine w f a y onto the fine stack dF (computed from the axis descriptor on dA, SetupS with the one register dF), the exposure e (FineBody6, forward eF or back eB), the tear-down pops it.

fxF_ok / fxB_ok: the step computes blkT (2^f) y a / blkT y (2^f) a on stack 0 at cost 2 Cs + C₀ cFine w f a y.

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*).

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs68

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.Ax
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {stUp stDn : IStmt HS Pp}
  {eF eB : Fin Pp} {dF dA : Fin HS} {desc : List ℤ} {C₀ Cs : ℝ}

Formal statement

theorem J6Seg.Ax.fx_frame (w f a y : ℕ) (hF0 : dF ≠ 0) (hFA : dF ≠ dA) (hA0 : dA ≠ 0)
    (hSet : SetupS Isym tbl stUp stDn ![dF] dA desc ![descFine w f a y] Cs)
    {e : Fin Pp} {g : List GI → List GI} {Ce : ℝ}
    (he : ∀ (s : IState HS) (F : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
      (∀ j, j ≠ 0 → j ≠ dF → F j = []) → F dF = descFine w f a y → F 0 = gflat zs ++ l →
      zs.length = a * (2 ^ f * y) → GB w zs →
      ∃ c : ℕ, IRuns Isym tbl (.call e) (encK s F)
        (encK s (Function.update F 0 (gflat (g zs) ++ l))) c ∧ (c : ℝ) ≤ Ce) :
    PassOK Isym tbl (fxSt stUp stDn e) dA desc
      (fun L => L.length = a * (2 ^ f * y) ∧ GB w L) g (2 * Cs + Ce) := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `J6Seg.Ax.fx_frame`, Solutions/J6SegAxA2.lean (lines 31–91) of the round-six development.

View graph