Chunk table bound ChunkTabBnd6 for every admissible $P$

Proved

J6Seg.chunkTabBnd6_all

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplication

For every admissible round-six parameter record $P$ , the chunk-table bound interface $\mathsf{ChunkTabBnd6}\,P$ holds: there is a threshold $n_1$ such that for all $n\ge n_1$ and every admissible source list, every axis $k$ satisfies the absolute-value bound $|T_{\bullet}|\le 2^{Q+R+2}$ on the chunk table $T=\mathrm{TT}(Q,R,s,t,\alpha)$ .

This is the pure table-size input to the chunk-budget assembly.

Preamble

import Definitions.Def_IntMul_Kappa_R6_Defs70

set_option autoImplicit false
set_option relaxedAutoImplicit false

open J6Seg
open IntMul.Kappa.R6

Formal statement

theorem J6Seg.chunkTabBnd6_all (P : IntMul.Kappa.R6.Prm) (hP : P.Ok) :
    J6Seg.ChunkTabBnd6 P := by
  sorry

Source

xuanji round-six κ; J6Seg TabBnd / AxBud

View graph

Chunk table bound ChunkTabBnd6 for every admissible PPP

Chunk table bound ChunkTabBnd6 for every admissible $P$