The read-out (round six, `fin_phase6`)

Proved

IntMul.Kappa.R6.fin_phase6

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

complexity-theoryinteger-multiplicationkappa-improvement

The read-out.

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

theorem IntMul.Kappa.R6.fin_phase6 (C : BigCtx6 ix Isym tab extM Q D) (t : IState HS) (hR : Q.Base t) (x y : ℕ)
    (hx : x < 2 ^ Q.n) (hy : y < 2 ^ Q.n) (zsZ : List GI)
    (Z : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ)
    (h0 : t.G 0 = ints (gflat zsZ)) (hZ : RepPad Q.p (Q.sB D) (Q.tB D) zsZ Z)
    (hg : GB (wU6 Q D) zsZ) (hcl : Close6 C x y Z) (hout : t.out = []) :
    ∃ s' c, IRuns Isym (IL.kTableP tab extM) (finP6 ix) t s' c ∧
      s'.out = bin (2 * Q.n) (x * y) ∧ (c : ℝ) ≤ kFin6 C

Context. Round-six machine: the read-out and one run

The frozen KFMBig9 / KFMBig10 at the round-six parameters.

zsz_cN6, cconv_ubar6, pt_val6, zsW_GB6: the rounded numerators are the coefficients.
fin_phase6: finA; Φ⁻¹; carries; write.
big_run6: bigP6 = setup; mulP6; finP6 from the state after the reads, the setup being a call into a sub-table.

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_Defs16

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6
open Finset AModel AModelL12 IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFT NLogN.RS IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFM Complex
variable {E : ℕ} {ix : Ix6 (7 + E)} {Isym : List Sym} {tab : Fin 1 → IStmt HS 1}
  {extM : Fin E → IStmt HS (7 + E)} {Q : Q6} {D : ℕ}
  [instS : ∀ i, NeZero (Q.sB D i)] [instT : ∀ i, NeZero (Q.tB D i)]

Formal statement

theorem IntMul.Kappa.R6.fin_phase6 (C : BigCtx6 ix Isym tab extM Q D) (t : IState HS) (hR : Q.Base t) (x y : ℕ)
    (hx : x < 2 ^ Q.n) (hy : y < 2 ^ Q.n) (zsZ : List GI)
    (Z : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ)
    (h0 : t.G 0 = ints (gflat zsZ)) (hZ : RepPad Q.p (Q.sB D) (Q.tB D) zsZ Z)
    (hg : GB (wU6 Q D) zsZ) (hcl : Close6 C x y Z) (hout : t.out = []) :
    ∃ s' c, IRuns Isym (IL.kTableP tab extM) (finP6 ix) t s' c ∧
      s'.out = bin (2 * Q.n) (x * y) ∧ (c : ℝ) ≤ kFin6 C := 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 `IntMul.Kappa.R6.fin_phase6`, Solutions/R6MFin.lean (lines 152–255) of the round-six development.

View graph