widestep.py

"""
widestep.py -- the class step's one-c integer test past the 136: does
c_inf stay c_ov or c_ov - 1, read by one low-side test in integers, at
every purely periodic alpha of period at most 3, quotients at most 6,
and m up to 12?

QUESTION. slackbar.py reads, at decide.py's 136 (period at most 4 on
the 48, at most 2 with quotients at most 5 on the 88, m = 2 .. 9),
c_inf = c_ov - 1 if c_ov - 1 has pinned moves and every zero-reply
piece there has an end with G_E + h- < G_lo (G_lo = -(a_(t+1) + 1), +
m U_c on the reduced flag: the G of the hull's lower end), else c_ov;
classform.py reads c_inf as the least c with pinned moves at which
every piece passes both sides with no closed end in the hull (c_form).
(Q) On W, every primitive period of length 1, 2 or 3 over the
quotients 1 .. 6 up to rotation (6 + 15 + 70 = 91 alphas) at m = 2 ..
12 (1001 cells), do c_crude (slackbar's CRUDE bar) and c_form equal
induct.least(F, m, "pin")?

DERIVED BY HAND (before the engine).
  ROTATION. induct.least reads the window, the pinned keys and the
  closure at every phase t of the period, so a rotation of the period
  is the same cell with its phases renamed: one alpha per necklace.
  Counts: primitive necklaces of length 3 over 6 letters (6^3 - 6) / 3
  = 70, of length 2 (6^2 - 6) / 2 = 15, of length 1 6. W meets the 136
  at its 15 alphas of period at most 2 (golden, silver, bronze, sqrt(3)
  - 1 [1, 2] and FRESH's 11) at m = 2 .. 9, 120 cells: 881 of W's are
  new.
  THE CRUDE FLOOR. On the full flag the exact G-range low is -(a_1 +
  1) + d, d in {-1, 0, 1} (slackbar's THE FLOOR); on the reduced flag
  it moves by m Z(K_c) = m U_c + m kappa_t (-1)^(c+1) P_c, the crude
  floor off by at most 1 + ceil(m kappa_t P_c). At c = c_ov - 1 the bar
  at c_ov holds: m P_(c+1) < m (P_(c+1) + P_(c+2)) <= P_1 < 1, and P_c
  < 7 P_(c+1) at quotients up to 6 (P_(c+1) = P_c r_(t+c+1), each r_j >
  1 / (a_(j+1) + 1)), so m P_c < 7: the crude floor's error
  is bounded but can
  pass 1, and grows with the quotients, not with m alone. A crude
  verdict can then differ from LOW's only where LOW's least margin is
  within that error of 0; the margins are printed per cell beside the
  bound 1 + ceil(m kappa_t P_c), so a flip is read against it.
  WHY ONE c, still not derived: c_inf <= c_ov is keyweld.py's gap step
  (derived) with the endpoint step and the reduced flag read at the 48
  and printed at the 136;
  c_inf >= c_ov - 1 is the TRANSPLANT from the 136, the first thing W
  can break. At c_ov - 2 the gaps are longer than at c_ov - 1, their
  records n+-(L) smaller, so a pass there needs ends lower still.
  WHERE THE KILL BITES. The arm c_inf = c_ov - 1 is where the bar must
  pass every piece; off it, any failing piece reads c_ov. At the 136
  the arm sat mostly at m equal to the least quotient (10 of 17), and
  the least margins on it ran 3 to 1032: the corner is small m against
  large quotients, which W holds whole (m = 2 .. 6 against quotients 2
  .. 6), not drawn.

DESIGN (frozen before the engine). Cells: W as above, each alpha its
necklace's least rotation, plus the 136 as control (a). Per cell:
c_inf = induct.least(F, m, "pin") (cmax 13; a None or a closure past
its limit is printed and counted apart, never read as a verdict); c_ov
= keyweld.c_ov; c_form = classform.c_form; at c = c_ov - 1 (pinned
moves required, else every bar reads c_ov) slackbar.read_c, giving the
FORM, LOW and CRUDE bars and the least exact and crude margins. Each
cell also prints max over phases of 1 + ceil(m kappa_t P_c) at c_ov -
1, the crude floor's error bound.
PREDICTIONS. (W1) c_inf in {c_ov - 1, c_ov} at every cell of W. (W2)
LOW's c = c_inf at every cell. (W3) CRUDE's c = c_inf at every cell.
(W4) c_form = c_inf at every cell.
KILL (printed as): "c_inf outside {c_ov - 1, c_ov} at n of N"; "LOW's c
!= c_inf at n of N"; "CRUDE's c != c_inf at n of N"; "c_form != c_inf
at n of N"; each n > 0 kills its prediction, N = 1001, each printed
also over the new 881 and over the arm (c_inf = c_ov - 1) and over the
cells where the bars can fire (pinned moves at c_ov - 1). A cell
where W3's line fires is read against c_form there first: c_form =
c_inf at it means the one-c cut or the crude floor broke and the
closed form did not; c_form != c_inf at it kills the closed form.
CONTROLS (read before the verdicts). (a) the 136 through this engine:
CRUDE, LOW, FORM and c_form != c_inf at 0 of 136 each (slackbar's and
classform's prints). (b) THE PLANT, h- halved in LOW (stricter) on W:
LOW's c rises above c_inf at some cell of W's arm, or the arm's least
margins all exceed half the records, printed. (c) THE INSTRUMENT:
induct.least against flush.PinGame's solved c_inf (as induct.py's
control) at the new period-3 cells [1, 1, 2] and [1, 2, 2] at m = 2,
3 and [1, 1, 6] at m = 2: equal at every one, else no verdict on W is
read. (d) THE PLANT on c_ov, the bar's m doubled: (W1)'s line must
fire on W.

FINDINGS (copied from the run's prints).
  CONTROLS. (a) the 136: W1 to W4 and FORM at 0 of 136 (arm 0 of 17,
      where bars fire 0 of 120). W: 1001 cells, 881 new, c_inf read at
      every one (no None, no closure past its limit). (b) h- halved:
      LOW's c != c_inf at 27 of W's arm's 106. (c) induct.least =
      PinGame at all five: [1, 1, 2] x2 3, x3 4; [1, 2, 2] x2 3, x3 3;
      [1, 1, 6] x2 3. (d) c_ov's m doubled: W1's line fires at 32 of
      1001.
  W1 to W4, KILLS MISSED. c_inf outside {c_ov - 1, c_ov}, LOW's c,
      CRUDE's c and c_form != c_inf: each at 0 of 1001 (arm 0 of 106,
      where bars fire 0 of 672), 0 of the new 881 (arm 0 of 92, 0 of
      568). The closed form's kill missed.
  MARGINS at c_ov - 1 on W's arm: least 3 (golden x2), 7 at a new cell
      ([1, 2, 2] x3); off the arm the nearest 0 is -5 (golden x3, x7).
      crude - exact is 0 or 1 wherever bars fire, and the crude floor's
      error bound 1 + ceil(m kappa_t P_c) is 2 at every such cell: m
      kappa_t P_c <= 1 at c_ov - 1 on W, read, not derived (the hand
      bound is 7).
  NOTICED (read, not filed). The arm holds [1, a, a] x(a + 1) for a = 2
      .. 6, c_inf 3, least margins 7, 13, 21, 31, 43 = a^2 + a + 1. W's
      arm by m: 31, 26, 17, 12, 5, 4, 2, 3, 3, 0, 3 at m = 2 .. 12; 55
      of 106 at m equal to the least quotient.

RUN RECORD. 32.6 s (the 136 2.0 s, W 30.4 s), peak commit 19.1 MB. The
engine was written whole after the freeze and run once. On shipping, the
verdicts were made the exit code: 0 iff (a) at 0 of 136 (arm 17, bars
firing at 120), W's 1001 cells read with 881 new, (b) at 27 of 106, (c)
equal at all five, (d) at 32, W1 to W4 at 0 over W (arm 106, firing 672)
and the new 881 (92, 568), and crude - exact in [0, 1] under a bound of
2 hold as printed. A review after the run read the c_ov bar in
keyweld.c_ov's indices, m (P_(c+1) + P_(c+2)) <= P_1 at every phase at c
= c_ov - 1 (the frozen m (P_(c+2) + P_(c+3)) - P_2 at phase t is r_t
times this at t + 1), which tightens the frozen hand bound 49 to 7. No
print depends on it.

Usage: python widestep.py
"""

