The correction, register-driven (round six, `corrU_spec`)

Proved

NLogN.KFX.corrU_spec

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

complexity-theoryinteger-multiplicationkappa-improvement

The correction, register-driven.

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

theorem NLogN.KFX.corrU_spec :
    ∃ Kc : ℝ, 0 < Kc ∧
      ∀ (K ρ f : ℕ), 6 ≤ K → ρ < K → 1 ≤ f →
      ∀ (g : Geo), g.Pos → g.Q = 2 ^ (f * K) →
      ∀ (I : List Sym) (iprog : Fin 1 → IStmt HS 1) (t : IState HS) (zs : List ℤ) (R : List Item),
      KFL.Bits zs → t.G 0 = ints zs ++ R → zs.length = g.V →
      ∀ (e1 e2 e3 e4 e5 e6 e7 e8 e9 e10 : Ex HS) (Bb : ℕ),
      ((corrPl e1 e2 e3 e4 e5 e6 e7 e8 e9 e10).map fun p => p.2.size + 1).sum ≤ 100 →
      NoLow e1 → NoLow e2 → NoLow e3 → NoLow e4 → NoLow e5 → NoLow e6 → NoLow e7 → NoLow e8 →
      NoLow e9 → NoLow e10 →
      ESp e1 t Bb (g.recG.S0 : ℤ) → ESp e2 t Bb ((2 : ℤ) ^ (f * K)) →
      ESp e3 t Bb (g.recG.S1 : ℤ) → ESp e4 t Bb (g.recG.S2 : ℤ) → ESp e5 t Bb (g.B : ℤ) →
      ESp e6 t Bb ((2 : ℤ) ^ ρ) → ESp e7 t Bb ((f - 1 : ℕ) : ℤ) → ESp e8 t Bb ((2 : ℤ) ^ K) →
      ESp e9 t Bb (g.recG.V : ℤ) → ESp e10 t Bb (zsz (g.V : ℤ) : ℤ) →
      ∃ c : ℕ, IRuns I iprog (corrU e1 e2 e3 e4 e5 e6 e7 e8 e9 e10) t
          (t.upd 0 (ints (rixT g (corrc K ρ f) zs) ++ R)) c ∧
        (c : ℝ) ≤ Kc * corrB K f g + 10 ^ 10 * ((Bb : ℝ) + 2) ^ 2

Context. KFX §3: the guard-set correction with register parameters

corrRSU is KFL.corrRS K ρ f g A with the size-dependent literals read from the registers 1 … 10: recG.S0, Q, recG.S1, recG.S2, B, 2^ρ, f-1, 2^K, M = recG.V, A. corrRSU_sub: the literal instance is RS.sub. corrU_spec: withPushI plC (fcode corrRSU) computes rixT g (corrc K ρ f) at the cost of KFL.corrI_spec (times 400, plus the pushes).

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFX
open IntMul NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW AModel Butterfly

Formal statement

theorem NLogN.KFX.corrU_spec :
    ∃ Kc : ℝ, 0 < Kc ∧
      ∀ (K ρ f : ℕ), 6 ≤ K → ρ < K → 1 ≤ f →
      ∀ (g : Geo), g.Pos → g.Q = 2 ^ (f * K) →
      ∀ (I : List Sym) (iprog : Fin 1 → IStmt HS 1) (t : IState HS) (zs : List ℤ) (R : List Item),
      KFL.Bits zs → t.G 0 = ints zs ++ R → zs.length = g.V →
      ∀ (e1 e2 e3 e4 e5 e6 e7 e8 e9 e10 : Ex HS) (Bb : ℕ),
      ((corrPl e1 e2 e3 e4 e5 e6 e7 e8 e9 e10).map fun p => p.2.size + 1).sum ≤ 100 →
      NoLow e1 → NoLow e2 → NoLow e3 → NoLow e4 → NoLow e5 → NoLow e6 → NoLow e7 → NoLow e8 →
      NoLow e9 → NoLow e10 →
      ESp e1 t Bb (g.recG.S0 : ℤ) → ESp e2 t Bb ((2 : ℤ) ^ (f * K)) →
      ESp e3 t Bb (g.recG.S1 : ℤ) → ESp e4 t Bb (g.recG.S2 : ℤ) → ESp e5 t Bb (g.B : ℤ) →
      ESp e6 t Bb ((2 : ℤ) ^ ρ) → ESp e7 t Bb ((f - 1 : ℕ) : ℤ) → ESp e8 t Bb ((2 : ℤ) ^ K) →
      ESp e9 t Bb (g.recG.V : ℤ) → ESp e10 t Bb (zsz (g.V : ℤ) : ℤ) →
      ∃ c : ℕ, IRuns I iprog (corrU e1 e2 e3 e4 e5 e6 e7 e8 e9 e10) t
          (t.upd 0 (ints (rixT g (corrc K ρ f) zs) ++ R)) c ∧
        (c : ℝ) ≤ Kc * corrB K f g + 10 ^ 10 * ((Bb : ℝ) + 2) ^ 2 := 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 `NLogN.KFX.corrU_spec`, Solutions/KFX3Corr.lean (lines 185–332) of the round-six development.

View graph