fweights.py

"""fweights.py -- the loss side over K_ab = F uniform in W_F's weights:
does every F with W_F nonempty carry a field K, K_ab = F, that loses?

QUESTION. Let F be abelian with 2 totally ramified, k >= 2 the largest
with C = Q(zeta_(2^k)) in F, and W_F the norms n > n_c = 2^k + 1 of
places of F with n - 1 a power of 2; B the least, w_B its share (the
places of F of norm B over [F : Q]). Where W_F is empty no field of
type (1, 0) with K_ab = F loses at any degree (abfloor.py, (B)). Where
it is not: does some such K lose at some degree, whatever w_B and the
later norms' weights? towerpast.lemma closes at fixed X only while
c = c1/w_B times the later norms' terms stays small, so at fixed X a
small w_B beside later norms at weight 1 can open it (the corner).

THE DERIVATION (by hand, before this code).
  The shares. A place of norm B lies over a prime p with residue degree
  f0 = 1 (B = p a Fermat prime) or f0 = 2 (B = 9, p = 3, k = 2); F is
  Galois, so w_B = g/[F : Q] = 1/(e f0) <= w_max, w_max = 1/2 at 9 and
  1 at a Fermat prime. B >= 9 (n_c >= 5), and every later norm n of
  W_F is a Fermat number past B: n >= 17 at B = 9, n >= (B - 1)^2 + 1
  at a Fermat B, so log2(n/B) >= q := log2(17/9) = 0.9175 at every B.
  The rule. Fix B's base row, the published K_ab = C row at w_max:
  (B, w_max, X_B, c1/w_max, Y_B) = (9, 1/2, 1/7, 1, 10^5), (17, 1, 1/4,
  1/3, 10^5), (B, 1, 0.381, 1/2, B^10) for a Fermat B >= 257, and at w
  = w_B <= w_max read the lemma at c = c1/w, X = X_B (w/w_max)^(1/q),
  so b = b_B + log2(w_max/w)/q, b_B = log2(1/X_B). Then term by term
  in towerpast.coeffs (later norms read at weight 1, every Fermat
  number past B, prime or not):
    B's own: c w/(1 - X^a) = c1/(1 - X^a) and c w X^(a-1)/(1 - X^(2a))
      fall as X does (a = log2 B > 3);
    a later n: c (B/n)^b = (c1/w)(B/n)^(b_B) (B/n)^(b - b_B), and
      (B/n)^(b - b_B) = (w/w_max)^(log2(n/B)/q) <= w/w_max, so the term
      is at most (c1/w_max)(B/n)^(b_B), its base value; 1/(1 - n^-b)
      falls in b;
    the missed mass of a later n: (2B/n^2)^b, log2(n^2/(2B)) >= q as
      n^2/(2B) > n/2 >= 8.5 (n > B, n >= 17), so the same; past Y: (B/Y)^b
      and (2B/Y)^b, log2(Y/(2B)) >= q, the same, fac(b) = (1 + Y/(b -
      1))/(1 - Y^-b) falling in b.
  So c_z(w) <= c_z(w_max) and c_s(w) <= c_s(w_max); with l(X) falling
  and lam0 = log(1/X) rising, g(w) = l(X) - (1 - c_z - c_s) lam0 + E'
  is at most g(w_max) + E'(w) wherever 1 - c_z - c_s > 0 at the base;
  M(w) = l(X) - c1 lam0 (1 - X^a/2) and M'(w) = 1/(1 - X) - a c1 lam0/(X
  (1 + X^a)) fall as X does. The base rows close (g, M, M' < 0: the K_ab
  = C rows of towerpast.py and fermatlemma.py, B = 257 bounding every
  Fermat B >= 257 at w_max). E' (places off W_F below Y, at most [F : Q]
  per p, norms >= n_c^m') falls in m' = d/[F : Q] to 0, and the lemma
  holds at every d >= d0, so at m' >= m_E it is below |g(w_max)|/2. So
  at every F with W_F nonempty, K of type (1, 0) with K_ab = F loses at
  every d = 0 mod [F : Q] from max(d0(B, w_B), m_E [F : Q], 6 [F : Q]),
  d0 = ceil(c lam0 X^-a), the realization over F as abfloor.py's (m' >=
  6, K_ab = F); with abfloor.py's no-loss half: a field of type (1, 0)
  with K_ab = F loses at some degree iff W_F is nonempty (theorem,
  uniform in the weights). d0 grows as w_B^-(1 + a/q), polynomial in e.
  At fixed X = X_B the later terms scale as w_max/w and the corner is
  real: hand estimates of the base c_z - c1/(1 - X^a) (later share
  ~0.168 at 9, ~0.0015 at 17, ~0.00022 at 257, ~2e-7 at 65537)
  against the base slack put the first failing j, w = w_max 2^-j, at j
  = 2 (B = 9), about 9 (17), 4 (257) and 12 to 16 (65537).

PREDICTIONS (frozen before the engine).
  P1 the rule's rows, B in {9, 17, 257, 65537}, w = w_max 2^-j, j =
     0..40, later norms every Fermat number past B to F_9 at weight 1
     (each past F_9 below c (B/2^1024)^b, bounded in the print), E' =
     0 arm: g, M, M' < 0 at every (B, j); c_z, c_s, g, M, M' each
     non-increasing in j at each B.
  P2 at fixed X = X_B, c = c1/w: g >= 0 first at j = 2 (B = 9), at j in
     8..10 (17), 3..5 (257), 12..16 (65537); the rule's row at that j
     closes.
  P3 E': at [F : Q] = 2^(k + j) (the most places the share allows, k =
     2, 3, 4, 8 at B = 9, 17, 257, 65537), the least m' >= 6 with E'
     <= |g|/2 is printed; it exists at every (B, j) of P1.
  KILL (frozen): some (B, j) of P1 with g, M or M' >= 0 on the E' = 0
  arm, or a c_z or c_s at j above its value at j - 1 (the derivation's
  step), read on the arms a confound would inflate: B = 9, where the
  later ratio 9/17 is largest, and B = 257, the thinnest base slack (g
  -0.0018); or P3 finding no m'. A P2 miss reads the corner estimate,
  not the theorem.

CONTROLS (frozen).
  C1 POSITIVE: the base rows at j = 0 reproduce the published prints:
     (9, 1/2, 1/7, 1, 10^5) g, M, M' = -0.475044, -0.817785, -20.3776
     (later norms 17, 257, 65537; adding F_5..F_9 moves no printed
     place); (17, 1, 1/4, 1/3, 10^5) g -0.6198, M -0.1736, M' -6.195;
     (257, 1, 0.381, 1/2, 257^10) g -0.001836, M -0.002721, M' -8.517.
  C2 POSITIVE for the fixed-X arm: at B = 9, j = 2, X = 1/7 the lemma
     fails (g >= 0), the corner the rule must close.
  C3 the monotonicity reader catches a planted break: c_z with the term
     at 17 read at b_B, unshrunk, times c = c1/w rises in j at B = 9, and
     the reader flags it.

FINDINGS (entered after the run, from its printed output).
  CONTROLS. C1: (9, 1/2, 1/7, 1, 1e5) g -0.475044, M -0.817785, M'
  -20.3776, the same g with F_5..F_9; (17, ...) g -0.619814, M -0.173617,
  M' -6.1958; (257, ...) g -0.001837, M -0.002721, M' -8.5179, each the
  published figure cut toward 0. C2: B = 9, j = 2, X = 1/7 fixed, g
  +0.507315. C3: the planted c_z reads 0.6689, 0.8357, 1.1711 at j = 0,
  1, 2, flagged.
  P1 HOLDS: at B = 9, 17, 257, 65537 and every j = 0..40 the rule's row
  closes, c_z, c_s, g, M, M' each non-increasing in j; the largest g is
  the base row's (-0.475044, -0.619814, -0.001837, -0.002828), and at j
  = 40 g is -10.687, -21.069, -15.591, -15.591; d0 at j = 40 is 6.7e57,
  1.5e69, 4.5e121, 8.2e229; each Fermat number past F_9 adds below
  10^-422. At B = 9 the term at 17 is held at its base value exactly (q
  is log2(17/9)), so c_z reads 0.667722 from j = 5 on.
  P2 MISSED at B = 17: the fixed-X lemma fails first at j = 2 (B = 9), 7
  (17, predicted 8..10), 4 (257), 15 (65537); the rule closes at each
  (g -1.116, -4.448, -1.975, -6.148). The hand estimate dropped the
  tails past Y = 10^5: at B = 17, j = 7, X = 1/4 the parts print c_z own
  0.3345, later 0.1867, past Y 0.1233, and c_s own 0.0046, past Y
  0.4932.
  P3 HOLDS: m' = 6 already puts E' below |g|/2 at every (B, j), at the
  one [F : Q] = 2^(k + j) read per (B, j). The share does not bound [F :
  Q] (w_B = 1/(e f0), g free), and E' grows linearly in it, so m_E
  depends on F, as the theorem's max(d0, m_E [F : Q], 6 [F : Q]) has
  it; the frozen "the most places the share allows" was false.
  KILL MISSED: the rule closes the lemma at every weight read, and the
  derivation's monotone step holds at every print; so a field of type
  (1, 0) with K_ab = F loses at some degree iff W_F is nonempty, at
  every F (theorem, uniform in the weights; the rows only re-read the
  base rows' sufficiency).

RUN RECORD. `python fweights.py` under a 2048 MB cap: 5 of 6 checks
(P2's band the one miss, above), 0.0 s, peak commit 56.9 MB. Then P2's
band became a print beside its check, which now reads that the fixed-X
lemma fails at some j at every B and the rule closes at the first (the
band missed a frozen estimate, not the kill): 6 of 6 checks, 0.5 s,
57.0 MB bare. The
engine was appended in one write after the frozen docstring. Changed
from the frozen text, named: C1 compares each published figure as the
value cut toward 0 at its places (helper held), not as its rounding:
the first run failed C1 on -6.1958 against -6.195 and on g at 257
(fermatlemma.py's -0.001836571) against -0.001836, both written as
bounds;
the Fermat numbers enter as integers (F_9 squared overflows a float).
At review, P2 prints its first failing row's parts (parts()), the
figures above, and the derivation's missed-mass step reads n^2/(2B) >
n/2 for an undefined n2.
"""

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 towerpast as tp  # noqa: E402

