""" phase.py -- T3's phase: at c = c_ov - 2 (pinned moves), does phase t + 1 or t + 2 of every hot t strand the full window's upper end? QUESTION. strand.py proves that at c = c_ov - 2 with pinned moves c is even and the full window's upper end E_h = m K_c - K_0 is a hull key, stranded at phase u iff some j P_1 lies in (m a_(c+2) P_(c+1), m (P_c + P_(c+1)) - P_2) (u's scale); some phase strands at all 115 of its 1017 cells, why not derived. Which phase must? DERIVED BY HAND (before the engine; strand.py's notation, a_k = a_(u+k), P_k = |theta_k| of r_u, hot t: L(c + 1, t) > 0). (R1) By T1 at the shifted phases m P_(c+k) < P_k for every k >= -1 (strict: theta_j = x_j r + y_j with (x_j, y_j) primitive, consecutive determinants being +-1, so theta_k = +-m theta_(c+k) would make m >= 2 divide (x_k, y_k)). So m P_c = a_(c+2) m P_(c+1) + m P_(c+2) < a_(c+2) P_1 + P_2: the interval's top is below (a_(c+2) + 1) P_1, and below (a_2 + 1) P_1, so a stranding j has 1 <= j <= min(a_2, a_(c+2)). (theorem) (R2) j = a_2 meets the top iff P_0 < m (P_c + P_(c+1)), which is L(c + 1, u - 2) > 0; the bottom has no j in it, so a smaller j only loses the bottom. Hence, t hot, phase t + 2 strands iff its top j = a_(t+4) clears the bottom: (C2) a_(t+4) P_3 > m a_(t+c+4) P_(c+3) in t's scale. Its failure forces a_(t+4) < a_(t+c+4) (by m P_(c+3) < P_3). (theorem) (R3) j = a_(c+2) clears the bottom free (m P_(c+1) < P_1), so (C1) a_(c+2) P_1 + P_2 < m (P_c + P_(c+1)) at phase u makes u strand. (theorem; sufficient, not necessary) Read off strand before the freeze: where t + 2 fails (37 of the 115), phase hot + 1 strands at all 37, by j = a_(c+2) of that phase. THE CONJECTURE (T3P): at every hot t, phase t + 1 or t + 2 strands. At period 2 it is T3 itself (t or t + 1), at period 1 "t strands"; only period >= 3 reads it as a choice of phase. DESIGN (frozen before the engine). Family X: primitive periods of length 3 over quotients 1 .. 8, of length 4 over 1 .. 6, of length 5 over 1 .. 4, least rotation, at m = 2 .. 12; with strand's 1017. Per cell c = c_ov - 2 >= 0 with pinned moves (strand.zero_in, by T1), else skipped and counted. KILLS (printed as, each killing at n > 0): K1 "T3P fails at n of N (cell, hot t)" over every read cell; K2 "(C2) apart from t + 2 stranding at n of N (cell, hot t)" (R2 is a proof: an index fault, read first); K3 "(C1) at u holds, u not stranding, at n of N (cell, u)" (R3); K4 "some phase strands at none of n of N cells" (T3 itself). Beside, no kill: K1's pairs by t + 2 only / t + 1 only / both; how often t + 1 strands by (C1); the read cells by period. CONTROLS (read first): strand's 115 reproduced (read 115, t + 2 for some hot t at 78); THE PLANT: (C2) with a_(t+c+4) replaced by a_(t+c+3) must put K2's line above 0 on X. FINDINGS (copied from the run's prints). CONTROLS. strand's 1017: read 115, t + 2 for some hot t at 78: held. THE PLANT: K2's line at 593 of 1084: the line can fire. CELLS. strand's 1017 read 115 (period 1, 2, 3, 4: 7, 28, 74, 6); X 7557 cells, no pinned moves at 6769, read 788 (period 3, 4, 5: 122, 370, 296); c odd at 0 of either (T2). K2, K3 MISSED (the proofs' lines): 0 of 152 and 1084 (cell, hot t); 0 of 309 and 3326 (cell, u). K1 FIRES: T3P fails at 4 of 1084 on X, all period 5: [1, 1, 1, 2, 3] x7, [1, 1, 1, 3, 3] x10, [1, 1, 1, 3, 4] x10, [1, 1, 1, 4, 3] x12, each at hot t = 2. T3P is killed; at strand's 1017, 0 of 152. K4 FIRES: no phase strands the upper end at 1 of 788, [1, 1, 1, 2, 3] x7 (c = 4). T3 is not universal past the 1017. Beside: on X, t + 2 only 90, t + 1 only 503, both 487; t + 1 by (C1) at 920 of 990. AFTER THE RUN (an arm added after the first run, then printed), at K1's four cells through strand.read_c and induct.least: c_inf - c_ov is -1, 0, -1, 0, and hull keys lie in pieces at c_ov - 2 at each (the hull's bounds hullform's, a rule at the 136, a TRANSPLANT here). At the three cells other than K4's the upper end strands at hot t = 2 itself (a closed end at phase 2, full flag), so T3 holds there by t, not t + 1 or t + 2. At K4's cell, [1, 1, 1, 2, 3] x7, only interior keys (phases 1, 2, 3, both flags) and c_inf = c_ov - 1: the upper end's route fails, H1 (some hull key in a gap) holds. RUN RECORD. 8.3 s, peak commit 11.6 MB. Written whole after the freeze, rehearsed at 60 cells per family, then run once; the AFTER THE RUN arm was added from a review and the whole rerun printed every frozen line unchanged, each of the four cells read (Field, least, read_c) in 0.06 s or less. On shipping, the verdicts were made the exit code: 0 iff the controls (115, 78; the plant at 593 of 1084), the cells as counted with odd c at 0, K1 to K4 at 0 on strand's 1017 and at 4, 0, 0, 1 on X, the beside line and the four cells' c_inf - c_ov (-1, 0, -1, 0, each with hull keys in pieces) hold as printed. Usage: python phase.py [cells] """ import os import sys import time from itertools import product os.environ.setdefault("OPENBLAS_NUM_THREADS", "1") from induct import Field, QF # noqa: E402 from keyweld import c_ov, lt # noqa: E402 from firstreturn import l_formula # noqa: E402 from strand import P, cells as strand_cells, strands_hi, zero_in # noqa: E402 from strand import read_c # noqa: E402 from induct import least # noqa: E402 def necklaces(L, A): out = [] for w in product(range(1, A + 1), repeat=L): rots = [w[i:] + w[:i] for i in range(L)] if len(set(rots)) < L or w != min(rots): continue out.append(w) return out def family(): out = [] for L, A in ((3, 8), (4, 6), (5, 4)): for per in necklaces(L, A): for m in range(2, 13): out.append((per, m)) return out def c2(F, m, c, t, shift=4): """(C2) a_(t+4) P_3 > m a_(t+c+shift) P_(c+3), t's scale.""" return lt(P(F, t, c + 3) * (m * F.a(t + c + shift)), P(F, t, 3) * F.a(t + 4)) def c1(F, m, c, u): """(C1) a_(c+2) P_1 + P_2 < m (P_c + P_(c+1)), u's scale.""" return lt(P(F, u, 1) * F.a(u + c + 2) + P(F, u, 2), (P(F, u, c) + P(F, u, c + 1)) * m) def read(per, m): F = Field(per) cov = c_ov(F, m) c = cov - 2 if c < 0: return dict(per=per, m=m, skip="neg") if not zero_in(F, m, c): return dict(per=per, m=m, skip="nopin") p = F.p hot = [t for t in range(p) if lt(QF(0), l_formula(F, t, m, c + 1))] st = {u: bool(strands_hi(F, m, c, u)) for u in range(p)} pairs = [] for t in hot: s1, s2 = st[(t + 1) % p], st[(t + 2) % p] pairs.append(dict(t=t, s1=s1, s2=s2, c2=c2(F, m, c, t), plant=c2(F, m, c, t, shift=3), c1=c1(F, m, c, (t + 1) % p))) c1u = [(c1(F, m, c, u), st[u]) for u in range(p)] return dict(per=per, m=m, skip=None, c=c, p=p, hot=hot, st=st, pairs=pairs, c1u=c1u) def main(): t0 = time.time() only = int(sys.argv[1]) if len(sys.argv) > 1 else None old = [read(per, m) for per, m in strand_cells()[:only]] t1 = time.time() X = [read(per, m) for per, m in family()[:only]] t2 = time.time() res = {} print("== CONTROLS") ro = [x for x in old if x["skip"] is None] n2 = sum(any(q["s2"] for q in x["pairs"]) for x in ro) print(f" strand's cells: {len(old)}, read {len(ro)}, t + 2 strands for " f"some hot t at {n2}") rx = [x for x in X if x["skip"] is None] pl = sum(q["plant"] != q["s2"] for x in rx for q in x["pairs"]) npx = sum(len(x["pairs"]) for x in rx) print(f" THE PLANT a_(t+c+3) for a_(t+c+4): K2's line at {pl} of {npx}") for name, R, allc in (("strand's 1017", ro, old), ("X", rx, X)): print(f"== {name}: {len(allc)} cells; c_ov - 2 < 0 at " f"{sum(x['skip'] == 'neg' for x in allc)}; no pinned moves at " f"{sum(x['skip'] == 'nopin' for x in allc)}; read {len(R)}") odd = sum(x["c"] % 2 for x in R) byp = {} for x in R: byp[x["p"]] = byp.get(x["p"], 0) + 1 print(f" read c odd at {odd} (T2); read by period " f"{dict(sorted(byp.items()))}") prs = [(x, q) for x in R for q in x["pairs"]] k1 = [(x["per"], x["m"], q["t"]) for x, q in prs if not (q["s1"] or q["s2"])] print(f" K1: T3P fails at {len(k1)} of {len(prs)} (cell, hot t): " f"{k1[:8]}") k2 = [(x["per"], x["m"], q["t"]) for x, q in prs if q["c2"] != q["s2"]] print(f" K2: (C2) apart from t + 2 stranding at {len(k2)} of " f"{len(prs)} (cell, hot t): {k2[:8]}") cu = [v for x in R for v in x["c1u"]] k3 = sum(a and not b for a, b in cu) print(f" K3: (C1) at u holds, u not stranding, at {k3} of " f"{len(cu)} (cell, u); (C1) holds at {sum(a for a, _ in cu)}, " f"u strands at {sum(b for _, b in cu)}") k4 = [(x["per"], x["m"]) for x in R if not any(x["st"].values())] print(f" K4: some phase strands at none of {len(k4)} of {len(R)} " f"cells: {k4[:8]}") res[name] = dict( cells=(len(allc), sum(x["skip"] == "neg" for x in allc), sum(x["skip"] == "nopin" for x in allc), len(R)), odd=odd, byp=dict(sorted(byp.items())), k=(len(k1), len(k2), len(prs), k3, len(cu), len(k4))) only2 = sum(q["s2"] and not q["s1"] for _, q in prs) only1 = sum(q["s1"] and not q["s2"] for _, q in prs) both = sum(q["s1"] and q["s2"] for _, q in prs) print(f" beside: t + 2 only {only2}, t + 1 only {only1}, both " f"{both}; t + 1 strands by (C1) at " f"{sum(q['s1'] and q['c1'] for _, q in prs)} of " f"{sum(q['s1'] for _, q in prs)}") res[name]["beside"] = (only2, only1, both, sum(q["s1"] and q["c1"] for _, q in prs), sum(q["s1"] for _, q in prs)) p3 = [(x, q) for x, q in prs if x["p"] >= 3] print(f" period >= 3 pairs {len(p3)}; K1 there " f"{sum(not (q['s1'] or q['s2']) for _, q in p3)}") print("== AFTER THE RUN: K1's and K4's cells through strand's engine") after = [] for x in rx: bad = [q["t"] for q in x["pairs"] if not (q["s1"] or q["s2"])] none = not any(x["st"].values()) if not (bad or none): continue t3 = time.time() F = Field(x["per"]) ci = least(F, x["m"], "pin") r = read_c(F, x["m"], x["c"]) kinds = sorted(set((k[0], "full" if k[1] else "red", k[3]) for k in r["keys"])) after.append((x["per"], x["m"], ci - x["c"] - 2, bool(r["keys"]))) print(f" {x['per']} x{x['m']} c {x['c']}: K1 at hot t {bad}, K4 " f"{none}; c_inf - c_ov {ci - x['c'] - 2}; hull keys in pieces " f"(phase, flag, kind) {kinds}; {time.time() - t3:.2f} s") if only is not None: return old_r, x_r = res["strand's 1017"], res["X"] checks = [ (len(old), len(ro), n2) == (1017, 115, 78), (pl, npx) == (593, 1084), old_r["cells"] == (1017, 0, 902, 115) and old_r["odd"] == 0 and old_r["byp"] == {1: 7, 2: 28, 3: 74, 4: 6}, x_r["cells"] == (7557, 0, 6769, 788) and x_r["odd"] == 0 and x_r["byp"] == {3: 122, 4: 370, 5: 296}, old_r["k"] == (0, 0, 152, 0, 309, 0), x_r["k"] == (4, 0, 1084, 0, 3326, 1), x_r["beside"] == (90, 503, 487, 920, 990), [(a[2], a[3]) for a in after] == [(-1, True), (0, True), (-1, True), (0, True)], ] print(f" {sum(checks)}/{len(checks)} checks as recorded; strand's " f"{t1 - t0:.1f} s, X {t2 - t1:.1f} s, all " f"{time.time() - t0:.1f} s") sys.exit(0 if all(checks) else 1) if __name__ == "__main__": main()