The uniform leaf (round six, `sImplQ_leafU`)

Proved

NLogN.KFW.sImplQ_leafU

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

complexity-theoryinteger-multiplicationkappa-improvement

The uniform leaf.

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

theorem NLogN.KFW.sImplQ_leafU {σ : Fin HS → Option ℤ} {K t S0 r H e B : ℕ}
    (hL : LevR σ K t S0 r H 0 e B) (hQ : ∀ s, Q s → Agree σ s) (hS : 1 ≤ S0) (hB : 1 ≤ B)
    (hr : 1 ≤ r) (het : e < t) (Z : ℕ) (hZ : zsz ((12 * (B * 2 ^ t * S0 * r)) : ℕ) ≤ Z)
    (Bq : ℕ) (hBq : zsz ((4 * (B * 2 ^ t * S0 * r)) : ℕ) ≤ Bq) :
    SImplQ Isym tbl Q lo hi r (fun i : Fin (mC ^ 0) => 2 ^ (e - K * i.val) * S0) (B * 2 ^ t * S0)
      (tens Cm) leafC (ES 0) 2 (fun w => 400 * (ck (B * 2 ^ t * S0 * r) Z w + xLeaf Bq))

Context. KFW: substituted pushes and the uniform leaf (level 0)

Ex.okBnd_sub, Ex.regs_sub_none, Ex.size_sub, ExV.sub: literal substitution keeps definedness, values and bit bounds.
href_sub_push: a push of an expression whose registers are all bound by σ is, after substitution, a header refinement of the push of its value.
sImplQ_leafU: the leaf code leafC (qopU [MC] eB1L eGL) implements tens Cm on the single bit of level 0, scale ES 0 = 1, width +2, from KFN.sImpl_leaf.

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.KFW
open IntMul NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN Complex Butterfly
variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {Q : IState HS → Prop}
  {lo hi : ℕ}

Formal statement

theorem NLogN.KFW.sImplQ_leafU {σ : Fin HS → Option ℤ} {K t S0 r H e B : ℕ}
    (hL : LevR σ K t S0 r H 0 e B) (hQ : ∀ s, Q s → Agree σ s) (hS : 1 ≤ S0) (hB : 1 ≤ B)
    (hr : 1 ≤ r) (het : e < t) (Z : ℕ) (hZ : zsz ((12 * (B * 2 ^ t * S0 * r)) : ℕ) ≤ Z)
    (Bq : ℕ) (hBq : zsz ((4 * (B * 2 ^ t * S0 * r)) : ℕ) ≤ Bq) :
    SImplQ Isym tbl Q lo hi r (fun i : Fin (mC ^ 0) => 2 ^ (e - K * i.val) * S0) (B * 2 ^ t * S0)
      (tens Cm) leafC (ES 0) 2 (fun w => 400 * (ck (B * 2 ^ t * S0 * r) Z w + xLeaf Bq)) := 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.KFW.sImplQ_leafU`, Solutions/KFWLeaf.lean (lines 161–317) of the round-six development.

View graph