""" deficit.py -- W in one number per phase: at c = c_ov - 2 (pinned moves), the full window's upper end E_h = m K_c - K_0 strands by a deficit inequality; does the planned route to W (T3P under S) hold past the families, and does W hold where that route breaks? QUESTION. lowend.py reduced H1 at c_ov - 2 to (W): where S(t): m P_(c+1) > P_2 holds at every phase, E_h strands at some phase (T3's interval); read at every read cell of the 1017 and of X, proved at period 1. The planned proof: at a hot t, phase t + 1 strands by (C1) or t + 2 by (C2) (phase.py), under S everywhere. A float probe over random periods, not kept, found that route failing at period 6 and 7. Here: the exact form of the stranding in the deficits, the route's failures exact, and W and H1 on a family built at the route's corner. DERIVED BY HAND (before the engine; strand.py's notation, c even, phase u, a_k = a_(u+k), P_k = |theta_k| of r_u, r_s = [0; a_(s+1), ...]). Put g_s = m P_c / P_0 at phase s = m r_(s+1) ... r_(s+c), and the DEFICIT eps_s = 1 - g_s; by P^(s+1)_k = P^(s)_(k+1) / P^(s)_0, m P_(c+k) / P_k at phase u is g_(u+k), so P_k - m P_(c+k) = eps_(u+k) P_k at u's scale. (D1) Pinned moves (T1, c even: m P_(c+1) <= P_1, m P_c <= P_0 at every phase) iff eps_s >= 0 at every s, > 0 by R1's strictness. S(s - 1) iff eps_s < 1 - r_(s+1) (S(t) is g_(t+1) > P_2 / P_1 = r_(t+2)). Hot t (L(c + 1, t) > 0) iff eps_s + r_(s+1) eps_(s+1) < r_(s+1), s = t + 2 (divide m (P_(c+2) + P_(c+3)) > P_2 by P_2). As g_(s+1) r_(s+1) = g_s rho_s, rho_s = r_(s+c+1), hot iff eps_s < rho_s / (1 + rho_s). (theorems: algebra.) (D2) At u put Q_k = m P_(c+k), delta_k = P_k - Q_k = eps_(u+k) P_k. T3's interval (m a_(c+2) P_(c+1), m (P_c + P_(c+1)) - P_2) is (Q_0 - Q_2, Q_0 + Q_1 - P_2), as Q_0 = a_(c+2) Q_1 + Q_2. With j = a_2 - i, P_0 = a_2 P_1 + P_2: j P_1 lies in it iff i P_1 < delta_0 - delta_2 and delta_0 + delta_1 < (i + 1) P_1. The recurrences give delta_0 = (a_2 - A) P_1 + A delta_1 + delta_2, A = a_(c+2) = a_(s+c+1) for s = u + 1; so z = delta_0 / P_1 = (a_2 - A) + A eps_s + r_(s+1) eps_(s+1), and the two conditions put i in (z - 1 + eps_s, z - r_(s+1) eps_(s+1)), of length below 1: only i = floor z can lie there, and it does iff frac(A eps_s) + eps_s + r_(s+1) eps_(s+1) < 1 (A eps_s is irrational, as g_s is at c >= 2; the case frac(A eps_s) + r eps' >= 1 fails both). At c = 0, g_s = m < 1 is rational and at A eps_s = k exactly no i lies there (z - r eps' is an integer, the open end) while frac = 0 passes the inequality under S: there the form holds with A eps_s not an integer, which every cell here meets (m >= 2 forces c >= 2 under pinned moves). i = floor z >= 0 (z > 0), and an i >= a_2 would put j <= 0, whose j P_1 cannot clear the interval's positive bottom, so the inequality fails there too. So, at every phase with pinned moves, A_s eps_s not an integer: E_h strands at phase s - 1 iff frac(A_s eps_s) + eps_s + r_(s+1) eps_(s+1) < 1, A_s = a_(s+c+1), in the gap e = floor(delta_0 / P_1) (theorem, by hand). c enters only through A_s, rho_s and the eps's; the hypotheses of W are eps_s in (0, 1 - r_(s+1)) at every s and eps_s < rho_s / (1 + rho_s) at some s. j = A_s is (C1) at s - 1 (frac = A eps when A eps < 1); hot at s - 3 (u - 2) is j = a_(s+1) below the top (R2). At period 1 the hot bound rho / (1 + rho) = 1 / (a + 1 + r) is the first non-stranding eps, so a hot phase strands: lowend's period-1 proof in one line (every phase of a period-1 cell is hot). DESIGN (frozen before the engine). Families: the 1017 (strand.cells), X (phase.family, 7557), and Y, built at the route's corner (the float probe's failures sat at period 6 and 7): primitive periods of length 6 over quotients 1 .. 4 at m = 2 .. 30, and of length 7 over 1 .. 3 at m = 2 .. 40, least rotation; Y/2, Y's length-6 periods at m = 5/2 .. 59/2 (half-integers: the float probe read W at real m). Read cells: c = c_ov - 2 >= 0 with pinned moves (strand.zero_in). Exact (QF) throughout. PREDICTIONS. (P1) (D2)'s form = strands_hi at every read (cell, phase) of every family. (P2) (D1)'s three forms = zero_in, lowend.S and l_formula > 0 at every read (cell, phase). (P3) W and H1 at every read cell of every family. (P4) the route, T3P under S ("S at every phase, a hot t, neither t + 1 nor t + 2 strands"), fails on Y, at (1, 2, 4, 2, 2, 4) x27 and (1, 2, 3, 3, 2, 3, 3) x31 among others (the float probe), and at 0 on the 1017 and X. KILLS (printed as, each n > 0 kills): "(D2) form != strands_hi at n of N (cell, phase)" over each family; "(D1) pinned / S / hot forms apart at n, n, n of N"; "(W) S at every phase and E_h at none: n of N cells"; "(H1) (F) at no phase and E_h at none: n of N cells", (F) lowend's. (D1), (D2) firing is an index fault, read first. Printed beside, no kill: "(route) T3P under S fails at n of N (cell, hot t)" and its first cells, per family; "(C1) at no phase under S: n of N cells" (whether j = A_s at one phase is W's witness); the read cells and the cells with S at every phase, per family. CONTROLS (read before the verdicts). (a) THE PLANT on (D2): r_(s+1) eps_(s+1) replaced by r_(s+1) eps_s: (D2)'s line must fire on some family. (b) lowend's (W) line reproduced on the 1017 and X: S at every phase at 76 and 321 cells, W failing at 0 and 0. (c) THE ENGINE: strand.control_a. FINDINGS (copied from the run's prints). CONTROLS. (c) strand.control_a held. (b) lowend's (W) line: S at every phase at 76 and 321, W failing at 0 and 0: held. (a) THE PLANT: (D2)'s line at 17 of 309, 146 of 3326, 1944 of 30593 and 1125 of 14598: it can fire. CELLS (read: c_ov - 2 >= 0 with pinned moves). The 1017: read 115, 309 (cell, phase). X: 788, 3326. Y: 31598 cells, read 4760, 30593. Y/2: 18760 cells, read 2433, 14598. c odd with pinned moves at 0 of 573, 3949, 16010 and 9379 cells (T2). KILLS MISSED. (D2) form != strands_hi at 0 of 309, 3326, 30593 and 14598 (cell, phase). (D1) apart at 0 (pinned, over the c-even cells: 444, 3608, 15588, 9381), 0 (S) and 0 (hot). (W) at 0 of 76, 321, 537 and 336 cells with S at every phase. (H1) at 0 of 115, 788, 4760 and 2433. THE ROUTE. T3P under S fails at 0 of 108 (the 1017) and 0 of 480 (X) (cell, hot t); at 2 of 1413 on Y, (1, 2, 4, 2, 2, 4) x27 and (1, 2, 3, 3, 2, 3, 3) x31, as predicted; at 3 of 759 on Y/2, (1, 4, 4, 4, a, 3) x9/2 for a = 2, 3, 4. W holds at all five: another phase strands. T3P under S is killed, so the route to W through t + 1 and t + 2 is dead. BESIDE. (C1) at no phase under S: 1 of 76 ((2, 4, 5) x8), 14 of 321 ((2, 4, 5) x8, (2, 5, 7) x10, (2, 6, 8) x12, (2, 3, 3, 4) x6 first), 5 of 537 ((2, 3, 3, 3, 3, 4) x6 first), 0 of 336: j = A_s at one phase is not W's witness either. RUN RECORD. 127.1 s, peak commit 29.9 MB, rehearsed at 60 cells per family, then run once. On shipping, the verdicts were made the exit code: 0 iff the engine's control, the plant's counts, the read and S-everywhere counts, the route's and (C1)'s counts hold as printed and the kills, (D1), (D2) and the odd-c pinned count print 0. (D2)'s scope, A eps_s not an integer, was added after an audit found the form wrong at c = 0 where A eps_s = k. Changed from the freeze: (D1)'s pinned form is compared at c even only, as derived, the odd-c cells printed apart (pinned at none, T2); the rehearsal had compared every cell. The pinned comparison is per cell over every cell with c_ov - 2 >= 0, read or not, not per read (cell, phase) as the frozen "n of N" was. Usage: python deficit.py [cells] """ import os import sys import time from fractions import Fraction as Fr 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 cells as strand_cells, zero_in, strands_hi # noqa: E402 from strand import control_a # noqa: E402 from phase import family, necklaces, c1 # noqa: E402 from lowend import S # noqa: E402 ONE = QF(1) def gs(F, m, c): """g_s = m r_(s+1) ... r_(s+c), by the tails alone (not strand.P).""" p = F.p out = [] for s in range(p): x = QF(m) for i in range(1, c + 1): x = x * F.r[(s + i) % p] out.append(x) return out def frac_lt(F, X, Y): """frac(X) + Y < 1, X > 0 exact, by the k with k <= X < k + 1.""" k = 0 while not lt(X, QF(k + 1)): k += 1 return lt(X - QF(k) + Y, ONE) def form(F, m, c, g, s, plant=False): """(D2): E_h strands at phase s - 1 iff frac(A eps_s) + eps_s + r_(s+1) eps_(s+1) < 1, A = a_(s+c+1).""" p = F.p e0, e1 = ONE - g[s % p], ONE - g[(s + 1) % p] r1 = F.r[(s + 1) % p] tail = r1 * (e0 if plant else e1) return frac_lt(F, e0 * F.a(s + c + 1), e0 + tail) def read(per, m): F = Field(per) p = F.p cov = c_ov(F, m) c = cov - 2 if c < 0: return None g = gs(F, m, c) pin_form = all(lt(x, ONE) for x in g) pin = zero_in(F, m, c) row = dict(per=per, m=m, c=c, p=p, pin=pin, pin_form=pin_form) if not pin: return row eps = [ONE - x for x in g] rr = [F.r[(s + 1) % p] for s in range(p)] Sv = [S(F, m, c, t) for t in range(p)] hot = [lt(QF(0), l_formula(F, t, m, c + 1)) for t in range(p)] st = [bool(strands_hi(F, m, c, u)) for u in range(p)] d1s = d1h = d2 = d2p = 0 for s in range(p): u, t = (s - 1) % p, (s - 2) % p d1s += lt(eps[s], ONE - rr[s]) != Sv[u] d1h += lt(eps[s] + rr[s] * eps[(s + 1) % p], rr[s]) != hot[t] d2 += form(F, m, c, g, s) != st[u] d2p += form(F, m, c, g, s, plant=True) != st[u] allS = all(Sv) Fend = any(Sv[t] and not Sv[(t - 1) % p] for t in range(p)) route = [t for t in range(p) if allS and hot[t] and not st[(t + 1) % p] and not st[(t + 2) % p]] nhot = sum(hot) if allS else 0 c1any = any(c1(F, m, c, u) for u in range(p)) row.update(read=True, d1s=d1s, d1h=d1h, d2=d2, d2p=d2p, allS=allS, W=allS and not any(st), H1=not Fend and not any(st), route=len(route), nhot=nhot, c1none=allS and not c1any) return row def report(name, rows): nc = len(rows) sub = [x for x in rows if x] rd = [x for x in sub if x.get("read")] nph = sum(x["p"] for x in rd) ev = [x for x in sub if x["c"] % 2 == 0] pin_bad = sum(x["pin"] != x["pin_form"] for x in ev) odd_pin = sum(x["pin"] for x in sub if x["c"] % 2) print(f"== {name}: {nc} cells, c_ov - 2 >= 0 at {len(sub)}, read {len(rd)}" f", (cell, phase) {nph}") print(f" (D2) form != strands_hi at {sum(x['d2'] for x in rd)} of {nph} " f"(cell, phase); (a) PLANT: at {sum(x['d2p'] for x in rd)}") print(f" (D1) pinned / S / hot forms apart at {pin_bad} of {len(ev)} " f"cells (c even), {sum(x['d1s'] for x in rd)} and " f"{sum(x['d1h'] for x in rd)} of {nph} (cell, phase); c odd at " f"{len(sub) - len(ev)} cells, pinned at {odd_pin} (T2)") aS = [x for x in rd if x["allS"]] w = [(x["per"], x["m"]) for x in rd if x["W"]] h = [(x["per"], x["m"]) for x in rd if x["H1"]] print(f" (W) S at every phase and E_h at none: {len(w)} of {len(aS)} " f"cells {w[:4]}") print(f" (H1) (F) at no phase and E_h at none: {len(h)} of {len(rd)} " f"cells {h[:4]}") ro = [(x["per"], str(x["m"])) for x in rd if x["route"]] print(f" (route) T3P under S fails at {sum(x['route'] for x in rd)} of " f"{sum(x['nhot'] for x in rd)} (cell, hot t), cells {ro[:6]}") cn = [(x["per"], str(x["m"])) for x in rd if x["c1none"]] print(f" (C1) at no phase under S: {len(cn)} of {len(aS)} cells {cn[:4]}") return dict(read=len(rd), allS=len(aS), W=len(w), H1=len(h), route=sum(x["route"] for x in rd), c1none=len(cn), d2=sum(x["d2"] for x in rd), d2p=sum(x["d2p"] for x in rd), d1=pin_bad + sum(x["d1s"] + x["d1h"] for x in rd), odd_pin=odd_pin) def fam_Y(): out = [(w, m) for w in necklaces(6, 4) for m in range(2, 31)] out += [(w, m) for w in necklaces(7, 3) for m in range(2, 41)] return out def fam_Y2(): return [(w, Fr(2 * k + 1, 2)) for w in necklaces(6, 4) for k in range(2, 30)] def main(): t0 = time.time() only = int(sys.argv[1]) if len(sys.argv) > 1 else None print("== CONTROLS") ctl = control_a() print(f" (c) strand.control_a held: {ctl}") res = {} for name, cells in (("the 1017", strand_cells()), ("X", family()), ("Y", fam_Y()), ("Y/2", fam_Y2())): if only: cells = cells[::max(1, len(cells) // only)] t1 = time.time() rows = [read(per, m) for per, m in cells] res[name] = report(name, rows) print(f" {name}: {time.time() - t1:.1f} s") print(f" (b) lowend's (W) line: S at every phase at " f"{res['the 1017']['allS']} and {res['X']['allS']}, W failing at " f"{res['the 1017']['W']} and {res['X']['W']}") print(f" all {time.time() - t0:.1f} s") if only: return res want = {"the 1017": (115, 76, 17, 0, 1), "X": (788, 321, 146, 0, 14), "Y": (4760, 537, 1944, 2, 5), "Y/2": (2433, 336, 1125, 3, 0)} checks = [ctl] for name, (rd, aS, d2p, route, c1n) in want.items(): x = res[name] checks += [x["read"] == rd, x["allS"] == aS, x["d2p"] == d2p, x["route"] == route, x["c1none"] == c1n, x["d2"] == 0, x["d1"] == 0, x["W"] == 0, x["H1"] == 0, x["odd_pin"] == 0] print(f" {sum(checks)}/{len(checks)} checks as recorded") sys.exit(0 if all(checks) else 1) if __name__ == "__main__": main()