""" strand.py -- the class step one c below the window's: at c = c_ov - 2, does some zero-reply piece hold a hull key, and where? QUESTION. (TRANSPLANT: the hull's bounds are hullform.forms', its ends a rule at the 136 only; here they are read at the 881 new cells.) widestep.py reads c_inf in {c_ov - 1, c_ov} at 1001 cells; c_inf >= c_ov - 1 is not derived. LOW's test fails at c_ov - 2 for free (D2 below), so its failure proves nothing: the content is a STRANDED HULL KEY at c_ov - 2, a valid key in a zero-reply gap with Z in the hull's [Z_lo, Z_hi] (then the closure's ends, open, make it reachable). DERIVED BY HAND (before the engine). Notation (slackbar.py's): phase t, a_k = a_(t+k), P_k = |theta_k| of r_t (P_(-1) = 1, P_0 = r_t), q_k = U_k, K_k = (q_k, p_k), y(K_k) = (-1)^(k+1) P_k, Z = G + kappa_t y. Gap length at c, phase t: L(c, t) = m (P_(c+1) + P_(c+2)) - P_2 (classform's convention, read off pieces(): E_a = m K_E - K_2 + e K_1, E_b = m K_O + e K_1, O/E the odd/ even of c+1, c+2; y_b - y_a = m (P_O + P_E) - P_2). c_ov = least c with L(c, t) <= 0 at every t (equivalent over phases to keyweld.c_ov). Let c = c_ov - 2 >= 0 and t a phase with L(c+1, t) > 0 (one exists, c+1 < c_ov). Write lam = L(c, t). (D1) lam > P_(c+1). Proof: lam = L(c+1, t) + m (P_(c+1) - P_(c+3)) = L(c+1, t) + m a_(c+3) P_(c+2) > 2 a_(c+3) P_(c+2) >= a_(c+3) P_(c+2) + P_(c+3) = P_(c+1), using m >= 2, P_(c+3) < P_(c+2), and P_(c+1) = a_(c+3) P_(c+2) + P_(c+3). (theorem, by hand) (D2) So every unclipped piece at (t, full) fails the LOW test. From E_b: K_O has y = +P_O < lam, so {-q_O r} = P_O < lam and n-(lam) <= q_O; G_b - n- >= (m - 1) q_O + e a_1 >= 1, while the full flag's G_lo is -(a_1 + 1) + d, d in {-1, 0, 1}, <= -a_1 <= -1. From E_a: K_E has y = -P_E, so n+(lam) <= q_E; G_a - n+ >= (m - 1) q_E - q_2 + e a_1 >= 0 > G_lo, as E >= 2. Both ends' margins are negative. (theorem, by hand) So LOW's failure at c_ov - 2 is free, and LOW failing is no proof of loss: it says the certificate is silent, not that a hull key sits in a gap. The content of c_inf >= c_ov - 1 is a STRANDED HULL KEY at c_ov - 2 (and then the closure's ends, already open, to make it reachable). Hand case, golden x3 (c_ov 5, c = 3, phase 0, full flag; r = 1/phi, P_k = phi^-(k+1), q = 1, 1, 2, 3, 5, 8). lam = 3 P_3 - P_2 = 0.2016 > P_4 = 0.0902 (D1). a_2 = 1: e = 0 only. E_b = 3 K_5 = (24, 15), y_b = 3 P_5 = 0.1672; E_a = 3 K_4 - K_2 = (13, 8), y_a = -0.0344. Window (full, c odd: lo = m K_c - K_1, hi = m K_(c+1) - K_0): lo = (8, 5), y = 3 P_3 - P_1 = 0.0557; hi = (14, 9), y = 0.3475. The piece is (0.0557, 0.1672), its lower end closed at (8, 5). Hull G-range on the full flag: -2 .. 9 (Z_lo = -Z(2, 1), Z_hi = Z(3 K_3) = Z(9, 6)). Keys inside: G = 3, H = 2: K_3 = (3, 2), y = P_3 = 0.1459, in the piece and the hull. The closed end (8, 5): Z = 8 + kappa 0.0557 < Z_hi, in the hull. Two stranded hull keys, one interior (K_c) and one closed end (the window's lower end). The closed end in general: c odd, lo = m K_c - K_1, G = m q_c - a_1, Z = Z_hi - a_1 - kappa P_1 < Z_hi and Z - Z_lo = m q_c + 1 + kappa (m P_c - P_0) > 0: the full window's lower end is ALWAYS a hull key at c odd. It is stranded iff it lies inside a gap: (e + 1) P_1 in (m a_(c+2) P_(c+1), m (P_c + P_(c+1)) - P_2), an interval of length lam, for some e + 1 in 1 .. a_2. Not forced by lam alone. TRANSPLANT from golden. QUESTION. At c = c_ov - 2 (>= 0, pinned moves), does some zero-reply piece hold a hull key, and where? CELLS: widestep.py's W (1001) and decide.py's 136, deduplicated (1017). Per cell: c_ov (keyweld), c = c_ov - 2; skip (counted apart) c < 0 and c without pinned moves (Window.pin_starts misses). Per (t, f), the pieces (classform.pieces), the hull bounds (hullform.forms); a HULL KEY IN A PIECE: an integer key (G, H) with y = H - G r_t in the open (y_a, y_b), or a closed end, with Z in [Z_lo, Z_hi] (exact, QF / lt / le), G enumerated over floor(Z_lo - kappa y_b) .. ceil(Z_hi - kappa y_a). PREDICTIONS. (D1) lam > P_(c+1) at every (cell, phase) with L(c+1, t) > 0: a proof, its print a control of the engine's indices. (D2) LOW fails at every unclipped full-flag piece at those phases: a proof, likewise. (H1) at every read cell, some piece at c_ov - 2 holds a hull key. (H2) at every read cell, some such key lies in a full-flag piece at a phase with L(c+1, t) > 0 (the named place). KILL (printed as): "D1 fails at n of N phases"; "D2 fails at n of N pieces"; "no hull key in any piece at c_ov - 2 at n of N cells" (H1); "no hull key at the named place at n of N cells" (H2). n > 0 kills each; D1 or D2 firing is an index fault (the proofs hold), read first. Printed beside, no kill: per cell the kind of the stranded keys (closed end; interior; K_c or -K_c or the window's lower end among them) and counts of each over the read cells; the cells skipped for c < 0 and for no pinned moves. CONTROLS (read before the verdicts). (a) golden x3 at c = 3, phase 0, full flag: the piece (0.0557, 0.1672) closed below at (8, 5), the hull keys in it exactly {(3, 2), (8, 5)}. (b) the enumerator's none-direction: at c = c_ov - 1 on the arm (c_inf = c_ov - 1, every piece passes FORM, so no hull key in any piece), the enumerator finds 0 hull keys at every arm cell. (c) beside it, the class step at W: at c_ov - 1 off the arm with pinned moves (c_inf = c_ov), the cells where no piece holds a hull key, printed (0 at the 48 by the class step's rule; read, not a kill). (d) THE PLANT: Z_hi lowered to Z_lo on every flag (the hull a sliver): H1's line must fire at most cells. FINDINGS (copied from the run's prints). CONTROLS. (a) golden x3, c 3, phase 0, full: the piece (0.0557, 0.1672) closed below at (8, 5), hull keys {(3, 2), (8, 5)}: held. (b) the arm at c_ov - 1: 109 cells, hull keys in pieces at 0. (c) off the arm with pinned moves at c_ov - 1: 579 cells, no hull key in any piece at 0: the class step reads c_inf at all 688 cells with pinned moves at c_ov - 1. (d) Z_hi := Z_lo: H1's line fires at 27 of 115, not "most" as frozen: at the other 88 the hull's lower end key itself lies in a piece. The line can fire. CELLS. 1017; c_ov - 2 < 0 at 0; no pinned moves at c_ov - 2 at 902; read 115. c_inf - c_ov in {-1, 0} at all 1017. D1, D2: 0 of 152 phases, 0 of 133 pieces (37 cells have no unclipped full piece at a hot phase): the indices are the proofs'. H1, H2, KILLS MISSED: a hull key in a piece at c_ov - 2 at all 115, and at the named place (full flag, hot phase) at all 115. KINDS. Every read cell holds both a closed end and an interior key in the hull; +-K_c among them at 23. AFTER THE RUN (derived by hand from those prints, then printed). T1 (theorem, by hand; printed apart at 0 of 4018 (cell, c), c = c_ov - 3 .. c_ov). The pinned key (0, 0) at phase t has the moves (-e, 0), e = 0 .. a_1, at y = e P_0. The full window is [m P_(c+1) - P_1, P_0 - m P_c] at c even and [m P_c - P_1, P_0 - m P_(c+1)] at c odd (win_keys' ends), whose top is below P_0, so only e = 0 can be valid: pinned moves at c iff 0 lies in V(t, full) at every phase, i.e. m P_(c+1) <= P_1 and m P_c <= P_0 (c even), m P_c <= P_1 and m P_(c+1) <= P_0 (c odd), at every t. T2 (theorem). c odd with pinned moves has c >= c_ov - 1. Phase t + 1's m P_c <= P_1 reads m P_(c+1) <= P_2 in t's scale (P^(t+1)_k = P_(k+1) / P_0); then L(c + 1, t) = m (P_(c+2) + P_(c+3)) - P_2 <= m P_(c+1) - P_2 <= 0, as P_(c+2) + P_(c+3) <= P_(c+1), at every t: c + 1 >= c_ov. Printed: odd c with pinned moves sit at c - c_ov in {-1, 0}. T3. At c even the full window's upper end E_h = m K_c - K_0 is a hull key (theorem): G = m q_c - 1, Z(E_h) = Z_hi - 1 + kappa_t P_0 < Z_hi, and Z(E_h) - Z_lo = m q_c + a_1 + kappa_t (P_1 - m P_c) > 0, as m P_c <= P_0 < 1 (T1) and 0 < kappa_t < 1. It lies in the gap e = a_2 - j iff j P_1 lies in (m a_(c+2) P_(c+1), m (P_c + P_(c+1)) - P_2), an interval of length L(c, t) (theorem); some phase has such a j at all 115 (rule, verified at the 115; printed: no phase at 0). Not derived: why a phase must. A hot phase t places the top j = a_(t+4) under the interval's top at phase t + 2 (m (P_(c+2) + P_(c+3)) - P_4 > P_2 - P_4 = a_4 P_3 in t's scale), the bottom unproved; t + 2 strands for some hot t at 78 of the 115 (printed). So c_inf >= c_ov - 1 reduces to: T3's phase at c_ov - 2 even, and a stranded hull key forcing a loss (the closure's ends). Printed beside: every closed end in the hull is the full window's upper end (others at 0), and the engine's closed-end finds agree with T3's interval at every (cell, phase). RUN RECORD. 23.3 s, peak commit 20.8 MB. The engine was written whole after the freeze, rehearsed on 40 cells, then run once; T1 to T3 and the closed-end flag line were added after that run, from its prints, and the whole rerun printed every frozen line unchanged; a review added the t + 2 count, the closed-end identity and T3's agreement with the engine. Changed from the freeze: the kinds print as counts over cells, not per cell, and (c) reads all 1017 cells, not W alone. On shipping, the verdicts were made the exit code: 0 iff (a) held, (b) at 0 of 109, (c) at 0 of 579, (d) at 27 of 115, the cells as counted, c_inf - c_ov in {-1, 0}, D1 to H2 at 0 (of 152 phases, 133 pieces, 115 cells), T1 apart at 0 of 4018 with odd c at c - c_ov in {-1, 0}, T3's phase at all 115, and the closed-end lines at 0, 0 and 78 hold as printed. Usage: python strand.py """ import math import os import sys import time os.environ.setdefault("OPENBLAS_NUM_THREADS", "1") from flush import PERIODIC # noqa: E402 from decide import FRESH # noqa: E402 from induct import Field, Window, least # noqa: E402 from hull import Coords # noqa: E402 from keyweld import c_ov, lt # noqa: E402 from induct import le, QF # noqa: E402 from firstreturn import l_formula # noqa: E402 from hullform import forms, uv # noqa: E402 from classform import pieces, win_keys, ykey # noqa: E402 from slackbar import low_margin # noqa: E402 from widestep import necklaces # noqa: E402 TOL = 1e-7 def P(F, t, k): """P_k = |theta_k| of r_t, exact.""" zero = QF(0) th = {-1: QF(-1), 0: F.r[t]} for j in range(k): th[j + 1] = th[j] * F.a(t + j + 1) + th[j - 1] x = th[k] return x if lt(zero, x) else zero - x def hull_keys(F, co, t, pc, zlo, zhi): """[(key, kind)]: hull keys in the piece, kind 'closed' or 'in'.""" ya, yb, ca, cb, Ea, Eb = pc out = [] for closed, E in ((ca, Ea), (cb, Eb)): z = co.Z(*E, t) if closed and le(zlo, z) and le(z, zhi): out.append((tuple(E), "closed")) if not lt(ya, yb): return out k, r = co.kap[t].f, F.r[t].f glo = math.floor(zlo.f - k * yb.f) - 1 ghi = math.ceil(zhi.f - k * ya.f) + 1 yaf, ybf, zlf, zhf = ya.f, yb.f, zlo.f, zhi.f for G in range(glo, ghi + 1): H = math.floor(yaf + G * r) + 1 for h in (H - 1, H, H + 1): y = h - G * r if y < yaf - TOL or y > ybf + TOL: continue z = G + k * y if z < zlf - TOL or z > zhf + TOL: continue yq = ykey(F, t, (G, h)) if not (lt(ya, yq) and lt(yq, yb)): continue zq = co.Z(G, h, t) if le(zlo, zq) and le(zq, zhi): out.append(((G, h), "in")) return out def read_c(F, m, c, plant=False): """None without pinned moves; else the hull keys in pieces and the D1, D2 reads at the hot phases (L(c + 1, t) > 0).""" win = Window(F, m, c) _st, miss = win.pin_starts() if miss: return None co = Coords(F, m, c) keys, d1, d2, named, nunc = [], [], [], [], 0 for t in range(F.p): l1 = l_formula(F, t, m, c + 1) hot = lt(QF(0), l1) if hot: d1.append(lt(P(F, t, c + 1), l_formula(F, t, m, c))) fm = forms(F, co, m, c, t) Kc = uv(F, t, c) lo_full = tuple(win_keys(F, t, m, c, True)[0]) for f in (True, False): zlo, zhi = fm[(f, True)], fm[(f, False)] if plant: zhi = zlo for pc in pieces(F, t, m, c, f): for key, kind in hull_keys(F, co, t, pc, zlo, zhi): tag = kind if key == tuple(Kc): tag += "+Kc" elif key == (-Kc[0], -Kc[1]): tag += "-Kc" if f and key == lo_full: tag += "+lo" keys.append((t, f, key, tag)) if hot and f: named.append(key) if hot and f and not pc[2] and not pc[3]: nunc += 1 me = low_margin(F, co, t, m, c, f, pc, zlo) d2.append(me is not None and me <= 0) return dict(keys=keys, d1=d1, d2=d2, named=named, nunc=nunc) def zero_in(F, m, c): """(T1) V(t, full) holds y = 0 at every phase, by its ends' y.""" for t in range(F.p): lo, hi = ((c + 1, 1), (c, 0)) if c % 2 == 0 else ((c, 1), (c + 1, 0)) for k, j in (lo, hi): if not le(P(F, t, k) * m, P(F, t, j)): return False return True def strands_hi(F, m, c, t): """(T3) the j in 1 .. a_2 with j P_1 in (m a_(c+2) P_(c+1), m (P_c + P_(c+1)) - P_2): the full window's upper end m K_c - K_0 in gap e = a_2 - j, c even.""" A = P(F, t, c + 1) * (m * F.a(t + c + 2)) B = (P(F, t, c) + P(F, t, c + 1)) * m - P(F, t, 2) return [j for j in range(1, F.a(t + 2) + 1) if lt(A, P(F, t, 1) * j) and lt(P(F, t, 1) * j, B)] def cells(): out = {} for _name, per in list(PERIODIC) + list(FRESH): for m in range(2, 10): out[(tuple(per), m)] = None for per in necklaces(): for m in range(2, 13): out[(tuple(per), m)] = None return list(out) def control_a(): F = Field((1,)) co = Coords(F, 3, 3) fm = forms(F, co, 3, 3, 0) got = [(round(pc[0].f, 4), round(pc[1].f, 4), pc[2], tuple(pc[4]), sorted(hull_keys(F, co, 0, pc, fm[(True, True)], fm[(True, False)]))) for pc in pieces(F, 0, 3, 3, True)] print(f" (a) golden x3, c 3, phase 0, full: {got}") return got == [(0.0557, 0.1672, True, (8, 5), [((3, 2), "in"), ((8, 5), "closed")])] def main(): t0 = time.time() print("== CONTROLS") ok_a = control_a() only = int(sys.argv[1]) if len(sys.argv) > 1 else None rows = [] for per, m in cells()[:only]: F = Field(per) cov = c_ov(F, m) cinf = least(F, m, "pin") row = dict(per=per, m=m, cov=cov, cinf=cinf, two=None, one=None, plant=None) if cov - 2 >= 0: row["two"] = read_c(F, m, cov - 2) if row["two"] is not None: row["plant"] = read_c(F, m, cov - 2, plant=True) if cov - 1 >= 0: row["one"] = read_c(F, m, cov - 1) row["t1"] = [] for c in range(max(cov - 3, 0), cov + 1): pin = not Window(F, m, c).pin_starts()[1] row["t1"].append((c, pin, pin == zero_in(F, m, c))) c = cov - 2 if row["two"] is not None and c % 2 == 0: row["t3"] = [t for t in range(F.p) if strands_hi(F, m, c, t)] rows.append(row) t1 = time.time() N = len(rows) arm = [x for x in rows if x["cinf"] == x["cov"] - 1] b = [x for x in arm if x["one"] is None or x["one"]["keys"]] print(f" (b) arm at c_ov - 1: {len(arm)} cells; hull keys found (or no " f"pinned moves) at {len(b)}: {[(x['per'], x['m']) for x in b[:6]]}") off = [x for x in rows if x["cinf"] == x["cov"] and x["one"] is not None] cc = [x for x in off if not x["one"]["keys"]] print(f" (c) off the arm with pinned moves at c_ov - 1: {len(off)}; no " f"hull key in any piece at {len(cc)}: " f"{[(x['per'], x['m']) for x in cc[:8]]}") read = [x for x in rows if x["two"] is not None] neg = [x for x in rows if x["cov"] - 2 < 0] nopin = [x for x in rows if x["cov"] - 2 >= 0 and x["two"] is None] dp = [x for x in read if not x["plant"]["keys"]] print(f" (d) THE PLANT Z_hi := Z_lo: H1's line fires at {len(dp)} of " f"{len(read)}") print(f"== CELLS: {N}; c_ov - 2 < 0 at {len(neg)}; no pinned moves at " f"c_ov - 2 at {len(nopin)}; read {len(read)}") print(f" c_inf - c_ov over all: " f"{sorted(set(x['cinf'] - x['cov'] for x in rows))}") d1 = [v for x in read for v in x["two"]["d1"]] d2 = [v for x in read for v in x["two"]["d2"]] print("== VERDICTS") print(f" D1 KILL: D1 fails at {d1.count(False)} of {len(d1)} phases") print(f" D2 KILL: D2 fails at {d2.count(False)} of {len(d2)} pieces; " f"cells with no unclipped full piece at a hot phase: " f"{sum(x['two']['nunc'] == 0 for x in read)}") h1 = [x for x in read if not x["two"]["keys"]] print(f" H1 KILL: no hull key in any piece at c_ov - 2 at {len(h1)} of " f"{len(read)} cells: {[(x['per'], x['m']) for x in h1[:8]]}") h2 = [x for x in read if not x["two"]["named"]] print(f" H2 KILL: no hull key at the named place at {len(h2)} of " f"{len(read)} cells: {[(x['per'], x['m']) for x in h2[:8]]}") kinds = {} for x in read: for tg in set(k[3] for k in x["two"]["keys"]): kinds[tg] = kinds.get(tg, 0) + 1 print(f"== KINDS (cells holding each tag): {dict(sorted(kinds.items()))}") noclosed = [x for x in read if not any(k[3].startswith("closed") for k in x["two"]["keys"])] nokc = [x for x in read if not any("Kc" in k[3] for k in x["two"]["keys"])] both = [x for x in noclosed if x in nokc] print(f" no closed end in the hull at {len(noclosed)}; no +-K_c at " f"{len(nokc)}; neither at {len(both)}: " f"{[(x['per'], x['m']) for x in both[:10]]}") print("== AFTER THE RUN (derived by hand from the first prints)") tt = [v for x in rows for v in x["t1"]] print(f" T1: pinned moves iff V(t, full) holds 0 at every phase, apart " f"at {sum(not v[2] for v in tt)} of {len(tt)} (cell, c), c = c_ov " f"- 3 .. c_ov") odd = sorted(set(v[0] - x["cov"] for x in rows for v in x["t1"] if v[1] and v[0] % 2)) print(f" T2: odd c with pinned moves sit at c - c_ov in {odd}") ev = [x for x in read if (x["cov"] - 2) % 2 == 0] print(f" T3: read cells with c_ov - 2 even {len(ev)} of {len(read)}; " f"no phase stranding the full window's upper end at " f"{sum(not x.get('t3') for x in ev)}") oth, apart, n2 = 0, 0, 0 for x in ev: F, m, c = Field(x["per"]), x["m"], x["cov"] - 2 hot = [t for t in range(F.p) if lt(QF(0), l_formula(F, t, m, c + 1))] n2 += any((t + 2) % F.p in x["t3"] for t in hot) for t in range(F.p): hi = tuple(win_keys(F, t, m, c, True)[1]) cl = [k for k in x["two"]["keys"] if k[0] == t and k[3].startswith("closed")] oth += sum(not (k[1] and k[2] == hi) for k in cl) apart += bool(cl) != (t in x["t3"]) print(f" closed hull keys other than the full window's upper end: " f"{oth}; engine's closed finds apart from T3's interval at " f"{apart} (cell, phase); t + 2 strands for some hot t at {n2} " f"of {len(ev)}") checks = [ ok_a, (len(arm), len(b), len(off), len(cc)) == (109, 0, 579, 0), (len(dp), len(read)) == (27, 115), (N, len(neg), len(nopin)) == (1017, 0, 902), sorted(set(x["cinf"] - x["cov"] for x in rows)) == [-1, 0], (d1.count(False), len(d1), d2.count(False), len(d2)) == (0, 152, 0, 133), (len(h1), len(h2)) == (0, 0), sum(not v[2] for v in tt) == 0 and len(tt) == 4018 and odd == [-1, 0], (len(ev), sum(not x.get("t3") for x in ev)) == (115, 0), (oth, apart, n2) == (0, 0, 78), ] print(f" {sum(checks)}/{len(checks)} checks as recorded; cells " f"{t1 - t0:.1f} s, all {time.time() - t0:.1f} s") sys.exit(0 if all(checks) else 1) if __name__ == "__main__": main()