CHECKS = []
Q = math.log2(17 / 9)
JMAX = 40
FERMAT = [2 ** (2 ** m) + 1 for m in range(1, 10)]   # F_1 .. F_9
# B: (w_max, X_B, c1, Y_B, k, n_c)
BASE = {9: (0.5, 1 / 7, 0.5, 1e5, 2, 5),
        17: (1.0, 0.25, 1 / 3, 1e5, 3, 9),
        257: (1.0, 0.381, 0.5, 257.0 ** 10, 4, 17),
        65537: (1.0, 0.381, 0.5, 65537.0 ** 10, 8, 257)}


def check(name, ok, detail=""):
    CHECKS.append(bool(ok))
    print(f"  [{'PASS' if ok else 'FAIL'}] {name}" + (f"  ({detail})"
                                                       if detail else ""))
    return ok


def guard():
    if not all(CHECKS):
        print("a control failed: no verdict")
        sys.exit(1)


def later(B):
    return tuple(n for n in FERMAT if n > B)


def row(B, j, fixed=False, norms=None):
    """The lemma at w = w_max 2^-j, c = c1/w; X by the rule, or X_B."""
    wmax, XB, c1, Y, k, nc = BASE[B]
    w = wmax * 2.0 ** -j
    X = XB if fixed else XB * (w / wmax) ** (1 / Q)
    ns = later(B) if norms is None else norms
    L = tp.lemma(X, c1 / w, w, math.log2(B), B, ns, Y, 0.0)
    L.update(X=X, w=w, c=c1 / w, b=-math.log2(X))
    return L


