fermatlemma.py
Checks: THERMAL: The 2-power tower raises the sill theorem; rule.
Cited on: THERMAL.
To run it: save fermatlemma.py, with fieldtop.py, growth.py, memory.py, sillclass.py, spectrum.py, splitend.py, splitloss.py, splitsharp.py, tower.py, towerlemma.py, towerpast.py, towerscan.py, typeloss.py beside it; needs mpmath, numpy, scipy.
"""fermatlemma.py -- the 2-power tower's loss side at every k: one lemma,
uniform in the least Fermat prime B above 2^k + 1, so that a field of
the shape loses at some degree iff a Fermat prime exceeds 2^k + 1.
QUESTION. With C = Q(zeta_(2^k)) in K, K_ab = C, type (1, 0), K != C, d
= D m', D = 2^(k-1): at every k >= 4 for which some Fermat prime exceeds
n_c = 2^k + 1, B the least such (so B = F_n = 2^(2^n) + 1 >= 257, 2^n >
k), does towerlemma.py's lemma at the one (X, c) = (0.381, 1/2), the law
fixed below Y = B^10, close (g_up, M, M' all below 0), so that a field
of the shape loses at every d = 0 mod D >= d0(B) = ceil(c lam0 X^-a), a
= log2 B? With W_k empty when no Fermat prime exceeds n_c (M = log P_k >
0, no loss) and the lemmas at k = 2 (B = 9) and k = 3 (B = 17), that
would make "a field of the shape loses at some degree iff a Fermat
prime exceeds 2^k + 1" a theorem at every k >= 2.
THE DERIVATION (by hand, before this code).
The lemma (towerpast.lemma) at X, c, w_B = 1, b = log2(1/X), lam0 =
log(1/X), y0 = X^a = B^-b, l(X) = log(1/(1 - X)):
c_z = c [1/(1 - y0) + S_z + (B/Y)^b fac],
c_s = c [X^(a-1)/(1 - y0^2) + S_s + (2B/Y)^b fac],
fac = (1 + Y/(b - 1))/(1 - Y^-b),
g_up <= l(X) - (1 - c_z - c_s) lam0 + E',
M <= l(X) - c lam0 (1 - y0/2),
M' <= 1/(1 - X) - a c lam0/(X (1 + y0)),
S_z, S_s over the norms of W_k past B. Which norms: a prime power n >
n_c with n - 1 a power of 2 and n = 1 mod 2^k is a Fermat prime F_m
with 2^m > k (9, the one prime power 2^j + 1 not prime, is past n_c
only at k = 2), so W_k is the Fermat primes from B on, and each later
one is among F_(n+j), j >= 1, F_(n+j) - 1 = (B - 1)^(2^j). Counting
every F_(n+j), prime or not, only adds terms to an upper bound:
S_z <= sum_j (B/(B - 1)^(2^j))^b / (1 - (B - 1)^(-2^j b)),
S_s <= sum_j (2B/(B - 1)^(2^(j+1)))^b / (1 - (B - 1)^(-2^(j+1) b)).
E', the places off W_k below Y (towerlemma.e_off): at most D per
rational p, of norm (p^f)^(m'), p^f = 1 mod 2^k distinct across p,
so p^f >= n_c, m' >= d0/D:
E' <= (1 + 1/X) D n_c^-s (1 + n_c/(s - 1))/(1 - n_c^-s), s = (d0/D) b.
Uniform in k: k >= 4 gives n_c >= 17, and 2^k + 1 < B gives D =
2^(k-1) <= (B - 1)/4 and D < n_c, so s >= s_min = 4 d0 b/(B - 1) and
E' <= E_u = (1 + 1/X) 17^(2 - s_min) (1/17 + 1/(s_min - 1)) /
(1 - 17^-s_min),
once s_min > 2: D n_c^-s (1 + n_c/(s - 1)) <= n_c^(2-s) (1/n_c + 1/(s
- 1)) by D < n_c, falling in n_c and in s.
Monotone in B, at the fixed X, c, b, Y = B^10: y0 = B^-b falls; the
j-th term of S_z is (B (B - 1)^(-2^j))^b over a factor rising to 1,
falling in B for j >= 1 (B/(B - 1)^2 falls for B > 3); likewise S_s's;
X^(a-1) falls (a rises, X < 1); the tails c B^(-9b) (1 + B^10/(b -
1))/(1 - B^(-10b)) and 2^b times it fall, since 10 - 9b = -2.53 < 0;
d0/B ~ c lam0 B^(b - 1) rises, so s_min does and E_u falls; a rises,
so M' falls; M's (1 - y0/2) rises, so M falls. So c_z - c, c_s and
E_u, hence g_up, M and M', are each at most their values at B = 257,
the least B the hypothesis admits, and the lemma closes at every
Fermat prime B >= 257 iff it closes there.
The margins at B = 257: c lam0 - l(X) = 0.0028279 (lam0 = 0.964956,
l = 0.479650); c_z - c = c (y0/(1 - y0) + S_z + tail) ~ 0.5 (0.000442
+ 0.000454) ~ 0.00045, c_s ~ c X^(a-1) = 0.00058, so g_up's excess
(c_z + c_s - c) lam0 + E' ~ 0.00099, g_up ~ -0.00184; M's c lam0 y0/2 = 1.07e-4 (M ~ -0.002721); M' ~
-8.518; d0 = 1093, s_min = 23.78, E_u ~ 17^-21.8 x 0.37 ~ 1e-27; the
tail at Y = 257^10: c 257^(-2.53)/0.392 ~ 1e-6. At B = 65537: y0 =
2.0e-7, d0 = 2447300, s_min ~ 208, g_up ~ M ~ -0.002828, M' ~
-18.646. At B = 17 (outside the hypothesis): y0 = 0.0194, X^(a-1) =
0.051, M ~ +0.0018 > 0 and g_up > 0: the lemma fails there at this
(X, c), as k = 3's own constants (towerpast) say it must be read.
Then for every k >= 4 with a Fermat prime above n_c, B the least, and
every d = 0 mod D >= d0(B): x1 <= X, g(x1) < 0, x_low >= x1, M(x1) <
0 and M'(x1) < 0, so the margin is below 0, the field realized as in
tower.py's construction (m' >= d0/D >= s_min/b >= 17, so S_(m')
closure and K_ab = C). TRANSPLANTS from towerlemma's reads, re-derived
above: that the coefficients are bounded at X (each rises with x, as
towerpast's derivation, B-free), that M rises then falls on [0, x_c]
(the W_k terms increasing on (0, 1/2] at a >= log2 9, B-free).
PREDICTIONS (frozen before the engine).
P1 at B = 257, Y = B^10, S_z, S_s over F_4, F_5, ..., E_u: c_z, c_s,
g_up, M, M' within 1e-5 of towerlemma's k = 4 print (0.500444,
0.000580, -0.001840, -0.002721, -8.5179), d0 = 1093, E_u < 1e-20.
P2 at B = 65537: g_up and M in [-0.00283, -0.00282], M' <= -18.6, d0
= 2447300.
P3 over the Fermat numbers B = F_n, n = 3..40, as reals in logs, and
over a log grid of 2000 real B in [257, 2^(2^40)]: c_z - c, c_s,
E_u, the tail, M and M' are non-increasing in B, and g_up, M, M' <
0 at every point.
KILL (frozen): some B on either grid where g_up >= 0, M >= 0 or M' >=
0, i.e. where (c_z + c_s - c) lam0 + E' is not below the margin c lam0
- l(X) = 0.0028279, or c lam0 y0/2 is not; or a term of P3 rising
between two consecutive grid points by more than 1e-15 relative (the
sup-at-257 argument then dead, the derivation not closing); read on
the arm where B is least, B = 257, which the confound (the tail at the
smallest Y and the largest y0) inflates.
CONTROLS (frozen).
C1 POSITIVE: the engine at B = 257 with W_4's true norms (65537 alone
past B), Y = 10^30 and towerlemma.e_off at k = 4 reproduces
towerlemma.lemma_k(4, 0.381, 1/2, 10^30) (c_z, c_s, G, M, Mp, E,
d0) to 1e-12.
C2 PLANT at the derivation's corner: at B = 17 the engine reads M > 0
and g_up > 0, so the kill can fire.
C3 E_u bounds towerlemma.e_off(D, n_c, d0, X) at every k = 4..7 at B
= 257 and every k = 4..15 at B = 65537.
C4 the S_z, S_s bounds against the sums over the true F_(n+j) (exact
integers, j <= 3, the rest below 1e-300) at B = 257 and 65537: bound
>= sum, and within 1e-3 relative.
C5 the log-domain engine against the float engine at B = 257, 65537
to 1e-12.
FINDINGS (entered after the run, from its printed output).
CONTROLS. C1: 1.1e-16, d0 1093. C2: at B = 17, M +0.00184396 and g_up
+0.0457639, so the kill can fire at the derivation's corner. C3: s_min
23.7751 at B = 257 (log10 E_u -27.2222 against e_off's -46.9903 at k =
7) and 207.945 at B = 65537 (-254.042 against -931.994 at k = 15). C4:
the S_z bound over the true sum by +2.12e-5 at F_3 (0.00044643382
against 0.00044642433) and +3.24e-10 at F_4; S_s by +4.25e-5 and
+6.48e-10. C5: 3.6e-15.
P1 HOLDS: at B = 257, Y = 257^10, c_z - c 0.000445145, c_s 0.000582233,
tail 2.05e-6, log10 E' -27.2222; g_up <= -0.001836571, M <=
-0.002721411, M' <= -8.51791, d0 1093: g_up's excess 0.000991375 and c
lam0 y0/2 0.0001065 against the margin 0.00282795.
P2 HOLDS: at B = 65537, d0 2447300, g_up <= -0.002827506, M <=
-0.002827898, M' <= -18.6461.
P3 HOLDS: no term rises between consecutive points of either grid; g_up,
M, M' < 0 and the excess and c lam0 y0/2 below the margin at every
point; the largest g_up on the real grid -0.001836571, the value P1
prints at B = 257, the grid's first point. The Fermat-number grid read B = 2^(2^n), one below F_n (its
first point 256, largest g_up -0.00183115): a smaller B only raises
every bound, so the read is conservative, and the real grid, from 257
exactly, carries the frozen claim. At F_40, E' is read at its clamp
e^-10^6 (log10 E_u -6.02e129791881613), an upper bound.
KILL MISSED: with the monotonicity by hand and the bounds below 0 at B
= 257, the lemma at (X, c) = (0.381, 1/2), Y = B^10, closes at every
Fermat prime B >= 257: at every k >= 4 with a Fermat prime above 2^k +
1, B the least, a field of the shape loses at every d = 0 mod 2^(k-1)
>= d0(B) = ceil(c lam0 B^b). With W_k empty otherwise (no loss) and
the lemmas at k = 2 and 3, a field of the shape loses at some degree
iff a Fermat prime exceeds 2^k + 1, at every k >= 2; so it loses at
every k iff there are infinitely many Fermat primes, and at 16 <= k <
2^33 iff a Fermat prime past F_32 exists (from 2^33 it must be F_m
with 2^m > k).
RUN RECORD. `python fermatlemma.py` under a 2048 MB cap: 5 of 5 checks,
0.9 s, peak commit 66.1 MB. The engine was appended to the frozen
docstring in one write and run once. After the run, the derivation's
one doc citation was repointed to tower.py's construction (a script cites
no doc); no print moved. At review: P1's code had allowed M' 5e-5 more
than the frozen 1e-5, a change not named (it passes at 1e-5: 9.3e-6), now
restored; P1, P2 and P3 entered the checks, so a failing prediction
exits red (a scratch copy with P1's c_z moved to 0.500544 printed "[FAIL]
P1", 8 of 9 checks, exit 1), with a plant that a rise of 1e-14 relative
is caught; the clamp's dropped factor moved to s_min log 17 >= 2 10^6,
past the clamp. C1 feeds towerlemma's E back in and C5 compares g_up less
E', so eu_log is read by C3's inequality alone. Every data line printed
as before: 9 of 9 checks, 0.9 s, 65.3 MB. Moved in from the lab
unchanged, run bare through the gate: every line printed as before, 9
of 9 checks, 1.4 s, 66.3 MB.
"""
import math
import os
import sys
import time
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, os.path.join(HERE, "..", "code"))
os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
import mpmath as mp # noqa: E402
import towerlemma as tl # noqa: E402
mp.mp.dps = 40
CHECKS = []
XF, CF = 0.381, 0.5
X, C = mp.mpf("0.381"), mp.mpf(1) / 2
B_ = -mp.log(X, 2)
LAM0 = -mp.log(X)
LX = -mp.log1p(-X)
MARGIN = C * LAM0 - LX
J = 6
def check(name, ok, detail=""):
CHECKS.append(bool(ok))
print(f" [{'PASS' if ok else 'FAIL'}] {name}" + (f" ({detail})"
if detail else ""))
def guard():
if not all(CHECKS):
print("a control failed: no verdict")
sys.exit(1)
def fermat_sums(LB, L1):
"""The S_z, S_s bounds over F_(n+j), j >= 1, F_(n+j) - 1 = (B - 1)^(2^j),
from LB = log B, L1 = log(B - 1); j <= J summed, the rest bounded by
twice term J + 1 (each ratio below (B - 1)^(-2^(J+1) b))."""
def tz(j):
return mp.exp(B_ * (LB - 2 ** j * L1)) / -mp.expm1(-2 ** j * B_ * L1)
def ts(j):
return (mp.exp(B_ * (mp.log(2) + LB - 2 ** (j + 1) * L1))
/ -mp.expm1(-2 ** (j + 1) * B_ * L1))
sz = mp.fsum(tz(j) for j in range(1, J + 1)) + 2 * tz(J + 1)
ss = mp.fsum(ts(j) for j in range(1, J + 1)) + 2 * ts(J + 1)
return sz, ss
def e_off_log(D, n, d0):
"""log of towerlemma.e_off(D, n, d0, X), in mpmath."""
s = mp.mpf(d0) / D * B_
return (mp.log(D) - s * mp.log(n) + mp.log1p(n / (s - 1))
- mp.log1p(-mp.power(n, -s)) + mp.log1p(1 / X))
def eu_log(LB, L1, d0):
"""log E_u, k-free: s_min = 4 d0 b/(B - 1), n_c >= 17 (the factor
1/(1 - 17^-s_min) dropped where s_min log 17 >= 2 10^6, a change below
e^-(2 10^6) in a log that is then below -10^6, where E' is read at its
clamp)."""
smin = 4 * d0 * B_ / mp.exp(L1)
q = smin * mp.log(17)
den = -mp.log1p(-mp.exp(-q)) if q < 2 * 10 ** 6 else mp.mpf(0)
return (mp.log1p(1 / X) + (2 - smin) * mp.log(17)
+ mp.log(mp.mpf(1) / 17 + 1 / (smin - 1)) + den), smin
def lemma_u(LB, L1=None, norms=None, LY=None, logE=None, ceil=True):
"""The lemma's bounds at B = e^LB, in mpmath. norms: the W_k norms
past B (default: the Fermat-number bounds); LY = log Y (default 10
LB); logE: log E' (default log E_u), E' read as e^max(logE, -10^6),
an upper bound; ceil: d0 rounded up (unrounded gives a smaller s_min,
so a larger E_u: the bound only weakens)."""
if L1 is None:
L1 = LB + mp.log1p(-mp.exp(-LB))
if LY is None:
LY = 10 * LB
a = LB / mp.log(2)
y0 = mp.exp(-B_ * LB)
if norms is None:
sz, ss = fermat_sums(LB, L1)
else:
sz = mp.fsum(mp.exp(B_ * (LB - mp.log(n))) / (1 - mp.power(n, -B_))
for n in norms)
ss = mp.fsum(mp.exp(B_ * (mp.log(2) + LB - 2 * mp.log(n)))
/ (1 - mp.power(n, -2 * B_)) for n in norms)
tail = ((mp.exp(-B_ * (LY - LB)) + mp.exp(LY - B_ * (LY - LB)) / (B_ - 1))
/ -mp.expm1(-B_ * LY))
d0 = C * LAM0 * mp.exp(B_ * LB)
if ceil:
d0 = mp.ceil(d0)
smin = None
if logE is None:
logE, smin = eu_log(LB, L1, d0)
E = mp.exp(max(logE, -10 ** 6))
czm = C * (y0 / (1 - y0) + sz + tail)
cs = C * (y0 / X / (1 - y0 ** 2) + ss + 2 ** B_ * tail)
cz = C + czm
return dict(cz=cz, czm=czm, cs=cs, tail=tail, y0=y0, E=E, logE=logE,
smin=smin, d0=d0, slope=1 - cz - cs,
G=LX - (1 - cz - cs) * LAM0 + E,
M=LX - C * LAM0 * (1 - y0 / 2),
Mp=1 / (1 - X) - a * C * LAM0 / (X * (1 + y0)),
excess=(cz + cs - C) * LAM0 + E, mexc=C * LAM0 * y0 / 2)
def lemma_float(B):
"""The same bounds at B in floats (B = 257, 65537), Y = B^10, E' out."""
b = -math.log2(XF)
a = math.log2(B)
lam0 = -math.log(XF)
y0 = XF ** a
fz = [(B / (B - 1) ** 2 ** j) ** b / (1 - (B - 1) ** (-2 ** j * b))
for j in range(1, J + 2)]
fs = [(2 * B / (B - 1) ** 2 ** (j + 1)) ** b
/ (1 - (B - 1) ** (-2 ** (j + 1) * b)) for j in range(1, J + 2)]
Y = float(B) ** 10
tail = (B / Y) ** b * (1 + Y / (b - 1)) / (1 - Y ** -b)
d0 = math.ceil(CF * lam0 * XF ** -a)
cz = CF * (1 / (1 - y0) + sum(fz[:J]) + 2 * fz[J] + tail)
cs = CF * (XF ** (a - 1) / (1 - y0 * y0) + sum(fs[:J]) + 2 * fs[J]
+ 2 ** b * tail)
lx = -math.log1p(-XF)
return dict(cz=cz, cs=cs, d0=d0,
G=lx - (1 - cz - cs) * lam0,
M=lx - CF * lam0 * (1 - y0 / 2),
Mp=1 / (1 - XF) - a * CF * lam0 / (XF * (1 + y0)))
def fermat(n):
return 2 ** (2 ** n) + 1
# ------------------------------------------------------------- controls
def controls():
print("=== CONTROLS")
want = tl.lemma_k(4, XF, CF, 10 ** 30)
got = lemma_u(mp.log(257), L1=mp.log(256), norms=[65537],
LY=30 * mp.log(10), logE=mp.log(want["E"]))
err = max(abs(float(got[q]) - want[q]) for q in ("cz", "cs", "G", "M",
"Mp"))
check("C1 POSITIVE: at B = 257, W_4's norms, Y = 10^30, e_off at k = 4, "
"the engine is towerlemma.lemma_k(4)", err < 1e-12
and int(got["d0"]) == want["d0"], f"{err:.1e}, d0 {int(got['d0'])}")
P = lemma_u(mp.log(17), L1=mp.log(16))
check("C2 PLANT: at B = 17 the engine reads M > 0 and g_up > 0",
P["M"] > 0 and P["G"] > 0,
f"M {mp.nstr(P['M'], 6)}, g_up {mp.nstr(P['G'], 6)}")
bad = []
for B, ks in ((257, range(4, 8)), (65537, range(4, 16))):
LB = mp.log(B)
L1 = mp.log(B - 1)
d0 = mp.ceil(C * LAM0 * mp.exp(B_ * LB))
lu, smin = eu_log(LB, L1, d0)
for k in ks:
le = e_off_log(2 ** (k - 1), 2 ** k + 1, d0)
if le > lu:
bad.append((B, k))
if B == 257:
f = tl.e_off(2 ** (k - 1), 2 ** k + 1, int(d0), XF)
if abs(mp.log(f) - le) > 1e-9:
bad.append((B, k, "e_off"))
print(f" B = {B}: s_min {mp.nstr(smin, 6)}, log10 E_u "
f"{mp.nstr(lu / mp.log(10), 6)}, log10 e_off at k = "
f"{ks[-1]} {mp.nstr(le / mp.log(10), 6)}")
check("C3 E_u bounds e_off at k = 4..7 (B = 257), 4..15 (B = 65537)",
not bad, f"{bad}")
bad = []
for n in (3, 4):
B = fermat(n)
LB, L1 = mp.log(B), mp.log(B - 1)
sz, ss = fermat_sums(LB, L1)
Fs = [mp.mpf(fermat(n + j)) for j in range(1, 4)]
ez = mp.fsum((mp.mpf(B) / F) ** B_ / (1 - F ** -B_) for F in Fs)
es = mp.fsum((2 * mp.mpf(B) / F ** 2) ** B_ / (1 - F ** (-2 * B_))
for F in Fs)
rz, rs = sz / ez - 1, ss / es - 1
if not (0 <= rz < 1e-3 and 0 <= rs < 1e-3):
bad.append(n)
print(f" B = F_{n}: S_z bound {mp.nstr(sz, 8)} over the sum "
f"{mp.nstr(ez, 8)} (+{mp.nstr(rz, 3)}); S_s "
f"{mp.nstr(ss, 8)} over {mp.nstr(es, 8)} (+{mp.nstr(rs, 3)})")
check("C4 the Fermat-number bounds over the true F_(n+j) sums, B = 257 "
"and 65537", not bad, f"{bad}")
err = 0.0
for B in (257, 65537):
u = lemma_u(mp.log(B), L1=mp.log(B - 1))
f = lemma_float(B)
err = max([err, abs(float(u["cz"]) - f["cz"]),
abs(float(u["cs"]) - f["cs"]),
abs(float(u["G"] - u["E"]) - f["G"]),
abs(float(u["M"]) - f["M"]),
abs(float(u["Mp"]) - f["Mp"]),
abs(int(u["d0"]) - f["d0"])])
check("C5 the mpmath engine against the float engine at B = 257, 65537",
err < 1e-12, f"{err:.1e}")
guard()
# ----------------------------------------------------------------- arms
def row(tag, L):
return (f" {tag}: d0 {mp.nstr(L['d0'], 8)}, c_z - c "
f"{mp.nstr(L['czm'], 6)}, c_s {mp.nstr(L['cs'], 6)}, tail "
f"{mp.nstr(L['tail'], 3)}, log10 E' "
f"{mp.nstr(L['logE'] / mp.log(10), 6)}; g_up <= "
f"{mp.nstr(L['G'], 7)}, M <= {mp.nstr(L['M'], 7)}, M' <= "
f"{mp.nstr(L['Mp'], 6)}; excess {mp.nstr(L['excess'], 6)}, "
f"c lam0 y0/2 {mp.nstr(L['mexc'], 4)} against the margin "
f"{mp.nstr(MARGIN, 6)}")
def part_p12():
print("\n=== P1, P2: B = 257 and 65537 at Y = B^10")
want = (0.500444, 0.000580, -0.001840, -0.002721, -8.5179)
L = lemma_u(mp.log(257), L1=mp.log(256))
print(row("B = 257", L))
got = [float(L[q]) for q in ("cz", "cs", "G", "M", "Mp")]
p1 = (all(abs(g - w) <= 1e-5 for g, w in zip(got, want))
and int(L["d0"]) == 1093 and L["E"] < 1e-20)
L2 = lemma_u(mp.log(65537), L1=mp.log(65536))
print(row("B = 65537", L2))
p2 = (-0.00283 <= L2["G"] <= -0.00282 and -0.00283 <= L2["M"] <= -0.00282
and L2["Mp"] <= -18.6 and int(L2["d0"]) == 2447300)
check("P1 B = 257 within 1e-5 of towerlemma's k = 4, d0 1093", p1)
check("P2 B = 65537 in its bands, d0 2447300", p2)
def monotone(seq, key):
"""Indices i where seq[i + 1][key] rises past seq[i][key] by more than
1e-15 relative."""
out = []
for i in range(len(seq) - 1):
u, v = seq[i][key], seq[i + 1][key]
if v > u + mp.mpf("1e-15") * abs(u):
out.append(i)
return out
def part_p3():
print("\n=== P3: the Fermat numbers n = 3..40 and a grid of real B")
grids = {}
grids["F_n"] = [(n, lemma_u(mp.mpf(2) ** n * mp.log(2), ceil=False))
for n in range(3, 41)]
lo, hi = mp.log(mp.log(257)), mp.log(mp.mpf(2) ** 40 * mp.log(2))
grids["real"] = [(i, lemma_u(mp.exp(lo + (hi - lo) * i / 1999),
ceil=False)) for i in range(2000)]
killed = False
up = [dict(q=mp.mpf(1)), dict(q=mp.mpf(1) + mp.mpf("1e-14"))]
check("P3 PLANT: a rise of 1e-14 relative is caught", monotone(up, "q")
== [0])
for name, G in grids.items():
seq = [L for _, L in G]
rises = {q: monotone(seq, q) for q in ("czm", "cs", "tail", "logE",
"M", "Mp", "G", "excess")}
nonneg = [i for i, L in G if not (L["G"] < 0 and L["M"] < 0
and L["Mp"] < 0)]
over = [i for i, L in G if not (L["excess"] < MARGIN
and L["mexc"] < MARGIN)]
anyrise = {q: v[:3] for q, v in rises.items() if v}
killed |= bool(nonneg or over or anyrise)
print(f" {name} ({len(seq)} points): rising terms {anyrise or 'none'}"
f"; g_up, M or M' >= 0 at {nonneg[:4]}; excess or c lam0 "
f"y0/2 not below the margin at {over[:4]}; largest g_up "
f"{mp.nstr(max(L['G'] for L in seq), 7)}, largest M "
f"{mp.nstr(max(L['M'] for L in seq), 7)}, largest M' "
f"{mp.nstr(max(L['Mp'] for L in seq), 6)}")
check("P3 no term rises, every bound below 0 and under the margin, on "
"both grids (the KILL missed)", not killed)
n, L = grids["F_n"][-1]
print(row(f"B = F_{n}", L))
def main():
t0 = time.time()
controls()
part_p12()
part_p3()
print(f"\n{sum(CHECKS)} of {len(CHECKS)} checks, {time.time() - t0:.1f} s")
return 0 if all(CHECKS) else 1
if __name__ == "__main__":
sys.exit(main())