R8 densified net0P histMoment equals Jain.bitR8

Open

IntMul.Kappa.R8.Bit.Oppbank.mom_eq

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

bitnbinteger-multiplicationkappamom-eqoppbankr8

For the densified opp-bank network $\mathrm{net0P}$ , the child-width moment function agrees with Jain's opposite-bank histogram on every positive scale:

\forall\tau:\mathbb{R},\quad \mathrm{histMoment}(\mathrm{net0P.hist},529,\tau)=\mathrm{histMoment}(\texttt{bitR8},529,\tau).

MomPack already identifies $\mathrm{oppbankHist}=\texttt{bitR8}$ . The remaining work is to expand $\mathrm{net0P.hist}$ through edge moments ( $\mathrm{EM}_{\mathrm{side}}/\mathrm{aux}/\mathrm{data}$ ) and GenCN/SideRanks to match $\mathrm{oppbankHist}$ .

Preamble

import Definitions.Def_IntMul_Kappa_RG_Defs
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_Kappa_R6_Defs4
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankNet0P
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankNetMom
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankMomPack
import Mathlib

set_option autoImplicit false
set_option relaxedAutoImplicit false

Formal statement

namespace IntMul.Kappa.R8.Bit.Oppbank

open IntMul.Kappa
open IntMul.Kappa.Jain
open IntMul.Kappa.R6.Bit
open IntMul.Kappa.R8.Bit.Oppbank.Net0P

/-- Child-width moments of densified `net0P` match `Jain.bitR8` on all τ. -/
theorem mom_eq :
    ∀ τ : ℝ, histMoment net0P.hist 529 τ = histMoment bitR8 529 τ := by
  sorry

end IntMul.Kappa.R8.Bit.Oppbank

Source

NetMom 84ad4683; MomPack cddcbe7a; Net0P 373d80bb; Jain.bitR8

View graph