def parts(B, j):
    """towerpast.coeffs' terms at fixed X = X_B, c = c1/w, w = w_max 2^-j:
    c_z's own, later and past-Y parts, c_s's own, later and past-Y."""
    wmax, X, c1, Y, k, nc = BASE[B]
    w = wmax * 2.0 ** -j
    c, b = c1 / w, -math.log2(X)
    y = B ** -b
    fac = (1 + Y / (b - 1)) / (1 - Y ** -b)
    zo = c * w / (1 - y)
    zl = c * sum((B / n) ** b / (1 - n ** -b) for n in later(B))
    zt = c * (B / Y) ** b * fac
    so = c * w * X ** (math.log2(B) - 1) / (1 - y * y)
    sl = c * sum((2 * B / n ** 2) ** b / (1 - n ** (-2 * b))
                 for n in later(B))
    st = c * (2 * B / Y) ** b * fac
    return (f"c_z own {zo:.4f}, later {zl:.4f}, past Y {zt:.4f}; c_s own "
            f"{so:.4f}, later {sl:.4f}, past Y {st:.4f}")


def tail_past_f9(B, L):
    """Each Fermat number past F_9 adds at most c (B/2^1024)^b to c_z, the
    next ones far less: log10 of c (B/2^1024)^b."""
    return math.log10(L["c"]) + L["b"] * (math.log10(B) - 1024 *
                                          math.log10(2))


