Round-seven plain bit network dominates Jain.bitR7plain moments

Round-seven plain bit network (witness 2), 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-seven plain bit histogram (witness 2 with the round-six entrance corner):

where $h^{\mathrm{old}}=\mathrm{Jain.bitR7plain}$ is the histogram whose certified saving is the $a_{\mathrm{old}}$ of round eight's stopped bit interchange.

In the platform vocabulary this is exactly

Relation to neighbouring nodes. The sister statement IntMul.Kappa.R6.Bit.bitNetR7_mom asserts the same interface for the other round-seven witness (Jain.bitR7, $W=108\,516\,254$). The round-eight opposite-bank network is IntMul.Kappa.R8.bitNetR8_mom (same $W=104\,719\,230$, histogram Jain.bitR8). The proved round-six instance is IntMul.Kappa.R6.Bit.NB.bitNetR6_mom_exp.

Role in round eight. Together with moment monotonicity in the exponent, this leaf discharges the stopped-mix branch $a_b\le a_{\mathrm{old}}$ of jain_round8_framework, feeding kappa_finalG_at when the convex combination sits on the plain side.

Formalization Note. BitNetMomStmtG is from IntMul_Kappa_RG_Defs; the histogram is from IntMul_KappaJainData (lean/Round7.lean, bitplainHist).