The program is the ideal map on good states (round six, `Psi_good`)

Proved

IntMul.Kappa.R6.IL2C.Psi_good

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

complexity-theoryinteger-multiplicationkappa-improvement

The program is the ideal map on good states.

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

theorem IntMul.Kappa.R6.IL2C.Psi_good (hK : 1 ≤ K) (hG : 1 ≤ G) (hL : ρ + n * K ≤ L) (x : ℕ) {c : CS}
    (hb : Box G n L c) (hg : IntMul.Kappa.R6.IL2C.Good K ρ G n c) : Psi K ρ G n L x c = TlS K ρ n x c

Context. Round six, compact controls (I2C): the value-level mechanism

Colkitt's compact dirty controls, uniform variant (see jain6/compact/DESIGN.md). The state of one record is (t, u, y) (the temporary T, the control U, the target slot Y); the source slot x is a parameter. Radices: W = 2^K (slot segments), R = 2^G (compact digits); n low selected positions j_s = ρ + s K.

dgt W s x = x / W^s % W; digits_add: digit-wise addition without carries; eq_of_digits: equal low digits and equal high part give equal numbers.
segSum tf ru rv rw w0 u v n = Σ_{s<n} w0 rw^s tf (u / ru^s) (v / rv^s) (the register loop).
The offsets oA (Y += Σ 2 z_s t_s 2^{j_s}), oB (Y += Σ z_s (1 - 2 t_s) 2^{j_s}), oS (packed selected bits), oC (Σ (y_s xor z_s) R^s), oT (the ideal toggle).
The pull maps rT, rU, rY, the inverse phase phInv and the whole pull composite Psi.
Psi_good: on a good state Psi is the ideal map (toggle the n low selected bits of y by those of x); Psi_bij-type facts are proved at rank level.

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_Defs20

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2C
open Finset
variable {K ρ G n L : ℕ}

Formal statement

theorem IntMul.Kappa.R6.IL2C.Psi_good (hK : 1 ≤ K) (hG : 1 ≤ G) (hL : ρ + n * K ≤ L) (x : ℕ) {c : CS}
    (hb : Box G n L c) (hg : IntMul.Kappa.R6.IL2C.Good K ρ G n c) : Psi K ρ G n L x c = TlS K ρ n x 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.IL2C.Psi_good`, Solutions/R6IL2CMath.lean (lines 637–712) of the round-six development.

View graph