"""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())