""" tie.py -- whether every pre-read at (s, s_0) = (0, 1) is a position of the pinned game: the fold behind c_saf <= c_inf. QUESTION. At a purely periodic alpha, x m, omega = 0, flush.py proves c_lo2 <= c_inf <= c_saf and prints c_inf = c_saf at 48 cells. The missing half: when every pinned state P_t is in the safety game's winning set W, is every initial state (every pre-read, all lifts)? DESIGN (written before this script). By Game.succ a branch's successor depends on g - e alone, so in a single-branch state g only positions the window of carries. THE FOLD: from P_t with t + c + 1 = kp, the opponent playing D_0 .. D_c at kp .. kp + c, the state at time kp holds the branch (y' + m D_0, .), (x', y') the branch at kp - 1; with y' = 0 it is one of the pre-read D's branches, with the same quotients, source state, pending digits and last-digit flag (position 0's cap a_1 - 1 + s_0 is the deep cap a_1), and W is upward closed in branch sets. Every state of the pinned game holds one branch (P_t holds one, and succ maps a branch to at most one), so a pre-read is COVERED, and in W, when a state reached from the winning P_t by W-moves (every reply in W) carries one of its branches and its quotients, source state, pending and flag. F at c = c_inf: covered / all pre-reads, per cell. F' the same, reached from the one P_t with t + c + 1 = 0 mod p in exactly c + 1 steps (the fold as derived, no free prefix). (1) side print, the flush's probe: from each initial state, along zero input and W-moves, is branch set {(0, 0)} with zeros pending reached? C0 c_inf (least c with every P_t in W, t = 1 .. 2p) and c_saf (least c with every initial state in W), recomputed here: c_saf = c_inf at every cell, and every P_t in W at c_inf + 1 (m <= 5). C1 at c_inf, each covered (pre-read, lift) pair's single-lift state in W, read in SingleGame (the pre-reads with one lift each, many of which lose); and every pre-read lost at c_inf - 1. C2 the zero pre-read covered at c_inf: P_p holds its key and its branch by construction, so C2 checks only that the two games pack a state alike. PLANT the cover test blind to the pending digits must break C1. At c_inf - 1 every P_t loses at every phase (P_t's only winning move is 0 and the zero reply is P_(t+1)), so nothing is reached there; a first run's control of that was vacuous and replaced by C1. PREDICTIONS (fixed before the run). F covers every pre-read at all 48 cells; (1) fails at no initial state. Kill of F as the mechanism: an uncovered pre-read, printed. FINDINGS (the --wide run, copied from its prints; the bare run reads m = 2 .. 5, 24 cells, F covering every pre-read at 23 of them). F KILLED as the mechanism. Every pre-read covered at 31 of 48 cells, 23 of the 24 at m <= 5; the exceptions start at golden x5 (c = 6: 18 of 21 covered), and coverage falls by m = 9 (golden x9 21 of 34, V2 x8 and x9 46 of 53, sqrt(3) - 1 x9 37 of 56). Of the 137 uncovered pre-reads all 137 have a winning single lift: a winning position, up to the two inert flags, that no pinned play reaches under winning moves. The twelve listed (golden x5, x6, x7) win by 1 or 2 lifts of 23 to 31, their pending digits opening 1. What is killed is the exact embedding; a reduction through positions shifted in g (a branch's successor depends on g - e alone, DESIGN) is not tested. F' covers every pre-read at 4 of 48 cells (golden x2, sqrt(3) - 1 x2 and x3, V1 x2), and part of them at the others. (1) every initial state reaches branch set {(0, 0)} with zeros pending along zero input, 0 failures at 48 cells: the flush on inputs ending within the pre-read; longer inputs are not tested. Controls: c_saf = c_inf at all 48 (C0); every pre-read lost at c_inf - 1 at 48 of 48; every covered (pre-read, lift) pair's single lift in W; the zero pre-read covered at 48 of 48 (by construction); the plant (cover blind to pending) broke C1 at 48 of 48. RUN RECORD. Default 13.2 s, peak 151.5 MB; --wide 77.8 s, peak 338.0 MB. The uncovered pre-reads' lift count over all of them, and the flush guard asking every zero reply, were added after an audit and both runs repeated. The FINDINGS entered with this script's first record; a later bare run reprinted their m <= 5 part, and the --wide part stands as first recorded. A first bare run's control (nothing covered at c_inf - 1) read nothing, every P_t losing there, and its plant went uncaught; replaced by C1 before any verdict. A first --wide run was refused at a 512 MB ceiling holding two pinned games; the run now holds one game at a time and reads C0's c_inf + 1 at m <= 5 only. Usage: python tie.py [--wide] (--wide adds m = 6 .. 9) """ import os import sys import time os.environ.setdefault("OPENBLAS_NUM_THREADS", "1") from flush import Game, PinGame, Source, PERIODIC # noqa: E402 WIDE = "--wide" in sys.argv CHECKS = [] def check(name, ok, detail=""): CHECKS.append(ok) print(f" [{'PASS' if ok else 'FAIL'}] {name}" + (f": {detail}" if detail else "")) def wmoves(g, i): return [succ for _nz, succ in g.trans[i].values() if all(j in g.W for j in succ)] def reached(g, starts, steps=None): """States reached from the starts in W by W-moves, every reply taken; with steps, only those at exactly that depth.""" layer = {i for i in starts if i in g.W} seen = set(layer) depth = 0 while layer and (steps is None or depth < steps): nxt = set() for i in layer: for succ in wmoves(g, i): nxt.update(succ) depth += 1 layer = nxt if steps is not None else nxt - seen seen |= nxt return layer if steps is not None else seen def key(st, blind=False): return (st[1], st[2], st[4]) if blind else (st[1], st[2], st[3], st[4]) class SingleGame(Game): """The pre-reads with one lift each.""" def initial(self): return [((b,),) + st[1:] for st in Game.initial(self) for b in st[0]] def index(pg, states, blind=False): """{key: the branches of the states in `states` (of pg) with it}.""" idx = {} for j in states: st = pg.states[j] idx.setdefault(key(st, blind), set()).update(st[0]) return idx def pairs(inits, idx, blind=False): """{index into inits (initial state tuples): its branches carried by an indexed state with its quotients, source state, pending and flag}.""" out = {} for i, st in enumerate(inits): hit = idx.get(key(st, blind), set()) & set(st[0]) if hit: out[i] = hit return out def single_bad(inits, sg, prs): """Covered (pre-read, lift) pairs whose single-lift state loses.""" return sum(sg.ids[((b,),) + inits[i][1:]] not in sg.W for i, hit in prs.items() for b in hit) def flushes(g): """The states of W from which zero input and W-moves reach branch set {(0, 0)} with zeros pending.""" good = {i for i in g.W if g.states[i][0] == (g.zero,) and not any(g.states[i][3])} grew = True while grew: grew = False for i in g.W: if i in good: continue for nz, succ in g.trans[i].values(): # the zero replies come first, nz of them if nz and all(j in g.W for j in succ) and all( j in good for j in succ[:nz]): good.add(i) grew = True break return good def main(): t0 = time.time() maps = (2, 3, 4, 5) + ((6, 7, 8, 9) if WIDE else ()) cells = c0bad = c1bad = soundbad = c2bad = plant = 0 nunc = unc_won = 0 full = fullp = flushbad = 0 uncovered = [] print("== F the fold at (0, 1): pre-reads covered by the pinned game") for name, per in PERIODIC: p = len(per) src = Source(period=per) ts = list(range(1, 2 * p + 1)) row = [] for m in maps: cinf = None 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): cinf = c break del pg reach = reached(pg, pg.init) idx, idxb = index(pg, reach), index(pg, reach, blind=True) t_f = [t for t in ts if (t + cinf + 1) % p == 0][0] idxp = index(pg, reached(pg, [pg.init[ts.index(t_f)]], steps=cinf + 1)) del pg, reach if m <= 5: nxt = PinGame(src, m, cinf + 1, ts) nxt.solve(False) c0bad += not all(i in nxt.W for i in nxt.init) del nxt g = Game(src, m, 0, 1, cinf - 1) g.solve(False) c0bad += g.wins c1bad += any(i in g.W for i in g.init) del g # c_inf: F, F', (1), C1, C2, the plant; one game held at a time g = Game(src, m, 0, 1, cinf) g.solve(False) c0bad += not g.wins ids = sorted(set(g.init)) inits = [g.states[i] for i in ids] zi = g.start_state([0] * (cinf + 2), [per[k % p] for k in range(cinf + 2)]) zpos = ids.index(zi) fl = flushes(g) flushbad += sum(i not in fl for i in ids) del g, fl prs = pairs(inits, idx) blind = pairs(inits, idxb, blind=True) covp = set(pairs(inits, idxp)) cov = set(prs) sg = SingleGame(src, m, 0, 1, cinf) sg.solve(False) soundbad += single_bad(inits, sg, prs) plant += single_bad(inits, sg, blind) > 0 c2bad += zpos not in cov n = len(inits) full += len(cov) == n fullp += len(covp) == n for i in sorted(set(range(n)) - cov): st = inits[i] won = sum(sg.ids[((b,),) + st[1:]] in sg.W for b in st[0]) nunc += 1 unc_won += won > 0 uncovered.append((name, m, cinf, st[3], st[4], won, len(st[0]))) cells += 1 row.append(f"x{m} c{cinf} {len(cov)}/{len(covp)}/{n}") del sg print(f" {name:20s} " + " ".join(row), flush=True) print(f" (c_inf, covered by F / by F' / pre-reads) F covers all at " f"{full} of {cells} cells, F' at {fullp} of {cells}") for u in uncovered[:12]: print(f" uncovered: {u[0]} x{u[1]} c = {u[2]} pending {u[3]} " f"last zero {u[4]}, single lifts winning {u[5]} of {u[6]}") print(f" uncovered pre-reads: {nunc}, with a winning single lift: " f"{unc_won}") print(f" (1) initial states not flushing along zero input: " f"{flushbad}") check("C0: c_saf = c_inf here, and every P_t in W at c_inf + 1 too " "(m <= 5)", c0bad == 0, f"{c0bad} off") check("C1: every pre-read lost at c_inf - 1", c1bad == 0, f"{c1bad} of {cells} cells") check("C1: every covered (pre-read, lift) pair's single-lift state " "in W", soundbad == 0, f"{soundbad} not") check("C2: the zero pre-read covered at c_inf", c2bad == 0, f"{c2bad} of {cells}") check("plant: the cover test blind to pending breaks C1", plant > 0, f"at {plant} of {cells} cells") print(f" {sum(CHECKS)}/{len(CHECKS)} checks, {time.time() - t0:.1f} s") sys.exit(0 if all(CHECKS) else 1) if __name__ == "__main__": main()