Round-six top-level assembly: the κ bound from the round-six interfaces

Let $\kappa\in\mathbb R$. Assume the six round-six interfaces hold for every admissible parameter record: SetupNeed6 (the §9.2 setup and sources), CrtNeed6 ($\Phi$ with the E′ CRT reversal), FineNeed6 (fine-bit exposure), LineNeed6 (the line maps), P14Need6 (the uniform Proposition 14) and P18IL6 (Proposition 18 from the uniform Proposition 14). Then for every parameter record $P$ with $P.\mathrm{Ok}$ and $\kappa<P.\mathrm{gap}$, if the bit-network histogram satisfies $\mathrm{histMoment}(\mathrm{bitR6},529,P.\tau)<148225616$, the complex-network histogram satisfies $\mathrm{histMoment}(\mathrm{cxR6},576,P.\sigma)<207387136$ and $2+576\log(\mathrm{histRankSum}(\mathrm{cxR6}))\le P.C_1$, the bit network statement Bit.BitNetR6MomStmt holds and a complex network interface Cx.Prop8IfaceH 207387136 T 576 cxR6 exists, then IntMul.KappaBound κ holds.

In Lean:

theorem IntMul.Kappa.R6.kappa_final6 (κ : ℝ)
    (hSet : ∀ P : Prm, P.Ok → SetupNeed6 P) (hCrt : ∀ P : Prm, P.Ok → CrtNeed6 P)
    (hFine : ∀ P : Prm, P.Ok → FineNeed6 P) (hLine : ∀ P : Prm, P.Ok → LineNeed6 P)
    (hP14 : ∀ P : Prm, P.Ok → P14Need6 P) (hP18 : ∀ P : Prm, P.Ok → P18IL6 P) :
    ∀ P : Prm, P.Ok → κ < P.gap →
      histMoment Jain.bitR6 529 P.τ < 148225616 →
      histMoment Jain.cxR6 576 P.σ < 207387136 →
      2 + 576 * Real.log (histRankSum Jain.cxR6) ≤ P.C1 →
      Bit.BitNetR6MomStmt →
      (∃ T, ∃ J : Cx.Prop8IfaceH 207387136 T 576 Jain.cxR6, ∃ A, IL3H.GClassH J A) →
      IntMul.KappaBound κ

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).