phase.py

"""
phase.py -- T3's phase: at c = c_ov - 2 (pinned moves), does phase t + 1
or t + 2 of every hot t strand the full window's upper end?

QUESTION. strand.py proves that at c = c_ov - 2 with pinned moves c is
even and the full window's upper end E_h = m K_c - K_0 is a hull key,
stranded at phase u iff some j P_1 lies in (m a_(c+2) P_(c+1), m (P_c +
P_(c+1)) - P_2) (u's scale); some phase strands at all 115 of its 1017
cells, why not derived. Which phase must?

DERIVED BY HAND (before the engine; strand.py's notation, a_k =
a_(u+k), P_k = |theta_k| of r_u, hot t: L(c + 1, t) > 0).
(R1) By T1 at the shifted phases m P_(c+k) < P_k for every k >= -1
(strict: theta_j = x_j r + y_j with (x_j, y_j) primitive, consecutive
determinants being +-1, so theta_k = +-m theta_(c+k) would make m >= 2
divide (x_k, y_k)).
So m P_c = a_(c+2) m P_(c+1) + m P_(c+2) < a_(c+2) P_1 + P_2: the
interval's top is below (a_(c+2) + 1) P_1, and below (a_2 + 1) P_1, so
a stranding j has 1 <= j <= min(a_2, a_(c+2)). (theorem)
(R2) j = a_2 meets the top iff P_0 < m (P_c + P_(c+1)), which is
L(c + 1, u - 2) > 0; the bottom has no j in it, so a smaller j only
loses the bottom. Hence, t hot, phase t + 2 strands iff its top j =
a_(t+4) clears the bottom: (C2) a_(t+4) P_3 > m a_(t+c+4) P_(c+3) in
t's scale. Its failure forces a_(t+4) < a_(t+c+4) (by m P_(c+3) <
P_3). (theorem)
(R3) j = a_(c+2) clears the bottom free (m P_(c+1) < P_1), so (C1)
a_(c+2) P_1 + P_2 < m (P_c + P_(c+1)) at phase u makes u strand.
(theorem; sufficient, not necessary)
Read off strand before the freeze: where t + 2 fails (37 of the 115),
phase hot + 1 strands at all 37, by j = a_(c+2) of that phase.

THE CONJECTURE (T3P): at every hot t, phase t + 1 or t + 2 strands.
At period 2 it is T3 itself (t or t + 1), at period 1 "t strands";
only period >= 3 reads it as a choice of phase.

DESIGN (frozen before the engine). Family X: primitive periods of
length 3 over quotients 1 .. 8, of length 4 over 1 .. 6, of length 5
over 1 .. 4, least rotation, at m = 2 .. 12; with strand's 1017. Per
cell c = c_ov - 2 >= 0 with pinned moves (strand.zero_in, by T1), else
skipped and counted.
KILLS (printed as, each killing at n > 0):
  K1 "T3P fails at n of N (cell, hot t)" over every read cell;
  K2 "(C2) apart from t + 2 stranding at n of N (cell, hot t)" (R2 is
     a proof: an index fault, read first);
  K3 "(C1) at u holds, u not stranding, at n of N (cell, u)" (R3);
  K4 "some phase strands at none of n of N cells" (T3 itself).
Beside, no kill: K1's pairs by t + 2 only / t + 1 only / both; how
often t + 1 strands by (C1); the read cells by period.
CONTROLS (read first): strand's 115 reproduced (read 115, t + 2 for
some hot t at 78); THE PLANT: (C2) with a_(t+c+4) replaced by
a_(t+c+3) must put K2's line above 0 on X.

FINDINGS (copied from the run's prints).
  CONTROLS. strand's 1017: read 115, t + 2 for some hot t at 78: held.
      THE PLANT: K2's line at 593 of 1084: the line can fire.
  CELLS. strand's 1017 read 115 (period 1, 2, 3, 4: 7, 28, 74, 6); X
      7557 cells, no pinned moves at 6769, read 788 (period 3, 4, 5:
      122, 370, 296); c odd at 0 of either (T2).
  K2, K3 MISSED (the proofs' lines): 0 of 152 and 1084 (cell, hot t);
      0 of 309 and 3326 (cell, u).
  K1 FIRES: T3P fails at 4 of 1084 on X, all period 5: [1, 1, 1, 2,
      3] x7, [1, 1, 1, 3, 3] x10, [1, 1, 1, 3, 4] x10, [1, 1, 1, 4, 3]
      x12, each at hot t = 2. T3P is killed; at strand's 1017, 0 of 152.
  K4 FIRES: no phase strands the upper end at 1 of 788, [1, 1, 1, 2, 3]
      x7 (c = 4). T3 is not universal past the 1017.
  Beside: on X, t + 2 only 90, t + 1 only 503, both 487; t + 1 by
      (C1) at 920 of 990.
  AFTER THE RUN (an arm added after the first run, then printed), at
  K1's four cells through strand.read_c and induct.least: c_inf - c_ov
  is -1, 0, -1, 0, and hull keys lie in pieces at c_ov - 2 at each (the
  hull's bounds hullform's, a rule at the 136, a TRANSPLANT here). At
  the three cells other than K4's the upper end strands at hot t = 2
  itself (a closed end at phase 2, full flag), so T3 holds there by t,
  not t + 1 or t + 2. At K4's cell, [1, 1, 1, 2, 3] x7, only interior
  keys (phases 1, 2, 3, both flags) and c_inf = c_ov - 1: the upper
  end's route fails, H1 (some hull key in a gap) holds.

RUN RECORD. 8.3 s, peak commit 11.6 MB. Written whole after the freeze,
rehearsed at 60 cells per family, then run once; the AFTER THE RUN arm
was added from a review and the whole rerun printed every frozen line
unchanged, each of the four cells read (Field, least, read_c) in 0.06 s
or less. On shipping, the verdicts were made the exit code: 0 iff the
controls (115, 78; the plant at 593 of 1084), the cells as counted with
odd c at 0, K1 to K4 at 0 on strand's 1017 and at 4, 0, 0, 1 on X, the
beside line and the four cells' c_inf - c_ov (-1, 0, -1, 0, each with
hull keys in pieces) hold as printed.

Usage: python phase.py [cells]
"""

