lowend.py

"""
lowend.py -- H1 by the hull's lower ends: at c = c_ov - 2 (pinned
moves), when does each flag's lower hull end strand, and does the full
window's upper end cover every cell where neither does?

QUESTION. strand.py and widex.py read H1 (some hull key in a zero-reply
gap at c_ov - 2) at all 115 of the 1017 and all 788 of X with pinned
moves there, unproved. Under widex's plant (c) (Z_hi := Z_lo, so only
keys at the flags' lower ends count) a key survives at 766 of 788, at
two cells read by hand the full flag's lower end. Which phase strands
each lower end, by a hand condition, and what is left?

DERIVED BY HAND (before the engine; strand.py's notation, c even, a_k =
a_(t+k), P_k = |theta_k| of r_t; read off classform.win_keys, pieces
and hullform.forms: y(K_k) = (-1)^(k+1) P_k, K_0 = (1, 0), K_1 = (a_1,
1); gap e, 0 <= e < a_2, on both flags y in (P_2 - m P_(c+2) + e P_1,
m P_(c+1) + e P_1), the flag only clipping; full window [m P_(c+1) -
P_1, P_0 - m P_c], reduced [m P_(c+1) - P_1, P_0 - m P_c + m P_(c+1)];
lower forms Z(-(K_1 + K_0)) full, Z(m K_c - K_1 - K_0) reduced, a rule
at the 136 and on X at c_ov - 2 (widex's HULL arm), so a valid key at
its flag's lower form is a hull key).
  (F) The full lower end -(a_1 + 1, 1) has y = P_0 - P_1. Valid iff m
  P_c <= P_1 (its bottom m P_(c+1) <= P_0 is T1's). With j = a_2 - 1 -
  e and P_0 = a_2 P_1 + P_2 it lies in gap e iff j P_1 + P_2 lies in
  (P_2 - m P_(c+2), m P_(c+1)), least at j = 0: some gap holds it iff
  S(t): m P_(c+1) > P_2. As P^(t)_k = P^(t-1)_(k+1) / P^(t-1)_0, m P_c
  <= P_1 at t iff not S(t - 1). So it strands at t iff S(t) and not
  S(t - 1) (theorem, given the lower form). A hot t (L(c + 1, t) > 0)
  has S(t), as P_(c+1) >= P_(c+2) + P_(c+3); one exists. So it strands
  at some phase iff S fails at some phase (theorem); never at period 1.
  (R) The reduced lower end m K_c - K_1 - K_0 has y = P_0 - P_1 - m P_c.
  Valid iff m (P_c + P_(c+1)) <= P_0. In gap e iff j P_1 (j = a_2 - 1 -
  e) lies in T3's interval (m a_(c+2) P_(c+1), m (P_c + P_(c+1)) -
  P_2), so j >= 1. It strands at t iff the interval holds some j P_1,
  j >= 1, and m (P_c + P_(c+1)) <= P_0 (then j <= a_2 - 1 is free, the
  top being <= a_2 P_1) (theorem, given the lower form). It is E_h -
  K_1, E_h = m K_c - K_0, so it strands only at a phase where E_h
  strands (strand.strands_hi, T3).
  So H1 at a cell follows from S failing at some phase, or from E_h
  stranding at some phase; (W), unproved: where S holds at every
  phase, E_h strands at some phase. Under S everywhere T3's top
  exceeds P_1, so j = 1 fails at t only if m a_(c+2) P_(c+1) >= P_1.

DESIGN (frozen before the engine). Cells: strand.cells() (the 1017)
and phase.family() (X, 7557); read those with c = c_ov - 2 >= 0 and
pinned moves (strand.zero_in). Per read cell and phase t, exact (QF):
S(t); (F)'s and (R)'s hand verdicts; E_h's by strand.strands_hi; and
the engine's, strand.read_c's keys: -(a_1 + 1, 1) on the full flag,
m K_c - K_1 - K_0 on the reduced, m K_c - K_0 on the full.
PREDICTIONS. (P1) (F)'s hand verdict = the engine's at every (cell,
phase). (P2) (R)'s likewise. (P3) E_h's = the engine's. (W) at every
read cell with S at every phase, E_h strands at some phase.
KILLS (printed as, each n > 0 kills): "(F) hand != engine at n of N
(cell, phase)"; "(R) hand != engine at n of N"; "(T3) hand != engine
at n of N"; "(W) S at every phase and E_h at none: n of N cells", N
the read cells with S at every phase, over each family. (P1) to (P3)
firing is an index fault or a lower form off its rule, read first.
Printed beside, no kill: per family the read cells, the cells with S
at every phase, and the cells covered by (F) only, E_h only, both; the
cells where (F) or (R) strands at some phase, against widex's plant
survivors (766 of 788) and strand's (88 of 115); every cell with S at
every phase, its period, m and E_h's phases.
CONTROLS (read before the verdicts).
  (a) THE PLANT on (F): the shift read the wrong way, S(t) and not
      S(t + 1): (P1)'s line must fire.
  (b) THE PLANT on (R): validity dropped: (P2)'s line must fire, or it
      is printed that validity binds nowhere read.
  (c) THE ENGINE: strand.py's own control (a), golden x3 at c = 3,
      phase 0, full: hull keys {(3, 2), (8, 5)} (strand.control_a).

FINDINGS (copied from the run's prints).
  CONTROLS. (c) strand.control_a held. (a) the shift read as t + 1:
      (F)'s line at 60 of 309 (the 1017) and 870 of 3326 (X): it can
      fire. (b) validity dropped: (R)'s line at 0 of 309 and 0 of
      3326: validity binds nowhere read (observation).
  KILLS MISSED. (F), (R), (T3) hand != engine at 0 of 309 (cell,
      phase) on the 1017's 115 read cells and 0 of 3326 on X's 788.
      Hot without S at 0; (R) without E_h at 0 (both proved). (W): S at
      every phase and E_h at none at 0 of 76 and 0 of 321 cells.
  BESIDE. The 1017: S at every phase at 76 of 115 (period 1, 2, 3, 4:
      7, 20, 47, 2); (F) only 0, E_h only 76, both 39, neither 0.
      X: S at every phase at 321 of 788 (period 3, 4, 5: 65, 169, 87);
      (F) only 1 ([1, 1, 1, 2, 3] x7), E_h only 321, both 466, neither
      0. (F) or (R) at some phase at 88
      of 115 and 766 of 788: the counts of the plant survivors of
      strand.py (d) and widex.py (c), the sets equal by argument (under
      Z_hi := Z_lo only keys at a lower form survive), not printed.
  SCOPE. The engine reads hullform's forms too, so (P1) to (P3) test
      the indices, not the forms; the forms are read at c_ov - 2 on X
      (widex's HULL arm) and at the 136 (classform.py's (ii)), not at
      the 1017's other 15 read cells. H1 by (F) or E_h needs the full
      flag's two forms (E_h's Z between Z_lo and Z_hi by T3); the
      reduced flag's adds nothing past E_h.

AFTER THE RUN (printed: the AFTER THE RUN line). At S everywhere, j =
1 strands E_h at some phase at 30 of 76 and 86 of 321; j = a_(c+2) at
75 of 76 and 307 of 321, not at [2, 4, 5] x8 among others. At period
1 (r = [0; a, a, ...], u = m r^c < 1 by T1, r^c
irrational) T3's interval over P_1 is
(a u, a u + u (1 + r) - r), and j = a lies in it (a u < a free) iff u >
(a + r) / (a + 1 + r) = 1 / (1 + r), which is the hot condition: W holds at period 1 (theorem,
by hand). In general neither j = 1 nor j = a_(c+2) is the witness.

RUN RECORD. 12.5 s, the engine written whole after the freeze,
rehearsed at 60 cells per family, then run once; the AFTER THE RUN
line and the (F) only line added after, the whole rerun printing every
line unchanged. Changed from the freeze: the cells with S at every
phase print the first 10, not all. On shipping, the verdicts were made
the exit code: 0 iff the controls (the engine's; the plants at 60 and
870, 0 and 0), the kills and the proofs' prints at 0, the read, S
everywhere, (F) or (R), j = 1 and j = a_(c+2) counts and the cover
line hold as printed.

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

import os
import sys
import time

os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
from induct import Field, QF, le  # noqa: E402
from keyweld import c_ov, lt  # noqa: E402
from firstreturn import l_formula  # noqa: E402
from hullform import uv  # noqa: E402
from classform import lin  # noqa: E402
from strand import P, cells as strand_cells, read_c, zero_in  # noqa: E402
from strand import strands_hi, control_a  # noqa: E402
from phase import family  # noqa: E402


def S(F, m, c, t):
    return lt(P(F, t, 2), P(F, t, c + 1) * m)


def hand_R(F, m, c, t, validity=True):
    a2 = F.a(t + 2)
    A = P(F, t, c + 1) * (m * F.a(t + c + 2))
    B = (P(F, t, c) + P(F, t, c + 1)) * m - P(F, t, 2)
    js = [j for j in range(1, a2) if lt(A, P(F, t, 1) * j)
          and lt(P(F, t, 1) * j, B)]
    ok = le((P(F, t, c) + P(F, t, c + 1)) * m, P(F, t, 0))
    return bool(js) and (ok or not validity)


def read(per, m):
    F = Field(per)
    cov = c_ov(F, m)
    c = cov - 2
    if c < 0 or not zero_in(F, m, c):
        return None
    r = read_c(F, m, c)
    if r is None:
        return None
    p = F.p
    keys = set((k[0], k[1], k[2]) for k in r["keys"])
    s = [S(F, m, c, t) for t in range(p)]
    rows = []
    for t in range(p):
        K0, K1, Kc = uv(F, t, 0), uv(F, t, 1), uv(F, t, c)
        lf = lin((-1, K1), (-1, K0))
        lr = lin((m, Kc), (-1, K1), (-1, K0))
        eh = lin((m, Kc), (-1, K0))
        hot = lt(QF(0), l_formula(F, t, m, c + 1))
        rows.append(dict(
            t=t, hot=hot, S=s[t],
            F=s[t] and not s[(t - 1) % p], Fp=s[t] and not s[(t + 1) % p],
            R=hand_R(F, m, c, t), Rp=hand_R(F, m, c, t, validity=False),
            T=bool(strands_hi(F, m, c, t)),
            eF=(t, True, lf) in keys, eR=(t, False, lr) in keys,
            eT=(t, True, eh) in keys))
    return dict(per=per, m=m, c=c, p=p, rows=rows, nkeys=len(keys))


def report(name, R):
    pr = [(x, q) for x in R for q in x["rows"]]
    n = len(pr)
    out = {}
    for tag, h, e in (("(F)", "F", "eF"), ("(R)", "R", "eR"),
                      ("(T3)", "T", "eT")):
        bad = [(x["per"], x["m"], q["t"]) for x, q in pr if q[h] != q[e]]
        out[tag] = len(bad)
        print(f"  {tag} hand != engine at {len(bad)} of {n} (cell, phase): "
              f"{bad[:6]}")
    pf = sum(q["Fp"] != q["eF"] for _, q in pr)
    pb = sum(q["Rp"] != q["eR"] for _, q in pr)
    print(f"  (a) PLANT shift t + 1: (F)'s line at {pf} of {n}; (b) PLANT "
          f"validity dropped: (R)'s line at {pb} of {n}")
    hs = sum(q["hot"] and not q["S"] for _, q in pr)
    rt = sum(q["R"] and not q["T"] for _, q in pr)
    print(f"  proofs' prints: hot without S at {hs}; (R) without E_h at {rt}")
    allS = [x for x in R if all(q["S"] for q in x["rows"])]
    w = [x for x in allS if not any(q["T"] for q in x["rows"])]
    out["W"] = len(w)
    print(f"  (W) S at every phase and E_h at none: {len(w)} of "
          f"{len(allS)} cells: {[(x['per'], x['m']) for x in w[:8]]}")
    f = [any(q["F"] for q in x["rows"]) for x in R]
    th = [any(q["T"] for q in x["rows"]) for x in R]
    fr = sum(any(q["F"] or q["R"] for q in x["rows"]) for x in R)
    print(f"  beside: read {len(R)}; S at every phase {len(allS)}; (F) only "
          f"{sum(a and not b for a, b in zip(f, th))}, E_h only "
          f"{sum(b and not a for a, b in zip(f, th))}, both "
          f"{sum(a and b for a, b in zip(f, th))}, neither "
          f"{sum(not (a or b) for a, b in zip(f, th))}; (F) or (R) at some "
          f"phase {fr}")
    fo = [(x["per"], x["m"]) for x, a, b in zip(R, f, th) if a and not b]
    print(f"  (F) only at {fo[:8]}")
    byp = {}
    for x in allS:
        byp[x["p"]] = byp.get(x["p"], 0) + 1
    first = [(x["per"], x["m"], [q["t"] for q in x["rows"] if q["T"]])
             for x in allS[:10]]
    print(f"  S at every phase by period {dict(sorted(byp.items()))}; "
          f"first: {first}")
    j1 = jc = 0
    miss = []
    for x in allS:
        F = Field(x["per"])
        m, c = x["m"], x["c"]
        j1 += any(lt(P(F, t, c + 1) * (m * F.a(t + c + 2)), P(F, t, 1))
                  for t in range(x["p"]))
        hit = any(F.a(t + c + 2) in strands_hi(F, m, c, t)
                  for t in range(x["p"]))
        jc += hit
        if not hit:
            miss.append((x["per"], m))
    print(f"  AFTER THE RUN, at S everywhere: j = 1 strands E_h at some phase "
          f"at {j1} of {len(allS)}; j = a_(c+2) at {jc}, not at {miss[:6]}")
    out.update(read=len(R), allS=len(allS), fr=fr, j1=j1, jc=jc,
               plants=(pf, pb), proofs=(hs, rt),
               cover=(sum(a and not b for a, b in zip(f, th)),
                      sum(b and not a for a, b in zip(f, th)),
                      sum(a and b for a, b in zip(f, th)),
                      sum(not (a or b) for a, b in zip(f, th))))
    return out


def main():
    t0 = time.time()
    only = int(sys.argv[1]) if len(sys.argv) > 1 else None
    print("== CONTROLS")
    print(f"  (c) strand.control_a held: {control_a()}")
    res = {}
    for name, cells in (("the 1017", strand_cells()), ("X", family())):
        if only:
            cells = cells[::max(1, len(cells) // only)]
        t1 = time.time()
        R = [x for x in (read(per, m) for per, m in cells) if x]
        print(f"== {name}: {len(cells)} cells, {time.time() - t1:.1f} s")
        res[name] = report(name, R)
    print(f"  all {time.time() - t0:.1f} s")
    if only:
        return res
    a, x = res["the 1017"], res["X"]
    checks = [
        control_a(),
        a["plants"] == (60, 0) and x["plants"] == (870, 0),
        [a[k] for k in ("(F)", "(R)", "(T3)", "W")] == [0, 0, 0, 0],
        [x[k] for k in ("(F)", "(R)", "(T3)", "W")] == [0, 0, 0, 0],
        a["proofs"] == (0, 0) and x["proofs"] == (0, 0),
        (a["read"], a["allS"], a["fr"], a["j1"], a["jc"])
        == (115, 76, 88, 30, 75),
        (x["read"], x["allS"], x["fr"], x["j1"], x["jc"])
        == (788, 321, 766, 86, 307),
        a["cover"] == (0, 76, 39, 0) and x["cover"] == (1, 321, 466, 0),
    ]
    print(f"  {sum(checks)}/{len(checks)} checks as recorded")
    sys.exit(0 if all(checks) else 1)


if __name__ == "__main__":
    main()