TP in [0.660161753699267, 0.660161753699267] 2e^{-gamma}TP >= 0.741308154605199 === hypotheses of JS Theorem 4.2 at X2 := N, checked at L0 = 2736.86 (each increasing in L) === OK loglog x1(X2) >= Y0: w - e^7.9 [0.004838947305, 0.004838947305] [w increasing] OK sqrt(x1)/log^7 x1 >= log^7 N: w/2 - 7 log w - 7 log L [1237.941605, 1237.941605] [derivative (1/2 - 7/w)(1 - 5/L) - 7/L > 0] OK ... its L-derivative [0.4939384099, 0.4939384099] [increasing in L] OK log^7 N >= 1e9: 7 log L - log 1e9 [34.67870006, 34.67870006] [increasing] OK 1 - xi/log^2 N >= 0 (xi <= 801) [0.9998930632, 0.9998930632] [increasing] OK X2 = N >= 4e18: L - log(4e18) [2694.027174, 2694.027174] [increasing] OK eps <= 1/74 [0.01295921351, 0.01295921351] [constant] OK N^a/(log^7 x1 log^2.5 N) >= exp(u0(1 + 9e-7/log u0)): L/4 - 7 log w - 2.5 log L - 400(1 + 9e-7/log 400) [209.128511, 209.128511] [derivative 1/4 - 7(1-5/L)/w - 2.5/L > 0] OK ... its L-derivative [0.2464960855, 0.2464960855] [increasing] OK N^{1/2-a}/log^14 N >= z^2: 0.2 L - 14 log L [436.5680682, 436.5680682] [derivative 0.2 - 14/L > 0] OK K_delta(x1) >= 3022: w^1.3 - 3022 [25831.95446, 25831.95446] [increasing] OK eps1 <= 1/11: K_delta(x1) - 15015 (= 3*5*7*11*13) [13838.95446, 13838.95446] [K_delta increasing, so pbar >= 13] OK z0 = N^{1/40} >= 1e12 (eps(400,1e12), xi(1e12,40) apply): L/40 - 12 log 10 [40.79047888, 40.79047888] [increasing] OK c >= 7 (mbar <= max(1-f(6), F(7)-1)): c(L) - 7 [1.380568508, 1.380568508] [c increasing (M7)] OK xi <= 801 from BJV22 Lemma 38 (both sides): 801 - L^2((1+a1)(1+a2)(1+a3) - 1) [1.0, 1.0] [L^2 a3 = 800 exactly; L^2 a1, L^2 a2 decrease (z = e^{L/40})] === monotonicity steps (checked at L0 / w0; persistence reason in brackets) === OK M3 dE_P/dlog w at w0 (increasing: E_P and 1-1/log w increase) [10.414974, 10.414974] >0 [both factors positive and increasing for w > e] OK M3 dE_S/dlog w at w0 (increasing: E_S and 0.35-2/log w increase for log w > 2/0.35) [1.4578674, 1.4578674] >0 [log w0 = 7.9 > 5.72] OK M2a nu*w > 2 (t^2 e^{-nu t} decreasing in t >= w): min(E_P, E_S)(w0) - 2 [9.9243901, 9.9243901] >0 [E_P, E_S increase (M3)] OK M2b t^6.5/v^7: 6.5 - 7 (w-5)/(w-5 log w) [-0.59086509, -0.59086509] <0 [(w-5)/(w-5log w) >= 1 for log w >= 1] OK M2b 18 t^3 e^{-t/12}: 3 - w/12 [-221.77393, -221.77393] <0 [w increasing] OK M2b 2.5 t^7.5 e^{-t/6}: 7.5 - w/6 [-442.04786, -442.04786] <0 [w increasing] OK M2d c1: t^2 e^{-E_P(t)}: 2 - dE_P/dlog t [-8.414974, -8.414974] <0 [dE_P/dlog t increasing (M3)] OK M2d c1: t^9 e^{-t/2}: 9 - w/2 [-1339.6436, -1339.6436] <0 [w increasing] OK M2d c1: t^3.515 e^{-0.8274 sqrt t}: 3.515 - 0.4137 sqrt w [-17.970681, -17.970681] <0 [w increasing] OK M5 w log w e^{-E_P}: 1 + 1/log w0 - dE/dlog w [-9.2883918, -9.2883918] <0 [b/log w decreases, dE/dlog w increases] OK M5 (x j) w log^2 w e^{-E_P}/log(7log w): 1 + 2/log w0 - dE/dlog w [-9.1618095, -9.1618095] <0 [same] OK M5 w log w e^{-E_S}: 1 + 1/log w0 - dE/dlog w [-0.33128518, -0.33128518] <0 [b/log w decreases, dE/dlog w increases] OK M5 (x j) w log^2 w e^{-E_S}/log(7log w): 1 + 2/log w0 - dE/dlog w [-0.20470293, -0.20470293] <0 [same] OK M5 C-term log w/w (x j: log^2 w/(w log(7 log w))): -1 + 2/log w0 [-0.7468355, -0.7468355] <0 [2/log w decreases] OK M5 4w^5.5/v^7 (x j): 5.5 - 7(w-5)/(w-5log w) + 2/log w0 [-1.3377006, -1.3377006] <0 [as M2b] OK M5 4w^-1.5 (x j): -1.5 + 2/log w0 [-1.2468355, -1.2468355] <0 [2/log w decreases] OK M5 18w^2 e^{-w/12} (x j): 2 + 2/log w0 - w/12 [-222.52077, -222.52077] <0 [w increasing] OK M5 2.5 w^6.5 e^{-w/6} (x j): 6.5 + 2/log w0 - w/6 [-442.7947, -442.7947] <0 [w increasing] OK M5 w^-4 e^{-w/2}, 0.4 w^4 e^{-w}, w^-6 (x j): 4 + 2/log w0 - w [-2693.034, -2693.034] <0 [w increasing] OK M5/M8 mult(L) decreasing: (1-4/w)L and L^2 w^3 increasing [w(L) increasing: 1 - 5/L] [0.99817309, 0.99817309] >0 [L increasing] OK M5 del/L x j: e^{-L/2} L^0.5 j/(w^7 log L): -1/2 + 0.5/L + 1/(w log w) [-0.49977038, -0.49977038] <0 [L increasing] OK M7 c(L) increasing: d/dL(-14 log L/L) = 14(log L - 1)/L^2 [6.9145666, 6.9145666] >0 [L increasing] OK M9 (L+7log L)/(L-7log L) decreasing: 1 - log L [-6.9145666, -6.9145666] <0 [L increasing] OK M9 L/w decreasing (log L/L decreasing): 1 - log L [-6.9145666, -6.9145666] <0 [L increasing] OK M9/M11 lll(L) > 0 (so 1 + log 1.3/lll and 2.5/(log(1.3 log w) lll) decrease) [2.0687049, 2.0687049] >0 [lll increasing] OK M9 log(1.3 log w) > 0 [2.3292273, 2.3292273] >0 [increasing] OK M10 log L/L^0.7 decreasing: 1 - 0.7 log L [-4.5401966, -4.5401966] <0 [L increasing] OK M11 lll (log7 + lll)/L^1.3 decreasing: (1/log L)(1/lll + 1/(log 7 + lll)) - 1.3 [-1.2074511, -1.2074511] <0 [LHS terms decrease] OK M11 lll/L^1.3 decreasing: 1/(log L lll) - 1.3 [-1.2389235, -1.2389235] <0 [LHS decreases] OK M8 c2 tail L^4 e^{-L}: 4 - L [-2732.86, -2732.86] <0 [L increasing] === route A (appendix chain) at L0, valid for all L >= L0 === a-form JSprint: c4/L < 1.18394235, c4* j/L < 22.5828447, c1 < 52.4063548, c2 < 52.4255318, c3 < 2.68184975, a1 < 4.58299598, a < 1.38715143e-6, h(c) = [8.20754203e-5, 8.20754203e-5], brace_b > 0.99958939112 case (a) > 38.394169843 ; case (b) > 9.5200706171 a-form BJV22 : c4/L < 1.18394235, c4* j/L < 22.5828447, c1 < 52.4063548, c2 < 52.4255318, c3 < 2.68184975, a1 < 4.58299598, a < 0.00379643926, h(c) = [8.20754203e-5, 8.20754203e-5], brace_b > 0.99579379637 case (a) > 38.394169843 ; case (b) > 9.3682468274 === route B (direct, exact c4/L and c4* j/L), cover of [L0, L1] plus route A at L1 for the tail === a-form JSprint: [L0, 3000.0] covered by 11 boxes, every box: case (b) > 9.950486019, case (a) > 38.41675407 first box [2736.86, 2737.11697266]: case (b) in [9.950486019, 9.99495281] tail L >= 3000.0 by route A: case (a) > 39.281968, case (b) > 26.32272 a-form BJV22 : [L0, 3000.0] covered by 12 boxes, every box: case (b) > 9.803684161, case (a) > 38.41700836 first box [2736.86, 2736.98848633]: case (b) in [9.803684161, 9.825922545] tail L >= 3000.0 by route A: case (a) > 39.281968, case (b) > 26.218294 point L = L0, a-form JSprint: case (a) [38.4172626293, 38.4172626293], case (b) [9.96054882588, 9.96054882588], a <= 1.3871514e-6 point L = L0, a-form BJV22 : case (a) [38.4172626293, 38.4172626293], case (b) [9.80872503613, 9.80872503613], a <= 0.0037964393 wrote js_cert.json