The `J` side conditions from the table bounds (round six, `JB_of`)
ProvedJ6Seg.PJ.JB_ofThe J side conditions from the table bounds.
The following holds (Lean statement, in the scope of module Solutions.J6SegILPreJK30):
theorem J6Seg.PJ.JB_of (TB : PreT.TabB Q R s t α lam (Q + R + 2)) (hs : 0 < s) (hl : 1 ≤ lam)
(hws : w ≤ s)
(hV : (2 : ℤ) ^ Q + ((lam * (2 * w + 1) : ℕ) : ℤ) *
((2 : ℤ) ^ (Q + R + 2) * 2 ^ (Q + R + 2) * (2 ^ (Q + R + 2) * 2 ^ (Q + R + 2) *
((lam : ℤ) * (2 ^ (Q + R + 2)) ^ 3)) * 2 ^ (Q + R + 2)) ≤ 2 ^ W)
(hEK : α ^ 2 * (t * w + s) ^ 2 ≤ 2 ^ W) :
JB Q R W s t α lam w
Context. B5 J side, part K30: the numeric side conditions JB from the table bounds
With every table entry ≤ X = 2^(Q+R+2) (TabB at Q + R + 2, and expNeg_le for the
couplings), JB Q R W s t α λ w holds as soon as 2^Q + λ(2w+1)·λX⁸ ≤ 2^W and
α²(tw + s)² ≤ 2^W (JB_of).
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs71
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.PJ
open IntMul NLogN NLogN.KIL Function Finset
variable {Q R W s t α lam w : ℕ}
theorem J6Seg.PJ.JB_of (TB : PreT.TabB Q R s t α lam (Q + R + 2)) (hs : 0 < s) (hl : 1 ≤ lam)
(hws : w ≤ s)
(hV : (2 : ℤ) ^ Q + ((lam * (2 * w + 1) : ℕ) : ℤ) *
((2 : ℤ) ^ (Q + R + 2) * 2 ^ (Q + R + 2) * (2 ^ (Q + R + 2) * 2 ^ (Q + R + 2) *
((lam : ℤ) * (2 ^ (Q + R + 2)) ^ 3)) * 2 ^ (Q + R + 2)) ≤ 2 ^ W)
(hEK : α ^ 2 * (t * w + s) ^ 2 ≤ 2 ^ W) :
JB Q R W s t α lam w := by sorry