import os
import sys
import time
from itertools import product

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
from induct import Field, QF  # noqa: E402
from keyweld import c_ov, lt  # noqa: E402
from firstreturn import l_formula  # noqa: E402
from strand import P, cells as strand_cells, strands_hi, zero_in  # noqa: E402
from strand import read_c  # noqa: E402
from induct import least  # noqa: E402


def necklaces(L, A):
    out = []
    for w in product(range(1, A + 1), 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 family():
    out = []
    for L, A in ((3, 8), (4, 6), (5, 4)):
        for per in necklaces(L, A):
            for m in range(2, 13):
                out.append((per, m))
    return out


def c2(F, m, c, t, shift=4):
    """(C2) a_(t+4) P_3 > m a_(t+c+shift) P_(c+3), t's scale."""
    return lt(P(F, t, c + 3) * (m * F.a(t + c + shift)),
              P(F, t, 3) * F.a(t + 4))


def c1(F, m, c, u):
    """(C1) a_(c+2) P_1 + P_2 < m (P_c + P_(c+1)), u's scale."""
    return lt(P(F, u, 1) * F.a(u + c + 2) + P(F, u, 2),
              (P(F, u, c) + P(F, u, c + 1)) * m)


def read(per, m):
    F = Field(per)
    cov = c_ov(F, m)
    c = cov - 2
    if c < 0:
        return dict(per=per, m=m, skip="neg")
    if not zero_in(F, m, c):
        return dict(per=per, m=m, skip="nopin")
    p = F.p
    hot = [t for t in range(p) if lt(QF(0), l_formula(F, t, m, c + 1))]
    st = {u: bool(strands_hi(F, m, c, u)) for u in range(p)}
    pairs = []
    for t in hot:
        s1, s2 = st[(t + 1) % p], st[(t + 2) % p]
        pairs.append(dict(t=t, s1=s1, s2=s2, c2=c2(F, m, c, t),
                          plant=c2(F, m, c, t, shift=3),
                          c1=c1(F, m, c, (t + 1) % p)))
    c1u = [(c1(F, m, c, u), st[u]) for u in range(p)]
    return dict(per=per, m=m, skip=None, c=c, p=p, hot=hot, st=st,
                pairs=pairs, c1u=c1u)


def main():
    t0 = time.time()
    only = int(sys.argv[1]) if len(sys.argv) > 1 else None
    old = [read(per, m) for per, m in strand_cells()[:only]]
    t1 = time.time()
    X = [read(per, m) for per, m in family()[:only]]
    t2 = time.time()
    res = {}
    print("== CONTROLS")
    ro = [x for x in old if x["skip"] is None]
    n2 = sum(any(q["s2"] for q in x["pairs"]) for x in ro)
    print(f"  strand's cells: {len(old)}, read {len(ro)}, t + 2 strands for "
          f"some hot t at {n2}")
    rx = [x for x in X if x["skip"] is None]
    pl = sum(q["plant"] != q["s2"] for x in rx for q in x["pairs"])
    npx = sum(len(x["pairs"]) for x in rx)
    print(f"  THE PLANT a_(t+c+3) for a_(t+c+4): K2's line at {pl} of {npx}")
    for name, R, allc in (("strand's 1017", ro, old), ("X", rx, X)):
        print(f"== {name}: {len(allc)} cells; c_ov - 2 < 0 at "
              f"{sum(x['skip'] == 'neg' for x in allc)}; no pinned moves at "
              f"{sum(x['skip'] == 'nopin' for x in allc)}; read {len(R)}")
        odd = sum(x["c"] % 2 for x in R)
        byp = {}
        for x in R:
            byp[x["p"]] = byp.get(x["p"], 0) + 1
        print(f"  read c odd at {odd} (T2); read by period "
              f"{dict(sorted(byp.items()))}")
        prs = [(x, q) for x in R for q in x["pairs"]]
        k1 = [(x["per"], x["m"], q["t"]) for x, q in prs
              if not (q["s1"] or q["s2"])]
        print(f"  K1: T3P fails at {len(k1)} of {len(prs)} (cell, hot t): "
              f"{k1[:8]}")
        k2 = [(x["per"], x["m"], q["t"]) for x, q in prs
              if q["c2"] != q["s2"]]
        print(f"  K2: (C2) apart from t + 2 stranding at {len(k2)} of "
              f"{len(prs)} (cell, hot t): {k2[:8]}")
        cu = [v for x in R for v in x["c1u"]]
        k3 = sum(a and not b for a, b in cu)
        print(f"  K3: (C1) at u holds, u not stranding, at {k3} of "
              f"{len(cu)} (cell, u); (C1) holds at {sum(a for a, _ in cu)}, "
              f"u strands at {sum(b for _, b in cu)}")
        k4 = [(x["per"], x["m"]) for x in R if not any(x["st"].values())]
        print(f"  K4: some phase strands at none of {len(k4)} of {len(R)} "
              f"cells: {k4[:8]}")
        res[name] = dict(
            cells=(len(allc), sum(x["skip"] == "neg" for x in allc),
                   sum(x["skip"] == "nopin" for x in allc), len(R)),
            odd=odd, byp=dict(sorted(byp.items())),
            k=(len(k1), len(k2), len(prs), k3, len(cu), len(k4)))
        only2 = sum(q["s2"] and not q["s1"] for _, q in prs)
        only1 = sum(q["s1"] and not q["s2"] for _, q in prs)
        both = sum(q["s1"] and q["s2"] for _, q in prs)
        print(f"  beside: t + 2 only {only2}, t + 1 only {only1}, both "
              f"{both}; t + 1 strands by (C1) at "
              f"{sum(q['s1'] and q['c1'] for _, q in prs)} of "
              f"{sum(q['s1'] for _, q in prs)}")
        res[name]["beside"] = (only2, only1, both,
                               sum(q["s1"] and q["c1"] for _, q in prs),
                               sum(q["s1"] for _, q in prs))
        p3 = [(x, q) for x, q in prs if x["p"] >= 3]
        print(f"  period >= 3 pairs {len(p3)}; K1 there "
              f"{sum(not (q['s1'] or q['s2']) for _, q in p3)}")
    print("== AFTER THE RUN: K1's and K4's cells through strand's engine")
    after = []
    for x in rx:
        bad = [q["t"] for q in x["pairs"] if not (q["s1"] or q["s2"])]
        none = not any(x["st"].values())
        if not (bad or none):
            continue
        t3 = time.time()
        F = Field(x["per"])
        ci = least(F, x["m"], "pin")
        r = read_c(F, x["m"], x["c"])
        kinds = sorted(set((k[0], "full" if k[1] else "red", k[3])
                           for k in r["keys"]))
        after.append((x["per"], x["m"], ci - x["c"] - 2, bool(r["keys"])))
        print(f"  {x['per']} x{x['m']} c {x['c']}: K1 at hot t {bad}, K4 "
              f"{none}; c_inf - c_ov {ci - x['c'] - 2}; hull keys in pieces "
              f"(phase, flag, kind) {kinds}; {time.time() - t3:.2f} s")
    if only is not None:
        return
    old_r, x_r = res["strand's 1017"], res["X"]
    checks = [
        (len(old), len(ro), n2) == (1017, 115, 78),
        (pl, npx) == (593, 1084),
        old_r["cells"] == (1017, 0, 902, 115) and old_r["odd"] == 0
        and old_r["byp"] == {1: 7, 2: 28, 3: 74, 4: 6},
        x_r["cells"] == (7557, 0, 6769, 788) and x_r["odd"] == 0
        and x_r["byp"] == {3: 122, 4: 370, 5: 296},
        old_r["k"] == (0, 0, 152, 0, 309, 0),
        x_r["k"] == (4, 0, 1084, 0, 3326, 1),
        x_r["beside"] == (90, 503, 487, 920, 990),
        [(a[2], a[3]) for a in after] == [(-1, True), (0, True),
                                          (-1, True), (0, True)],
    ]
    print(f"  {sum(checks)}/{len(checks)} checks as recorded; strand's "
          f"{t1 - t0:.1f} s, X {t2 - t1:.1f} s, all "
          f"{time.time() - t0:.1f} s")
    sys.exit(0 if all(checks) else 1)


if __name__ == "__main__":
    main()