""" widex.py -- the closed form's KILL past period 3: on X (period 3 to quotients 8, 4 to 6, 5 to 4, m = 2 .. 12), does c_inf stay c_ov or c_ov - 1, read by widestep's crude bar and by classform's c_form, and does a hull key strand at c_ov - 2 wherever pinned moves exist there? QUESTION. widestep.py reads c_crude = c_form = induct.least at its 1001 cells (period <= 3, quotients <= 6, m <= 12); strand.py reads a hull key in a zero-reply piece at c_ov - 2 at all 115 of the 1017 with pinned moves there (H1). phase.py widened to X (7557 cells) and found the full window's upper end unstranded at [1, 1, 1, 2, 3] x7, where c_inf = c_ov - 1 still (four cells read). X is the first widening past period 3; the closed form's KILL is owed there, and H1, the open front the upper end's route left, is read at every X cell with pinned moves at c_ov - 2. DERIVED BY HAND (before the engine). THE BARS' RANGE. widestep.cell's c_crude is c_ov - 1 when slackbar's crude bar passes every piece at c_ov - 1 (pinned moves there), else c_ov: it never reads outside {c_ov - 1, c_ov}. So the KILL (c_crude != c_inf and c_form != c_inf at one cell) can fire two ways: c_inf leaves {c_ov - 1, c_ov} (X1's line) while c_form misses it too, or the crude bar errs inside the pair and the closed form errs with it. c_form reads the forms' hull at every c from the first pinned c up, so a hull end off its form (below) can move it. X1, a TRANSPLANT. c_inf <= c_ov is keyweld's gap step, derived with the endpoint step and the reduced flag read at the 48; c_inf >= c_ov - 1 is read at the 1017 and at phase.py's four X cells only. (M) Pinned moves at c give them at c + 1 (theorem, by hand). By T1 (strand.py) they are, at every t, m P_(c+1) <= P_1 and m P_c <= P_0 at c even, m P_c <= P_1 and m P_(c+1) <= P_0 at c odd. At c even, c + 1 odd needs m P_(c+1) <= P_1 (given) and m P_(c+2) < m P_c <= P_0; at c odd, c + 1 even needs m P_(c+2) < m P_c <= P_1 and m P_(c+1) <= P_0 (given); P_k falls strictly in k. So where c_ov - 2 has no pinned moves no c below has them, induct.least (which needs them) reads c_inf >= c_ov - 1, and X1's low side can fire only at the cells read for H1. Printed beside: pinned moves at c and none at c + 1, over c <= c_ov at every cell (0 by M). H1's READING leans on hullform's forms (a rule at the 136, a TRANSPLANT at every X cell): a form above the true top makes a key "in the hull" that is not, so H1 could pass falsely. The arm HULL reads, at c_ov - 2 at the read cells, hull.py's exact fixed points against the forms at every node, and the pinned closure's keys (the closure grown at that c, induct's) against the forms' [Z_lo, Z_hi]. A cell where either fires is printed apart, its H1 verdict unread. DESIGN (frozen before the engine). Cells: X = phase.family() (7557), and strand.cells() (the 1017: widestep's W and the 136) as control. Per cell widestep.cell (c_inf = induct.least "pin", c_ov, c_ov at 2m, c_form, the FORM, LOW, CRUDE bars at c_ov - 1); then at c = c_ov - 2 >= 0 with pinned moves (strand.zero_in), strand.read_c (hull keys in pieces) and read_c with plant (Z_hi := Z_lo). The HULL arm at the read cells of X (all, or the period-5 ones if the rehearsal prices all past ten minutes, named): hull.py's hull(low) for both ends against hullform.forms at every node, exact; the pinned closure's keys at c with Z outside the forms' range on their node. PREDICTIONS. (X1) c_inf in {c_ov - 1, c_ov} at every X cell. (X2) CRUDE's c = c_inf and (X3) c_form = c_inf at every X cell. (X4) H1: some piece at c_ov - 2 holds a hull key at every read X cell. KILLS (printed as, each n > 0 kills): "THE KILL: c_crude != c_inf and c_form != c_inf at n of N"; "X1: c_inf outside {c_ov - 1, c_ov} at n of N"; "X2: CRUDE's c != c_inf at n of N"; "X3: c_form != c_inf at n of N"; "X4 (H1): no hull key in any piece at c_ov - 2 at n of N read cells", N = 7557 for the first four, each also over the arm (c_inf = c_ov - 1) and where the bars fire, and by period. Beside, no kill: LOW's c; c_inf unread (None or past the closure's limit), counted apart; the HULL arm's two lines; per read cell the kinds of the stranded keys (closed end, interior, +-K_c); the K1 cells of phase.py (period 5, [1, 1, 1, ...], hot t = 2): which keys strand there. CONTROLS (read before the verdicts). (a) THE 1017 through this engine: on W (1001) X1 to X3 at 0 with arm 106, bars firing 672 (widestep's prints); on the 136 at 0 with arm 17, firing 120; H1 read at 115, no hull key at 0 (strand's). (b) THE PLANT on c_ov, m doubled (widestep's (d)): X1's line read against c_ov(2m) must fire on X. (c) THE PLANT on H1, Z_hi := Z_lo (strand's (d)): X4's line must fire at some read X cell. (d) THE INSTRUMENT: induct.least against flush.PinGame's solved c_inf (widestep.game_cinf) at K4's cell [1, 1, 1, 2, 3] x7 and at [1, 1, 1, 1, 2] x2, x3 (period 5): equal at each, else no verdict on X is read. (e) THE PLANT on the HULL arm: hull.py's plant (d_max full - 1) must put its node line above 0. FINDINGS (copied from the run's prints). CONTROLS. (a) W: 1001 cells, arm 106, bars can fire (pinned moves at c_ov - 1) at 672; the 136: arm 17, bars can fire at 120; the 1017: X1 to X3, LOW and the KILL at 0, H1 at 0 of 115 read: held. (b) c_ov's m doubled: X1's line at 106 of 7557. (c) Z_hi := Z_lo: X4's line at 22 of 788. (d) induct.least = PinGame at [1, 1, 1, 2, 3] x7 (5), [1, 1, 1, 1, 2] x2 (3), x3 (5). (e) hull.py's plant moves 8 of 12 nodes at the first read cell where it moves any. X1's, X4's and the HULL arm's node line can fire; the KILL, X2, X3 and the closure-key line carry no plant here or in widestep (whose (b) planted LOW, (d) c_ov). Under (c) a key survives at 766 of 788: at the two cells read by hand, [1, 1, 1, 2, 3] x7 and [1, 1, 1, 3, 3] x10, the full flag's lower hull end -(a_(t+1) + 1, 1) = (-2, -1) at phase 2, a_(t+1) = 1, inside a gap, and at x10 a reduced-flag key beside it (observation). THE HULL ARM. At c_ov - 2 on X's 788 read cells: nodes whose exact hull end != its form 0 of 13304; pinned-closure keys outside the forms' range 0 of 201139. hullform's four ends hold there. (M): 0 cells with pinned moves at c and none at c + 1. KILLS MISSED on X (7557 cells, c_inf read at all, arm 826, bars can fire at 4737): THE KILL 0; X1 0; X2 0; X3 0; LOW's c 0; X4 (H1) 0 of 788 read (period 3, 4, 5: 122, 370, 296). KINDS on X: a closed end in the hull at 787 of 788 (all but K4's cell), an interior key at all 788, -K_c among them at 128. phase.py's four K1 cells strand interior keys at phases 1 to 3 at each, and on the reduced flag at phase 4 at two (phase.py's AFTER THE RUN print; the first 12 printed here are a sample). RUN RECORD. 432.6 s (the 1017 31.9 s, X 398.6 s), peak commit 199.9 MB, estimated at seven to eight minutes from a 60-cell rehearsal (5.8 s). The engine was written whole after the freeze, rehearsed, then run once. On shipping, the verdicts were made the exit code: 0 iff the controls (a) to (e), the HULL arm, (M), the verdicts on X and the kinds' three counts hold as printed; X4's split by period and the K1 cells' keys are printed, unchecked. Usage: python widex.py [cells] """ import os import sys import time os.environ.setdefault("OPENBLAS_NUM_THREADS", "1") from induct import Field, Window, le # noqa: E402 from hull import Coords, hull, eq # noqa: E402 from hullform import forms # noqa: E402 from strand import cells as strand_cells, read_c as strand_read # noqa: E402 from strand import zero_in # noqa: E402 from widestep import cell as wcell, game_cinf, necklaces # noqa: E402 from induct import least # noqa: E402 from flush import PERIODIC # noqa: E402 from decide import FRESH # noqa: E402 from phase import family # noqa: E402 def hull_arm(F, m, c, plant=False): """At c: (nodes, nodes whose exact hull end != its form, closure keys, closure keys outside the forms' range on their node).""" win = Window(F, m, c) st, _miss = win.pin_starts() co = Coords(F, m, c) fm = {t: forms(F, co, m, c, t) for t in range(F.p)} nodes = off = 0 for low in (False, True): val, _ = hull(win, co, st, low=low, plant=plant) for (t, f), v in val.items(): nodes += 1 off += not eq(v, fm[t][(f, low)]) _ok, S, _bad = win.closure(st) out = 0 for G, H, f, t in S: z = co.Z(G, H, t) out += not (le(fm[t][(f, True)], z) and le(z, fm[t][(f, False)])) return nodes, off, len(S), out def mono(F, m, cov): """c <= c_ov with pinned moves at c and none at c + 1 (M).""" bad = [] pin = [zero_in(F, m, c) for c in range(cov + 2)] for c in range(cov + 1): if pin[c] and not pin[c + 1]: bad.append(c) return bad def read(per, m, do_hull): x = wcell(per, m) F = Field(per) x["p"] = F.p x["mono"] = mono(F, m, x["cov"]) c = x["cov"] - 2 x["read"] = False if c >= 0 and zero_in(F, m, c): r = strand_read(F, m, c) if r is not None: x["read"] = True x["c2"] = c x["keys"] = r["keys"] x["plant"] = bool(strand_read(F, m, c, plant=True)["keys"]) if do_hull: x["hull"] = hull_arm(F, m, c) return x def verdicts(label, rows): n = len(rows) ok = [x for x in rows if isinstance(x["cinf"], int)] arm = [x for x in ok if x["cinf"] == x["cov"] - 1] fire = [x for x in ok if x["fire"]] tests = ( ("THE KILL", "c_crude != c_inf and c_form != c_inf", lambda x: x["bars"]["crude"] != x["cinf"] and x["cf"] != x["cinf"]), ("X1", "c_inf outside {c_ov - 1, c_ov}", lambda x: x["cinf"] not in (x["cov"] - 1, x["cov"])), ("X2", "CRUDE's c != c_inf", lambda x: x["bars"]["crude"] != x["cinf"]), ("X3", "c_form != c_inf", lambda x: x["cf"] != x["cinf"]), ("beside", "LOW's c != c_inf", lambda x: x["bars"]["low"] != x["cinf"]), ) print(f"== {label}: {n} cells, c_inf read at {len(ok)}, arm " f"{len(arm)}, bars can fire at {len(fire)}") out = {} for tag, what, bad in tests: b = [x for x in ok if bad(x)] out[tag] = len(b) byp = {} for x in b: byp[x["p"]] = byp.get(x["p"], 0) + 1 print(f" {tag}: {what} at {len(b)} of {n}; arm " f"{sum(bad(x) for x in arm)} of {len(arm)}; where bars can fire " f"{sum(bad(x) for x in fire)} of {len(fire)}; by period " f"{dict(sorted(byp.items()))}") if b: print(" first (alpha, m, c_inf, c_ov, crude, c_form):", [(x["per"], x["m"], x["cinf"], x["cov"], x["bars"]["crude"], x["cf"]) for x in b[:8]]) rd = [x for x in rows if x["read"]] h1 = [x for x in rd if not x["keys"]] out["X4"] = len(h1) byp = {} for x in rd: byp[x["p"]] = byp.get(x["p"], 0) + 1 print(f" X4 (H1): no hull key in any piece at c_ov - 2 at {len(h1)} of " f"{len(rd)} read cells (by period {dict(sorted(byp.items()))}): " f"{[(x['per'], x['m']) for x in h1[:8]]}") out.update(n=n, ok=len(ok), arm=len(arm), fire=len(fire), read=len(rd)) return out def main(): t0 = time.time() only = int(sys.argv[1]) if len(sys.argv) > 1 else None old = [read(per, m, False) for per, m in strand_cells()[:only]] t1 = time.time() fam = family() if only: step = max(1, len(fam) // only) fam = fam[::step] X = [read(per, m, True) for per, m in fam] t2 = time.time() print("== CONTROLS") wset = {(tuple(per), m) for per in necklaces() for m in range(2, 13)} s136 = {(tuple(per), m) for _n, per in list(PERIODIC) + list(FRESH) for m in range(2, 10)} a1 = verdicts("(a) W", [x for x in old if (x["per"], x["m"]) in wset]) a2 = verdicts("(a) the 136", [x for x in old if (x["per"], x["m"]) in s136]) a3 = verdicts("(a) the 1017", old) d = [x for x in X if isinstance(x["cinf"], int) and x["cinf"] not in (x["cov2"] - 1, x["cov2"])] print(f" (b) THE PLANT c_ov's m doubled: X1's line fires at {len(d)} of " f"{len(X)}") rx = [x for x in X if x["read"]] pc = sum(not x["plant"] for x in rx) print(f" (c) THE PLANT Z_hi := Z_lo: X4's line fires at {pc} of " f"{len(rx)}") games = [] for per, ms in (((1, 1, 1, 2, 3), (7,)), ((1, 1, 1, 1, 2), (2, 3))): for m in ms: t3 = time.time() li = least(Field(per), m, "pin") g = game_cinf(per, m) games.append((per, m, li, g, round(time.time() - t3, 1))) print(f" (d) THE INSTRUMENT (alpha, m, induct.least, PinGame, s): " f"{games}; apart {sum(g[2] != g[3] for g in games)}") hp = None for x in rx: F = Field(x["per"]) hp = hull_arm(F, x["m"], x["c2"], plant=True) if hp[1]: break print(f" (e) THE PLANT d_max full - 1 on the HULL arm, first read cell " f"where it moves a node: {hp}") print("== THE HULL ARM at c_ov - 2 on X's read cells (TRANSPLANT check)") hn = sum(x["hull"][0] for x in rx) ho = [x for x in rx if x["hull"][1]] cn = sum(x["hull"][2] for x in rx) co_ = [x for x in rx if x["hull"][3]] print(f" nodes whose exact hull end != its form: " f"{sum(x['hull'][1] for x in rx)} of {hn}, at {len(ho)} cells: " f"{[(x['per'], x['m']) for x in ho[:8]]}") print(f" pinned-closure keys outside the forms' range: " f"{sum(x['hull'][3] for x in rx)} of {cn}, at {len(co_)} cells: " f"{[(x['per'], x['m']) for x in co_[:8]]}") mb = [(x["per"], x["m"], x["mono"]) for x in old + X if x["mono"]] print(f" (M) pinned at c, none at c + 1, c <= c_ov: at {len(mb)} cells " f"{mb[:4]}") print("== VERDICTS on X") v = verdicts("X", X) unread = [(x["per"], x["m"], x["cinf"]) for x in X if not isinstance(x["cinf"], int)] print(f" c_inf unread (None or limit) at {len(unread)}: {unread[:8]}") print("== BESIDE: stranded keys' kinds at c_ov - 2 on X") kinds = {} for x in rx: ks = set(k[3] for k in x["keys"]) for kd in ks: kinds[kd] = kinds.get(kd, 0) + 1 print(f" cells holding each kind: {dict(sorted(kinds.items()))}") for x in rx: if x["per"][:3] == (1, 1, 1) and x["p"] == 5 and ( (x["per"], x["m"]) in (((1, 1, 1, 2, 3), 7), ((1, 1, 1, 3, 3), 10), ((1, 1, 1, 3, 4), 10), ((1, 1, 1, 4, 3), 12))): ks = sorted(set(tuple(k) for k in x["keys"]))[:12] print(f" K1 {x['per']} x{x['m']} c {x['c2']} c_inf - c_ov " f"{x['cinf'] - x['cov']}: keys {ks}") if only: return closed = sum(any(k[3].startswith("closed") for k in x["keys"]) for x in rx) inner = sum(any(k[3].startswith("in") for k in x["keys"]) for x in rx) mkc = sum(any("-Kc" in k[3] for k in x["keys"]) for x in rx) zero = ("THE KILL", "X1", "X2", "X3", "beside") checks = [ (a1["n"], a1["arm"], a1["fire"]) == (1001, 106, 672), (a2["n"], a2["arm"], a2["fire"]) == (136, 17, 120), a3["n"] == 1017 and a3["read"] == 115 and a3["X4"] == 0 and all(a[k] == 0 for a in (a1, a2, a3) for k in zero), (len(d), len(X)) == (106, 7557), (pc, len(rx)) == (22, 788), [(g[2], g[3]) for g in games] == [(5, 5), (3, 3), (5, 5)], hp is not None and (hp[0], hp[1]) == (12, 8), (hn, sum(x["hull"][1] for x in rx), cn, sum(x["hull"][3] for x in rx)) == (13304, 0, 201139, 0), mb == [], (v["n"], v["ok"], v["arm"], v["fire"], v["read"]) == (7557, 7557, 826, 4737, 788) and all(v[k] == 0 for k in zero + ("X4",)), unread == [], (closed, inner, mkc) == (787, 788, 128), ] print(f" {sum(checks)}/{len(checks)} checks as recorded; 1017 " 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()