Round-eight complex histogram child widths are less than 576

Proved

IntMul.Kappa.R8.cxR8_widths_lt

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

complexity-theoryinteger-multiplicationround-eight

Let cxR8 be S. Jain's round-eight complex-side child-width histogram. The complex interchange runs at width $m=576$ . The interface Prop8IfaceH requires every recorded child width to satisfy $w<m$ . This theorem is the finite check

\forall (w,n_w)\in\texttt{cxR8},\qquad w<576.

(The largest listed child is $529$ .)

Preamble

import Definitions.Def_IntMul_KappaJainData

set_option autoImplicit false
set_option relaxedAutoImplicit false

Formal statement

namespace IntMul.Kappa.R8

open IntMul.Kappa.Jain

/-- Every child width appearing in `Jain.cxR8` is strictly less than the complex-network width $m = 576$
(as required by `Prop8IfaceH.small`). -/
theorem cxR8_widths_lt : ∀ p ∈ cxR8, p.1 < 576 := by
  sorry

end IntMul.Kappa.R8

Source

S. Jain, integer-mult-kappa, lean/Round8.lean cxHist; Def_IntMul_KappaJainData Jain.cxR8; Prop8IfaceH.small in Def_IntMul_Kappa_R6_Defs2

View graph