Positive bounded widths of Jain.cxR8

Proved

IntMul.Kappa.R8.cxR8_widths

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

histogramjainkappa-r8

Every child width appearing in the round-eight complex histogram Jain.cxR8 is strictly positive and at most $529$ .

That is, for every pair $(w,n_w)$ in the histogram,

0 < w \le 529.

This is the width hypothesis needed to instantiate the parametric Prop.~14 interface at $w_{\max}=529$ and $m_c=576$ , and to compare complex moments across exponents.

Preamble

import Definitions.Def_IntMul_KappaJainData

set_option autoImplicit false
set_option relaxedAutoImplicit false

Formal statement

namespace IntMul.Kappa.R8

open IntMul.Kappa.Jain

/-- Width side-condition for `p14NeedG_all` / moment comparisons on `Jain.cxR8`:
every child width lies in $(0, 529]$. -/
theorem cxR8_widths : ∀ p ∈ cxR8, 0 < p.1 ∧ p.1 ≤ 529 := by
  sorry

end IntMul.Kappa.R8

Source

xuanji / Jain integer-mult-kappa round 8 complex histogram (Def_IntMul_KappaJainData.cxR8); side condition for R6.IL3H.p14NeedG_all at Wc=12869228, mc=576

View graph