import math
import os
import sys
import time
from itertools import product

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
from flush import PERIODIC, PinGame, Source  # noqa: E402
from decide import FRESH  # noqa: E402
from induct import Field, least  # noqa: E402
from hull import Coords  # noqa: E402
from keyweld import c_ov  # noqa: E402
from classform import c_form  # noqa: E402
from slackbar import read_c  # noqa: E402

KEYS = ("form", "low", "crude", "half")


def necklaces():
    """Each primitive period of length 1 .. 3 over 1 .. 6, its least
    rotation."""
    out = []
    for L in (1, 2, 3):
        for w in product(range(1, 7), repeat=L):
            rots = [w[i:] + w[:i] for i in range(L)]
            if len(set(rots)) < L or w != min(rots):
                continue
            out.append(w)
    return out


def err_bound(F, m, c):
    """max over phases of 1 + ceil(m kappa_t P_c), P_c = r_t ... r_(t+c)."""
    co = Coords(F, m, c)
    best = 0
    for t in range(F.p):
        P = 1.0
        for i in range(c + 1):
            P *= F.r[(t + i) % F.p].f
        best = max(best, 1 + math.ceil(m * co.kap[t].f * P))
    return best


def cell(per, m):
    F = Field(per)
    try:
        cinf = least(F, m, "pin")
    except RuntimeError:
        cinf = "limit"
    cov = c_ov(F, m)
    cov2 = c_ov(F, 2 * m)
    _cp, cf = c_form(F, m)
    r = read_c(F, m, cov - 1, None) if cov >= 1 else None
    bars = {k: cov - 1 if (r is not None and r[0][k]) else cov
            for k in KEYS}
    eb = err_bound(F, m, cov - 1) if r is not None else None
    return dict(per=tuple(per), m=m, cinf=cinf, cov=cov, cov2=cov2, cf=cf,
                bars=bars, fire=r is not None, mex=r[1] if r else None,
                mcr=r[2] if r else None, eb=eb)


