Round-six lemma `setup_of_native`

Proved

J6Seg.PJ.setup_of_native

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.J6SegILPreJC9):

theorem J6Seg.PJ.setup_of_native {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (eUp eDn : Fin Pp)
    (ρ : Fin 19 → Fin HS) (dA : Fin HS) (desc : List ℤ) (V : Fin 19 → List ℤ) (C : ℝ)
    (σ : Equiv.Perm (Fin HS)) (hσ : FixHi σ) (Zn : Fin HS) (oN : Fin 19 → Fin HS)
    (hinj : Injective oN) (hZ : σ Zn = dA) (hO : ∀ i, σ (oN i) = ρ i)
    (pU pD : RS) (hU : tbl eUp = (pU.ren σ).code) (hD : tbl eDn = (pD.ren σ).code) (cU cD : ℕ)
    (SU : ∀ s0, Sp pU (encK s0 (F0 Zn desc)) (encK s0 (extend oN V (F0 Zn desc))) cU)
    (SD : ∀ s0, Sp pD (encK s0 (extend oN V (F0 Zn desc))) (encK s0 (F0 Zn desc)) cD)
    (hCU : ((cU + 2 : ℕ) : ℝ) ≤ C) (hCD : ((cD + 2 : ℕ) : ℝ) ≤ C) :
    SetupBody6 Isym tbl eUp eDn ρ dA desc V C

Context. B5 set-up, part 9: from a native set-up pair to SetupBody6

A native pair pU, pD working on the descriptor on Zn and the output stacks oN (pU : F0 ↦ extend oN V F0, pD back), relocated by a permutation σ (σ Zn = dA, σ ∘ oN = ρ, fixing ≥ 55), gives SetupBody6 … ρ dA desc V C (setup_of_native). nativeLayout: such σ exists, with Zn ∈ {49, 55} and oN i ∈ {i + 1, 55}.

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_Defs69

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function

Formal statement

theorem J6Seg.PJ.setup_of_native {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (eUp eDn : Fin Pp)
    (ρ : Fin 19 → Fin HS) (dA : Fin HS) (desc : List ℤ) (V : Fin 19 → List ℤ) (C : ℝ)
    (σ : Equiv.Perm (Fin HS)) (hσ : FixHi σ) (Zn : Fin HS) (oN : Fin 19 → Fin HS)
    (hinj : Injective oN) (hZ : σ Zn = dA) (hO : ∀ i, σ (oN i) = ρ i)
    (pU pD : RS) (hU : tbl eUp = (pU.ren σ).code) (hD : tbl eDn = (pD.ren σ).code) (cU cD : ℕ)
    (SU : ∀ s0, Sp pU (encK s0 (F0 Zn desc)) (encK s0 (extend oN V (F0 Zn desc))) cU)
    (SD : ∀ s0, Sp pD (encK s0 (extend oN V (F0 Zn desc))) (encK s0 (F0 Zn desc)) cD)
    (hCU : ((cU + 2 : ℕ) : ℝ) ≤ C) (hCD : ((cD + 2 : ℕ) : ℝ) ≤ C) :
    SetupBody6 Isym tbl eUp eDn ρ dA desc V 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 `J6Seg.PJ.setup_of_native`, Solutions/J6SegILPreJC9.lean (lines 24–70) of the round-six development.

View graph