""" lowend.py -- H1 by the hull's lower ends: at c = c_ov - 2 (pinned moves), when does each flag's lower hull end strand, and does the full window's upper end cover every cell where neither does? QUESTION. strand.py and widex.py read H1 (some hull key in a zero-reply gap at c_ov - 2) at all 115 of the 1017 and all 788 of X with pinned moves there, unproved. Under widex's plant (c) (Z_hi := Z_lo, so only keys at the flags' lower ends count) a key survives at 766 of 788, at two cells read by hand the full flag's lower end. Which phase strands each lower end, by a hand condition, and what is left? DERIVED BY HAND (before the engine; strand.py's notation, c even, a_k = a_(t+k), P_k = |theta_k| of r_t; read off classform.win_keys, pieces and hullform.forms: y(K_k) = (-1)^(k+1) P_k, K_0 = (1, 0), K_1 = (a_1, 1); gap e, 0 <= e < a_2, on both flags y in (P_2 - m P_(c+2) + e P_1, m P_(c+1) + e P_1), the flag only clipping; full window [m P_(c+1) - P_1, P_0 - m P_c], reduced [m P_(c+1) - P_1, P_0 - m P_c + m P_(c+1)]; lower forms Z(-(K_1 + K_0)) full, Z(m K_c - K_1 - K_0) reduced, a rule at the 136 and on X at c_ov - 2 (widex's HULL arm), so a valid key at its flag's lower form is a hull key). (F) The full lower end -(a_1 + 1, 1) has y = P_0 - P_1. Valid iff m P_c <= P_1 (its bottom m P_(c+1) <= P_0 is T1's). With j = a_2 - 1 - e and P_0 = a_2 P_1 + P_2 it lies in gap e iff j P_1 + P_2 lies in (P_2 - m P_(c+2), m P_(c+1)), least at j = 0: some gap holds it iff S(t): m P_(c+1) > P_2. As P^(t)_k = P^(t-1)_(k+1) / P^(t-1)_0, m P_c <= P_1 at t iff not S(t - 1). So it strands at t iff S(t) and not S(t - 1) (theorem, given the lower form). A hot t (L(c + 1, t) > 0) has S(t), as P_(c+1) >= P_(c+2) + P_(c+3); one exists. So it strands at some phase iff S fails at some phase (theorem); never at period 1. (R) The reduced lower end m K_c - K_1 - K_0 has y = P_0 - P_1 - m P_c. Valid iff m (P_c + P_(c+1)) <= P_0. In gap e iff j P_1 (j = a_2 - 1 - e) lies in T3's interval (m a_(c+2) P_(c+1), m (P_c + P_(c+1)) - P_2), so j >= 1. It strands at t iff the interval holds some j P_1, j >= 1, and m (P_c + P_(c+1)) <= P_0 (then j <= a_2 - 1 is free, the top being <= a_2 P_1) (theorem, given the lower form). It is E_h - K_1, E_h = m K_c - K_0, so it strands only at a phase where E_h strands (strand.strands_hi, T3). So H1 at a cell follows from S failing at some phase, or from E_h stranding at some phase; (W), unproved: where S holds at every phase, E_h strands at some phase. Under S everywhere T3's top exceeds P_1, so j = 1 fails at t only if m a_(c+2) P_(c+1) >= P_1. DESIGN (frozen before the engine). Cells: strand.cells() (the 1017) and phase.family() (X, 7557); read those with c = c_ov - 2 >= 0 and pinned moves (strand.zero_in). Per read cell and phase t, exact (QF): S(t); (F)'s and (R)'s hand verdicts; E_h's by strand.strands_hi; and the engine's, strand.read_c's keys: -(a_1 + 1, 1) on the full flag, m K_c - K_1 - K_0 on the reduced, m K_c - K_0 on the full. PREDICTIONS. (P1) (F)'s hand verdict = the engine's at every (cell, phase). (P2) (R)'s likewise. (P3) E_h's = the engine's. (W) at every read cell with S at every phase, E_h strands at some phase. KILLS (printed as, each n > 0 kills): "(F) hand != engine at n of N (cell, phase)"; "(R) hand != engine at n of N"; "(T3) hand != engine at n of N"; "(W) S at every phase and E_h at none: n of N cells", N the read cells with S at every phase, over each family. (P1) to (P3) firing is an index fault or a lower form off its rule, read first. Printed beside, no kill: per family the read cells, the cells with S at every phase, and the cells covered by (F) only, E_h only, both; the cells where (F) or (R) strands at some phase, against widex's plant survivors (766 of 788) and strand's (88 of 115); every cell with S at every phase, its period, m and E_h's phases. CONTROLS (read before the verdicts). (a) THE PLANT on (F): the shift read the wrong way, S(t) and not S(t + 1): (P1)'s line must fire. (b) THE PLANT on (R): validity dropped: (P2)'s line must fire, or it is printed that validity binds nowhere read. (c) THE ENGINE: strand.py's own control (a), golden x3 at c = 3, phase 0, full: hull keys {(3, 2), (8, 5)} (strand.control_a). FINDINGS (copied from the run's prints). CONTROLS. (c) strand.control_a held. (a) the shift read as t + 1: (F)'s line at 60 of 309 (the 1017) and 870 of 3326 (X): it can fire. (b) validity dropped: (R)'s line at 0 of 309 and 0 of 3326: validity binds nowhere read (observation). KILLS MISSED. (F), (R), (T3) hand != engine at 0 of 309 (cell, phase) on the 1017's 115 read cells and 0 of 3326 on X's 788. Hot without S at 0; (R) without E_h at 0 (both proved). (W): S at every phase and E_h at none at 0 of 76 and 0 of 321 cells. BESIDE. The 1017: S at every phase at 76 of 115 (period 1, 2, 3, 4: 7, 20, 47, 2); (F) only 0, E_h only 76, both 39, neither 0. X: S at every phase at 321 of 788 (period 3, 4, 5: 65, 169, 87); (F) only 1 ([1, 1, 1, 2, 3] x7), E_h only 321, both 466, neither 0. (F) or (R) at some phase at 88 of 115 and 766 of 788: the counts of the plant survivors of strand.py (d) and widex.py (c), the sets equal by argument (under Z_hi := Z_lo only keys at a lower form survive), not printed. SCOPE. The engine reads hullform's forms too, so (P1) to (P3) test the indices, not the forms; the forms are read at c_ov - 2 on X (widex's HULL arm) and at the 136 (classform.py's (ii)), not at the 1017's other 15 read cells. H1 by (F) or E_h needs the full flag's two forms (E_h's Z between Z_lo and Z_hi by T3); the reduced flag's adds nothing past E_h. AFTER THE RUN (printed: the AFTER THE RUN line). At S everywhere, j = 1 strands E_h at some phase at 30 of 76 and 86 of 321; j = a_(c+2) at 75 of 76 and 307 of 321, not at [2, 4, 5] x8 among others. At period 1 (r = [0; a, a, ...], u = m r^c < 1 by T1, r^c irrational) T3's interval over P_1 is (a u, a u + u (1 + r) - r), and j = a lies in it (a u < a free) iff u > (a + r) / (a + 1 + r) = 1 / (1 + r), which is the hot condition: W holds at period 1 (theorem, by hand). In general neither j = 1 nor j = a_(c+2) is the witness. RUN RECORD. 12.5 s, the engine written whole after the freeze, rehearsed at 60 cells per family, then run once; the AFTER THE RUN line and the (F) only line added after, the whole rerun printing every line unchanged. Changed from the freeze: the cells with S at every phase print the first 10, not all. On shipping, the verdicts were made the exit code: 0 iff the controls (the engine's; the plants at 60 and 870, 0 and 0), the kills and the proofs' prints at 0, the read, S everywhere, (F) or (R), j = 1 and j = a_(c+2) counts and the cover line hold as printed. Usage: python lowend.py [cells] """ import os import sys import time os.environ.setdefault("OPENBLAS_NUM_THREADS", "1") from induct import Field, QF, le # noqa: E402 from keyweld import c_ov, lt # noqa: E402 from firstreturn import l_formula # noqa: E402 from hullform import uv # noqa: E402 from classform import lin # noqa: E402 from strand import P, cells as strand_cells, read_c, zero_in # noqa: E402 from strand import strands_hi, control_a # noqa: E402 from phase import family # noqa: E402 def S(F, m, c, t): return lt(P(F, t, 2), P(F, t, c + 1) * m) def hand_R(F, m, c, t, validity=True): a2 = F.a(t + 2) 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) js = [j for j in range(1, a2) if lt(A, P(F, t, 1) * j) and lt(P(F, t, 1) * j, B)] ok = le((P(F, t, c) + P(F, t, c + 1)) * m, P(F, t, 0)) return bool(js) and (ok or not validity) def read(per, m): F = Field(per) cov = c_ov(F, m) c = cov - 2 if c < 0 or not zero_in(F, m, c): return None r = read_c(F, m, c) if r is None: return None p = F.p keys = set((k[0], k[1], k[2]) for k in r["keys"]) s = [S(F, m, c, t) for t in range(p)] rows = [] for t in range(p): K0, K1, Kc = uv(F, t, 0), uv(F, t, 1), uv(F, t, c) lf = lin((-1, K1), (-1, K0)) lr = lin((m, Kc), (-1, K1), (-1, K0)) eh = lin((m, Kc), (-1, K0)) hot = lt(QF(0), l_formula(F, t, m, c + 1)) rows.append(dict( t=t, hot=hot, S=s[t], F=s[t] and not s[(t - 1) % p], Fp=s[t] and not s[(t + 1) % p], R=hand_R(F, m, c, t), Rp=hand_R(F, m, c, t, validity=False), T=bool(strands_hi(F, m, c, t)), eF=(t, True, lf) in keys, eR=(t, False, lr) in keys, eT=(t, True, eh) in keys)) return dict(per=per, m=m, c=c, p=p, rows=rows, nkeys=len(keys)) def report(name, R): pr = [(x, q) for x in R for q in x["rows"]] n = len(pr) out = {} for tag, h, e in (("(F)", "F", "eF"), ("(R)", "R", "eR"), ("(T3)", "T", "eT")): bad = [(x["per"], x["m"], q["t"]) for x, q in pr if q[h] != q[e]] out[tag] = len(bad) print(f" {tag} hand != engine at {len(bad)} of {n} (cell, phase): " f"{bad[:6]}") pf = sum(q["Fp"] != q["eF"] for _, q in pr) pb = sum(q["Rp"] != q["eR"] for _, q in pr) print(f" (a) PLANT shift t + 1: (F)'s line at {pf} of {n}; (b) PLANT " f"validity dropped: (R)'s line at {pb} of {n}") hs = sum(q["hot"] and not q["S"] for _, q in pr) rt = sum(q["R"] and not q["T"] for _, q in pr) print(f" proofs' prints: hot without S at {hs}; (R) without E_h at {rt}") allS = [x for x in R if all(q["S"] for q in x["rows"])] w = [x for x in allS if not any(q["T"] for q in x["rows"])] out["W"] = len(w) print(f" (W) S at every phase and E_h at none: {len(w)} of " f"{len(allS)} cells: {[(x['per'], x['m']) for x in w[:8]]}") f = [any(q["F"] for q in x["rows"]) for x in R] th = [any(q["T"] for q in x["rows"]) for x in R] fr = sum(any(q["F"] or q["R"] for q in x["rows"]) for x in R) print(f" beside: read {len(R)}; S at every phase {len(allS)}; (F) only " f"{sum(a and not b for a, b in zip(f, th))}, E_h only " f"{sum(b and not a for a, b in zip(f, th))}, both " f"{sum(a and b for a, b in zip(f, th))}, neither " f"{sum(not (a or b) for a, b in zip(f, th))}; (F) or (R) at some " f"phase {fr}") fo = [(x["per"], x["m"]) for x, a, b in zip(R, f, th) if a and not b] print(f" (F) only at {fo[:8]}") byp = {} for x in allS: byp[x["p"]] = byp.get(x["p"], 0) + 1 first = [(x["per"], x["m"], [q["t"] for q in x["rows"] if q["T"]]) for x in allS[:10]] print(f" S at every phase by period {dict(sorted(byp.items()))}; " f"first: {first}") j1 = jc = 0 miss = [] for x in allS: F = Field(x["per"]) m, c = x["m"], x["c"] j1 += any(lt(P(F, t, c + 1) * (m * F.a(t + c + 2)), P(F, t, 1)) for t in range(x["p"])) hit = any(F.a(t + c + 2) in strands_hi(F, m, c, t) for t in range(x["p"])) jc += hit if not hit: miss.append((x["per"], m)) print(f" AFTER THE RUN, at S everywhere: j = 1 strands E_h at some phase " f"at {j1} of {len(allS)}; j = a_(c+2) at {jc}, not at {miss[:6]}") out.update(read=len(R), allS=len(allS), fr=fr, j1=j1, jc=jc, plants=(pf, pb), proofs=(hs, rt), cover=(sum(a and not b for a, b in zip(f, th)), sum(b and not a for a, b in zip(f, th)), sum(a and b for a, b in zip(f, th)), sum(not (a or b) for a, b in zip(f, th)))) return out def main(): t0 = time.time() only = int(sys.argv[1]) if len(sys.argv) > 1 else None print("== CONTROLS") print(f" (c) strand.control_a held: {control_a()}") res = {} for name, cells in (("the 1017", strand_cells()), ("X", family())): if only: cells = cells[::max(1, len(cells) // only)] t1 = time.time() R = [x for x in (read(per, m) for per, m in cells) if x] print(f"== {name}: {len(cells)} cells, {time.time() - t1:.1f} s") res[name] = report(name, R) print(f" all {time.time() - t0:.1f} s") if only: return res a, x = res["the 1017"], res["X"] checks = [ control_a(), a["plants"] == (60, 0) and x["plants"] == (870, 0), [a[k] for k in ("(F)", "(R)", "(T3)", "W")] == [0, 0, 0, 0], [x[k] for k in ("(F)", "(R)", "(T3)", "W")] == [0, 0, 0, 0], a["proofs"] == (0, 0) and x["proofs"] == (0, 0), (a["read"], a["allS"], a["fr"], a["j1"], a["jc"]) == (115, 76, 88, 30, 75), (x["read"], x["allS"], x["fr"], x["j1"], x["jc"]) == (788, 321, 766, 86, 307), a["cover"] == (0, 76, 39, 0) and x["cover"] == (1, 321, 466, 0), ] print(f" {sum(checks)}/{len(checks)} checks as recorded") sys.exit(0 if all(checks) else 1) if __name__ == "__main__": main()