splitend.py
Checks: THERMAL: A loss needs degree 16 to 732 where 2 splits theorem; rule; observation.
Cited on: THERMAL.
To run it: save splitend.py, with fieldtop.py, growth.py, memory.py, spectrum.py, splitloss.py beside it; needs mpmath, numpy, scipy.
"""splitend.py -- where does the band of losing degrees end, over the
fields where 2 splits completely?
QUESTION. splitloss.py: where 2 and 5 split completely the sill's
margin at the F_2 point is negative at 1033 fields K(m, d), at d = 18,
20, 22, 24, 26 and every d from 28 read to 200, and the bare law's margin is
negative at d = 28..676 only, of 12..2000. At the F_2 point x falls
like log(d)/d and each place of Fermat norm n moves the margin by about
d n^-b, which over x tends to 0. Is there a degree D past which the
F_2 place tops every column of norm above 3 at EVERY number field where
2 splits completely, and a degree below which it does too; where are
the band's two ends?
THE DERIVATION (by hand, before any engine). 2 splits completely in K
of degree d; x = 2^-b; l(x) = log(1/(1 - x)), l4(x) = log(1/(1 - x^4)).
The F_2 column holds the d - 1 other places of norm 2 without bound and
each place of norm n = 3, 5, 9, 17, 257, 65537 or a Fermat prime past
them once (n - 1 a power of 2; 9 is the only prime power of that form
that is not prime, Mihailescu). Put zeta_K = (1 - x)^-d Z', Z' =
S3 W (1 + rho), S3 over the places of norm 3, W = exp(w(x)) over those
of norm 5, 9, 17, ..., rho >= 0. Then zeta_K - sigma_F2 = (1 - x)^-d
S3 W (x + rho), and the F_2 point solves
(E) d l(x) + log S3 + w(x) + log(x + rho) = 0,
and, the sill being S3 (1 + x + x^2 + x^3)^d (2 unramified),
(M) log(1 + margin) = l(x) - d l4(x) - w(x).
Let the field's counts be c = (n5, n9, n17, n257, n65537, n_k): places
of norm 5, 9, 17, ... in the column, w_c(x) = sum n_n log(1 + x^a_n),
a_n = log2 n. Each n_n <= d (places over one prime with f = 1), and
n9 <= floor(d/2).
STEP 1 (quasi-concave). M_c(x) := l - d l4 - w_c has M_c(0) = 0,
M_c'(0) = 1, and (1 - x) M_c' = 1 - 4 d x^3/((1 + x)(1 + x^2)) -
sum n_n a_n (1 - x) x^(a_n - 1)/(1 + x^a_n). Each subtracted term
increases on (0, 0.4): the first's log-derivative is 3/x - 1/(1 + x)
- 2x/(1 + x^2) > 0; the others' is (a - 1)/x - 1/(1 - x) -
a x^(a-1)/(1 + x^a), falling in x and, at a = log2 5, 1.02 at 0.4
(splitloss.py's C4), larger at larger a. So M_c rises, then falls
once, on [0, 0.4]: on any [0, X] it is >= min(0, M_c(X)).
STEP 2 (the point's ceiling). The left side of (E) increases with x
(zeta_K - sigma_F2 is a Dirichlet series with nonnegative
coefficients, the column's ideals being among all ideals); S3 >= 1
and rho >= 0, so the field's point x_f <= x_c, the root of
d l(x) + w_c(x) + log x = 0; and x_c <= x0(d), the root of
d l(x) + log x = 0 (x0(2) = 0.382 < 0.4, falling with d).
STEP 3 (the margin at the ceiling is a function of the point). At x_c,
w_c = -d l - log x, so M_c(x_c) = h(x_c), h(x) = (d + 1) l(x) -
d l4(x) + log x, and h' = (d + 1)/(1 - x) - 4 d x^3/(1 - x^4) + 1/x
> 0 on (0, 1) (4x^3 < 1 + x + x^2 + x^3 there). So a larger w lowers
the ceiling and with it h: the margin at the ceiling falls with
every count.
THE WORST LAW. Let w* = sum N_n log(1 + x^a_n), N = d at 5, 17, 257,
65537 and every Fermat number 2^(2^k) + 1, k >= 5 (counted as prime,
a bound), N9 = floor(d/2); x*(d) the root of d l + w* + log x = 0.
Then w_c <= w* pointwise, so x* <= x_c, and every field of degree d
where 2 splits completely has
log(1 + margin) >= min(0, M_c(x_c)) = min(0, h(x_c)) >=
min(0, h(x*(d))).
So the margin is positive at every such field wherever h(x*(d)) > 0
(strictly: M_c rises from 0, then falls once, to a positive value):
one root and one number per degree, the WORST LAW's (2, 5, 17, 257,
65537 split, every place over 3 of degree 2, rho = 0; realizable or
not, it bounds).
THE TAIL. For all large d at once: with x_f <= x0(d) and w_c <= w*,
M_c(x_f) >= f_d(x_f) >= min(0, f_d(x0)), f_d = l - d l4 - w*
quasi-concave by STEP 1, and f_d(x0) >= x0 (1 - d B(x0)), B(t) =
t^3/(1 - t^4) + sum c_n t^(a_n - 1) (c = 1, 1/2 at 9; l >= x,
l4 <= t^4/(1 - t^4), log(1 + s) <= s). At x0, d = log(1/x0)/l(x0)
<= log(1/x0)/x0, so d B(x0) <= Q(x0), Q(t) = log(1/t) (t^2/(1 - t^4)
+ sum c_n t^(a_n - 2)). Each term log(1/t) t^s increases on
(0, exp(-1/s)); the least s is a5 - 2 = 0.3219, so Q increases on
(0, 0.0448]. If Q(t*) < 1 at some t* <= 0.0448, every d >= delta(t*)
= log(1/t*)/l(t*) has x0(d) <= t* and so a positive margin at every
field. By hand: Q(0.006) ~ 0.993, Q(0.007) ~ 1.012, so t* ~ 0.0065
and delta ~ 770, just past the bare law's 676: the tail is nearly
sharp, since w moves (E) by only d x^2.32 ~ 0.007 against log(1/x)
~ 5 there.
FIRST ORDER (a TRANSPLANT of small x, for the predictions only): the
9-term adds (1/2) x^0.85 ~ 0.8% to the 5-term's d x^1.32 near
d = 700, and log(d x^1.32) falls about 0.05 per unit of log d, so the
worst law's end sits about 60 to 100 degrees past 676.
DESIGN.
ENGINE. h(x*(d)) by brentq on d l + w* + log x in logs, d = 2..D,
D = ceil(delta(t*)) + 200; t* the root of Q - 1 on (0, 0.0448],
bisected, taken 1e-9 below it.
PRINTS. h(x*(d)) at d = 2..40 and every 50th; the least d with
h(x*) <= 0 (d_lo) and the greatest (d_hi); every d in d_lo..d_hi
where h(x*) > 0 (gaps); the least h(x*) and its d; t*, Q(t*),
delta(t*); the largest grid step of each W-term's log-derivative on
(0, 0.4] and its value at 0.4; x*(2), x0(2).
THE CHECK ON FIELDS. splitloss.py's family (the 3417 fields K(m, d),
12 <= d <= 200) and its C1 fields: each bracket's top against
min(0, h(x*(d))) - 1e-9; the population printed, and the least slack.
CONTROLS, read before any verdict.
C1 the solver on the bare law's counts (n5 = d alone) with splitloss's
rho_bare = (1 - 5^-2b)^-d - 1 restored equals splitloss.py's bare(d)
to 1e-10 at d = 12, 60, 676, 677; with rho = 0 it is below bare(d)
by less than 1e-6 there.
C2 the identity of STEP 3: M_c(x_c) = h(x_c) to 1e-12 at the worst
law, d = 12, 100, 700.
C3 PLANT: the bound with the places of norm 9 dropped from w* (N9 = 0)
prints a field of the sweep below min(0, h) - 1e-9 (K(6082471, 18),
-0.000527, sits where the bound so planted is >= 0): the check on
fields can fire.
C4 PLANT on the tail: Q without its 9-term gives a t* above the true
one and a delta below it (the 9-term is what moves the end).
PREDICTIONS, frozen before the run.
(p1) THE BOUND: no field of the check falls below min(0, h(x*(d))).
(p2) THE TAIL: Q(t*) < 1 at a t* in 0.005..0.008, delta(t*) in
700..900.
(p3) THE UPPER END: d_hi, the greatest d with h(x*) <= 0, lies in
700..800, d_hi >= 676, and d_hi < delta(t*).
(p4) THE LOWER END: d_lo lies in 14..18 (K(6082471, 18) loses, so
d_lo <= 18); h(x*) > 0 at every d from 2 to d_lo - 1.
(p5) ONE BAND: no gap in d_lo..d_hi but at odd d below 30.
KILL, written as what the script prints: the worst-law bound is dead
if (p1) prints a field below it (its bar on the bracket's TOP, the
side the tail confound inflates), and then no end is claimed; the
tail is dead if Q(t) >= 1 at every t of (0, 0.0448] printed, and
then the upper end is claimed only to D computed. The answer to the
question is yes, with the band inside [d_lo, d_hi], if (p1) holds and
Q(t*) < 1.
FINDINGS.
CONTROLS. C1: the solver with rho_bare restored equals bare(d) to
1.1e-15, 2.1e-15, 3.2e-14, 4.7e-15 at d = 12, 60, 676, 677; rho = 0
lowers the margin by 4.4e-04, 1.7e-05, 1.7e-08, 1.7e-08 there (the
frozen "< 1e-6" was a TRANSPLANT of large d, false at 12 and 60; the
check now reads the bound's direction, the size printed). C2: M = h
at d = 12, 100, 700 (+0.005323918608, -0.004185213188,
-0.000032080814). STEP 1: the log-derivatives at 0.4 are 1.0202,
3.3466, 5.8161, 15.8344, 35.8334 at n = 5, 9, 17, 257, 65537, each
falling on the grid; the x^4 term's at least 6.0961. x0(2) = 0.381966,
x*(2) = 0.344473.
THE TAIL: t* = 0.006366569169, Q(t*) = 0.999999999869, delta(t*) =
791.7263: at every d >= 792 every field where 2 splits completely has
a positive margin. C4: Q without its 9-term puts t* at 0.006728553,
delta 740.8056.
THE WORST LAW, d = 2..991: h(x*) <= 0 at exactly the 717 degrees
d = 16..732, no gap; +0.000707 at 15, -0.001073 at 16, least
-0.006794121 at d = 36; -8.26e-07 at 732, +1.65e-07 at 733, and at
least +1.645e-07 from 733 to 991. So at every number field where 2
splits completely, of degree 2 <= d <= 15 or d >= 733, the margin is
positive and the F_2 place tops every column of norm above 3; a loss
needs 16 <= d <= 732.
THE IDEAL (added after the run): the worst law with its W-places'
powers (rho_c) and, at odd d, the one place of norm 3 that floor(d/2)
places of norm 9 leave over 3, with its square: log(1 + margin)
+3.3854e-03 at 15, -7.2912e-04 at 16, +6.3714e-04 at 17, -1.0913e-06
at 731, -8.1194e-07 at 732, +7.5461e-07 at 733: both ends survive
the squares; at odd d the worst law is not attained (its S3 = 1 asks
no place of norm 3), and at 17 the ideal is positive.
THE CHECK ON FIELDS: 3443 fields (splitloss.py's 3417 and C1's 26),
none below min(0, h(x*(d))) in margin; the least slack +6.357e-05 at
K(2838889, 36), the sweep's least field, so the bound is within 1e-4
of a real field there. C3: with N9 = 0 the bound is broken by 56
fields, the first K(756271, 18) at -0.000526.
(p1) to (p5) hold: d_lo = 16, d_hi = 732, t* in 0.005..0.008, delta
791.7. The kill missed. Unread: whether any field of degree 16, 17 or
near 732 loses (the K(m, d) read lose from 18; the ideal is a law,
and a field near it at even d needs 2, 5, 17 split, every place
over 3 of degree 2 and every other small prime of residue degree
>= 2).
RUN RECORD. `python splitend.py` under a 2048 MB cap: 21 of 21 checks,
37.5 s, peak commit 96.9 MB, after THE IDEAL gained its forced place
of norm 3 at odd d, a check that it raises the margin there, and C5,
the odd ideal against zeta_K and sigma_F2 written out as products (to
2.6e-11 at d = 15, 17, 731, 733); a scratch copy with n3 = 0 fails C5
at all four (-1.2516066631e-03 against +6.3714351247e-04 at 17). Every
other line as at 16 of 16, 96.5 MB. Changed after the freeze: brentq's rtol
4e-16 -> 1e-15 (its floor); C1's size clause, named above; THE IDEAL's
print added after the first run, every other line the same.
"""
import math
import os
import sys
import time
os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
sys.path.insert(0, os.path.join(os.path.dirname(os.path.dirname(
os.path.abspath(__file__))), "code"))
import numpy as np # noqa: E402
from scipy.optimize import brentq # noqa: E402
import splitloss as sl # noqa: E402
CHECKS = []
# the column's odd norms past 3, with a = log2 n; the Fermat numbers
# 2^(2^k) + 1, k = 5..9, counted as prime (a bound); past k = 9 their
# terms total below d 0.382^1024 < 1e-420 in w* and below 3.2 * 0.0448^1022
# in Q, against slacks of 1.6e-7 in h and 1.3e-10 in Q
NORMS = [5, 9, 17, 257, 65537] + [2 ** (2 ** k) + 1 for k in range(5, 10)]
EXPS = [math.log2(n) for n in NORMS]
def check(name, ok, detail=""):
CHECKS.append(bool(ok))
print(f" [{'PASS' if ok else 'FAIL'}] {name}" + (f" ({detail})"
if detail else ""))
def counts(d, n9=True):
"""The worst law's counts N_n, in NORMS' order."""
return [d, d // 2 if n9 else 0] + [d] * (len(NORMS) - 2)
def lf(x):
return -math.log1p(-x)
def l4(x):
return -math.log1p(-x ** 4)
def wlog(x, cnt):
lx = math.log(x)
return sum(c * math.log1p(math.exp(a * lx)) for c, a in zip(cnt, EXPS)
if c)
def root(d, cnt, rho=None):
"""The point's ceiling: the root of d l + w + log(x + rho) = 0."""
def g(x):
r = 0.0 if rho is None else rho(x)
return d * lf(x) + wlog(x, cnt) + math.log(x + r)
return brentq(g, 1e-14, 0.4, xtol=1e-18, rtol=1e-15, maxiter=500)
def h(d, x):
return (d + 1) * lf(x) - d * l4(x) + math.log(x)
def mlog(d, x, cnt):
"""(M): log(1 + margin) at x with the counts' W."""
return lf(x) - d * l4(x) - wlog(x, cnt)
def rho_c(cnt):
"""rho of the ideal field: the W-places and their powers alone,
Z'/W - 1 = prod (1 - n^-2b)^-N - 1."""
def r(x):
lx = math.log(x)
return math.expm1(sum(-c * math.log1p(-math.exp(2 * a * lx))
for c, a in zip(cnt, EXPS) if c))
return r
def ideal(d, n3=None):
"""The ideal field's log(1 + margin): the worst law's places, their
powers (rho_c) and, at odd d, the one place of norm 3 that floor(d/2)
places of norm 9 leave over 3, with its square; S3 enters (E) only."""
cnt = counts(d)
n3 = d % 2 if n3 is None else n3
a3 = math.log2(3)
r0 = rho_c(cnt)
def g(x):
lx = math.log(x)
s3 = n3 * math.log1p(math.exp(a3 * lx))
r = math.expm1(math.log1p(r0(x))
- n3 * math.log1p(-math.exp(2 * a3 * lx)))
return d * lf(x) + wlog(x, cnt) + s3 + math.log(x + r)
x = brentq(g, 1e-14, 0.4, xtol=1e-18, rtol=1e-15, maxiter=500)
return mlog(d, x, cnt)
def worst(d, n9=True):
x = root(d, counts(d, n9))
return h(d, x), x
def q_tail(t, n9=True):
cs = [1.0, 0.5 if n9 else 0.0] + [1.0] * (len(NORMS) - 2)
s = t ** 2 / (1 - t ** 4) + sum(c * t ** (a - 2) for c, a in
zip(cs, EXPS) if c)
return math.log(1 / t) * s
def delta(t):
return math.log(1 / t) / lf(t)
def tail_point(n9=True):
"""The root of Q - 1 below e^(-1/(a5 - 2)), and t* 1e-9 below it."""
top = math.exp(-1 / (EXPS[0] - 2)) * (1 - 1e-12)
if q_tail(top, n9) < 1:
return top, top
r = brentq(lambda t: q_tail(t, n9) - 1, 1e-6, top, xtol=1e-18,
rtol=1e-15)
return r, r * (1 - 1e-9)
# ------------------------------------------------------------ controls
def control_c1():
print("=== C1: the solver on the bare law against splitloss.py's bare")
for d in (12, 60, 676, 677):
cnt = [d] + [0] * (len(NORMS) - 1)
def rb(x, d=d):
return (1 - x ** (2 * EXPS[0])) ** -d - 1
xr = root(d, cnt, rb)
x0 = root(d, cnt)
mr = math.expm1(mlog(d, xr, cnt))
m0 = math.expm1(mlog(d, x0, cnt))
bm = sl.bare(d)[0]
print(f" d={d}: rho restored {mr:+.12f} | splitloss {bm:+.12f} | "
f"rho = 0 {m0:+.12f}")
check(f"C1 d={d}: rho restored = bare(d) to 1e-10; rho = 0 at or "
f"below it", abs(mr - bm) < 1e-10 and bm - m0 >= 0,
f"{abs(mr - bm):.1e}; rho = 0 lower by {bm - m0:.1e}")
def control_c5():
"""THE IDEAL by another road: zeta_K and sigma_F2 written out as
products at odd d (d places of norm 2, the worst law's places, one
of norm 3), the F_2 point solved on zeta_K - sigma_F2 = 1 and the
margin by the sill's ratio; against ideal(d)."""
print("=== C5: ideal(d) at odd d against the products written out")
for d in (15, 17, 731, 733):
cnt = counts(d)
a3 = math.log2(3)
def parts(x):
lx = math.log(x)
lz = (-d * math.log1p(-x) - math.log1p(-math.exp(a3 * lx))
- sum(c * math.log1p(-math.exp(a * lx))
for c, a in zip(cnt, EXPS) if c))
ls = (-(d - 1) * math.log1p(-x) + math.log1p(math.exp(a3 * lx))
+ wlog(x, cnt))
return lz, ls
def g(x):
lz, ls = parts(x)
return math.exp(ls) * math.expm1(lz - ls) - 1
x = brentq(g, 1e-6, 0.4, xtol=1e-18, rtol=1e-15, maxiter=500)
direct = math.log((1 - x ** 4) ** d / (1 - x)) - wlog(x, cnt)
check(f"C5 d={d}: ideal(d) = the products' margin to 1e-10",
abs(ideal(d) - direct) < 1e-10,
f"{ideal(d):+.10e} | {direct:+.10e}")
def control_c2():
print("=== C2: STEP 3's identity M_c(x_c) = h(x_c) at the worst law")
for d in (12, 100, 700):
cnt = counts(d)
x = root(d, cnt)
a, b = mlog(d, x, cnt), h(d, x)
check(f"C2 d={d}: M = h to 1e-12", abs(a - b) < 1e-12,
f"M {a:+.12f}, h {b:+.12f}")
def control_steps():
print("=== STEP 1's load: each W-term's log-derivative on (0, 0.4]")
xs = np.linspace(1e-4, 0.4, 40001)
ok = True
for n, a in zip(NORMS[:5], EXPS[:5]):
ld = (a - 1) / xs - 1 / (1 - xs) - a * xs ** (a - 1) / (1 + xs ** a)
st = np.diff(ld).max()
ok = ok and st < 0 and ld[-1] > 0
print(f" n={n}: at 0.4 {ld[-1]:.4f}, largest step {st:.2e}")
l3 = 3 / xs - 1 / (1 + xs) - 2 * xs / (1 + xs ** 2)
print(f" the x^4 term's: least {l3.min():.4f}")
check("STEP 1: every W-term's log-derivative falls and is positive at "
"0.4; the x^4 term's positive", ok and l3.min() > 0)
x02 = brentq(lambda x: 2 * lf(x) + math.log(x), 1e-6, 0.45)
xs2 = worst(2)[1]
print(f" x0(2) = {x02:.6f}, x*(2) = {xs2:.6f}")
check("STEP 2: x0(2) < 0.4", x02 < 0.4)
# ------------------------------------------------------------ the run
def main():
t0 = time.time()
control_c1()
control_c2()
control_c5()
control_steps()
if not all(CHECKS):
print("a control failed: no verdict")
sys.exit(1)
print(f"controls read ({time.time() - t0:.1f} s)")
print("\n=== THE TAIL")
r, ts = tail_point()
D = math.ceil(delta(ts))
print(f" root {r:.12f}; t* = {ts:.12f}, Q(t*) = {q_tail(ts):.12f}, "
f"delta(t*) = {delta(ts):.4f}, so every d >= {D}")
rp, tp = tail_point(n9=False)
print(f" C4 PLANT, Q without the 9-term: t* = {tp:.9f}, delta "
f"{delta(tp):.4f}")
check("C4 PLANT: the 9-term's removal raises t* and lowers delta",
tp > ts and delta(tp) < delta(ts))
print("\n=== THE WORST LAW, d = 2..D + 200")
H = {d: worst(d) for d in range(2, D + 201)}
for d in list(range(2, 41)) + list(range(50, D + 201, 50)):
print(f" d={d:4d}: h(x*) {H[d][0]:+.9f} at x* {H[d][1]:.9f}")
neg = [d for d in H if H[d][0] <= 0]
dlo, dhi = neg[0], neg[-1]
gaps = [d for d in range(dlo, dhi + 1) if H[d][0] > 0]
lst = min(H, key=lambda d: H[d][0])
print(f" h(x*) <= 0 at {len(neg)} degrees, d_lo = {dlo}, d_hi = {dhi};"
f" gaps {gaps}; least {H[lst][0]:+.9f} at d = {lst}")
print(" h(x*) around d_hi: " + ", ".join(
f"{d}: {H[d][0]:+.2e}" for d in range(dhi - 2, dhi + 4)))
print(f" least h(x*) from d_hi + 1 to D + 200: "
f"{min(H[d][0] for d in range(dhi + 1, D + 201)):+.3e}")
print(" THE IDEAL (added after the run): the worst law with the W-places'"
" powers and, at odd d, its forced place of norm 3, at the ends")
odd_up = []
for d in (dlo - 1, dlo, dlo + 1, dhi - 1, dhi, dhi + 1):
v = ideal(d)
if d % 2:
odd_up.append(v > ideal(d, n3=0))
print(f" d={d}: log(1 + margin) {v:+.4e} "
f"(rho = 0: {H[d][0]:+.4e})")
check("THE IDEAL: at each odd d printed the forced place of norm 3 "
"raises the ideal's margin", odd_up and all(odd_up))
print("\n=== THE CHECK ON FIELDS (splitloss.py's family and C1)")
PR = sl.primes_to(10 ** 7)
fam = sl.family(PR)
fields = [(m, d) for d, ms in fam.items() for m in ms]
fields += [(7, 2), (17, 2)]
for d in (4, 6, 8, 10):
for m in PR[PR < 5000].tolist():
if (m - 1) % d or m == 5:
continue
e = (m - 1) // d
if pow(2, e, m) == 1 and pow(5, e, m) == 1:
fields.append((m, d))
hb = {}
bad, badp, slack = [], [], []
for m, d in fields:
if d not in hb:
hb[d] = (math.expm1(min(0.0, worst(d)[0])),
math.expm1(min(0.0, worst(d, n9=False)[0])))
K = sl.Light(m, d, 10 ** 5, PR)
lo, hi, b = sl.bracket(K)
slack.append((hi - hb[d][0], d, m))
if hi < hb[d][0] - 1e-9:
bad.append((d, m, hi, hb[d][0]))
if hi < hb[d][1] - 1e-9:
badp.append((d, m, hi, hb[d][1]))
slack.sort()
print(f" {len(fields)} fields; least slack {slack[0][0]:+.3e} at "
f"K({slack[0][2]}, {slack[0][1]}); below the bound: {len(bad)}")
print(f" C3 PLANT (N9 = 0): {len(badp)} fields below, first "
f"{badp[:3]}")
check("C3 PLANT: the bound without norm 9 is broken by some field",
bool(badp))
check("(p1) THE BOUND: no field below min(0, h(x*(d)))", not bad,
f"{len(bad)} below")
check("(p2) Q(t*) < 1, t* in 0.005..0.008, delta in 700..900",
q_tail(ts) < 1 and 0.005 <= ts <= 0.008
and 700 <= delta(ts) <= 900)
check("(p3) d_hi in 700..800, >= 676, below delta(t*)",
700 <= dhi <= 800 and dhi < delta(ts), f"{dhi}")
check("(p4) d_lo in 14..18, h(x*) > 0 below it",
14 <= dlo <= 18 and all(H[d][0] > 0 for d in range(2, dlo)),
f"{dlo}")
check("(p5) no gap but at odd d below 30",
all(d % 2 and d < 30 for d in gaps), f"{gaps}")
print(f"\n{sum(CHECKS)} of {len(CHECKS)} checks, "
f"{time.time() - t0:.1f} s")
if __name__ == "__main__":
main()