towerscan.py
Checks: THERMAL: The 2-power tower raises the sill theorem; rule.
Cited on: THERMAL.
To run it: save towerscan.py, with fieldtop.py, growth.py, memory.py, sillclass.py, spectrum.py, splitend.py, splitloss.py, splitsharp.py, tower.py, typeloss.py beside it; needs mpmath, numpy, scipy.
"""towerscan.py -- the 2-power tower's no-loss half: where the bound's
minimum over the count of n_c sits, where its count-0 end turns, and the
first losing degree at k = 5 to 15.
QUESTION. With Q(zeta_(2^k)) in K, K_ab = Q(zeta_(2^k)), type (1, 0), K
!= Q(zeta_(2^k)), d = D m', D = 2^(k-1), tower.py's bound is the least
over the count n of places of norm n_c = 2^k + 1, 0 <= n <= cap, of
F(n) = M(x_c(n)). (A) Is that least always at n = 0 or n = cap? (B) Is
the count-0 end's turn in d exactly computable, and is the first
admissible d past it the first past d* = l(x0)/u_k(x0)? (C) With (A)
and (B), is the cap end positive at every admissible d from 2D to below
D(k), at k = 2, 3, 4, 8, so that no such field loses below D(k)? (D) At
k = 5..7 and 9..15, where n_c is not a prime power (cap 0), does a field
lose at the first admissible degree past the turn?
THE DERIVATION (by hand, before this code).
(A) At x_c, l + w + log x = 0 with w = w_k + n phi, phi = log(1 +
x^(a_c)), a_c = log2 n_c, so M(x_c) = l - l_c - w_k = h_c(x_c) + n
phi(x_c), h_c = 2l - l_c + log x: tower.py's bound_at is F(n) = M(x_c
(n)) with M = l - l_c - w_k the SAME function at every n (the places
of norm n_c cancel in M). g(x, n) = l + log x + w_k + n phi rises in x
and in n, so x_c(n) falls strictly in n, and x_c < 1/2 (g(1/2) = w >
0). (1 - x)M' = 1 - (2^k + 1)x^(2^k)/P_k - the W_k terms, each term
increasing on (0, 1/2] (tower.py's derivation (5)), so (1 - x)M'
falls there, M' changes sign at most once, from +
to -, and M rises then falls on (0, 1/2]. As n runs over [0, cap],
x_c runs over [x_c(cap), x_c(0)], and a function that rises then falls
takes its least on an interval at an end: min_n F(n) = min(F(0),
F(cap)), for real n and so for integer n. Differentiating: dF/dn =
-phi M'(x_c)/g_x, g_x = dg/dx > 0, so F rises in n while x_c is past
M's peak and falls after: F rises (if at all) then falls in n, its
peak interior exactly where x_c(cap) < M's peak < x_c(0). (A) is a
theorem; the run can fail only through an engine fault.
(B) At count 0, F0(d) = h_c(x_c(d)), h_c increasing (tower.py's (5):
(2^k + 1)x^(2^k) <= P_k) and x_c(d) falling strictly in d (g rises in
d through d u_k), so F0 falls strictly in d. Let x_h be the root of
h_c: log x_h = l_c - 2l at x_h. F0(d) <= 0 iff x_c(d) <= x_h iff g(x_h,
d) >= 0 iff l + log x + d u_k >= 0 at x_h iff d >= d_h = (l(x_h) -
l_c(x_h))/u_k(x_h). d* is d_h with l_c set to 0 (x_h -> x0): a
TRANSPLANT that the shift is below one step, re-derived here: l_c(x0)
= -log(1 - x0^(2^k + 1)), x0^5 = 8.1e-3 at k = 2, x0^9 = 1.7e-4 at k =
3, x0^17 = 7.8e-8 at k = 4, below 1e-100 at k = 8; the shift in d is
about d l_c' / (u_k' ...) of relative size l_c/l: at k = 2 about 0.1
of d* = 11.2, so about 1, a full step of 2 at risk; elsewhere far below
a step. So the bound at count 0 is positive at every d < d_h and at
most 0 at every d >= d_h: a theorem, d_h one computed number per k.
(C) By (A), the bound at d is min(F0(d), Fcap(d)); by (B), F0 > 0 below
d_h. So no field of the shape loses at an admissible d < d_h where
Fcap(d) > 0, and the bound is at most 0 from d_h. Fcap's monotonicity
in d is not derived (cap rises with d as x_c falls); it is read at
every admissible d: k = 2 (d even, 4..10), 3 (cap d/2, 8..24), 4
(16..1064), 8 (cap d, 256..2343936, 18,311 degrees). At k = 8, d near
D(8): x_c(cap) solves d x^8.006 ~ log(1/x), about 0.172, and Fcap ~
l(0.172) ~ 0.19, far above F0's 1e-6: the argmin is 0 there.
(D) At k = 5, 6, 7, n_c = 33, 65, 129 and at k = 9..15, 2^k + 1 = 513,
1025, 2049, 4097, 8193, 16385, 32769 are not prime powers, so no place
has norm n_c, cap = 0, and (B) alone gives no loss below d_h. W_k is
{257, 65537} at k = 5..7 (d* = k = 4's 1067.55: D(5) = 1072, D(6) =
D(7) = 1088) and {65537} at k = 9..15 (d* = k = 8's 2343958.59: D(k)
= 2344192, 2344448, 2344960, 2344960, 2347008, 2351104, 2359296), the
composite F_5..F_9 counted by tower.wk (they only lower the bound; no
norm equals them). The realization is tower.py's (m' >= 6 at each:
m' = 67, 34, 17 at k = 5..7, 144 at k = 15). F0 at D(k) is about -(D(k)
- d_h) 4.9e-8 at k >= 9 (k = 8's slope: 6.3e-6 per 128), -1.1e-5 at k
= 9 down to -7.5e-4 at k = 15; the tail past Y = 10^60 is about d
Y^(1 - b)/(b - 1) ~ 3e-17; at k = 5..7 the margin is k = 4's order
(-4.8e-4 at 1072 at Y = 10^30).
PREDICTIONS (frozen before the engine).
P1 (A) the least of F over every count is at n = 0 or n = cap, never
below min(F(0), F(cap)) by more than 1e-12: at every admissible d
to 200 at k = 2, 3 and to 1080 at k = 4 (tower.bound's full scan),
and at k = 8 by a vectorized bisection over every count at d =
1280, 1171968, 2343936 and 2344064; at k = 4 the argmin is cap at
16..200 and 0 at 400..1080, at k = 8 it is 0 at 2343936 and 2344064.
P2 (B) the count-0 turn over admissible d equals the first admissible
d >= d_h at k = 2, 3, 4, 8 (read 3 steps either side), and the
first admissible d past d_h equals the first past d* at every k =
2..15, |d_h - d*| < 1 at every k >= 3 (at k = 2 a guess).
P3 (C) Fcap > 0 at every admissible d from 2D to below D(k) at k = 2,
3, 4, 8 (D(k) = 12, 28, 1072, 2344064), so with P1 the bound is
positive at each.
P4 (D) at k = 5, 6, 7 (Y = 10^30) and 9..15 (Y = 10^60) the
certificate is negative with M' < 0 and x_c < 1/2 at D(k), D(k) + D
and D(k) + 2D, and at k = 5..7 positive at D(k) - D.
KILL of the no-loss half as a theorem: P1 failing (an interior argmin
below the ends by more than 1e-12), or P3 failing (then D(k) is not
the count-0 turn, a new first degree). KILL of the pattern "D(k) the
first admissible degree past d*": P2's first-degree equality failing
at any k = 2..15.
CONTROLS (frozen).
C1 POSITIVE: the vectorized bisection reproduces tower.bound_at(k, d,
n) at k = 4, d = 1072 and k = 8, d = 2344064, at n = 0, cap/2, cap
and 5 random counts, to 1e-12; and at k = 4 the endpoint engine's
argmin reproduces tower.py's printed argmins (cap at 16..200, 0 at
400..1080).
C2 PLANT: F plus -1e-9 * 4n(cap - n)/cap^2 (an interior dip) at k = 8,
d = 2344064, read by the same interior test, reports an interior
argmin.
C3 dF/dn = -phi M'(x_c)/g_x against a central difference in n (real n)
at k = 4, d = 1072, n = 300 and k = 8, d = 2344064, n = 10^6, to
1e-6 relative.
C4 at k = 5 and 9, bound_at(k, d, 0) equals TowerLaw(k, law of exactly
those counts, no tail).m(x_c) at D(k), to 1e-12 (the k >= 5
wiring, as towerpast's C4 at k = 8).
C5 (added before the run) order2, the least 2^j with p^(2^j) = 1 mod
2^k, equals tower.order_mod at k = 5, 9 on the first 3000 odd
primes, and replaces it, so tower.law is fast at k = 15.
FINDINGS (entered after the run, from its printed output).
CONTROLS. C1: 8.2e-15; the k = 4 argmins cap at 16..200 and 0 at
400..1080, at every such d (this half reruns tower.bound, the engine
that printed them, so it reads nothing new). C2 FAILED as frozen, missed by
construction: F's interior sits above its ends (by 3.423e-04 at the
least interior count, the peak (A) derives), so a dip of 1e-9 cannot
reach below them. Replaced after its run by C2': M swapped for (x -
x_m)^2 through the same bisection, x_m bound_at's x_c at cap/3: argmin
781354 = cap/3, read as interior. C2' is caught by construction (x_c
falls strictly, so (x - x_m)^2 vanishes at cap/3 alone): it reads the
argmin's wiring (its own copy of the interior test), and no plant
here could miss; P1 rests on (A)'s proof, at k = 8 also on C1's
agreement of fvec with bound_at. C3: at k
= 4, -1.211527e-04 by difference and by formula; at k = 8,
-2.597615e-08 by both; 3.2e-08 relative. C4: 5.6e-16. C5: no
mismatch.
(A) P1 HOLDS: at the 282 fully scanned degrees no interior count lies
below the ends; at k = 8 over every count, the interior least minus
the ends' least is +4.191e-05 at d = 1280 (argmin cap, F falling from
its maximum at 0, so no interior peak there), +4.337e-04 at
1171968, +3.423e-04 at 2343936 and
2344064 (argmin 0, the maximum at count 3959, 6461, 6461).
(B) P2 HOLDS: d_h - d* is -0.286 at k = 2 (d_h 10.9186), -0.0141 at
3, -4.3e-04 at 4, below 1e-8 from 5; the first admissible d past d_h
is the first past d* at every k = 2..15 (12, 28, 1072, 1072, 1088,
1088, 2344064, 2344192, 2344448, 2344960, 2344960, 2347008,
2351104, 2359296), and count 0 turns there at k = 2, 3, 4, 8
(-2.997e-02, -4.315e-02, -8.176e-04, -5.193e-06).
(C) P3 HOLDS: F(cap) > 0 at every admissible d from 2D below D(k): 4
degrees at k = 2 (least +0.1670), 5 at 3 (+0.1242), 132 at 4
(+0.2174), 18311 at 8 (+0.1858, at 2343936); the least over both ends
+2.746495e-02, +3.125616e-03, +6.555276e-04, +1.113163e-06, each at
the last d below D(k).
KILL of the no-loss half MISSED; KILL of the first-degree pattern
MISSED. So with (A) and (B) proved, the bound is positive at every
admissible d from 2D below D(k) at k = 2, 3, 4, 8 (and at k = 5..7,
9..15, cap 0, by (B) alone), and at most 0 from D(k), at every k =
2..15.
(D) P4 HOLDS: the certificate is negative with M' < 0 and x_c < 1/2 at
D(k), D(k) + D and D(k) + 2D at every k = 5..7 (Y = 10^30; -4.827e-04
at 1072, -3.398e-03 at 1088, 1088) and 9..15 (Y = 10^60; -1.128e-05 at
2344192 to -7.530e-04 at 2359296), and positive at D(k) - D at k = 5..7
(+2.475e-03 at 1056, 1056, +8.524e-03 at 1024).
RUN RECORD. `python towerscan.py` under a 2048 MB cap: 6 of 6 checks,
79.8 s, peak commit 256.2 MB. The first run stopped at C2's guard (5
of 6 checks, 18.7 s, 221.6 MB, C1 and C3 to C5 printing as here); C2'
was added and the script run again. At review, after the findings: the
derivation's "F is unimodal in n, its peak interior" was wider than
(A) (the peak is at 0 at d = 1280), its x0^17 misread (7.6e-8 for
7.8e-8), and a doc citation cut; C2' relabelled as the wiring check it
is; C5's text added to the controls with the findings. Every line
printed as before but C2''s label: 6 of 6 checks, 80.1 s, peak commit
257.5 MB. Moved in from the lab unchanged, run bare through the gate:
every line printed as before, 6 of 6 checks, 80.3 s, 256.3 MB; at its
next review a 1088 repeated in (B)'s list of first degrees was cut.
"""
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 numpy as np # noqa: E402
from scipy.optimize import brentq # noqa: E402
import splitend as se # noqa: E402
import splitsharp as ss # noqa: E402
import tower as tw # noqa: E402
CHECKS = []
TOL = 1e-12
DK = {2: 12, 3: 28, 4: 1072, 8: 2344064}
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 is_pp(n):
p = 2
while p * p <= n:
if n % p == 0:
while n % p == 0:
n //= p
return n == 1
p += 1
return n > 1
def step(k):
return 2 ** (k - 1)
def cap(k, d):
if not is_pp(tw.nc(k)):
return 0
return d // 2 if k == 3 else d
def wterms(k):
"""(a, weight per unit of d) over W_k, 9 at weight 1/2."""
return [(math.log2(n), 0.5 if n == 9 else 1.0) for n in tw.wk(k)]
# ------------------------------------------------- the vectorized bound
def fvec(k, d, n, iters=80):
"""F = M(x_c) at arrays d, n (broadcast), x_c by bisection."""
d = np.asarray(d, dtype=float)
n = np.asarray(n, dtype=float)
d, n = np.broadcast_arrays(d, n)
ac = math.log2(tw.nc(k))
W = wterms(k)
lo = np.full(d.shape, 1e-14)
hi = np.full(d.shape, 0.5)
for _ in range(iters):
x = 0.5 * (lo + hi)
lx = np.log(x)
g = -np.log1p(-x) + lx + n * np.log1p(np.exp(ac * lx))
for a, c in W:
g = g + c * d * np.log1p(np.exp(a * lx))
up = g > 0
hi = np.where(up, x, hi)
lo = np.where(up, lo, x)
x = 0.5 * (lo + hi)
lx = np.log(x)
hc = 2 * -np.log1p(-x) + np.log1p(-x ** tw.nc(k)) + lx
return hc + n * np.log1p(np.exp(ac * lx)), x
def ends(k, d):
c = cap(k, d)
f0 = tw.bound_at(k, d, 0)[0]
fc = tw.bound_at(k, d, c)[0] if c else f0
return f0, fc, c
def xh(k):
return brentq(lambda x: tw.hc(k, x), 0.2, 0.5, xtol=1e-18, rtol=1e-15,
maxiter=500)
def dh(k):
x = xh(k)
u = sum(c * math.log1p(x ** a) for a, c in wterms(k))
return (se.lf(x) - tw.lc(k, x)) / u
def first_past(v, s):
return s * math.floor(v / s) + s
ORDER = tw.order_mod
def order2(p, q):
"""The order of p mod q = 2^k: a power of 2, the least 2^j with
p^(2^j) = 1 mod q."""
f = 1
while pow(p, f, q) != 1:
f *= 2
return f
# ------------------------------------------------------------- controls
def controls():
print("=== CONTROLS")
rng = np.random.default_rng(1940)
err = 0.0
for k, d in ((4, 1072), (8, 2344064)):
c = cap(k, d)
ns = [0, c // 2, c] + [int(v) for v in rng.integers(0, c + 1, 5)]
fv, _ = fvec(k, d, np.array(ns))
for n, f in zip(ns, fv):
err = max(err, abs(f - tw.bound_at(k, d, n)[0]))
check("C1 POSITIVE: the vectorized bisection is bound_at at 8 counts "
"each at (4, 1072), (8, 2344064)", err < TOL, f"{err:.1e}")
bad = []
for d in range(16, 1081, 8):
if 200 < d < 400:
continue
v, n, _ = tw.bound(4, d, True)
want = d if d <= 200 else 0
if n != want:
bad.append((d, n))
check("C1 POSITIVE: k = 4 argmin cap at 16..200, 0 at 400..1080",
not bad, f"else at {bad[:6]}" if bad else "")
k, d = 8, 2344064
c = cap(k, d)
ns = np.arange(c + 1, dtype=float)
F, xs = fvec(k, d, ns)
Fp = F - 1e-9 * 4 * ns * (c - ns) / c ** 2
inner = Fp[1:-1].min() < min(Fp[0], Fp[-1]) - TOL
print(f" C2 as frozen (missed by construction, F's interior above its "
f"ends): interior least - ends' least "
f"{Fp[1:-1].min() - min(Fp[0], Fp[-1]):+.3e}, read {inner}")
nm = c // 3
xm = tw.bound_at(k, d, nm)[2]
Mp = (xs - xm) ** 2
am = int(Mp.argmin())
inner = Mp[1:-1].min() < min(Mp[0], Mp[-1]) - TOL
check("C2' WIRING (replacing C2 after its run; by construction): M "
"-> (x - x_m)^2, x_m bound_at's x_c at cap/3, (8, 2344064): an "
"interior argmin at cap/3", inner and abs(am - nm) <= 1,
f"argmin {am}, cap/3 {nm}")
worst = 0.0
for k, d, n in ((4, 1072, 300), (8, 2344064, 10 ** 6)):
h = 1e-3 if k == 4 else 1.0
fp, _ = fvec(k, d, np.array([n + h]))
fm, _ = fvec(k, d, np.array([n - h]))
num = (fp[0] - fm[0]) / (2 * h)
_, x = fvec(k, d, np.array([float(n)]))
x = float(x[0])
ac = math.log2(tw.nc(k))
phi = math.log1p(x ** ac)
W = [(a, c * d) for a, c in wterms(k)]
gx = (1 / (1 - x) + 1 / x + n * ac * x ** (ac - 1) / (1 + x ** ac)
+ sum(c * a * x ** (a - 1) / (1 + x ** a) for a, c in W))
q = tw.nc(k)
mp = (1 / (1 - x) - q * x ** (q - 1) / (1 - x ** q)
- sum(c * a * x ** (a - 1) / (1 + x ** a) for a, c in W))
form = -phi * mp / gx
rel = abs(num - form) / abs(form)
worst = max(worst, rel)
print(f" k = {k}, d = {d}, n = {n}: dF/dn {num:+.6e} by "
f"difference, {form:+.6e} by the formula")
check("C3 dF/dn = -phi M'(x_c)/g_x", worst < 1e-6, f"{worst:.1e}")
e4 = 0.0
for k in (5, 9):
d = first_past(tw.dstar(k), step(k))
v, _, xc = tw.bound_at(k, d, 0)
w, _ = tw.caps(k, d)
Wl = [(math.log2(m), c, 1) for m, c in w]
e4 = max(e4, abs(v - tw.TowerLaw(k, ss.Law(d, Wl, tail=False))
.m(xc)))
check("C4 k = 5, 9: bound_at(k, d, 0) = M(x_c) on its law at D(k)",
e4 < TOL, f"{e4:.1e}")
bad = [(p, k) for k in (5, 9) for p in tw.PR_Y[:3000]
if order2(p, 2 ** k) != ORDER(p, 2 ** k)]
check("C5 (added before the run) order2 is tower.order_mod at k = 5, "
"9 on the first 3000 odd primes", not bad, f"{bad[:4]}")
guard()
tw.order_mod = order2
# ----------------------------------------------------------------- arms
def part_a():
print("\n=== (A) the least over the count sits at an end")
bad, n_read = [], 0
for k, dmax in ((2, 200), (3, 200), (4, 1080)):
s = step(k)
for d in range(2 * s, dmax + 1, s):
v, n, _ = tw.bound(k, d, True)
f0, fc, c = ends(k, d)
n_read += 1
if v < min(f0, fc) - TOL:
bad.append((k, d, n, v - min(f0, fc)))
print(f" full scans at {n_read} degrees (k = 2, 3 to 200, k = 4 to "
f"1080): interior below the ends at {bad[:6]}")
for d in (1280, 1171968, 2343936, 2344064):
c = cap(8, d)
F, _ = fvec(8, d, np.arange(c + 1, dtype=float))
gap = F[1:-1].min() - min(F[0], F[-1])
am = int(F.argmin())
if gap < -TOL:
bad.append((8, d, am, gap))
print(f" k = 8, d = {d}: every count 0..{c}; F(0) {F[0]:+.6e}, "
f"F(cap) {F[-1]:+.6e}, interior least - ends' least "
f"{gap:+.3e}, argmin {am}, max {F.max():+.6e} at "
f"{int(F.argmax())}")
print(f" P1 {'holds' if not bad else 'FAILS'}")
return not bad
def part_b():
print("\n=== (B) the count-0 turn")
ok_turn, ok_first, ok_gap = True, True, True
for k in range(2, 16):
s = step(k)
h, st = dh(k), tw.dstar(k)
fh, fs = first_past(h, s), first_past(st, s)
line = (f" k = {k:2d}: x_h {xh(k):.10f}, d_h {h:.4f}, d* {st:.4f}"
f" (d_h - d* {h - st:+.3e}); first d = 0 mod {s} past each "
f"{fh}, {fs}")
ok_first &= fh == fs
if k >= 3:
ok_gap &= abs(h - st) < 1
if k in DK:
vals = [(d, tw.bound_at(k, d, 0)[0])
for d in range(fh - 3 * s, fh + 3 * s + 1, s)
if d >= 2 * s]
turn = min(d for d, v in vals if v <= 0)
pos = all(v > 0 for d, v in vals if d < fh)
ok_turn &= turn == fh and pos
line += (f"; count 0 turns at {turn} ({dict(vals)[fh]:+.3e} "
f"there)")
print(line)
print(f" P2 turn = first past d_h: {ok_turn}; first past d_h = first "
f"past d*: {ok_first}; |d_h - d*| < 1 at k >= 3: {ok_gap}")
return ok_turn and ok_first and ok_gap
def part_c():
print("\n=== (C) the cap end below D(k)")
ok = True
for k in (2, 3, 4, 8):
s = step(k)
ds = np.arange(2 * s, DK[k], s, dtype=float)
cs = np.array([cap(k, int(d)) for d in ds], dtype=float)
F, x = fvec(k, ds, cs)
F0, _ = fvec(k, ds, np.zeros_like(ds))
j = int(F.argmin())
spot = [0, len(ds) // 2, len(ds) - 1]
err = max(abs(F[i] - tw.bound_at(k, int(ds[i]), int(cs[i]))[0])
for i in spot)
good = bool((F > 0).all())
ok &= good and err < TOL
print(f" k = {k}: {len(ds)} degrees {int(ds[0])}..{int(ds[-1])}: "
f"F(cap) > 0 at all: {good}; least F(cap) {F[j]:+.6e} at d = "
f"{int(ds[j])} (x_c {x[j]:.6f}); F(cap) - F(0) at the last d "
f"{F[-1] - F0[-1]:+.6e}; the least over both ends "
f"{min(F.min(), F0.min()):+.6e}; spot check against bound_at "
f"{err:.1e}")
print(f" P3 {'holds' if ok else 'FAILS'}")
return ok
def part_d():
print("\n=== (D) k = 5..7 and 9..15: the first losing degree")
ok = True
for k in list(range(5, 8)) + list(range(9, 16)):
s = step(k)
D0 = first_past(dh(k), s)
Yc = 10 ** 30 if k <= 7 else 10 ** 60
tag = "10^30" if k <= 7 else "10^60"
assert cap(k, D0) == 0
ds = [D0, D0 + s, D0 + 2 * s] + ([D0 - s] if k <= 7 else [])
row = []
for d in ds:
C, dm, xl, xc = tw.TowerLaw(k, tw.BigLaw(tw.law(k, d), Yc,
s)).cert()
good = C < 0 and dm < 0 and xc < 0.5
if d >= D0:
ok &= good
else:
ok &= C > 0
row.append(f"{d} {C:+.3e}")
print(f" k = {k:2d}, Y = {tag}, m' = {D0 // s}: certificate at "
+ "; ".join(row) + f" (F0 at {D0}: "
f"{tw.bound_at(k, D0, 0)[0]:+.3e})")
print(f" P4 {'holds' if ok else 'FAILS'}")
return ok
def main():
t0 = time.time()
controls()
p1 = part_a()
p2 = part_b()
p3 = part_c()
p4 = part_d()
nl = "fires" if not (p1 and p3) else "missed"
print(f"\nKILL of the no-loss half: {nl}; KILL of the first-degree "
f"pattern: {'fires' if not p2 else 'missed'}; P4 "
f"{'holds' if p4 else 'FAILS'}")
print(f"{sum(CHECKS)} of {len(CHECKS)} checks, {time.time() - t0:.1f} s")
return 0 if all(CHECKS) else 1
if __name__ == "__main__":
sys.exit(main())