""" 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()