#!/usr/bin/env python3 """js_cert.py: an interval (mpmath.iv) certificate for the paper's (I4'), S(A, N^{1/40}) > c * U_N N / log^2 N for every even N >= X2' := exp(2736.86), from Johnston-Starichkova's Theorem 4.2 (arXiv:2208.01229v3) applied, for each N, with its threshold X2 := N (Appendix B of the paper). Written from the arXiv v3 source of Johnston-Starichkova (definitions, Theorem 4.2, parameters), the authors' public notebook, Bordignon-Johnston-Starichkova (arXiv:2207.09452) and Appendix B of the paper. Two routes, both rigorous (outward-rounded intervals): Route A ("appendix chain"): the uniform majorants of Appendix B (w/L -> 1 in each positive summand, 1/beta frozen at w0, decreasing majorants for the sups), evaluated at a left end Ls; every monotonicity step is checked in monotonicity_checks(). Valid for all L >= Ls. Route B ("direct"): the exact X2 := N expressions (c4/L and c4* j/L with no w/L replacement), enclosed on a cover of [L0, L1] by adaptive bisection; the tail L >= L1 by route A at Ls = L1. Each route is run with the two forms of a(X2): 'BJV22' : a = a1 * max_{N'>=N}[ lll/log^delta N' * ... ] (the definition and proof of Bordignon-Johnston-Starichkova; the authors' notebook) 'JSprint': a = a1 * max_{N'>=N}[ lll/log^{1+delta} N' * ... ] (the form printed in Johnston-Starichkova, Section 2.1) """ import json, sys from mpmath import iv, mp iv.dps = 50; mp.dps = 50 def I(x): return iv.mpf(x) def lo(x): return mp.make_mpf(x._mpi_[0]) def hi(x): return mp.make_mpf(x._mpi_[1]) def imin(a, b): return iv.mpf([min(lo(a), lo(b)), min(hi(a), hi(b))]) def imax(a, b): return iv.mpf([max(lo(a), lo(b)), max(hi(a), hi(b))]) def s(x, n=12): return '[' + mp.nstr(lo(x), n) + ', ' + mp.nstr(hi(x), n) + ']' # ---------------- fixed parameters (JS l. 586-600; Theorem 4.2; BJV22 Table 1 via JS) : REPORTED ---------------- C = I('3.98'); A1 = 7; DELTA = I('1.3'); ALPHA = I('0.25'); M = 40; KK = 40 # (Y0, alpha1, alpha2, C) = (7.9, 7, 2, 3.98) R1 = I('2.0452'); B = 2 * R1 * A1 # Kadiri's R1; b = 2 R1 alpha1 EPS = I('5.543e-4'); C1E = 113; C2E = 114; XI = 801 # eps(400, 1e12), C1(eps), C2(eps), xi(1e12, 40) <= 801 EPS1 = I(1) / 11 # eps1(X2', delta) = 1/(13-2); nonincreasing in N RHO = I('1.05e-4'); F7 = I('5e-6') # 1 - f(6) <= 1.05e-4, F(7) - 1 <= 5e-6 (JS (2.8)-(2.9)) MBAR = imax(RHO, F7) # m-bar <= max(1 - f(c), F(c) - 1) <= rho for c >= 7 GAMMA = iv.euler; E2 = iv.e ** 2 TP_LO = I(open('tp_bound.out').read().split('TP_lo_str ')[1].split()[0]) # rigorous lower bound (tp_bound.py) TP = iv.mpf([lo(TP_LO), hi(TP_LO)]) T_LO = 2 * iv.exp(-GAMMA) * TP # 2 e^{-gamma} prod(1 - 1/(p-1)^2), lower bound L0 = I('2736.86') def w_of(L): return L - 5 * iv.log(L) # log x1(N), x1 = N / log^5 N def lll(L): return iv.log(iv.log(L)) # log log log N def jfac(w): return I('1.3841') * A1 * iv.log(w) / iv.log(A1 * iv.log(w)) # 1.3841 log(log^7 x1)/loglog(log^7 x1) def nuP(w): return 1 / (B * iv.log(w)) # (strongbetabound): 1/(2 R1 log Q(x1)), Q = log^7 def nuS(w): return 100 / (w ** (DELTA / 2) * (DELTA * iv.log(w)) ** 2) # 100/(sqrt(K_delta) log^2 K_delta), K_delta = w^1.3 def EPf(w): return nuP(w) * w def ESf(w): return nuS(w) * w def hfun(x): # h(s) = 3 e^{-s}/s for s >= 3 assert lo(x) >= 3 return 3 * iv.exp(-x) / x def cK(L): return KK * (I('0.5') - ALPHA - 2 * A1 * iv.log(L) / L) # c_{alpha, X2, K} at X2 = N def Ecal_y(t): # E(y)/y, log y = t (JS l. 199), alpha1 = 7 v = t - 5 * iv.log(t) return (4 * t ** I('4.5') / v ** 7 + 4 / t ** I('2.5') + 18 * t * iv.exp(-t / 12) + I('2.5') * t ** I('5.5') * iv.exp(-t / 6)) def mult(L): w = w_of(L) return 1 + 1 / (L ** 2 * w ** 3) + 1 / ((1 - 4 / w) * L) # ---------------- exact X2 := N quantities (route B) ---------------- def p2_exact(L, nu): # the sup over y >= x1(N) is attained at y = x1(N) (monotonicity_checks, items M2*) w = w_of(L); lw = iv.log(w) return (I('1.1') * A1 * lw * (C + w ** 2 * iv.exp(-nu * w) / (1 - nu)) + 27 * w ** 2 * Ecal_y(w) + w ** 2 * iv.exp(-w / 2) / (2 * iv.log(2) * w ** 5) + I('0.4') * w ** 5 * iv.exp(-w)) def c4_exact(L, nu): # c4(N) (nu = min(nuS, nuP), case a) or c4*(N) (nu = nuP, case b) w = w_of(L) p1 = p2_exact(L, nu) + (I('0.67') + 2 * iv.exp(-w / 6)) / w ** 5 p = p1 * mult(L) + I('2.2') / L ** 2 dele = I('0.9') * iv.exp(w / 2 - L) * L ** 4 / (w ** 7 * iv.log(L)) return p + dele def c1_exact(L): # sup over y >= x1(N) attained at y = x1(N) (M2d) w = w_of(L) return C + w ** 2 * (iv.exp(-EPf(w)) / (1 - nuP(w)) + w ** 7 * (I('1.02') * iv.exp(-w / 2) + 3 * iv.exp(-2 * w / 3)) + I('9.4') * w ** I('1.515') * iv.exp(-I('0.8274') * iv.sqrt(w))) def c2_exact(L): return c1_exact(L) * mult(L) + 1 / L ** 2 + I('1.3841') * L ** 4 * iv.exp(-L) / iv.log(L) def M3(L): # decreasing majorant of the bracket defining c3 (sup over N' >= N): c3(N) <= M3(log N) (M9) w = w_of(L) return ((I('1.5') / L + (L + 7 * iv.log(L)) / (L - 7 * iv.log(L))) * (L / w) ** DELTA * (iv.exp(GAMMA) * (1 + iv.log(DELTA) / lll(L)) + I('2.5') / (iv.log(DELTA * iv.log(w)) * lll(L))) + I('1.3841') * L ** (2 + DELTA) * iv.exp(-L) / (iv.log(L) * lll(L))) def Gfac(L): # decreasing majorant of the a1 bracket without c2: 1.3841*7*log L'/(L'^0.7 lll' log(7 log w')) (M10) w = w_of(L) return I('1.3841') * A1 * iv.log(L) / (L ** (2 - DELTA) * lll(L) * iv.log(A1 * iv.log(w))) def Afac(L, form): # decreasing majorant of the a bracket (sup over N' >= N) (M11) w = w_of(L) expo = DELTA if form == 'BJV22' else 1 + DELTA return (1 / TP) * lll(L) * (iv.exp(GAMMA) * (iv.log(A1) + lll(L)) + I('2.5') / iv.log(A1 * iv.log(w))) / L ** expo def a_bound(L_box, L_left, form): # a(N) for log N in L_box; sups bounded by majorants at the box's left end c2 = c2_exact(L_box) a1 = I(hi(c2)) * Gfac(L_left) + M3(L_left) return I(hi(a1)) * Afac(L_left, form), a1, c2 def brace_b(L, a): # case (b) brace without its final term, f(c) >= 1-rho, 1-f(c) <= rho, mbar <= rho, xi <= 801 hc = hfun(cK(L)) return ((1 - RHO) - EPS1 * RHO - (1 + EPS1) * EPS * C2E * E2 * hc - (3 * EPS1 + a) * (MBAR + EPS * C1E * E2 * hc) - a - 2 * XI / L ** 2) def coefs_direct(La, Lb, form): """Rigorous lower bounds, valid for every L = log N in [La, Lb], for the coefficient of U_N N/L^2 in cases (a) and (b).""" L = iv.mpf([La, Lb]); Ll = I(La) w = w_of(L) nu_a = imin(nuS(w), nuP(w)); nu_b = nuP(w) a, a1, c2 = a_bound(L, Ll, form) bb = brace_b(L, a) assert lo(bb) > 0 cb = M * bb - c4_exact(L, nu_b) * jfac(w) / (L * T_LO) # M(1 + xi/L^2) * brace >= M * brace (brace > 0); |A| > N/L ba = (1 - RHO) - C2E * EPS * E2 * hfun(M * (I('0.5') - ALPHA)) ca = M * (1 - XI / L ** 2) * ba - c4_exact(L, nu_a) / (L * T_LO) return ca, cb, a # ---------------- route A: the appendix's uniform chain at a left end Ls (valid for all L >= Ls) ---------------- def chainA(Ls, form): L = I(Ls); w = w_of(L); lw = iv.log(w) beta_min = 1 - nuP(w) # 1/beta frozen at its largest value on [Ls, inf) (M6) out = {} def normalised(E): # (p1/w) with w/L -> 1, as a function of w only, plus the L-terms main = (I('1.1') * A1 * lw * (C / w + w * iv.exp(-E) / beta_min) + 27 * w * Ecal_y(w) + (w ** 2 * iv.exp(-w / 2) / (2 * iv.log(2) * w ** 5) + I('0.4') * w ** 5 * iv.exp(-w)) / w + (I('0.67') + 2 * iv.exp(-w / 6)) / w ** 6) tail = I('2.2') / L ** 3 + I('0.9') * iv.exp(w / 2 - L) * L ** 3 / (w ** 7 * iv.log(L)) return main * mult(L) + tail nP = normalised(EPf(w)); nS = normalised(ESf(w)) norm_a = imax(nP, nS) # case (a): E = min(E_P, E_S); both normalised terms decrease (M5) norm_bj = nP * jfac(w) # case (b): E_P alone, times j (M5, with j) c2 = c2_exact(L) # decreasing in L (M8) a1 = c2 * Gfac(L) + M3(L) a = a1 * Afac(L, form) bb = brace_b(L, a) hc = hfun(cK(L)) cb = M * bb - norm_bj / T_LO ca = M * (1 - XI / L ** 2) * ((1 - RHO) - C2E * EPS * E2 * hfun(M * (I('0.5') - ALPHA))) - norm_a / T_LO out.update(dict(L=L, w=w, c=cK(L), h_c=hc, c4_over_L_uniform=norm_a, c4star_j_over_L_uniform=norm_bj, c1=c1_exact(L), c2=c2, c3_majorant=M3(L), a1=a1, a=a, brace_b=bb, case_a=ca, case_b=cb)) return out # ---------------- monotonicity and hypothesis checks (each an inequality verified at the left end; persistence noted) ---------------- def monotonicity_checks(Ls): L = I(Ls); w = w_of(L); lw = iv.log(w); res = [] def chk(name, val, cond, why): ok = (lo(val) > 0) if cond == '>0' else (hi(val) < 0) res.append((name, s(val, 8), cond, ok, why)); return ok dEP = EPf(w) * (1 - 1 / lw); dES = ESf(w) * (I('0.35') - 2 / lw) chk('M3 dE_P/dlog w at w0 (increasing: E_P and 1-1/log w increase)', dEP, '>0', 'both factors positive and increasing for w > e') chk('M3 dE_S/dlog w at w0 (increasing: E_S and 0.35-2/log w increase for log w > 2/0.35)', dES, '>0', 'log w0 = %s > 5.72' % mp.nstr(lo(lw), 6)) chk('M2a nu*w > 2 (t^2 e^{-nu t} decreasing in t >= w): min(E_P, E_S)(w0) - 2', imin(EPf(w), ESf(w)) - 2, '>0', 'E_P, E_S increase (M3)') chk('M2b t^6.5/v^7: 6.5 - 7 (w-5)/(w-5 log w)', I('6.5') - 7 * (w - 5) / (w - 5 * lw), '<0', '(w-5)/(w-5log w) >= 1 for log w >= 1') chk('M2b 18 t^3 e^{-t/12}: 3 - w/12', 3 - w / 12, '<0', 'w increasing'); chk('M2b 2.5 t^7.5 e^{-t/6}: 7.5 - w/6', I('7.5') - w / 6, '<0', 'w increasing') chk('M2d c1: t^2 e^{-E_P(t)}: 2 - dE_P/dlog t', 2 - dEP, '<0', 'dE_P/dlog t increasing (M3)') chk('M2d c1: t^9 e^{-t/2}: 9 - w/2', 9 - w / 2, '<0', 'w increasing') chk('M2d c1: t^3.515 e^{-0.8274 sqrt t}: 3.515 - 0.4137 sqrt w', I('3.515') - I('0.4137') * iv.sqrt(w), '<0', 'w increasing') # route A's w-terms: log-derivative wrt log w of w^a (log w)^b (log(7 log w))^{-c} e^{-phi}: <= a + b/log w0 - w phi'(w0) for E, nm, dE in ((EPf(w), 'E_P', dEP), (ESf(w), 'E_S', dES)): chk('M5 w log w e^{-%s}: 1 + 1/log w0 - dE/dlog w' % nm, 1 + 1 / lw - dE, '<0', 'b/log w decreases, dE/dlog w increases') chk('M5 (x j) w log^2 w e^{-%s}/log(7log w): 1 + 2/log w0 - dE/dlog w' % nm, 1 + 2 / lw - dE, '<0', 'same') chk('M5 C-term log w/w (x j: log^2 w/(w log(7 log w))): -1 + 2/log w0', -1 + 2 / lw, '<0', '2/log w decreases') chk('M5 4w^5.5/v^7 (x j): 5.5 - 7(w-5)/(w-5log w) + 2/log w0', I('5.5') - 7 * (w - 5) / (w - 5 * lw) + 2 / lw, '<0', 'as M2b') chk('M5 4w^-1.5 (x j): -1.5 + 2/log w0', I('-1.5') + 2 / lw, '<0', '2/log w decreases') chk('M5 18w^2 e^{-w/12} (x j): 2 + 2/log w0 - w/12', 2 + 2 / lw - w / 12, '<0', 'w increasing') chk('M5 2.5 w^6.5 e^{-w/6} (x j): 6.5 + 2/log w0 - w/6', I('6.5') + 2 / lw - w / 6, '<0', 'w increasing') chk('M5 w^-4 e^{-w/2}, 0.4 w^4 e^{-w}, w^-6 (x j): 4 + 2/log w0 - w', 4 + 2 / lw - w, '<0', 'w increasing') chk('M5/M8 mult(L) decreasing: (1-4/w)L and L^2 w^3 increasing [w(L) increasing: 1 - 5/L]', 1 - 5 / L, '>0', 'L increasing') chk('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)', I('-0.5') + I('0.5') / L + 1 / (w * lw), '<0', 'L increasing') chk('M7 c(L) increasing: d/dL(-14 log L/L) = 14(log L - 1)/L^2', iv.log(L) - 1, '>0', 'L increasing') chk('M9 (L+7log L)/(L-7log L) decreasing: 1 - log L', 1 - iv.log(L), '<0', 'L increasing') chk('M9 L/w decreasing (log L/L decreasing): 1 - log L', 1 - iv.log(L), '<0', 'L increasing') chk('M9/M11 lll(L) > 0 (so 1 + log 1.3/lll and 2.5/(log(1.3 log w) lll) decrease)', lll(L), '>0', 'lll increasing') chk('M9 log(1.3 log w) > 0', iv.log(DELTA * lw), '>0', 'increasing') chk('M10 log L/L^0.7 decreasing: 1 - 0.7 log L', 1 - I('0.7') * iv.log(L), '<0', 'L increasing') chk('M11 lll (log7 + lll)/L^1.3 decreasing: (1/log L)(1/lll + 1/(log 7 + lll)) - 1.3', (1 / iv.log(L)) * (1 / lll(L) + 1 / (iv.log(7) + lll(L))) - I('1.3'), '<0', 'LHS terms decrease') chk('M11 lll/L^1.3 decreasing: 1/(log L lll) - 1.3', 1 / (iv.log(L) * lll(L)) - I('1.3'), '<0', 'LHS decreases') chk('M8 c2 tail L^4 e^{-L}: 4 - L', 4 - L, '<0', 'L increasing') return res def gates(Ls): L = I(Ls); w = w_of(L); lw = iv.log(w); g = [] def chk(name, val, why): g.append((name, s(val, 10), lo(val) > 0, why)); return lo(val) > 0 chk('loglog x1(X2) >= Y0: w - e^7.9', w - iv.exp(I('7.9')), 'w increasing') chk('sqrt(x1)/log^7 x1 >= log^7 N: w/2 - 7 log w - 7 log L', w / 2 - 7 * lw - 7 * iv.log(L), 'derivative (1/2 - 7/w)(1 - 5/L) - 7/L > 0') chk(' ... its L-derivative', (I('0.5') - 7 / w) * (1 - 5 / L) - 7 / L, 'increasing in L') chk('log^7 N >= 1e9: 7 log L - log 1e9', 7 * iv.log(L) - iv.log(I(10) ** 9), 'increasing') chk('1 - xi/log^2 N >= 0 (xi <= 801)', 1 - XI / L ** 2, 'increasing') chk('X2 = N >= 4e18: L - log(4e18)', L - iv.log(4 * I(10) ** 18), 'increasing') chk('eps <= 1/74', I(1) / 74 - EPS, 'constant') chk('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)', L / 4 - 7 * lw - I('2.5') * iv.log(L) - 400 * (1 + I('9e-7') / iv.log(400)), 'derivative 1/4 - 7(1-5/L)/w - 2.5/L > 0') chk(' ... its L-derivative', I('0.25') - 7 * (1 - 5 / L) / w - I('2.5') / L, 'increasing') chk('N^{1/2-a}/log^14 N >= z^2: 0.2 L - 14 log L', I('0.2') * L - 14 * iv.log(L), 'derivative 0.2 - 14/L > 0') chk('K_delta(x1) >= 3022: w^1.3 - 3022', w ** DELTA - 3022, 'increasing') chk('eps1 <= 1/11: K_delta(x1) - 15015 (= 3*5*7*11*13)', w ** DELTA - 15015, 'K_delta increasing, so pbar >= 13') chk('z0 = N^{1/40} >= 1e12 (eps(400,1e12), xi(1e12,40) apply): L/40 - 12 log 10', L / 40 - 12 * iv.log(10), 'increasing') chk('c >= 7 (mbar <= max(1-f(6), F(7)-1)): c(L) - 7', cK(L) - 7, 'c increasing (M7)') z = iv.exp(L / 40) a1v = I('1.45') * L / (z - 1) * (1 + 10 * iv.log(L) / L); a2v = I('1.002') / (z - 3); a3v = 1 / (2 * (L / 40) ** 2) xi_need = L ** 2 * ((1 + a1v) * (1 + a2v) * (1 + a3v) - 1) chk('xi <= 801 from BJV22 Lemma 38 (both sides): 801 - L^2((1+a1)(1+a2)(1+a3) - 1)', 801 - xi_need, 'L^2 a3 = 800 exactly; L^2 a1, L^2 a2 decrease (z = e^{L/40})') return g def cover_direct(L_start, L_end, form, target_b, target_a, min_w=mp.mpf('1e-6')): """Adaptive bisection of [L_start, L_end]; every accepted box has lower bounds > targets. Returns stats and the box minima.""" stack = [(mp.mpf(L_start), mp.mpf(L_end))]; boxes = 0; worst_b = None; worst_a = None; first = None while stack: La, Lb = stack.pop() ca, cb, a = coefs_direct(La, Lb, form) if lo(cb) > target_b and lo(ca) > target_a: boxes += 1 worst_b = lo(cb) if worst_b is None else min(worst_b, lo(cb)) worst_a = lo(ca) if worst_a is None else min(worst_a, lo(ca)) if La == mp.mpf(L_start): first = (La, Lb, lo(ca), lo(cb), hi(cb)) continue if Lb - La < min_w: raise RuntimeError('cannot certify near L = %s: case a %s, case b %s' % (mp.nstr(La, 15), s(ca), s(cb))) mid = (La + Lb) / 2 stack.append((mid, Lb)); stack.append((La, mid)) return dict(boxes=boxes, min_lower_b=worst_b, min_lower_a=worst_a, first_box=first) if __name__ == '__main__': out = {} print('TP in', s(TP, 15), ' 2e^{-gamma}TP >=', mp.nstr(lo(T_LO), 15)) print('\n=== hypotheses of JS Theorem 4.2 at X2 := N, checked at L0 = 2736.86 (each increasing in L) ===') gg = gates(mp.mpf('2736.86')) for g in gg: print(' %-5s %s %s [%s]' % ('OK' if g[2] else 'FAIL', g[0], g[1], g[3])) assert all(g[2] for g in gg) print('\n=== monotonicity steps (checked at L0 / w0; persistence reason in brackets) ===') mm = monotonicity_checks(mp.mpf('2736.86')) for m in mm: print(' %-5s %s %s %s [%s]' % ('OK' if m[3] else 'FAIL', m[0], m[1], m[2], m[4])) assert all(m[3] for m in mm) out['gates'] = [(g[0], g[1]) for g in gg]; out['monotonicity'] = [(m[0], m[1]) for m in mm] print('\n=== route A (appendix chain) at L0, valid for all L >= L0 ===') for form in ('JSprint', 'BJV22'): r = chainA(mp.mpf('2736.86'), form) print(' a-form %-7s: c4/L < %s, c4* j/L < %s, c1 < %s, c2 < %s, c3 < %s, a1 < %s, a < %s, h(c) = %s, brace_b > %s' % ( form, mp.nstr(hi(r['c4_over_L_uniform']), 9), mp.nstr(hi(r['c4star_j_over_L_uniform']), 9), mp.nstr(hi(r['c1']), 9), mp.nstr(hi(r['c2']), 9), mp.nstr(hi(r['c3_majorant']), 9), mp.nstr(hi(r['a1']), 9), mp.nstr(hi(r['a']), 9), s(r['h_c'], 9), mp.nstr(lo(r['brace_b']), 11))) print(' case (a) > %s ; case (b) > %s' % (mp.nstr(lo(r['case_a']), 11), mp.nstr(lo(r['case_b']), 11))) out['routeA_' + form] = {k: s(v, 16) for k, v in r.items()} print('\n=== route B (direct, exact c4/L and c4* j/L), cover of [L0, L1] plus route A at L1 for the tail ===') L1 = mp.mpf('3000') for form, tb in (('JSprint', mp.mpf('9.95')), ('BJV22', mp.mpf('9.80'))): st = cover_direct(mp.mpf('2736.86'), L1, form, tb, mp.mpf('38.40')) tail = chainA(L1, form) print(' a-form %-7s: [L0, %s] covered by %d boxes, every box: case (b) > %s, case (a) > %s' % ( form, mp.nstr(L1, 6), st['boxes'], mp.nstr(st['min_lower_b'], 10), mp.nstr(st['min_lower_a'], 10))) fb = st['first_box'] print(' first box [%s, %s]: case (b) in [%s, %s]' % (mp.nstr(fb[0], 12), mp.nstr(fb[1], 12), mp.nstr(fb[3], 10), mp.nstr(fb[4], 10))) print(' tail L >= %s by route A: case (a) > %s, case (b) > %s' % (mp.nstr(L1, 6), mp.nstr(lo(tail['case_a']), 8), mp.nstr(lo(tail['case_b']), 8))) assert lo(tail['case_b']) > tb and lo(tail['case_a']) > mp.mpf('38.40') out['routeB_' + form] = dict(L1=str(L1), boxes=st['boxes'], min_lower_case_b=mp.nstr(st['min_lower_b'], 15), min_lower_case_a=mp.nstr(st['min_lower_a'], 15), tail_case_b=mp.nstr(lo(tail['case_b']), 15), tail_case_a=mp.nstr(lo(tail['case_a']), 15), target_b=str(tb)) # point values at L0 (degenerate box) for the explanation table for form in ('JSprint', 'BJV22'): ca, cb, a = coefs_direct(mp.mpf('2736.86'), mp.mpf('2736.86'), form) print(' point L = L0, a-form %-7s: case (a) %s, case (b) %s, a <= %s' % (form, s(ca, 12), s(cb, 12), mp.nstr(hi(a), 8))) out['point_L0_' + form] = dict(case_a=s(ca, 15), case_b=s(cb, 15), a=mp.nstr(hi(a), 12)) json.dump(out, open('js_cert.json', 'w'), indent=1) print('\nwrote js_cert.json')