Round-six assembly at one parameter record with rational ε

For one round-six parameter record $P$ with $P.\mathrm{Ok}$ and rational $\varepsilon$, and $\kappa<P.\mathrm{gap}$: the interfaces SetupNeed6 P, CrtNeed6 P, FineNeed6 P, LineNeed6 P, P14Need6 P, P18IL6 P, the histogram moment bounds for the bit and complex networks, the bound $2+576\log(\mathrm{histRankSum}(\mathrm{cxR6}))\le P.C_1$, the bit network statement and a complex network interface together give IntMul.KappaBound κ.

In Lean:

theorem IntMul.Kappa.R6.kappa_final6_at (P : Prm) (hP : P.Ok) (hq : ∃ q : ℚ, P.ε = q) (κ : ℝ) (hκ : κ < P.gap)
    (hSet : SetupNeed6 P) (hCrt : CrtNeed6 P) (hFine : FineNeed6 P) (hLine : LineNeed6 P)
    (hP14 : P14Need6 P) (hP18 : P18IL6 P)
    (hJb : histMoment Jain.bitR6 529 P.τ < 148225616)
    (hJc : histMoment Jain.cxR6 576 P.σ < 207387136)
    (hC1 : 2 + 576 * Real.log (histRankSum Jain.cxR6) ≤ P.C1)
    (hBit : Bit.BitNetR6MomStmt)
    (hCx : ∃ 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*).