Round-six lemma `cgP_sp`

Proved

J6Seg.Src.cgP_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6Seg.Src.cgP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {R Y : Fin HS} (hR5 : R.val < 56)
    (hY5 : Y.val < 56) (hRY : R ≠ Y) (hY43 : Y ≠ 43) (hR43 : R ≠ 43) (h43 : F 43 = []) {m A : ℕ}
    {LR : List ℤ} (hFR : F R = (m : ℤ) :: LR) (hmA : 2 ^ Nat.clog 2 m ≤ 2 ^ A) (hA : 2 ≤ A) :
    Sp (cgP R Y) (encK s0 F) (encK s0 (update F Y (((2 ^ Nat.clog 2 m : ℕ) : ℤ) :: F Y)))
      (2 * uC A DD + (m + 1) * ((2 * (10 * uC A DD) + 200 * (A * DD + 1 + 1)) + uC A DD))

Context. B-line IL, source-table producers, part 12: loops of the set-up

pw2P X Y: push 2^m on Y for m on X (doubling loop, counter 43);
cgP R Y: push 2^⌈log₂ m⌉ on Y for m on R (conditional doubling, counter 43);
dropP R X k: pop k · m entries of X for m on R (counter 43).

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
open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg
open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg

Formal statement

theorem J6Seg.Src.cgP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {R Y : Fin HS} (hR5 : R.val < 56)
    (hY5 : Y.val < 56) (hRY : R ≠ Y) (hY43 : Y ≠ 43) (hR43 : R ≠ 43) (h43 : F 43 = []) {m A : ℕ}
    {LR : List ℤ} (hFR : F R = (m : ℤ) :: LR) (hmA : 2 ^ Nat.clog 2 m ≤ 2 ^ A) (hA : 2 ≤ A) :
    Sp (cgP R Y) (encK s0 F) (encK s0 (update F Y (((2 ^ Nat.clog 2 m : ℕ) : ℤ) :: F Y)))
      (2 * uC A DD + (m + 1) * ((2 * (10 * uC A DD) + 200 * (A * DD + 1 + 1)) + 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.cgP_sp`, Solutions/J6SegILSrc12.lean (lines 103–168) of the round-six development.

View graph