def log10_e_off(DF, nc, m, X):
    """log10 of abfloor.e_off at m' = m: (1 + 1/X) DF nc^-s (1 + nc/(s -
    1))/(1 - nc^-s), s = m b."""
    s = m * -math.log2(X)
    return (math.log10(1 + 1 / X) + math.log10(DF) - s * math.log10(nc)
            + math.log10(1 + nc / (s - 1)) - math.log10(1 - nc ** -s))


def monotone(seq, tol=1e-12):
    return all(b <= a + tol * max(1.0, abs(a)) for a, b in zip(seq, seq[1:]))


def held(x, pub):
    """The published figure is x cut toward 0 at its places (a bound kept
    in its direction): x <= pub < x + 10^-places."""
    places = len(pub.split(".")[1])
    return x <= float(pub) < x + 10.0 ** -places


def controls():
    print("=== CONTROLS")
    L9 = tp.lemma(1 / 7, 1.0, 0.5, math.log2(9), 9, (17, 257, 65537),
                  1e5, 0.0)
    L9f = row(9, 0)
    print(f"  C1 (9, 1/2, 1/7, 1, 1e5): g {L9['G']:.6f}, M {L9['M']:.6f}, "
          f"M' {L9['Mp']:.4f}; with F_5..F_9: g {L9f['G']:.6f}")
    ok1 = (f"{L9['G']:.6f} {L9['M']:.6f} {L9['Mp']:.4f}"
           == "-0.475044 -0.817785 -20.3776"
           and f"{L9f['G']:.6f}" == f"{L9['G']:.6f}")
    L17 = row(17, 0)
    print(f"  C1 (17, 1, 1/4, 1/3, 1e5): g {L17['G']:.6f}, M {L17['M']:.6f},"
          f" M' {L17['Mp']:.4f}")
    ok1 &= all(held(L17[key], pub) for key, pub in
               (("G", "-0.6198"), ("M", "-0.1736"), ("Mp", "-6.195")))
    L257 = row(257, 0)
    print(f"  C1 (257, 1, 0.381, 1/2, 257^10): g {L257['G']:.6f}, M "
          f"{L257['M']:.6f}, M' {L257['Mp']:.4f}")
    ok1 &= all(held(L257[key], pub) for key, pub in
               (("G", "-0.001836"), ("M", "-0.002721"), ("Mp", "-8.517")))
    check("C1 POSITIVE: the base rows reproduce the published prints", ok1)
    L = row(9, 2, fixed=True)
    print(f"  C2 B = 9, j = 2, X = 1/7 fixed: g {L['G']:.6f}")
    check("C2 POSITIVE: the fixed-X lemma fails at B = 9, j = 2", L["G"] >= 0)
    wmax, XB, c1, Y, k, nc = BASE[9]
    bB = -math.log2(XB)
    plant = []
    for j in range(JMAX + 1):
        L = row(9, j, norms=later(9)[1:])
        plant.append(L["cz"] + L["c"] * (9 / 17) ** bB / (1 - 17 ** -bB))
    check("C3 the monotonicity reader flags the planted unshrunk term at 17",
          not monotone(plant), f"c_z plant j = 0, 1, 2: {plant[0]:.4f}, "
          f"{plant[1]:.4f}, {plant[2]:.4f}")
    guard()


