""" hull.py -- the pinned closure against the carry's contracting coordinate: the tops are not the bound's, but the window is inductive on the bound's whole set at c_inf. QUESTION. saturate.py prints that at c_inf the pinned closure S_PIN (induct.py) is, per phase t and flag f, every valid key with G in [G_lo, G_top](t, f), the ends read off the closure. Along a play Z = G + kappa_t y, the limit of |theta_(t-1)| Q, contracts: Z' = r_t Z + m d A_t - e B_t, e >= 0, B_t > 0. Dropping e bounds Z by the fixed point Z_hi(t, f) of a max-affine contraction. Is G_top(t, f) = T(t, f), the greatest G with a valid key (G, H) and G + kappa_t y <= Z_hi(t, f), at every row? DESIGN (frozen before the engine). Z(G, H; t) = lambda_t G + kappa_t H, kappa_t = s_t / (1 + r_t s_t), s_t = [0; a_t, a_(t-1), ...] (the limit of q_(n-1)/q_n, t = n mod p), lambda_t = 1 - kappa_t r_t, all exact in the quadratic field. A_t = lambda_(t+1) U_t + kappa_(t+1) V_t (the reply's step m d (U, V)), B_t = lambda_(t+1) (the move's step -e on G). THE HULL: Z_hi(t+1, R) = max over f with d_max(f) >= 1 of r_t Z_hi(t, f) + m d_max(f) A_t, d_max(full) = a_(t+c+2), d_max(reduced) = a_(t+c+2) - 1; Z_hi(t+1, F) = max(r_t max_f Z_hi(t, f), the pinned starts' Z at t+1); solved exactly on the policy a float iteration picks, the policy then checked exactly (Bellman). c_inf is induct.py's c_pin, equal to the pinned game's at all 48 cells (induct.py), so no game is solved. PREDICTION: T = G_top at every (t, f) row of the 48 cells. KILL: "T != G_top at n of N (t, R) rows" or "... (t, F) rows", n > 0 on either. A row with T < G_top is an instrument fault (the bound is proved), printed apart. THE LOW SIDE (no kill; predicted loose): the hull with d_min and e_max = a_(t+2) gives Z_lo, and G_lo's hull value is the least G with a valid key and Z >= Z_lo. CONTROLS: (a) Z's linear part, kappa_(t+1) = r_t lambda_t and lambda_(t+1) - a_(t+1) kappa_(t+1) = r_t kappa_t, exact at every phase; A_t > 0; kappa_t, lambda_t, A_t against q_(n-1) |theta_(n-1)|, q_n |theta_(n-1)|, q_(n+c+1) |theta_n| at n near 40 p; (b) THE BOUND: every key of S has Z <= Z_hi(t, f), exactly; (c) THE PLANT: d_max(full) lowered by 1 must put keys of S above the planted Z_hi at some cell and its T below G_top at some row. SECOND QUESTION, HULL-WI (frozen after the first verdict, before its engine). A move's validity reads the offset alone: y' = -y / r_t + m d (V_t - U_t r_(t+1)) + e r_(t+1), G's coefficient 1 - (a_(t+1) + r_(t+1)) r_t being 0. THE HULL SET H(c): every valid key with Z_lo <= Z <= Z_hi, closed under every reply and valid move by the fixed points' Bellman inequalities, holding the pinned starts, so S_PIN(c) inside H(c) and c_hull (least c with the pinned moves and WI on H(c)) >= c_inf. PREDICTION: c_hull = c_inf at all 48 cells; every pre-read's valid landing in H(c_inf). KILL: "c_hull != c_inf at n of 48 cells" or "landings outside H(c_inf)" > 0. CONTROLS: (a) the WI routine on S_PIN gives c_inf; (b) S_PIN(c_inf) inside H(c_inf); (c) THE PLANT, in the kill's direction: Z_lo lowered by 3 at golden x2, c = 3, admits the key (-5, -3), whose offset has no valid move after the zero reply, and must fail. FINDINGS (the --wide run, copied from its prints). KILL FIRED. T != G_top at 104 of 104 (t, R) rows and at 100 of 104 (t, F) rows; T - G_top is 1 at 84, 2 at 15, 3 at 5 reduced rows, and 0 at 4, 1 at 72, 2 at 17, 3 at 11 full rows (golden x2: T 10 against G_top 9 at t0R, Z_hi 9.9193; T 6 against 5 at t0F). T < G_top at 0 rows. The bound dropping e is loose by 0 to 3 carries at the top (1 to 3 at 204 of 208 rows): e >= 0 alone is not enough; what the bound misses (moves the window forces, a sup not attained, the lattice's grain) is not separated. THE HULL IS THE CARRY'S LIMIT. Z_hi(t, R) equals the carry bound's max over the last 3 p of t <= 40 p, m |theta_(t-1)| (q_(t+c+1) - 1), at 104 of 104 (t, R) rows: the bound with e dropped is the limit the carry bound tends to. On the full flag Z_hi is far below it (golden x2: 6.13 against 9.92). THE LOW SIDE. G_lo - the low hull's value is 1 to 4 on the reduced flag and 2 to 4 on the full flag over the 104 rows each, 0 at none: the crude floor (d_min, e_max) is loose on both flags. CONTROLS. (a) 0 exact failures of Z's linear part, A > 0 and B > 0; kappa, lambda and A against q |theta| at n near 40 p, worst 2.2e-12; 0 Bellman failures of the exact fixed points. (b) 0 of 17983 keys of S with Z > Z_hi. (c) the plant puts keys of S above it at 48 of 48 cells and its T below G_top at 208 of 208 rows: (b) can fire. HULL-WI, KILL MISSED. c_hull != c_inf at 0 of 48 cells; valid landings outside H(c_inf): 0; pre-reads with no valid landing at c_inf: 0. H(c_inf) holds 3 to 20 keys beyond S_PIN (470 over the 48 cells), and the window is inductive on them all. So at each cell c_pin = c_inf is the least c at which the window is inductive on a set cut out by the window and two exact inequalities on Z, no closure grown and no game solved, and with COVER, the landings inside, the fixed points' Bellman certificates and the completion reader's theorem, c_saf <= c_inf rests on that check. HULL-WI CONTROLS. (a) the WI routine on S_PIN gives c_inf at 48 of 48. (b) H(c_inf) holds S_PIN(c_inf) at 48 of 48. (c) Z_lo - 4 at golden x2 adds 4 keys, (-5, -3) among them, and WI fails first at (-5, -3, full, t 0) under the zero reply: the kill can fire. (d) successors of keys of H(c_inf) outside it: 0 (the closure, proved, read directly; no plant shows that print can fire). RUN RECORD. Bare 0.5 s, --wide 1.0 s. The first bare run broke on the plant at golden (d_max(full) - 1 = 0 leaves the reduced node with no predecessor); such a node now takes a constant far below every key. The OVERSHOOT print was added after the bare run, before the --wide one. HULL-WI: bare 0.7 s, --wide 1.9 s. Its frozen plant, Z_lo - 3, missed (-5, -3) (Z_lo(0, full) = -1.894, the key's Z = -4.960); it was resized to Z_lo - 4 after the bare run, before the verdict was read. COVER and (d) were added after the first --wide run, which printed the kill and (a) to (c) as now. The landing kill as first frozen counted cells; this DESIGN and the print count landings and list their cells. Added to the frozen DESIGN after the verdict, with no change to the run: "c_inf is induct.py's c_pin" and the plant's frozen amount "by 3". The Bellman count at every c stage_wi solves, and the label "max over the last 3 p" (it read "sup over t <= 40 p"), were added after the verdict: 0 failures, the rows unchanged. Usage: python hull.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 PERIODIC # noqa: E402 from induct import Field, Window, least, QF, le, carry_bounds # noqa: E402 WIDE = "--wide" in sys.argv def inv(x): n = x.a * x.a - x.b * x.b * QF.D return QF(x.a / n, -x.b / n) def eq(x, y): return (x - y).sign() == 0 def isqrt_fr(q): """sqrt of a non-negative rational square, else None.""" a, b = q.numerator, q.denominator ra, rb = math.isqrt(a), math.isqrt(b) return Fr(ra, rb) if ra * ra == a and rb * rb == b else None def back_ratio(F, t): """s_t = [0; a_t, a_(t-1), ...], exact.""" M = [[1, 0], [0, 1]] for j in range(t, t - F.p, -1): b = F.a(j) M = [[M[0][1], M[0][0] + b * M[0][1]], [M[1][1], M[1][0] + b * M[1][1]]] (m00, m01), (m10, m11) = M d = Fr((m11 - m00) ** 2 + 4 * m10 * m01) k = isqrt_fr(d / QF.D) assert k is not None, "backward period outside the field" return QF(Fr(-(m11 - m00), 2 * m10), k / (2 * m10)) class Coords: """kappa_t, lambda_t, A_t, B_t of one cell.""" def __init__(self, F, m, c): self.F, self.m, self.c, p = F, m, c, F.p self.s = [back_ratio(F, t) for t in range(p)] self.kap = [self.s[t] * inv(QF(1) + F.r[t] * self.s[t]) for t in range(p)] self.lam = [QF(1) - self.kap[t] * F.r[t] for t in range(p)] self.A, self.B = [], [] for t in range(p): t1 = (t + 1) % p U, V = F.uv(t, c) self.A.append(self.lam[t1] * U + self.kap[t1] * V) self.B.append(self.lam[t1]) def Z(self, G, H, t): return self.lam[t] * G + self.kap[t] * H def control_a(self): F, p = self.F, self.F.p bad = 0 for t in range(p): t1 = (t + 1) % p bad += not eq(self.kap[t1], F.r[t] * self.lam[t]) bad += not eq(self.lam[t1] - self.kap[t1] * F.a(t + 1), F.r[t] * self.kap[t]) bad += self.A[t].sign() <= 0 or self.B[t].sign() <= 0 T = 40 * p + p q = {-1: 0, 0: 1} for k in range(0, T + self.c + 3): q[k + 1] = F.a(k + 1) * q[k] + q[k - 1] th = {-1: 1.0} for k in range(0, T + 1): th[k] = th[k - 1] * F.r[k % p].f worst = 0.0 for n in range(40 * p, 41 * p): t = n % p worst = max(worst, abs(q[n - 1] * th[n - 1] - self.kap[t].f), abs(q[n] * th[n - 1] - self.lam[t].f), abs(q[n + self.c + 1] * th[n] - self.A[t].f)) return bad, worst def dmax(F, c, t, f): cap = F.a(t + c + 2) return cap if f else cap - 1 def hull(win, co, starts, plant=False, low=False): """{(t, f): Z bound}: the top (or, low, the floor) hull, exact.""" F, m, c, p = win.F, win.m, win.c, win.F.p sZ = {} for G, H, f, t in starts: z = co.Z(G, H, t) if (t, f) not in sZ or (z.f < sZ[(t, f)].f if low else z.f > sZ[(t, f)].f): sZ[(t, f)] = z sgn = -1 if low else 1 def options(t1, f1): """[(pred node or None, coefficient, constant)]: the node's value is the best of coef * value(pred) + const.""" t = (t1 - 1) % p out = [] if (t1, f1) in sZ: out.append((None, QF(0), sZ[(t1, f1)])) emax = F.a(t1 + 1) if low else 0 for f in (True, False): if f1: d = 0 else: dm = dmax(F, c, t, f) - (1 if plant and f else 0) if dm < 1: continue d = 1 if low else dm out.append(((t, f), F.r[t], co.A[t] * (m * d) - co.B[t] * emax)) if not out: # unreachable node (the plant) out.append((None, QF(0), QF(-sgn * 10 ** 6))) return out nodes = [(t, f) for t in range(p) for f in (True, False)] opts = {n: options(*n) for n in nodes} val = {n: 0.0 for n in nodes} for _ in range(3000): val = {n: sgn * max(sgn * (k.f * (val[pr] if pr else 0) + b.f) for pr, k, b in opts[n] if pr is None or pr in val) for n in nodes} pol = {} for n in nodes: pol[n] = max(opts[n], key=lambda o: sgn * (o[1].f * ( val[o[0]] if o[0] else 0) + o[2].f)) exact = {} def solve(n): path, seen = [], {} cur = n while cur is not None and cur not in exact and cur not in seen: seen[cur] = len(path) path.append(cur) cur = pol[cur][0] if cur is None: base = None elif cur in exact: base = exact[cur] else: cyc = path[seen[cur]:] S, P = QF(0), QF(1) for x in cyc: _pr, k, b = pol[x] S = S + P * b P = P * k exact[cur] = S * inv(QF(1) - P) path = path[:seen[cur]] base = exact[cur] for x in reversed(path): pr, k, b = pol[x] exact[x] = b + (k * base if pr is not None else QF(0)) base = exact[x] for n in nodes: if n not in exact: solve(n) bell = 0 for n in nodes: for pr, k, b in opts[n]: v = b + (k * exact[pr] if pr is not None else QF(0)) bell += not (le(exact[n], v) if low else le(v, exact[n])) return exact, bell def top(win, co, t, f, zhi): """T(t, f): the greatest G with a valid key and Z <= zhi, exact.""" lo, hi = win.V[(t, f)] r, k = win.F.r[t], co.kap[t] G = math.floor(zhi.f - k.f * lo.f) + 2 for _ in range(100000): base = r * G for H in range(math.floor((lo + base).f) - 1, math.ceil((hi + base).f) + 2): if win.ok(G, H, f, t): if le(co.Z(G, H, t), zhi): return G break G -= 1 raise RuntimeError("no top") def bottom(win, co, t, f, zlo): """The least G with a valid key and Z >= zlo (floats: a side print).""" lo, hi = win.V[(t, f)] r, k = win.F.r[t], co.kap[t] G = math.ceil(zlo.f - k.f * hi.f) - 2 for _ in range(100000): base = r * G for H in range(math.ceil((hi + base).f) + 1, math.floor((lo + base).f) - 2, -1): if win.ok(G, H, f, t): if co.Z(G, H, t).f >= zlo.f - 1e-9: return G break G += 1 raise RuntimeError("no bottom") def hull_set(win, co, zlo, zhi): """Every valid key with Z_lo <= Z <= Z_hi, exact.""" out = set() for (t, f), z1 in zhi.items(): z0 = zlo[(t, f)] lo, hi = win.V[(t, f)] r, k = win.F.r[t], co.kap[t] for G in range(math.floor(z0.f - k.f * hi.f) - 2, math.floor(z1.f - k.f * lo.f) + 3): base = r * G for H in range(math.floor((lo + base).f) - 1, math.ceil((hi + base).f) + 2): if win.ok(G, H, f, t): z = co.Z(G, H, t) if le(z0, z) and le(z, z1): out.add((G, H, f, t)) return out def wi(win, keys): """The first key with a reply and no valid move, or None.""" p = win.F.p for G, H, f, t in sorted(keys): 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) % p): return (G, H, f, t, d) return None def stage_wi(maps): """HULL-WI: the least c with WI on the hull set, against c_inf.""" t0 = time.time() kill, n, ctl_a, ctl_b, land_out, land_cells = 0, 0, 0, 0, 0, [] plant = None sizes = [] cover = esc = bell = 0 for name, per in PERIODIC: F = Field(per) p = F.p for m in maps: c_inf = least(F, m, "pin") c_hull = c_mine = None for c in range(14): win = Window(F, m, c) st, miss = win.pin_starts() if miss: continue co = Coords(F, m, c) zhi, b1 = hull(win, co, st) zlo, b2 = hull(win, co, st, low=True) bell += b1 + b2 _ok, S, _bad = win.closure(st) if c_mine is None and wi(win, S) is None: c_mine = c Hs = hull_set(win, co, zlo, zhi) if c == c_inf: ctl_b += not S <= Hs cover += win.pre_starts()[1] for G, H, f, t in Hs: t1 = (t + 1) % p for d in win.replies(f, t): G1, H1 = win.pre(G, H, t, d) for G2, H2 in win.moves(G1, H1, d == 0, t1): esc += (G2, H2, d == 0, t1) not in Hs sizes.append(len(Hs) - len(S)) for digs, N, _P in win.prereads(): f = digs[-1] == 0 for G, H in win.landings(N, f): if (G, H, f, 0) not in Hs: land_out += 1 cell = f"{name.split()[0]} x{m}" if cell not in land_cells: land_cells.append(cell) if name.startswith("golden") and m == 2: z3 = {k: v - 4 for k, v in zlo.items()} H3 = hull_set(win, co, z3, zhi) plant = (len(H3 - Hs), wi(win, H3), any(k[0] == -5 and k[1] == -3 for k in H3)) if c_hull is None and wi(win, Hs) is None: c_hull = c if c_hull is not None and c_mine is not None: break n += 1 kill += c_hull != c_inf ctl_a += c_mine != c_inf print(f" {name:20s} x{m} c_inf {c_inf} c_hull {c_hull} " f"(WI routine on S_PIN: {c_mine}); |H| - |S| at c_inf " f"{sizes[-1]}", flush=True) print("== HULL-WI: the window on the hull set") print(f" (a) the WI routine on S_PIN gives c_inf at {n - ctl_a} of {n}") print(f" (b) H(c_inf) holds S_PIN(c_inf) at {n - ctl_b} of {n}") print(f" (c) THE PLANT (Z_lo - 4, golden x2): {plant[0]} keys added, " f"G = -5, H = -3 among them {plant[2]}, first WI failure " f"{plant[1]}") print(f" (d) THE CLOSURE OF H, read: successors of keys of H(c_inf) " f"outside it {esc}") print(f" COVER: pre-reads with no valid landing at c_inf {cover}") print(f" Bellman failures of the fixed points at every c solved: " f"{bell}") print(f" keys of H beyond S at c_inf: {min(sizes)} to {max(sizes)}, " f"sum {sum(sizes)}") print(f" LANDING: valid landings outside H(c_inf): {land_out} (cells " f"{', '.join(land_cells) or '-'})") print(f" KILL: c_hull != c_inf at {kill} of {n} cells") print(f" {time.time() - t0:.1f} s") def ranges(S): out = {} for G, _H, f, t in S: lo, hi = out.get((t, f), (G, G)) out[(t, f)] = (min(lo, G), max(hi, G)) return out def main(): t0 = time.time() maps = (2, 3, 4, 5) + ((6, 7, 8, 9) if WIDE else ()) a_bad, a_worst, bell_bad = 0, 0.0, 0 b_bad, b_keys = 0, 0 pl_above_cells, pl_low_rows = 0, 0 kill = {True: 0, False: 0} nrows = {True: 0, False: 0} under = 0 hunch_eq, hunch_n = 0, 0 low_rows = {True: [], False: []} over = {True: [], False: []} fails = [] for name, per in PERIODIC: F = Field(per) for m in maps: c = least(F, m, "pin") win = Window(F, m, c) co = Coords(F, m, c) ab, aw = co.control_a() a_bad += ab a_worst = max(a_worst, aw) st, _ = win.pin_starts() _ok, S, _bad = win.closure(st) rng = ranges(S) zhi, bb = hull(win, co, st) bell_bad += bb zlo, bb = hull(win, co, st, low=True) bell_bad += bb bad_here = sum(not le(co.Z(G, H, t), zhi[(t, f)]) for G, H, f, t in S) b_bad += bad_here b_keys += len(S) zpl, _ = hull(win, co, st, plant=True) pl_above_cells += any(not le(co.Z(G, H, t), zpl[(t, f)]) for G, H, f, t in S) bounds = carry_bounds(F, m, c, 40 * F.p) row = [] for (t, f), (g0, g1) in sorted(rng.items()): T = top(win, co, t, f, zhi[(t, f)]) over[f].append(T - g1) nrows[f] += 1 if T != g1: kill[f] += 1 under += T < g1 if len(fails) < 12: fails.append(f" {name:20s} x{m} t{t}" f"{'F' if f else 'R'}: T {T}, " f"G_top {g1}, Z_hi {zhi[(t, f)].f:.4f}") pl_low_rows += top(win, co, t, f, zpl[(t, f)]) < g1 B = bottom(win, co, t, f, zlo[(t, f)]) low_rows[f].append(g0 - B) if not f: L = max(hi for ph, _lo, hi, _k in bounds[-3 * F.p:] if ph == t) hunch_n += 1 hunch_eq += abs(L - zhi[(t, f)].f) < 1e-6 row.append(f"t{t}{'F' if f else 'R'} T {T}/{g1} " f"Z {zhi[(t, f)].f:.2f}") print(f" {name:20s} x{m} c {c} " + " ".join(row), flush=True) print("== HULL: the closure's tops against the contracting bound") print(f" (a) Z's linear part, A > 0, B > 0: {a_bad} exact failures; " f"kappa, lambda, A against q |theta| at n near 40 p: worst " f"{a_worst:.1e}; Bellman failures of the exact fixed points " f"{bell_bad}") print(f" (b) THE BOUND: keys of S with Z > Z_hi: {b_bad} of {b_keys}") print(f" (c) THE PLANT (d_max(full) - 1): cells with keys of S above " f"it {pl_above_cells}; rows with its T below G_top {pl_low_rows}") print(f" the carry bound's max over the last 3 p of t <= 40 p " f"(m |theta| (q - 1)) equals Z_hi(t, R) at {hunch_eq} of {hunch_n} (t, R) rows") for f in (False, True): g = low_rows[f] print(f" LOW SIDE, {'full' if f else 'reduced'}: G_lo - hull " f"value over {len(g)} rows: min {min(g)}, max {max(g)}, " f"0 at {g.count(0)}") for f in (False, True): g = over[f] print(f" OVERSHOOT, {'full' if f else 'reduced'}: T - G_top over " f"{len(g)} rows: " + ", ".join( f"{v} at {g.count(v)}" for v in sorted(set(g)))) print(f" T < G_top (instrument fault): {under} rows") if fails: print(" first mismatches:") print("\n".join(fails)) print(f" KILL: T != G_top at {kill[False]} of {nrows[False]} (t, R) " f"rows; at {kill[True]} of {nrows[True]} (t, F) rows") print(f" {time.time() - t0:.1f} s") stage_wi(maps) if __name__ == "__main__": main()