tie.py
Cited on: FLUSH.
To run it: save tie.py, with flush.py, ostrowski.py beside it; standard library only.
"""
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()