Opposite-bank recompile lifts bitR7plain moment network to bitR8
OpenIntMul.Kappa.R8.Bit.oppbank_mom_of_plainRound eight's bit-side witness (S. Jain, integer-mult-kappa, round eight) reuses the deferred round-seven witness 2: the same schedule, frames and payload word that produce the child-width histogram bitplainHist ( roles, width ), whose certified saving is the stopped-interchange parameter .
The only change is the address geometry of each interchange. In a generic rational basis every residual idempotent of rank has nonzero leading principal minors ; storing the tail bank in reverse atom order collapses the generic anti-diagonal Bruhat cell of each partial swap to one contiguous reversed run, so a residual of rank becomes a single child of width . An outer wrapper of three lower updates restores the ordinary interchange. The resulting child-width multiset is bitHist / Jain.bitR8.
On Prove2me the bit-network obligation is the parametric moment statement BitNetMomStmtG Wb mb hb: existence of a QH-network over with roles and width that runs correctly, is edge- and formally OK at all large prime powers, and whose child-width moments are dominated by those of the histogram at every exponent .
This problem asks for the opposite-bank recompile as a map of those statements: any witness of
yields a witness of
Together with the open leaf IntMul.Kappa.R8.bitNetR7plain_mom, this reduces IntMul.Kappa.R8.bitNetR8_mom.
import Definitions.Def_IntMul_Kappa_RG_Defs import Definitions.Def_IntMul_KappaJainData set_option autoImplicit false set_option relaxedAutoImplicit false
namespace IntMul.Kappa.R8.Bit
open IntMul.Kappa IntMul.Kappa.R6.Bit
/-- Jain's round-eight bit interchange keeps the round-seven witness-2 schedule, frames and
payload word (`bitplainHist` / `Jain.bitR7plain`, $W = 104719230$, $m = 529$) and only
recompiles the address geometry: opposite bank orders (icekylinx) turn each residual of
rank $r$ into one contiguous reversed child of width $r$, producing histogram `Jain.bitR8`.
This lemma packages that recompile as a map of moment-dominance network statements: from any
QH-network witnessing `BitNetMomStmtG` at `Jain.bitR7plain`, one obtains a (possibly different)
QH-network witnessing the same statement at `Jain.bitR8`. -/
theorem oppbank_mom_of_plain :
BitNetMomStmtG 104719230 529 Jain.bitR7plain →
BitNetMomStmtG 104719230 529 Jain.bitR8 := by
sorry
end IntMul.Kappa.R8.Bit