def game_cinf(per, m):
    src = Source(period=per)
    p = len(per)
    ts = list(range(1, 2 * p + 1))
    for c in range(13):
        pg = PinGame(src, m, c, ts)
        pg.solve(False)
        if all(i in pg.W for i in pg.init):
            return c
    return None


def report(label, rows):
    n = len(rows)
    arm = [x for x in rows if x["cinf"] == x["cov"] - 1]
    fire = [x for x in rows if x["fire"]]
    tests = (("W1", "c_inf outside {c_ov - 1, c_ov}",
              lambda x: x["cinf"] not in (x["cov"] - 1, x["cov"])),
             ("W2", "LOW's c != c_inf",
              lambda x: x["bars"]["low"] != x["cinf"]),
             ("W3", "CRUDE's c != c_inf",
              lambda x: x["bars"]["crude"] != x["cinf"]),
             ("W4", "c_form != c_inf", lambda x: x["cf"] != x["cinf"]))
    print(f"== {label}: {n} cells, arm {len(arm)}, bars can fire at "
          f"{len(fire)}")
    out = {}
    for tag, what, bad in tests:
        b = [x for x in rows if bad(x)]
        out[tag] = len(b)
        print(f"  {tag} KILL: {what} at {len(b)} of {n}; arm "
              f"{sum(bad(x) for x in arm)} of {len(arm)}; where bars fire "
              f"{sum(bad(x) for x in fire)} of {len(fire)}")
        if b:
            print("     first:", [(x["per"], x["m"], x["cinf"], x["cov"],
                                   x["bars"]["crude"], x["cf"]) for x in b[:8]])
    out["n"], out["arm"], out["fire"] = n, len(arm), len(fire)
    return out, arm


