""" saturate.py -- is the pinned closure every valid key of one carry interval per phase and flag? QUESTION. induct.py's S_PIN (the forward closure of the pinned keys' valid moves under every reply and every valid move) gives c_pin = c_inf, and with TWIN c_saf <= c_inf, at 48 cells. At c_inf, each phase t and flag f, is S_PIN every valid lattice key (G, H, f, t) with G in [G_lo, G_top](t, f), S_PIN's own least and greatest G there? DESIGN (frozen before the engine). Valid: y = H - G r_t in the closed range Window.V[(t, f)], decided exactly by Window.ok. For G in [G_lo, G_top], H runs over floor(lo + G r_t) - 1 .. ceil(hi + G r_t) + 1. c_inf is taken as induct.py's c_pin (least c with the pinned moves and WI on S_PIN), equal to the pinned game's c_inf at all 48 cells (induct.py), so no game is solved. PREDICTION: saturation at all 48 cells. KILL: "missing valid keys inside [G_lo, G_top]" > 0 at a cell; a (t, f) with no key of S_PIN is printed empty, never counted. CONTROL: S_PIN with one key removed by hand, its G strictly inside (G_lo, G_top) at its (t, f), must print missing >= 1 at every cell with such a key. SIDE PRINTS: G_lo, G_top per (t, f); the pre-reads' valid landings with G outside [G_lo, G_top] of their flag at phase 0, and the reduced twins against the full flag's range; G_lo(t, True) = 0 at every phase. FINDINGS (the --wide run, copied from its prints). KILL MISSED. Missing valid keys inside [G_lo, G_top]: 0 keys at 0 of 48 cells; every (t, f) prints S's count equal to the valid count (golden x2: t0R [6, 9] 3/3, t0F [0, 5] 4/4; bronze x9: t0R [980, 3237] 841/841, t0F [0, 980] 358/358). Keys of S outside the valid enumeration: 0. So at each cell the pinned closure is, per phase and flag, every valid key of one carry interval. THE ENDS (side prints). G_lo(t, full) = 0 at every row (frozen). The reduced range starts where the full one ends (printed after the frozen run): G_lo(t, R) - G_top(t, F) over the 104 phases is 0 at 43, 1 at 33, 2 at 17 and 3 at 11 (silver x2 9 - 9, golden x2 6 - 5). G_top(t, R) < G_top(t, F) at 0 phases. LANDING. Valid landings with G outside their flag's range at phase 0: 28, at 28 cells; landings off S on the reduced flag: 28, all inside the full flag's range. The two counts are printed apart; that they are the same 28 keys follows from saturation (a valid landing inside its flag's range lies in S) with the equal counts, and is not printed. CONTROLS. One interior key removed prints missing >= 1 at 48 of 48 cells: caught by construction, given 0 keys of S outside the valid enumeration, so it reads only missing()'s bookkeeping. The H window holds the exact valid range ceil(lo + G r_t) .. floor(hi + G r_t) by construction, so the kill's only blind side is the float wall; the H WINDOW control (added after the frozen run) reads that: searched 10 past floor and ceiling it adds 0 keys. Its narrow plant (-1) drops 208 keys over the 208 (cell, phase, flag) rows and reads nothing of the kill. (t, f) rows holding no key of S: 0, so no row was skipped. RUN RECORD. Bare 0.3 s, --wide 1.2 s with the H WINDOW control, no game solved. The first run (bare, m = 2 .. 5) had the side print "keys of S outside the valid enumeration" count S's keys of every (t, f) against each row (18460); fixed to the row's own keys, it prints 0; the kill and the control were unchanged. THE ENDS print was added after that run. A name reused in the examples loop broke THE ENDS print whenever the kill fired (TypeError, read by forcing one interior key out of S in a scratch copy); renamed, the forced run prints the kill at 24 of 24 cells and THE ENDS whole. Usage: python saturate.py [--wide] (--wide adds m = 6 .. 9) """ import math import os import sys import time os.environ.setdefault("OPENBLAS_NUM_THREADS", "1") from flush import PERIODIC # noqa: E402 from induct import Field, Window, least # noqa: E402 WIDE = "--wide" in sys.argv def valid_keys(win, F, t, f, g_lo, g_top, pad=1): """Every valid lattice key at (t, f) with G in [g_lo, g_top], H searched pad beyond the range's floor and ceiling.""" lo, hi = win.V[(t, f)] out = set() for G in range(g_lo, g_top + 1): base = F.r[t] * G for H in range(math.floor((lo + base).f) - pad, math.ceil((hi + base).f) + pad + 1): if win.ok(G, H, f, t): out.add((G, H, f, t)) return out def ranges(S, p): """{(t, f): (G_lo, G_top)} over the keys of 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 missing(win, F, S): """[(t, f, n missing, n valid)] per (t, f) holding a key of S.""" rows = [] for (t, f), (g0, g1) in sorted(ranges(S, F.p).items()): full = valid_keys(win, F, t, f, g0, g1) mine = {k for k in S if k[2] == f and k[3] == t} rows.append((t, f, len(full - S), len(full), g0, g1, len(mine - full))) return rows def main(): t0 = time.time() maps = (2, 3, 4, 5) + ((6, 7, 8, 9) if WIDE else ()) cells = kill_cells = kill_keys = 0 ctl_cells = ctl_hit = 0 off_valid = 0 floor_bad = 0 land_out = twin_in_full = twin_n = 0 land_out_cells = [] examples = [] gaps, tops_bad = [], 0 wide_add = narrow_drop = empty_rows = 0 for name, per in PERIODIC: F = Field(per) for m in maps: c = least(F, m, "pin") win = Window(F, m, c) st, _miss = win.pin_starts() _ok, S, _bad = win.closure(st) rows = missing(win, F, S) n_miss = sum(r[2] for r in rows) off_valid += sum(r[6] for r in rows) cells += 1 kill_cells += n_miss > 0 kill_keys += n_miss floor_bad += sum(r[4] != 0 for r in rows if r[1]) if n_miss and len(examples) < 8: for t, f, nm, nv, g0, g1, _x in rows: if nm: holes = sorted(valid_keys(win, F, t, f, g0, g1) - S) examples.append(f" {name:20s} x{m} t {t} " f"{'full' if f else 'red.'}: {nm} " f"of {nv} missing, G in [{g0}, " f"{g1}], first {holes[:3]}") break rng = ranges(S, F.p) empty_rows += sum((t, f) not in rng for t in range(F.p) for f in (True, False)) for (t, f), (g0, g1) in rng.items(): base_k = valid_keys(win, F, t, f, g0, g1) wide_add += len(valid_keys(win, F, t, f, g0, g1, 10) - base_k) narrow_drop += len(base_k - valid_keys(win, F, t, f, g0, g1, -1)) for t in range(F.p): if (t, True) in rng and (t, False) in rng: gaps.append(rng[(t, False)][0] - rng[(t, True)][1]) tops_bad += rng[(t, False)][1] < rng[(t, True)][1] # control: drop one interior key inner = sorted(k for k in S if rng[(k[3], k[2])][0] < k[0] < rng[(k[3], k[2])][1]) if inner: ctl_cells += 1 drop = inner[len(inner) // 2] S2 = S - {drop} ctl_hit += sum(r[2] for r in missing(win, F, S2)) >= 1 # LANDING side print for digs, N, _P in win.prereads(): f = digs[-1] == 0 for G, H in win.landings(N, f): k = (G, H, f, 0) r = rng.get((0, f)) if r is None or not r[0] <= G <= r[1]: land_out += 1 if f"{name.split()[0]} x{m}" not in land_out_cells: land_out_cells.append(f"{name.split()[0]} x{m}") if k not in S and not f: twin_n += 1 rf = rng.get((0, True)) twin_in_full += bool(rf and rf[0] <= G <= rf[1]) lines = " ".join( f"t{t}{'F' if f else 'R'} [{g0},{g1}] {nv - nm}/{nv}" for t, f, nm, nv, g0, g1, _x in rows) print(f" {name:20s} x{m} c {c} |S| {len(S)} {lines}", flush=True) print(f" ... {name} done, {time.time() - t0:.1f} s", flush=True) print("== SATURATION: the pinned closure against the valid keys of its " "carry intervals") print(f" CONTROL: one interior key removed prints missing >= 1 at " f"{ctl_hit} of {ctl_cells} cells with such a key") print(f" keys of S outside the valid enumeration (must be 0): " f"{off_valid}") print(f" H WINDOW: searched 10 past floor and ceiling it adds " f"{wide_add} keys (must be 0); the planted narrow window (-1) " f"drops {narrow_drop} (must be > 0)") print(f" (t, f) rows holding no key of S: {empty_rows}") print(f" G_lo(t, full) != 0 at {floor_bad} (t, full) rows") print(f" G_lo(t, R) - G_top(t, F) over {len(gaps)} phases: " f"{sorted(set(gaps))}, counts " f"{[gaps.count(g) for g in sorted(set(gaps))]}; " f"G_top(t, R) < G_top(t, F) at {tops_bad}") print(f" LANDING: valid landings with G outside their flag's range at " f"phase 0: {land_out} (cells {', '.join(land_out_cells) or '-'});" f" landings off S on the reduced flag {twin_n}, of them inside " f"the full flag's range {twin_in_full}") if examples: print(" missing keys, first cells:") print("\n".join(examples)) print(f" KILL: missing valid keys inside [G_lo, G_top]: {kill_keys} " f"keys at {kill_cells} of {cells} cells") print(f" {time.time() - t0:.1f} s") if __name__ == "__main__": main()