typeloss.py
Checks: THERMAL: The losses by 2's splitting type theorem; rule; observation.
Cited on: THERMAL.
To run it: save typeloss.py, with fieldtop.py, growth.py, memory.py, spectrum.py, splitend.py, splitloss.py, splitsharp.py beside it; needs mpmath, numpy, scipy.
"""typeloss.py -- at which degrees can the F_2 place lose to infinitely
many columns where 2 does not split completely, and what does 2's
splitting type allow?
QUESTION. Where 2 splits completely a loss to infinitely many columns
of norm above 3 exists at exactly d = 16..732 (splitend.py,
splitsharp.py). With t places of residue degree 1 over 2, u of them
unramified, the rest of residue degree >= 2, at which d does some field
lose so? The cubic losses (cubrace.py) are to the column of norm 3,
which the sill does not govern.
THE DERIVATION, beyond the bound (t l + log S3 + w + log(x + rho') = 0
at the point, M = l - u l4 - (t - u) l3 - w, h_{t,u} at the worst law's
x*_{t,d}, the bound min(0, h) monotone in u and d, no tail at fixed t).
STEP 1 at t = 1. The point can pass 0.4 (x0(1) = 1/2). D(x, log2 5),
the 5-term's log-derivative, has its root CEIL (printed 0.487937);
past it w = log((1 - x)/x) is below one place of norm 5, so n5 = 0, and the
9-term rises on (0, 1/2]. So M is quasi-concave on [0, x_c] at every
type.
THE CERTIFICATE. A law fixes the algebras below Y = 10^5; x_low is the
root of g_up = t l + log Z2' + lz + lt + log(1 - (1 - x) e^(-lr - lt
- log Z2')), lz the log zeta of the odd places below Y, lr its excess
over log S3 + w, lt splitsharp's tail past Y; where M'(x_low) < 0 and
x_c < CEIL, M(x_low) bounds log(1 + margin) above at every field with
those algebras. At type (1, 0) A_2 = Q_2(2^(1/d)); 5, 17, 257, 65537
split; 3 as splitsharp's law; every other p < Y of residue degree d;
q1, q2, q3 >= Y give S_d, and q4 >= Y with Q_q4(sqrt q4) x
Q_q4^(d - 2) puts q4 in the discriminant, so chi_D(a) = 1 is met by
a's residue mod q4 and the sill's hypothesis holds.
THE LEMMA (type (1, 0), d >= 867). x1 the root of d x^a5 = (1/2)
log(1/x), so x1 <= 1/16; at x1, with lam = log(1/x): lz <= c lam, lr/x
<= c' lam plus absolute terms from the place of norm 27; then g_up(x1)
<= 1/15 + (c + c' - 1) lam < 0, M(x1) <= 1/15 - (lam/2)(1 - 1/1250),
M'(x1) <= 16/15 - a5 lam/(2 x1 (1 + 1/625)), each falling with x1.
THE MAP. The extremal law of type (t, u): t > u puts the spare degree
into the ramified places' e (Z2' = 1, valid at d - u >= 2(t - u)); t
= u < d one unramified place of degree d - t >= 2 (Z2' = 1/(1 -
x^(d-t))).
DESIGN.
BOUND. x*_{t,d} by brentq on t l + w*_d + log x over (1e-14, 0.5);
D(t, u) by scanning d upward to 2000, the bound checked monotone.
THE SWEEP: type (1, 0), d = 3..1416, at odd d the lesser of kinds A
and B. THE LEMMA: its constants and its three inequalities at x =
1/16 printed. THE MAP: t = 1..12, u = 0..t, d <= 60, D(t, u), the
least losing d and the gaps (valid d past D(t, u) where the
certificate is not negative).
CONTROLS.
C1 at t = u = d the bound equals splitend.worst(d) to 1e-12 at d = 15,
16, 732, 733.
C2 at t = u = d, TypeLaw gives splitsharp.law's certificate to 1e-12
at (16, E), (17, B), (732, E).
C3 (known answer) at d = 3 every certificate is >= 0, at type (1, 0)
and at the (1, 1), (2, 1), (3, 3) laws: no cubic loses to a column
of norm above 3 (cubtop.py).
C4 fieldtop.py's 18 margins at 2 totally ramified sit at or above
the bound min(0, h_{1,0}(x*_{1,d})).
C5 PLANT: the d = 4 law with 5, 17, 257, 65537 inert prints C >= 0
(the certificate can say "no loss").
C6 STEP 1's repair: D(x, log2 5) below CEIL >= 0, w(CEIL) below one
place of norm 5, D(0.5, log2 9) > 0.
C7 no certificate is negative where the bound is positive (the map).
C8 every negative certificate of the map has M' < 0 and x_c < CEIL,
so it is a certificate.
FINDINGS.
CONTROLS. C1: differences 0, 8.9e-16, 8.9e-16, 2.7e-15 at 15, 16,
732, 733. C2: 8.3e-17, 5.6e-17, 1.0e-17. C3: +0.0692, +0.0755 at
(1, 0) kinds A and B, +0.098 to +0.138 elsewhere, the bound at
(1, 0, 3) -0.003757. C4: least slack +0.102. C5: +0.3333. C6: D(x,
log2 5) +0.08640, -0.00069, -0.02235, -0.13012 at 0.48, 0.488, 0.49,
0.5; CEIL 0.487937, w there 0.04826 against 0.17309; D(0.5, log2 9)
+1.7059.
THE BOUND: h at (1, 0, 2) +0.105175, (1, 0, 3) -0.003757, (1, 0, 4)
-0.122274, (1, 0, 8) -0.389201, (1, 1, 3) +0.034461, (1, 1, 4)
-0.089217, (2, 1, 3) +0.066042, (2, 2, 4) -0.001596; D(1, 0) = 2,
D(1, 1) = 3.
THE SWEEP: negative, M' < 0 and x_c < CEIL at every d = 4..1416; the
largest C -0.07561 at d = 4, then -0.1151 at 5, -0.3322 at 8, -1.694
at 200, -2.328 at 866 and 867, -2.538 at 1416; the largest x_c
0.369980.
THE LEMMA: 866.4340; lz/lam <= 0.50080 + 0.02382 + 0.00374 + 7.2e-08
+ 1.0e-13 = 0.52836, absolute 1.9e-06; lr/(x lam) <= 0.01286, lt/(x
lam) <= 1.7e-12, absolute 3.0e-05; at x = 1/16 g_up <= -1.20531, M <=
-1.31852, M' <= -50.3531. The inert term underflows to 0.0e+00 in
float (2(7^-3468 + 11^-3468 + 13^-3468)).
THE MAP: no certificate negative where the bound is positive, each
negative one with M' < 0 and x_c < CEIL (C8); every
valid d past D(t, u) negative but the first valid one at ten (t, u):
(1, 0) at 3, (2, 2) at 4, (3, 2) at 5, (3, 3) at 5, (4, 4) at 6, (5,
5) at 7, (6, 6) at 8, (7, 7) at 9, (8, 7) at 9, (9, 9) at 11 (D = 9,
d = 10 not valid). D(t, u) runs 2 at (1, 0) to 12 at (12, 10..12).
RUN RECORD. `python typeloss.py` under a 2048 MB cap: 24 of 24 checks,
25.2 s, peak commit 59.4 MB. The certificate's bracket top is 1/2(1
- 1e-9) and w is read without the tail term (both divide by b - 1 = 0
at x = 1/2, which no point reaches); a scratch copy with CEIL = 0.488
fails C6. The map's check was frozen as "at most one gap per (t, u), at
D + 1"; it failed at (9, 9), where D + 1 = 10 is no valid degree, and
was restated as the found law, the gap at the first valid degree past
D(t, u). C8 was added after a review read the map's C alone.
"""
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 splitend as se # noqa: E402
import splitsharp as ss # noqa: E402
CHECKS = []
Y = ss.Y
A5 = math.log2(5)
LN16 = math.log(16)
TOP = 0.5
def check(name, ok, detail=""):
CHECKS.append(bool(ok))
print(f" [{'PASS' if ok else 'FAIL'}] {name}" + (f" ({detail})"
if detail else ""))
lf, l4 = se.lf, se.l4
def l3(x):
return -math.log1p(-x ** 3)
def h(t, u, x):
return (t + 1) * lf(x) - u * l4(x) - (t - u) * l3(x) + math.log(x)
def xstar(t, d, n9=True):
cnt = se.counts(d, n9)
return brentq(lambda x: t * lf(x) + se.wlog(x, cnt) + math.log(x),
1e-14, TOP, xtol=1e-18, rtol=1e-15, maxiter=500)
def bound(t, u, d):
return h(t, u, xstar(t, d))
def valid(t, u, d):
if t > u:
return d - u >= 2 * (t - u)
return d == t or d - t >= 2
class TypeLaw:
"""A law of type (t, u, f2) at 2 beside a splitsharp.Law of odd
places: f2 the residue degrees >= 2 of the places over 2 (Z2')."""
def __init__(self, t, u, f2, base):
self.t, self.u, self.f2, self.base = t, u, list(f2), base
def z2(self, x):
return sum(-math.log1p(-x ** f) for f in self.f2)
def w(self, x):
"""w of the law's places below Y (no tail term)."""
B = self.base
ww = B.k == 1
u = np.exp(math.log(x) * B.a[ww])
return float((B.c[ww] * np.log1p(u)).sum())
def g_up(self, x, use_t=True):
lz, sw, w, lt = self.base.parts(x)
lt = lt if use_t else 0.0
z2 = self.z2(x)
lr = lz - sw
return (self.t * lf(x) + z2 + lz + lt
+ math.log1p(-(1 - x) * math.exp(-lr - lt - z2)))
def m(self, x):
return (lf(x) - self.u * l4(x) - (self.t - self.u) * l3(x)
- self.w(x))
def dm(self, x):
B = self.base
ww = B.k == 1
aa = B.a[ww]
dw = float((B.c[ww] * aa * x ** (aa - 1) / (1 + x ** aa)).sum())
return (1 / (1 - x) - 4 * self.u * x ** 3 / (1 - x ** 4)
- 3 * (self.t - self.u) * x ** 2 / (1 - x ** 3) - dw)
def xc(self):
return brentq(lambda x: self.t * lf(x) + self.w(x) + math.log(x),
1e-14, TOP, xtol=1e-18, rtol=1e-15, maxiter=500)
def cert(self, use_t=True):
"""(C, M'(x_low), x_low, x_c)."""
x = brentq(lambda s: self.g_up(s, use_t), 1e-9, TOP * (1 - 1e-9),
xtol=1e-18,
rtol=1e-15, maxiter=500)
return self.m(x), self.dm(x), x, self.xc()
def extremal(t, u, d, kind):
f2 = [] if (t > u or d == t) else [d - t]
return TypeLaw(t, u, f2, ss.law(d, kind))
def kinds(d):
return ("E",) if d % 2 == 0 else ("A", "B")
def best_cert(t, u, d):
"""The lesser certificate over the kinds of law at d, with its kind."""
out = None
for k in kinds(d):
C, dm, x, xc = extremal(t, u, d, k).cert()
if out is None or C < out[0]:
out = (C, dm, x, xc, k)
return out
# ------------------------------------------------------------ controls
def control_c1():
print("=== C1: the bound at t = u = d against splitend.worst(d)")
for d in (15, 16, 732, 733):
a, ref = bound(d, d, d), se.worst(d)[0]
check(f"C1 d={d}", abs(a - ref) < 1e-12,
f"{a:+.12e} | {ref:+.12e}, diff {abs(a - ref):.1e}")
def control_c2():
print("=== C2: TypeLaw at t = u = d against splitsharp.law(d, kind)")
for d, k in ((16, "E"), (17, "B"), (732, "E")):
C = TypeLaw(d, d, [], ss.law(d, k)).cert()[0]
ref = ss.law(d, k).cert()[0]
check(f"C2 ({d}, {k})", abs(C - ref) < 1e-12,
f"{C:+.12e} | {ref:+.12e}, diff {abs(C - ref):.1e}")
def control_c3():
print("=== C3: d = 3, no cubic loses to a column of norm above 3")
for t, u in ((1, 0), (1, 1), (2, 1), (3, 3)):
for k in kinds(3):
C, dm, x, xc = extremal(t, u, 3, k).cert()
check(f"C3 ({t}, {u}) kind {k}: C >= 0", C >= 0,
f"C {C:+.6e}, x_low {x:.6f}, bound {bound(t, u, 3):+.6f}")
FT = {8: [-0.18202, -0.14242, -0.17642, -0.18937, -0.16030, -0.18828],
4: [0.05723, -0.02005, 0.06318, 0.12171, 0.07513, 0.04604,
0.07932, 0.11173, 0.09431, 0.08627, 0.06588, -0.01989]}
def control_c4():
print("=== C4: fieldtop.py's 18 fields, 2 totally ramified")
least = None
for d, ms in FT.items():
bd = min(0.0, bound(1, 0, d))
for mg in ms:
s = math.log1p(mg) - bd
least = s if least is None or s < least else least
print(f" d = {d}: bound {bd:+.6f}, least log(1 + margin) "
f"{math.log1p(min(ms)):+.6f}")
check("C4: every field at or above the bound", least >= 0,
f"least slack {least:+.6f}")
def control_c5():
print("=== C5 PLANT: the (1, 0) law at d = 4, 5, 17, 257, 65537 inert")
base = ss.law(4, "E")
fer = [math.log2(n) for n in (5, 17, 257, 65537)]
keep = [(a, c, k) for a, c, k in zip(base.a, base.c, base.k)
if not any(abs(a - f) < 1e-12 for f in fer)]
pl = [(4 * f, 1, 0) for f in fer]
L = TypeLaw(1, 0, [], ss.Law(4, keep + pl))
C, dm, x, xc = L.cert()
check("C5 PLANT: C >= 0", C >= 0, f"C {C:+.6e} at x_low {x:.6f}")
def dlog(x, a):
"""The W-term's log-derivative D(x, a) of STEP 1."""
return (a - 1) / x - 1 / (1 - x) - a * x ** (a - 1) / (1 + x ** a)
# STEP 1's ceiling at t = 1: the root of D(x, log2 5), below which the
# 5-term increases; above it the repair forces n5 = 0
CEIL = brentq(lambda x: dlog(x, A5), 0.4, 0.5, xtol=1e-15)
def control_c6():
print("=== C6: STEP 1's repair at t = 1")
for x in (0.48, 0.488, 0.49, 0.5):
print(f" D({x}, log2 5) = {dlog(x, A5):+.5f}")
wc = math.log((1 - CEIL) / CEIL)
one5 = math.log1p(5 ** math.log2(CEIL))
d9 = dlog(0.5, math.log2(9))
below = dlog(CEIL * (1 - 1e-9), A5)
print(f" ceiling (the root) {CEIL:.6f}; w there {wc:.5f}; one place of "
f"norm 5 there {one5:.5f}; D(0.5, log2 9) = {d9:+.4f}")
check("C6: the 5-term rising below the ceiling, w(ceiling) < one "
"5-place, the 9-term rising at 0.5",
below >= 0 and wc < one5 and d9 > 0, f"D below {below:+.2e}")
# ------------------------------------------------------------ the run
def dmax(t, u, cap=2000):
"""The largest d with a positive bound (monotone in d), from t."""
last, seen_neg = t - 1, False
for d in range(max(t, 2), cap + 1):
pos = bound(t, u, d) > 0
if pos and seen_neg:
raise AssertionError(f"bound not monotone at ({t}, {u}, {d})")
if pos:
last = d
else:
seen_neg = True
if d > last + 5:
break
return last
def bound_points():
print("\n=== THE BOUND at hand points")
for t, u, d in ((1, 0, 2), (1, 0, 3), (1, 0, 4), (1, 0, 8), (1, 1, 3),
(1, 1, 4), (2, 1, 3), (2, 2, 4)):
print(f" ({t}, {u}, {d}): x* {xstar(t, d):.6f}, h "
f"{bound(t, u, d):+.6f}")
D10, D11 = dmax(1, 0), dmax(1, 1)
h4, h8 = bound(1, 0, 4), bound(1, 0, 8)
check("the bound: D(1,0) = 2, D(1,1) = 3, h(1,0,4) in -0.15..-0.09, "
"h(1,0,8) in -0.45..-0.33",
D10 == 2 and D11 == 3 and -0.15 <= h4 <= -0.09
and -0.45 <= h8 <= -0.33,
f"D {D10}, {D11}; h {h4:+.5f}, {h8:+.5f}")
def sweep(lo=3, hi=1416):
print(f"\n=== THE SWEEP: type (1, 0), d = {lo}..{hi}")
t0 = time.time()
bad, worst_c, worst_xc, rows = [], None, 0.0, []
for d in range(lo, hi + 1):
C, dm, x, xc, k = best_cert(1, 0, d)
rows.append((d, C, dm, x, xc, k))
if d >= 4:
if not (C < 0 and dm < 0 and xc < CEIL):
bad.append(d)
if worst_c is None or C > worst_c[1]:
worst_c = (d, C)
worst_xc = max(worst_xc, xc)
for d, C, dm, x, xc, k in rows:
if d <= 12 or d % 200 == 0 or d in (866, 867, hi):
print(f" d={d:4d} {k}: C {C:+.6e}, M' {dm:+.4f}, x_low "
f"{x:.6f}, x_c {xc:.6f}")
print(f" the largest C at d >= 4: {worst_c[1]:+.6e} at d = "
f"{worst_c[0]}; the largest x_c {worst_xc:.6f}; "
f"{time.time() - t0:.1f} s")
check(f"the sweep: C < 0, M' < 0, x_c < CEIL at every d = 4..{hi}",
not bad, f"failing d: {bad[:10]}")
def lemma():
print("\n=== THE LEMMA: type (1, 0), every d >= 867")
phi = LN16 * 625 / 2
print(f" d x^a5 = log(1/x)/2 at x = 1/16 gives d = {phi:.4f}")
def q(n):
return (5 / n) ** 4 / (1 - n ** -4.0)
def r(n, c):
return c * (10 / n ** 2) ** 4 / (1 - n ** -8.0)
c5 = 0.5 / (1 - 5 ** -4.0)
c9 = 0.25 * q(9)
c17 = 0.5 * q(17)
crest = 0.5 * (q(257) + q(65537) + 2 * q(2 ** 32 + 1))
clt = 0.5 * ((5 / Y) ** 4 + Y * (5 / Y) ** 4 / 3) / (1 - Y ** -4.0)
a27 = -math.log1p(-27 ** -4.0)
inert = 2 * sum(p ** (-867 * 4.0) for p in (7, 11, 13))
clr = r(5, 0.5) + r(9, 0.25) + r(17, 0.5) + 1.5 * r(257, 1)
cltx = 0.5 * ((10 / Y) ** 4 + Y * (10 / Y) ** 4 / 3) / (1 - Y ** -4.0)
a27x = (2 / 27) ** 4 / (1 - 27 ** -4.0)
clz = c5 + c9 + c17 + crest + clt
print(f" lz/lam <= {c5:.5f} + {c9:.5f} + {c17:.5f} + {crest:.2e} + "
f"{clt:.2e} = {clz:.5f}; absolute {a27:.2e} (27) + {inert:.1e} "
f"(inert)")
print(f" lr/(x lam) <= {clr:.5f}; lt/(x lam) <= {cltx:.2e}; "
f"absolute {a27x:.2e} (27)")
G = (1 / 15 + clz * LN16 + a27 + inert - LN16 + clr * LN16
+ cltx * LN16 + a27x)
Mb = 1 / 15 - (LN16 / 2) * (1 - 1 / 1250)
Mp = 16 / 15 - A5 * 16 * LN16 / (2 * (1 + 1 / 625))
print(f" at x = 1/16: g_up <= {G:+.5f}; M <= {Mb:+.5f}; M' <= "
f"{Mp:+.4f} (each falls as x does)")
check("the lemma: g_up < -1, M < -1, M' < -40, 867 > phi",
G < -1 and Mb < -1 and Mp < -40 and 867 > phi)
def tmap(T=12, dcap=60):
print(f"\n=== THE MAP: t = 1..{T}, u = 0..t, d <= {dcap}")
t0 = time.time()
many_gaps, contra, bare = [], [], []
for t in range(1, T + 1):
for u in range(0, t + 1):
D = dmax(t, u)
least, gaps = None, []
for d in range(max(t, 2), dcap + 1):
if not valid(t, u, d):
continue
C, dm, _, xc, _ = best_cert(t, u, d)
if C < 0 and not (dm < 0 and xc < CEIL):
bare.append((t, u, d))
if d <= D:
if C < 0:
contra.append((t, u, d))
continue
if C < 0:
least = d if least is None else least
else:
gaps.append(d)
first = next(e for e in range(D + 1, dcap + 2)
if valid(t, u, e))
if len(gaps) > 1 or (gaps and gaps[0] != first):
many_gaps.append((t, u, gaps))
print(f" ({t:2d}, {u:2d}): D {D:3d}, least losing d "
f"{least}, gaps {gaps}")
print(f" {time.time() - t0:.1f} s")
check("C7: no certificate negative where the bound is positive",
not contra, f"{contra[:5]}")
check("C8: every negative certificate of the map has M' < 0 and "
"x_c < CEIL", not bare, f"{bare[:5]}")
check("the map: at most one gap per (t, u), at the first valid "
"degree past D(t, u)", not many_gaps,
f"{many_gaps[:5]}")
def main():
t0 = time.time()
control_c1()
control_c2()
control_c3()
control_c4()
control_c5()
control_c6()
bound_points()
sweep()
lemma()
tmap()
print(f"\n{sum(CHECKS)} of {len(CHECKS)} checks, "
f"{time.time() - t0:.1f} s")
return 0 if all(CHECKS) else 1
if __name__ == "__main__":
sys.exit(main())