Child-width moment at exponent 1 equals rank sum over width

Proved

IntMul.Kappa.histMoment_one

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

complexity-theoryinteger-multiplication

Let $h=((w_i,n_i))_i$ be a child-width histogram and let $m>0$ be a network width. The moment at exponent $1$ collapses to the normalized rank sum:

\mathrm{histMoment}(h,m,1)=\sum_i n_i\cdot\frac{w_i}{m}=\frac{1}{m}\sum_i w_i n_i=\frac{\mathrm{histRankSum}(h)}{m}.

This identity is the $\tau=1$ endpoint used when comparing frozen round-seven/eight bit histograms (equal rank sums imply equal moments at exponent $1$ ).

Preamble

import Definitions.Def_IntMul_KappaFramework

set_option autoImplicit false
set_option relaxedAutoImplicit false

Formal statement

namespace IntMul.Kappa

/-- At exponent $1$, the child-width moment equals the rank sum divided by the network width:
$\mathrm{histMoment}(h,m,1)=(\mathrm{histRankSum}\,h)/m$. -/
theorem histMoment_one (h : List (ℕ × ℕ)) (m : ℕ) (hm : (m : ℝ) ≠ 0) :
    histMoment h m 1 = (histRankSum h : ℝ) / m := by
  sorry

end IntMul.Kappa

Source

Def_IntMul_KappaFramework histMoment / histRankSum; used with Jain bitR7plain / bitR8 rank-sum identities

View graph