The near-boundary test and record (`near_runs`)

Proved

J6Seg.Src.near_runs

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

complexity-theoryinteger-multiplicationkappa-improvement

The near-boundary test and record.

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

theorem J6Seg.Src.near_runs (s0 : IState HS) (G : Fin HS → List ℤ) {iW : Fin HS} (fW : Free iW)
    {w : ℕ} {LW : List ℤ} (hGW : G iW = (w : ℤ) :: LW)
    (x13 x14 x15 x30 x31 x32 x33 x44 : List ℤ) {j cn st E A : ℕ}
    (hjA : j + 1 ≤ 2 ^ A) (hcA : cn + 1 ≤ 2 ^ A) (hsA : st ≤ 2 ^ A) (hEA : E ≤ 2 ^ A)
    (hwA : w ≤ 2 ^ A) (hA : 2 ≤ A) :
    Sp (.ite (c1E iW) pushJ (.ite (c2E iW) pushJ .skip))
      (encK s0 (J6Seg.Src.bS G x13 ((st : ℤ) :: x14) ((E : ℤ) :: x15) x30 ((cn : ℤ) :: x31) x32 x33
        [(j : ℤ) + 1] x44))
      (encK s0 (J6Seg.Src.bS G x13 ((st : ℤ) :: x14) ((E : ℤ) :: x15)
        (if j < st + w ∨ E < j + w + 1 then (j : ℤ) :: x30 else x30)
        (((if j < st + w ∨ E < j + w + 1 then cn + 1 else cn : ℕ) : ℤ) :: x31) x32 x33
        [(j : ℤ) + 1] x44)) (50 * uC A DD)

Context. B-line IL, source-table producers, part 4: ljP, the backward pass

State after k backward steps (m = s - k positions left, the next one j = m - 1): 14 holds the forward starts of 0, …, m-1 (last first) over the sentinel, 15 the block end ncv m = eB (m-1), and 30, 31, 32, 33 the outputs on positions m, …, s-1.

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_Defs65

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.Src
set_option maxRecDepth 20000
open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg.PreT J6Seg

Formal statement

theorem J6Seg.Src.near_runs (s0 : IState HS) (G : Fin HS → List ℤ) {iW : Fin HS} (fW : Free iW)
    {w : ℕ} {LW : List ℤ} (hGW : G iW = (w : ℤ) :: LW)
    (x13 x14 x15 x30 x31 x32 x33 x44 : List ℤ) {j cn st E A : ℕ}
    (hjA : j + 1 ≤ 2 ^ A) (hcA : cn + 1 ≤ 2 ^ A) (hsA : st ≤ 2 ^ A) (hEA : E ≤ 2 ^ A)
    (hwA : w ≤ 2 ^ A) (hA : 2 ≤ A) :
    Sp (.ite (c1E iW) pushJ (.ite (c2E iW) pushJ .skip))
      (encK s0 (J6Seg.Src.bS G x13 ((st : ℤ) :: x14) ((E : ℤ) :: x15) x30 ((cn : ℤ) :: x31) x32 x33
        [(j : ℤ) + 1] x44))
      (encK s0 (J6Seg.Src.bS G x13 ((st : ℤ) :: x14) ((E : ℤ) :: x15)
        (if j < st + w ∨ E < j + w + 1 then (j : ℤ) :: x30 else x30)
        (((if j < st + w ∨ E < j + w + 1 then cn + 1 else cn : ℕ) : ℤ) :: x31) x32 x33
        [(j : ℤ) + 1] x44)) (50 * uC A DD) := 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.Src.near_runs`, Solutions/J6SegILSrc4.lean (lines 170–249) of the round-six development.

View graph