Every width in Jain.bitR8 lies in $(0,529]$

Proved

IntMul.Kappa.R8.bitR8_widths

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

complexity-theoryinteger-multiplicationround-eight

Width bounds for the round-eight bit histogram.

Every child-width pair $(w,n)$ in Jain's round-eight bit histogram $h^{\mathrm{bit}}=\mathrm{Jain.bitR8}$ (opposite bank orders on the round-seven witness 2; width bound $m=529$ ) satisfies

0 < w \le 529.

Together with the proved histMoment_mono_tau, this unlocks upgrading a moment bound at exponent $1-a^*$ to the stopped-mix exponent $1-a_b$ whenever $a_b\le a^*$ . The sister lemma bitR8_widths_le only records $w\le 529$ ; the strict positivity $w>0$ is required by the monotonicity hypothesis.

Formalization Note. bitR8 is from IntMul_KappaJainData (lean/Round8.lean, bitHist).

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 applying `histMoment_mono_tau` to the round-eight bit histogram.
Stronger than `bitR8_widths_le` by also requiring positive widths. -/
theorem bitR8_widths : ∀ p ∈ bitR8, 0 < p.1 ∧ p.1 ≤ 529 := by
  sorry

end IntMul.Kappa.R8

Source

S. Jain, integer-mult-kappa, lean/Round8.lean (bitHist), https://github.com/Swapnil-jain/integer-mult-kappa/tree/5868dc701a9bec375c9dc5391d992ab3b8c35f3f; used with Prove2me IntMul.Kappa.R8.histMoment_mono_tau and IntMul.Kappa.R8.bitR8_widths_le

View graph

Every width in Jain.bitR8 lies in (0,529](0,529](0,529]

Every width in Jain.bitR8 lies in $(0,529]$