def part_p1():
    print("\n=== P1 the rule's rows, w = w_max 2^-j, j = 0..40, E' = 0")
    ok = True
    out = {}
    for B in BASE:
        rows = [row(B, j) for j in range(JMAX + 1)]
        out[B] = rows
        closes = all(L["G"] < 0 and L["M"] < 0 and L["Mp"] < 0 for L in rows)
        mono = {key: monotone([L[key] for L in rows])
                for key in ("cz", "cs", "G", "M", "Mp")}
        worst = max(rows, key=lambda L: L["G"])
        tails = max(tail_past_f9(B, L) for L in rows)
        for j in (0, 1, 2, 5, 10, 20, 40):
            L = rows[j]
            print(f"  B {B}, j {j:2d}: X {L['X']:.4g}, c {L['c']:.4g}, d0 "
                  f"{L['d0']:.4g}, c_z {L['cz']:.6f}, c_s {L['cs']:.6f}, g "
                  f"{L['G']:.6f}, M {L['M']:.6f}, M' {L['Mp']:.4g}")
        print(f"  B {B}: closes at every j {closes}; non-increasing "
              f"{mono}; largest g {worst['G']:.6f}; log10 tail past F_9 <= "
              f"{tails:.1f}")
        ok &= closes and all(mono.values()) and tails < -100
    check("P1 the rule closes at every (B, j), each of c_z, c_s, g, M, M' "
          "non-increasing in j", ok)
    return out, ok


def part_p2():
    print("\n=== P2 the corner at fixed X = X_B")
    want = {9: (2, 2), 17: (8, 10), 257: (3, 5), 65537: (12, 16)}
    ok = True
    for B in BASE:
        first = next((j for j in range(JMAX + 1)
                      if row(B, j, fixed=True)["G"] >= 0), None)
        r = row(B, first) if first is not None else None
        lo, hi = want[B]
        hit = first is not None and lo <= first <= hi
        rc = r is not None and r["G"] < 0 and r["M"] < 0 and r["Mp"] < 0
        print(f"  B {B}: fixed X fails first at j = {first} (predicted "
              f"{lo}..{hi}, {'in' if hit else 'OUT OF'} band); the rule's "
              f"row there g {r['G'] if r else float('nan'):.6f}")
        if first is not None:
            print("    its parts: " + parts(B, first))
        ok &= rc
    check("P2 the fixed-X lemma fails at some j at every B; the rule closes "
          "at the first", ok)


def part_p3(out):
    print("\n=== P3 E': the least m' >= 6 with E' <= |g|/2, [F : Q] = "
          "2^(k + j)")
    ok = True
    for B in BASE:
        wmax, XB, c1, Y, k, nc = BASE[B]
        ms = []
        for j, L in enumerate(out[B]):
            target = math.log10(abs(L["G"]) / 2)
            m = 6
            while log10_e_off(2.0 ** (k + j), nc, m, L["X"]) > target:
                m += 1
                if m > 10 ** 6:
                    m = None
                    break
            ms.append(m)
        print(f"  B {B} (n_c {nc}): m' at j = 0, 10, 20, 40: {ms[0]}, "
              f"{ms[10]}, {ms[20]}, {ms[40]}; largest {max(ms)}")
        ok &= all(m is not None for m in ms)
    check("P3 an m' exists at every (B, j)", ok)
    return ok


def main():
    t0 = time.time()
    controls()
    out, k1 = part_p1()
    part_p2()
    k3 = part_p3(out)
    n = sum(CHECKS)
    print(f"\n{n} of {len(CHECKS)} checks, {time.time() - t0:.1f} s")
    print("KILL MISSED: the rule closes the lemma at every weight read"
          if k1 and k3 else "KILL FIRED")
    return 0 if n == len(CHECKS) else 1


if __name__ == "__main__":
    sys.exit(main())