induct.py
Checks: FLUSH: The cylinder bound theorem.
Cited on: FLUSH.
To run it: save induct.py, with flush.py, ostrowski.py, tie.py beside it; standard library only.
"""
induct.py -- the window's induction on the keys a play reaches, as an
exact check with no game solve: c_inf and c_saf at (s, s_0) = (0, 1)
from the window alone.
QUESTION. tie.py prints that at c_inf an after-move key (G, H, f, t)
the box holds wins iff its offset y = H - G r_t lies in the closed
valid range (its target u + m R inside the window I_(t+1)), and that
on the whole real range the window is not inductive (golden x2, c = 3:
offsets in (phi^-6, 2 phi^-6) have no valid move after the zero
reply). Is the carry, the integer G, what makes it inductive, and is
then c_inf the least c at which the window is inductive on the keys a
play reaches, with no game solved?
DESIGN (frozen before the engine). Conventions: a_j = per[(j - 1) %
p], r_t = |theta_t / theta_(t-1)| = [0; a_(t+1), ...] (exact, in the
quadratic field of alpha), sign theta_k = (-1)^k. THE CARRY: along any
play Q = G q_t + H q_(t-1) = m N_(<=t+c) - E_(<=t) (the lift drops
out, q_(-1) = 0), so G = |theta_(t-1)| Q - kappa_t y, kappa_t = q_(t-1)
|theta_(t-1)|, and -|theta_(t-1)| (q_(t+1) + q_t - 1) <= G + kappa_t y
<= m |theta_(t-1)| (q_(t+c+1) - 1), no box. THE MAP: from after-move
(G, H) at phase t, the reply d (cap a_(t+c+2), less 1 off the full
flag) gives the pre-move key (H + m d U, G - a_(t+1) H + m d V) at t +
1, theta_(t+c+1) = U theta_(t+1) + V theta_t; the move e' <= a_(t+2)
subtracts e' from G; the flag is d = 0. S(c): the forward closure,
under every reply and every valid move, of a start set. WI: every key
of S, every reply, has a valid move. Start sets: PIN, each phase's
pinned key (0, 0), full, its valid moves; PRE, every pre-read's valid
landings (m N - e, H) at phase 0, e <= a_1, H any integer (COVER: each
pre-read has one). A valid play keeps a bounded carry, so WI on S_PIN
with PIN's moves puts every P_t in W, and WI on S_PRE with COVER every
pre-read, given S inside the box.
PREDICTIONS (frozen). c_pin (least c with PIN's moves and WI on
S_PIN) = c_inf and c_pre (least c with COVER and WI on S_PRE) = c_inf
at all 48 cells, c_inf the pinned game's. S inside the games' held
after-move keys, every key of S winning there. KILL: "c_pre != c_inf
at n cells" or "c_pin != c_inf at n cells", n > 0.
CONTROLS (read before the verdict).
(a) the map against the game: every single-branch successor's
tentative key (flush.py) equals the map's, over the single-lift
game at c_inf (m <= 5), and every pre-read's key is (m N, h + m
sum_(j>=1) d_j p_j);
(b) THE CARRY REMOVED: WI over every lattice key with valid y and
|G| <= 30 at c_inf must fail at golden x2;
(c) THE PLANT: the valid range widened by 0.02 at both ends puts
held losing keys in S_PRE at some cell;
(d) the carry bound holds at every key of S (sup over t <= 40 p).
FINDINGS (the --wide run, copied from its prints; the bare run, m = 2
.. 5, prints the same 24 rows).
KILL MISSED. c_pin != c_inf at 0 cells, c_pre != c_inf at 0 cells,
of 48: the window, checked exactly on a finite closure (|S_PRE|
8 at golden x2 to 1400 at V2 x9), is inductive at c_inf and
fails at c_inf - 1 (golden x2, c = 2: the key (3, 2), reduced,
phase 0, has no valid move after the zero reply; the bare run's
silver x2 lacks a pinned move). No game is solved for either
column.
INSIDE THE GAMES. Every key of S_PIN is held by the pinned game and
every key of S_PRE by the single-lift game, none losing there; no
pre-read needs a lift outside the box. SOUNDNESS: a play valid
at every step keeps y in the valid range, so sigma = G theta_t +
H theta_(t-1) = +-|theta_(t-1)| y and the pending digits' O(m
|theta_t|) tend to 0, its output codes m x + M and it is a
completion reader, with no box; flush.py's (6), a completion
reader plays safe (at omega = 0, s_0 <= s + 1), so WI and COVER
at c make every pre-read safe at c, and c_saf <= c_inf at each of
the 48 cells rests on this exact check and (6). "Held" is read
over single-branch states, by key.
TWIN (added after the frozen run). S_PIN lies inside S_PRE at all 48
cells, and S_PRE adds at most one key per cell, at 28 of them,
always a phase-0 landing on the reduced flag whose full twin is
in S_PIN. A reduced key's replies are a subset of its full twin's,
landing on the same keys, so WI on S_PRE follows from WI on S_PIN:
at a cell, c_saf <= c_inf comes down to every valid landing lying
in S_PIN or a twin of one.
THE CARRY. G >= 0 at every key of S; its top runs 9 (golden x2) to
3237 (bronze x9); (d) 0 violations of the bound, which allows
G < 0 where S has none. Removed, the one
step (every lattice key with valid y and |G| <= 30 has a valid
move after each reply, its successor not followed) fails at 3 of
48 cells: golden x2 (6 keys), V1 x2 and V1 x3; at |G| <= 300 at
6 (those, silver x2, bronze x3, V2 x4), none at m >= 6. A one
step does not show the lattice inductive where it passes. By hand,
golden x2, c = 3, after the zero reply: e' = 0 needs y <= phi^-6,
e' = 1 needs y >= 2 phi^-6, and the one lattice key between with
|G| <= 25 is G = -5, H = -3, below the carry's floor.
Controls: (a) 0 off of 997301 successors and pre-read keys (m <= 5,
at c_inf; the pre-read clause added with the engine, beyond the
freeze); (c) the widened range puts 1174 held losing keys in S_PRE at
45 of 48 cells: keys outside the valid range, which VALID says lose,
so it reads the matching of keys to the game, not an interior end.
RUN RECORD. Bare 9.5 s, peak 78 MB; --wide 56.0 s, peak 232 MB. The
TWIN print and (b)'s |G| <= 300 arm were added after
the first --wide run, whose rows and checks the later runs reprinted
unchanged.
Usage: python induct.py [--wide] (--wide adds m = 6 .. 9)
"""
import math
import os
import sys
import time
from fractions import Fraction as Fr
os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
from flush import PinGame, Source, PERIODIC, real_ratios, \
conj_ratios # noqa: E402
from tie import SingleGame, key1 # noqa: E402
WIDE = "--wide" in sys.argv
CHECKS = []
EPS = 1e-9
def check(name, ok, detail=""):
CHECKS.append(ok)
print(f" [{'PASS' if ok else 'FAIL'}] {name}" + (f": {detail}"
if detail else ""))
class QF:
"""a + b sqrt(D), a and b rational; D fixed per alpha."""
D = None
__slots__ = ("a", "b", "f")
def __init__(self, a, b=0):
self.a, self.b = Fr(a), Fr(b)
self.f = float(self.a) + float(self.b) * math.sqrt(QF.D)
def __add__(self, o):
o = o if isinstance(o, QF) else QF(o)
return QF(self.a + o.a, self.b + o.b)
def __sub__(self, o):
o = o if isinstance(o, QF) else QF(o)
return QF(self.a - o.a, self.b - o.b)
def __mul__(self, o):
if not isinstance(o, QF):
return QF(self.a * o, self.b * o)
return QF(self.a * o.a + self.b * o.b * QF.D,
self.a * o.b + self.b * o.a)
def sign(self):
a, b = self.a, self.b
if b == 0 or a == 0:
return (a > 0) - (a < 0) if b == 0 else (b > 0) - (b < 0)
if (a > 0) == (b > 0):
return 1 if a > 0 else -1
bigger_a = a * a > b * b * QF.D
return (1 if a > 0 else -1) if bigger_a else (1 if b > 0 else -1)
def le(x, y):
"""x <= y exactly, x and y QF; floats decide when far apart."""
d = y.f - x.f
if d > 1e-7:
return True
if d < -1e-7:
return False
return (y - x).sign() >= 0
class Field:
"""The exact ratios r_t and the quantities of one alpha."""
def __init__(self, per):
self.per, p = per, len(per)
self.p = p
rs, D = [], None
for t in range(p):
M = [[1, 0], [0, 1]]
for j in range(t + 1, t + p + 1):
a = per[(j - 1) % p]
M = [[M[0][0] * a + M[0][1], M[0][0]],
[M[1][0] * a + M[1][1], M[1][0]]]
(P, P1), (Q, Q1) = M
d = (P - Q1) ** 2 + 4 * Q * P1
assert D is None or d == D
D = d
rs.append((Fr(-(P - Q1), 2 * P1), Fr(1, 2 * P1)))
QF.D = D
self.r = [QF(a, b) for a, b in rs]
for x, y in zip(self.r, real_ratios(per)):
assert abs(x.f - y) < 1e-12
def a(self, j):
return self.per[(j - 1) % self.p]
def uv(self, t, c):
"""theta_(t+c+1) = U theta_(t+1) + V theta_t."""
lo, hi = (0, 1), (1, 0) # theta_t, theta_(t+1)
for k in range(t + 1, t + c + 1):
a = self.a(k + 1)
lo, hi = hi, (a * hi[0] + lo[0], a * hi[1] + lo[1])
return hi
def valid(self, t, f, m, c, widen=0):
p = self.p
def P(k):
out = QF(1)
for i in range(k + 1):
out = out * self.r[(t + i) % p]
return out
def neg_th(k):
return P(k) * ((-1) ** k)
w = sorted((neg_th(0), neg_th(1)), key=lambda x: x.f)
lo, hi = neg_th(c), neg_th(c + 1)
R = sorted((lo, hi) if f else (hi, lo + hi), key=lambda x: x.f)
dw = QF(Fr(widen))
return (w[0] - R[0] * m - dw, w[1] - R[1] * m + dw)
class Window:
"""The key game of one cell at lookahead c."""
def __init__(self, F, m, c, widen=0):
self.F, self.m, self.c, p = F, m, c, F.p
self.V = {(t, f): F.valid(t, f, m, c, widen)
for t in range(p) for f in (True, False)}
self.UV = [F.uv(t, c) for t in range(p)]
def y(self, G, H, t):
return QF(H) - self.F.r[t] * G
def ok(self, G, H, f, t):
lo, hi = self.V[(t, f)]
yf = H - G * self.F.r[t].f
if lo.f + EPS < yf < hi.f - EPS:
return True
if yf < lo.f - EPS or yf > hi.f + EPS:
return False
y = self.y(G, H, t)
return le(lo, y) and le(y, hi)
def replies(self, f, t):
cap = self.F.a(t + self.c + 2)
return range(cap + 1 if f else cap)
def pre(self, G, H, t, d):
"""After-move (G, H) at phase t, reply d: the pre-move key at
phase t + 1."""
U, V = self.UV[t]
m = self.m
return H + m * d * U, G - self.F.a(t + 1) * H + m * d * V
def moves(self, G1, H1, f, t1):
"""The valid after-move keys of the pre-move key at phase t1."""
cap = self.F.a(t1 + 1)
return [(G1 - e, H1) for e in range(cap + 1)
if self.ok(G1 - e, H1, f, t1)]
def closure(self, starts, limit=400000):
"""(WI holds, S, a failing key or None)."""
p = self.F.p
S = set(starts)
todo = list(S)
bad = None
while todo:
G, H, f, t = todo.pop()
t1 = (t + 1) % p
for d in self.replies(f, t):
G1, H1 = self.pre(G, H, t, d)
mv = self.moves(G1, H1, d == 0, t1)
if not mv and bad is None:
bad = (G, H, f, t, d)
for (G2, H2) in mv:
k = (G2, H2, d == 0, t1)
if k not in S:
S.add(k)
todo.append(k)
if len(S) > limit:
raise RuntimeError("closure past its limit")
return bad is None, S, bad
def pin_starts(self):
out, missing = [], 0
for t in range(self.F.p):
mv = self.moves(0, 0, True, t)
missing += not mv
out += [(G, H, True, t) for G, H in mv]
return out, missing
def prereads(self):
"""Every legal pre-read d_0 .. d_c: (digits, N, pend_p)."""
F, c = self.F, self.c
q = [1, F.a(1)]
pp = [0, 1]
for k in range(1, c + 1):
q.append(F.a(k + 1) * q[k] + q[k - 1])
pp.append(F.a(k + 1) * pp[k] + pp[k - 1])
out = []
def rec(digs, lastzero):
k = len(digs)
if k == c + 1:
N = sum(d * q[j] for j, d in enumerate(digs))
P = sum(d * pp[j] for j, d in enumerate(digs) if j >= 1)
out.append((tuple(digs), N, P))
return
a = F.a(k + 1)
top = a - 1 if k == 0 else (a if lastzero else a - 1)
for d in range(top + 1):
rec(digs + [d], d == 0)
rec([], True)
return out
def landings(self, N, f):
"""The valid after-move keys (m N - e, H) at phase 0."""
lo, hi = self.V[(0, f)]
r0 = self.F.r[0]
out = []
for e in range(self.F.a(1) + 1):
G = self.m * N - e
base = r0 * G
for H in range(math.floor((lo + base).f) - 1,
math.ceil((hi + base).f) + 2):
if self.ok(G, H, f, 0):
out.append((G, H))
return out
def pre_starts(self, by=None):
out, missing, boxed = [], 0, 0
for digs, N, P in self.prereads():
f = digs[-1] == 0
ks = self.landings(N, f)
missing += not ks
if by is not None and ks and all(
abs(H - self.m * P) > by for _G, H in ks):
boxed += 1
out += [(G, H, f, 0) for G, H in ks]
return out, missing, boxed
def carry_bounds(F, m, c, T):
"""[(t mod p, lower(t), upper(t), kappa_t)] for t = 0 .. T: the carry
G + kappa_t y between lower and upper."""
q = {-1: 0, 0: 1}
th = {-1: 1.0}
r = [x.f for x in F.r]
for k in range(0, T + c + 3):
q[k + 1] = F.a(k + 1) * q[k] + q[k - 1]
th[k] = th[k - 1] * r[k % F.p]
out = []
for t in range(T + 1):
out.append((t % F.p, -th[t - 1] * (q[t + 1] + q[t] - 1),
m * th[t - 1] * (q[t + c + 1] - 1), q[t - 1] * th[t - 1]))
return out
def carry_bad(S, F, bounds):
bad = 0
for G, H, _f, t in S:
y = H - G * F.r[t].f
if not any(ph == t and lo - 1e-9 <= G + k * y <= hi + 1e-9
for ph, lo, hi, k in bounds):
bad += 1
return bad
def after_keys(g, Z):
"""{after-move key: in W} over g's single-branch states."""
out = {}
for i, st in enumerate(g.states):
if len(st[0]) != 1:
continue
G, H, f, ph = key1(g, st, Z)
for e, (_nz, succ) in g.trans[i].items():
out[(G - e, H, f, ph)] = all(j in g.W for j in succ)
return out
def map_bad(sg, Z, win, F):
"""Control (a): successors' keys against the map; pre-read keys."""
bad = n = 0
for i, st in enumerate(sg.states):
G, H, f, ph = key1(sg, st, Z)
for e in sg.trans[i]:
for a_new, src2, d in sg.replies(st):
st2 = sg.succ(st, e, a_new, src2, d)
n += 1
want = win.pre(G - e, H, ph, d) + (d == 0,
(ph + 1) % F.p)
bad += key1(sg, st2, Z) != want
q = [1, F.a(1)]
pp = [0, 1]
for k in range(1, sg.look + 1):
q.append(F.a(k + 1) * q[k] + q[k - 1])
pp.append(F.a(k + 1) * pp[k] + pp[k - 1])
for i in set(sg.init):
st = sg.states[i]
x, h = divmod(st[0][0], sg.K)
x, h = x - sg.bx, h - sg.by
digs = (x // sg.m,) + st[3]
N = sum(d * q[j] for j, d in enumerate(digs))
P = sum(d * pp[j] for j, d in enumerate(digs) if j >= 1)
n += 1
bad += key1(sg, st, Z)[:2] != (sg.m * N, h + sg.m * P)
return bad, n
def lattice_bad(win, F, G_max=30):
"""Control (b): lattice keys with valid y and |G| <= G_max lacking a
valid move after some reply."""
bad = 0
for t in range(F.p):
for f in (True, False):
lo, hi = win.V[(t, f)]
for G in range(-G_max, G_max + 1):
base = F.r[t] * G
for H in range(math.floor((lo + base).f) - 1,
math.ceil((hi + base).f) + 2):
if not win.ok(G, H, f, t):
continue
for d in win.replies(f, t):
G1, H1 = win.pre(G, H, t, d)
if not win.moves(G1, H1, d == 0, (t + 1) % F.p):
bad += 1
break
return bad
def least(F, m, kind, cmax=13):
for c in range(cmax + 1):
w = Window(F, m, c)
if kind == "pin":
st, miss = w.pin_starts()
else:
st, miss, _b = w.pre_starts()
if miss:
continue
ok, _S, _bad = w.closure(st)
if ok:
return c
return None
def main():
t0 = time.time()
maps = (2, 3, 4, 5) + ((6, 7, 8, 9) if WIDE else ())
rows = []
cells = pin_off = pre_off = 0
ctl_a = ctl_a_n = 0
lat_cells, lat_golden2, lat300 = [], None, []
plant_hit = plant_cells = 0
carry_viol = 0
unheld_pre = unheld_pin = lose_pre = lose_pin = 0
boxed_all = 0
sub_bad = extra_max = twin_bad = extra_cells = 0
witnesses = []
for name, per in PERIODIC:
F = Field(per)
p = F.p
src = Source(period=per)
Z = conj_ratios(per)
ts = list(range(1, 2 * p + 1))
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
c_pin = least(F, m, "pin")
c_pre = least(F, m, "pre")
pin_off += c_pin != cinf
pre_off += c_pre != cinf
win = Window(F, m, cinf)
by = pg.by
pst, _mp = win.pin_starts()
_okp, S_pin, _bp = win.closure(pst)
prst, _mr, boxed = win.pre_starts(by)
_okr, S_pre, _br = win.closure(prst)
boxed_all += boxed
extra = S_pre - S_pin
sub_bad += not S_pin <= S_pre
extra_max = max(extra_max, len(extra))
extra_cells += bool(extra)
twin_bad += sum(f or t != 0 or (G, H, True, 0) not in S_pin
for G, H, f, t in extra)
bounds = carry_bounds(F, m, cinf, 40 * p)
carry_viol += carry_bad(S_pin | S_pre, F, bounds)
# the pinned game's held keys
ak = after_keys(pg, Z)
unheld_pin += sum(k not in ak for k in S_pin)
lose_pin += sum(ak.get(k) is False for k in S_pin)
del pg, ak
# the single-lift game: held keys, control (a), the plant
sg = SingleGame(src, m, 0, 1, cinf)
sg.solve(False)
ak = after_keys(sg, Z)
unheld_pre += sum(k not in ak for k in S_pre)
lose_pre += sum(ak.get(k) is False for k in S_pre)
if m <= 5:
b, n = map_bad(sg, Z, win, F)
ctl_a += b
ctl_a_n += n
pw = Window(F, m, cinf, widen=Fr(1, 50))
pps, _pm, _pb = pw.pre_starts()
_ok, S_w, _bw = pw.closure(pps)
hit = sum(ak.get(k) is False for k in S_w)
plant_hit += hit
plant_cells += hit > 0
del sg, ak
lb = lattice_bad(win, F)
if lb:
lat_cells.append(f"{name.split()[0]} x{m}")
if lattice_bad(win, F, 300):
lat300.append(f"{name.split()[0]} x{m}")
if name.startswith("golden") and m == 2:
lat_golden2 = lb
if cinf >= 1 and len(witnesses) < 6:
wl = Window(F, m, cinf - 1)
st, miss = wl.pin_starts()
okl, _S, badk = wl.closure(st) if not miss else (False,
None, None)
witnesses.append(f" {name:20s} x{m} c = {cinf - 1}: "
f"pinned moves missing at {miss} phases, "
f"WI {'holds' if okl else 'fails'}"
+ (f" at key (G, H, f, t, reply) = {badk}"
if badk else ""))
Gs = [k[0] for k in S_pre]
rows.append(f" {name:20s} x{m} c_inf {cinf} c_pin {c_pin}"
f" c_pre {c_pre} |S_PIN| {len(S_pin)} |S_PRE| "
f"{len(S_pre)} G in [{min(Gs)}, {max(Gs)}]")
cells += 1
print(f" ... {name} done, {time.time() - t0:.1f} s", flush=True)
print("== WI + COVER: c_inf from the window's induction on the keys a "
"play reaches")
print("\n".join(rows))
print(" at c_inf - 1 (the first cells):")
print("\n".join(witnesses))
check("(a) the key map equals the game's successors and pre-read "
"keys (m <= 5)", ctl_a == 0 and ctl_a_n > 0,
f"{ctl_a} off of {ctl_a_n}")
check("(b) the carry removed (|G| <= 30): WI fails at golden x2",
bool(lat_golden2), f"{lat_golden2} failing keys there; cells "
f"failing: {len(lat_cells)} of {cells} ({', '.join(lat_cells)})")
print(f" (b) one step at |G| <= 300: cells failing {len(lat300)} of "
f"{cells} ({', '.join(lat300)})")
check("(c) the plant: the range widened by 0.02 puts held losing keys "
"in S_PRE", plant_hit > 0,
f"{plant_hit} keys at {plant_cells} of {cells} cells")
check("(d) the carry bound at every key of S", carry_viol == 0,
f"{carry_viol} violations")
print(f" S_PIN keys the pinned game does not hold: {unheld_pin}; "
f"held and losing: {lose_pin}")
print(f" S_PRE keys the single-lift game does not hold: "
f"{unheld_pre}; held and losing: {lose_pre}")
print(f" pre-reads whose every valid landing needs a lift outside "
f"the box: {boxed_all}")
print(f" TWIN: cells with S_PIN not inside S_PRE: {sub_bad}; keys of "
f"S_PRE off S_PIN at most {extra_max} per cell, at {extra_cells} "
f"cells, of them not a "
f"phase-0 reduced twin of a full key of S_PIN: {twin_bad}")
print(f" c_pin != c_inf at {pin_off} cells")
print(f" c_pre != c_inf at {pre_off} cells")
print(f" {sum(CHECKS)}/{len(CHECKS)} checks, {cells} cells, "
f"{time.time() - t0:.1f} s")
sys.exit(0 if all(CHECKS) else 1)
if __name__ == "__main__":
main()