Prove2Me

The chunk output bound at one axis (round six, `chunkOutAt_of`)

Proved
J6Seg.AxCh.chunkOutAt_of

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

complexity-theoryinteger-multiplicationkappa-improvement

The chunk output bound at one axis.

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

theorem J6Seg.AxCh.chunkOutAt_of (hT : TabAt P n src k) (hc : ChunkPlan6 ap) : ChunkOutAt P ap n src k

Context. B-line axis: the chunk kernel's output bound (ChunkOut6)

  • AB_chunkB, AB_chunkG2: all-blocks growth (chunkOK) bounds the chunk output;
  • Xs_le_pow: Xs K X i ≤ 2^((a+1) i) X for 0 ≤ K ≤ 2^a;
  • ChunkPlan6 ap: linear lower bounds on pkA, pkC, wA, wC (value-only plan conditions);
  • chunkOutAt_of: TabAt → ChunkPlan6 ap → ChunkOutAt (one axis);
  • chunkOut6_of: ChunkTabBnd6 P → ChunkPlan6 ap → ChunkOut6 P ap (whole regime).

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_Defs67

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.AxCh
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function J6Seg J6Seg.KR J6Seg.Ax
variable (P : Prm) (ap : AxPlan6) (n : ℕ) (src : ℕ → ℕ) (D k : ℕ)
Formal statement
theorem J6Seg.AxCh.chunkOutAt_of (hT : TabAt P n src k) (hc : ChunkPlan6 ap) : ChunkOutAt P ap n src k := 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.AxCh.chunkOutAt_of`, Solutions/J6SegAxChunk.lean (lines 106–157) of the round-six development.

View graph