def main():
    t0 = time.time()
    old = {}
    for name, per in list(PERIODIC) + list(FRESH):
        for m in range(2, 10):
            old[(tuple(per), m)] = cell(per, m)
    t1 = time.time()
    W = []
    for per in necklaces():
        for m in range(2, 13):
            W.append(cell(per, m))
    t2 = time.time()
    print("== CONTROLS")
    a = report("(a) the 136", list(old.values()))[0]
    fb = sum(x["bars"]["form"] != x["cinf"] for x in old.values())
    print(f"  (a) FORM's c != c_inf at {fb} of {len(old)}")
    nw = len(W)
    new = [x for x in W if (x["per"], x["m"]) not in old]
    unread = [x for x in W if not isinstance(x["cinf"], int)]
    print(f"  W: {nw} cells, {len(new)} new; c_inf unread (None or "
          f"limit) at {len(unread)}: {[(x['per'], x['m'], x['cinf']) for x in unread[:8]]}")
    armW = [x for x in W if x["cinf"] == x["cov"] - 1]
    hb = [x for x in armW if x["bars"]["half"] != x["cinf"]]
    print(f"  (b) THE PLANT h- halved: LOW's c != c_inf at {len(hb)} of "
          f"{len(armW)} on W's arm")
    games = []
    for per, ms in (((1, 1, 2), (2, 3)), ((1, 2, 2), (2, 3)),
                    ((1, 1, 6), (2,))):
        for m in ms:
            g = game_cinf(per, m)
            x = next(y for y in W if y["per"] == per and y["m"] == m)
            games.append((per, m, x["cinf"], g))
    print(f"  (c) THE INSTRUMENT (alpha, m, induct.least, PinGame): {games}; "
          f"apart {sum(x[2] != x[3] for x in games)}")
    d = [x for x in W if isinstance(x["cinf"], int)
         and x["cinf"] not in (x["cov2"] - 1, x["cov2"])]
    print(f"  (d) THE PLANT c_ov's m doubled: W1's line fires at {len(d)} of "
          f"{nw}")
    print("== MARGINS at c_ov - 1 on W's arm (alpha, m, exact, crude, "
          "crude floor's error bound)")
    for x in sorted(armW, key=lambda x: x["mex"] if x["mex"] is not None
                    else 1e9)[:25]:
        print(f"    {x['per']} x{x['m']} c_inf {x['cinf']} exact {x['mex']} "
              f"crude {x['mcr']} bound {x['eb']}")
    offW = [x for x in W if x["fire"] and x not in armW]
    near = sorted(offW, key=lambda x: -x["mex"])[:10]
    print("  off the arm, the margins nearest 0 (alpha, m, exact, crude, "
          "bound):", [(x["per"], x["m"], x["mex"], x["mcr"], x["eb"])
                      for x in near])
    dif = [x["mcr"] - x["mex"] for x in W if x["fire"]]
    print(f"  crude - exact over W where bars fire: min {min(dif)}, max "
          f"{max(dif)}; error bound max {max(x['eb'] for x in W if x['fire'])}")
    by_m = {}
    for x in armW:
        by_m[x["m"]] = by_m.get(x["m"], 0) + 1
    print(f"  W's arm by m: {dict(sorted(by_m.items()))}; at m = least "
          f"quotient {sum(x['m'] == min(x['per']) for x in armW)}")
    print("== VERDICTS")
    v = report("W", W)[0]
    vn = report("W new", new)[0]
    zero = {"W1": 0, "W2": 0, "W3": 0, "W4": 0}
    checks = [
        a == dict(zero, n=136, arm=17, fire=120) and fb == 0,
        (nw, len(new), len(unread)) == (1001, 881, 0),
        (len(hb), len(armW)) == (27, 106),
        [g[3] for g in games] == [3, 4, 3, 3, 3]
        and all(g[2] == g[3] for g in games),
        len(d) == 32,
        v == dict(zero, n=1001, arm=106, fire=672)
        and vn == dict(zero, n=881, arm=92, fire=568),
        (min(dif), max(dif), max(x["eb"] for x in W if x["fire"]))
        == (0, 1, 2),
    ]
    print(f"  {sum(checks)}/{len(checks)} checks as recorded; 136 "
          f"{t1 - t0:.1f} s, W {t2 - t1:.1f} s, all "
          f"{time.time() - t0:.1f} s")
    sys.exit(0 if all(checks) else 1)


if __name__ == "__main__":
    main()