Round-eight bit network dominates Jain.bitR8 moments

Round-eight bit network, moment-dominance form.

There exists a QH-network $C$ over $\mathbb{Z}/2\mathbb{Z}$ with $W_b = 104\,719\,230$ roles and width $m_b = 529$, together with a prime cutoff $q_0$, such that:

1. $C$ runs correctly (RunsOK);
2. for every prime $q > q_0$ and every exponent $f$, the edge and formal checks hold at the prime power $q^f$;
3. for every exponent $\tau \in (0,1]$, the child-width moment of $C$ is at most that of Jain's round-eight bit histogram:

where $h^{\mathrm{bit}}=\mathrm{Jain.bitR8}$ is the opposite-bank-order bit interchange of round eight (width classes up to $22$, a $484$-class, and the $506$–$528$ tail).

In the platform vocabulary this is exactly

At the round-six constants $(148225616,529,\mathrm{Jain.bitR6})$ the same predicate is Bit.BitNetR6MomStmt, already proved as IntMul.Kappa.R6.Bit.NB.bitNetR6_mom_exp.

This is the bit-network machine interface needed to feed Jain's round-eight histogram into the parametric assembly IntMul.Kappa.R6.kappa_finalG_at, and thence into IntMul.Kappa.jain_round8_framework.