""" firstreturn.py -- the class step of the integer reader's key window by the rotation's first return into a gap, against keyweld.py's norm-form certificate. QUESTION. At c_inf the real window V(t, f) has forbidden pieces after a reply (keyweld.py::forbidden), and the hull set holds no key inside any: the class step. keyweld.py's norm form certifies 7 of the 22 pieces. A key inside a piece (y_a, y_b), L = y_b - y_a, differs from an end E (a lattice key) by v with y(v) in (0, L) from E_a or in (-L, 0) from E_b. Let h-(E) < 0 < h+(E) be the nearest G(v) on either side with y(v) in that one-sided interval: the first returns of the rotation by r_t into it (Slater's three-gap theorem). Then no key inside has G strictly between G_E + h- and G_E + h+, since G(v) = 0 forces y(v) an integer, 0 as L < 1. (Q) Does one end's first-return window hold the hull's whole G-range at the piece, at every one of the 22? DERIVED BY HAND (before the engine; the numbers read off hull.py's and keyweld.py's functions at bronze x3, c = c_inf = 2, phase 0). alpha = r_0 = [0; 3, 3, ...] = (sqrt 13 - 3)/2, 1/alpha = alpha + 3, so y u = H^2 + 3GH - G^2 (den = 1) and kappa sqrt 13 = 1: Z = G + kappa y. The zero reply leaves three open pieces on each flag, (0.02012, 0.02521), (0.1118, 0.11688), (0.20347, 0.20856), each a translate of the first by the key (3, 1) (y = |theta_1| = 1 - 3 alpha). The first's ends are E_a = (317, 96), Z 317.006, and E_b = (99, 30), Z 99.007, E_b being the reduced flag's top hull key (Z = Z_hi(0, R)); they differ by 2 (q_4, p_4) = 2 (109, 33), so L = 2 |theta_4| = 2 alpha^5 = 0.00509 and N(E_a - E_b) = -4, whence |Z_b - Z_a| = 4 mu / L exactly: the norm certificate's middle test fails by equality, and its low side reads margin 0.70 (full flag) and 0.93 (reduced). The hull's keys have G -4 .. 29 on the full flag (Z_lo -3.94, Z_hi 29.98) and 26 .. 99 on the reduced (Z_lo 26.04, Z_hi 99.007); the DESIGN's range formula reads -4 .. 30 and 26 .. 100. The nearest keys inside the first piece: (208, 63) = E_b + (109, 33), its midpoint, Z 208.006, and (-152, -46) = E_b - (251, 76), 251 = 2 q_4 + q_3, Z -151.99; so from E_b, h+ = 109 and h- = -251, the window (-152, 208) holds both flags' key ranges, by 148 and 109 at the near sides (108 by the formula's 100). The norm form prices the same v at |Z(v)| >= mu / L = 54.5: it charges every v the piece's whole length, while Lagrange's bound gives |G(v)| >= q_4 = 109 for |y(v)| < L <= |theta_3|, the norm bound being attained only at |y(v)| = |theta_4| = L / 2. The other two pieces read the same h+ and h-, shifted by (3, 1); their norm margins differ (full 0.68, 0.67; reduced 0.90, 0.87). DESIGN (frozen before the engine). Cells, windows, hulls and pieces as keyweld.py (m = 2 .. 5, --wide to 9), at c_inf. Per piece and each end that is a lattice key, h+ and h- by exact enumeration of G(v) over |G(v)| <= B, B = max over the range of |G - G_E| plus a margin 4 (Z_hi - Z_lo) + 4 that only widens what is read, at the piece's flag, a side with no return inside B read as beyond it (that side then holds the range); the hull's G-range: G from floor(Z_lo - kappa y_b) to ceil(Z_hi - kappa y_a). A piece is CERTIFIED when for some end both the range's least G exceeds G_E + h- and its greatest falls below G_E + h+ (a closed end read directly, as keyweld.py's certify). Beside it, h+ and h- from r_t's continued fraction by the three-gap theorem, the enumeration its reference. THE THREE-GAP SIDES BY HAND (before (P2)'s code). Write r = r_t = [0; a_1, a_2, ...] with a_k = a_(t+k), q_(-1) = 0, q_0 = 1, theta_(-1) = -1, theta_0 = r, theta_(k+1) = a_(k+1) theta_k + theta_(k-1), so theta_k = q_k r - p_k has sign (-1)^k and |theta_k| falls. A key E_a + v inside the piece has y(v) = dH - dG r in (0, L), so dH = ceil(dG r) and the offset is {-dG r} for dG > 0 and {n r} for dG = -n < 0; from E_b, y(v) in (-L, 0) reads {n r} at dG = n and {-n r} at dG = -n. So two counts carry both ends: n+(L), the least n >= 1 with {n r} < L, and n-(L), the least n >= 1 with {-n r} < L; then from E_a, h+ = n-(L) and h- = -n+(L), and from E_b, h+ = n+(L) and h- = -n-(L). The records of {n r} are n = q_i + j q_(i+1), i even, j = 0 .. a_(i+2), at value |theta_i| - j |theta_(i+1)| (falling from |theta_i| to |theta_(i+2)|); those of {-n r} the same with i odd, from i = -1 (n = j, value 1 - j r). Each side: take the first i of its parity (from 0, resp. -1) with |theta_(i+2)| < L; then n = q_i if |theta_i| < L (only at i = 0), else n = q_i + j q_(i+1) with j = floor((|theta_i| - L) / |theta_(i+1)|) + 1, at most a_(i+2) since |theta_(i+2)| < L. Bronze x3: |theta_k| = alpha^(k+1), q = 1, 3, 10, 33, 109, L = 2 alpha^5. n+: i = 2 (alpha^5 < L <= alpha^3), j = floor(1/alpha - 2 alpha) + 1 = floor(2.697) + 1 = 3, n = 10 + 3 * 33 = 109. n-: i = 3 (alpha^6 < L <= alpha^4), j = floor(1/alpha - 2) + 1 = 2, n = 33 + 2 * 109 = 251. From E_b, h+ = 109 and h- = -251: the derivation's. PREDICTIONS (frozen). (P1) every piece certified, at all 22. (P2) the three-gap h+, h- equal the enumerated ones per side read, a side beyond B matching any three-gap |h| > B. KILL: "uncertified pieces at c_inf: n of 22", n > 0; and for (P2) "three-gap h != enumerated h at n sides", n > 0. A certified piece holding a key of the hull is an instrument fault (the window's exclusion is proved), printed apart. CONTROLS (read before the verdict). (a) bronze x3's first piece: E_b = (99, 30), h+ = 109, h- = -251 on the reduced flag (B = 369), and on the full flag (B = 242.7) h+ = 109 and h- beyond B, as derived. (b) SOUNDNESS, as keyweld.py's (c): at every c from the first with pinned moves to c_inf, every stranded (key, reply) pair of H(c) inside a piece lies in an uncertified one. (c) THE PLANT, in the direction it pushes: h+ and h- doubled must certify some piece holding a stranded pair below c_inf, so (b) can fire. (d) the enumeration bound: with B doubled, each side read inside B unchanged, and each side beyond B still beyond B or read with |h| > B (it reads nothing and left the script: FINDINGS). AFTER THE FREEZE, before any engine: the bound was 4 (Z_hi - Z_lo) + 4 alone, 139.7 at bronze x3's full flag, below |h-| = 251, so (a) could not print and (d) would fire; B gained the range's reach from G_E and the reading of a side beyond it; (d) and (P2) read per side (the first repair of (d), "where read", still fired at the full flag once B doubled). FINDINGS (the --wide run, copied from its prints; the bare run prints the same pieces, P1, P2 and (a), with (b) at 159 pairs and (c) at 34, its cells being m = 2 .. 5). CONTROLS. (a) bronze x3's first piece, E_b = (99, 30): full flag B 242.67, h+ 109, h- beyond B; reduced B 368.89, h+ 109, h- -251; as derived. (b) 1165 stranded (key, reply) pairs of H(c), c <= c_inf, lie in pieces, 0 in a certified one (keyweld.py's control (c) counts the same 1165). (c) h+ and h- doubled certify pieces holding 48 stranded pairs: (b) can fire. (d) B doubled: 0 of 88 sides changed or brought inside at |h| <= B; it reads nothing, as enum_side returns the least n, which no larger B can move, and it left the script after the run. The fault print (a certified piece holding a stranded pair at c_inf) prints 0 on an empty population: keyweld.py's (c) finds no stranded pair at c_inf. P1, KILL MISSED. Uncertified pieces at c_inf: 0 of 22; per cell (pieces, certified) golden x2 (2, 2), silver x2 (4, 4), bronze x3 (6, 6), V1 x2 (6, 6), V1 x3 (2, 2), V2 x4 (2, 2). At bronze x3 only E_b's window holds the range (E_a's low margin is -182 to -218); at the other 16 pieces both ends' do. The least margin of a holding window is 3, at golden x2's full flag, both ends' low side. P2, KILL MISSED. Three-gap h != enumerated h at 0 sides: 80 read inside B agree, 8 beyond B carry three-gap |h| > B: E_b's h- at bronze x3's 3 full-flag pieces, E_b's h+ at silver x2's 4, and E_a's h+ at V1 x2's first t = 2 reduced-flag piece. (n+, n-) per cell: golden x2 (13, 21), silver x2 (99, 70), bronze x3 (109, 251), V1 x2 (19, 31) at t = 1 and (29, 40) at t = 2, V1 x3 (69, 50), V2 x4 (251, 198): 7 distinct (r_t, L), toy-scale, none reaching three_gap's n = q_0 branch. So the class step at every piece read is one end's first-return window, and the window is r_t's records at the piece's length L. ARGUED AFTER THE RUN. c_inf is the least c with pinned moves at which every piece passes, at all 48 (rule). The certificate is a proof (kappa_t > 0, so Z = G + kappa_t y puts every hull key of the piece in the G-range; a key strictly inside a window is ruled out by the first returns, dG = 0 forcing v = 0 as L < len V < 1): a passing piece holds no hull key. A key of H(c) is stranded after reply d iff it lies in one of that reply's pieces (forbidden is built so; keyweld.py's control (e), 0 apart at c <= c_inf). At c < c_inf with pinned moves H(c) has a stranded key (hull.py's HULL-WI: the first c whose hull strands nothing is c_inf at all 48), so some piece fails. At c_inf the 22 pieces all lie at the 6 cells above (the per-cell table) and all pass; the other 42 have none. DERIVED AFTER THE RUN (by hand, read off induct.py's Field.valid; its print was added after the run). The full window is V(t, F) = [-P_1 - m R_0, P_0 - m R_1], P_k = |theta_(t+k) / theta_(t-1)|, R the sorted pair (-1)^c P_c, (-1)^(c+1) P_(c+1), so len V(t, F) = P_0 + P_1 - m (P_c + P_(c+1)). The zero reply's gap between consecutive translates is r_(t+1) - len V(t+1, F), and its preimage, scaled by r_t, has length, in units of |theta_(t-1)|, L = m (|theta_(t+c+1)| + |theta_(t+c+2)|) - |theta_(t+2)|, positive exactly where c_ov's bar fails at phase t + 1. Bronze x3, t = 0, c = 2: 3 (alpha^4 + alpha^5) - alpha^3 = alpha^3 (3 alpha + 3 alpha^2 - 1) = 2 alpha^5, as 3 alpha = 1 - alpha^2. Golden x2, c = 3: 2 (phi^-5 + phi^-6) - phi^-3 = phi^-4 (2 - phi) = phi^-6. Both as printed, and the print of L against l_formula reads 0 of 22 zero-reply pieces apart, exactly, at the bare and --wide runs (in a scratch copy with c + 1 put for c, 22 of 22 apart: it can fire, though the script makes no such print); so none of the 22 is clipped. A piece clipped at an end of V(t, f) is shorter. So, unclipped, the window's side is q-scale in alpha's coordinates: n+ and n- are r_t's records at that L. The ends' G_E should be integer combinations, with m, of the U of theta_(t+j) = U theta_t + V theta_(t-1) (induct.py's uv read from phase t - 1; at bronze 99 = 3 * 33 and 317 = 99 + 2 * 109), not derived; the hull's G-range is Z_lo, Z_hi less kappa_t y, and Z_lo, Z_hi are the Z of integer keys in the U_k, V_k of q_(n+k) = U_k q_n + V_k q_(n-1), the policy argued and the starts read, at c_inf at decide.py's 136 cells (hullform.py). RUN RECORD. Bare 1.3 s, --wide 2.8 s. The engine was written whole after the hand derivation of the three-gap sides and run once bare, once --wide, nothing changed between. After the run control (d) left, the piece-length print was added (every earlier line unchanged), and the verdicts were made the exit code: 0 iff (a) holds as printed, (b) finds stranded pairs and none in a certified piece nor a fault, (c) certifies a piece holding one, P1's 0 of 22 with its per-cell table, P2's 80 read and 8 beyond B with 0 sides apart, and the length's 0 of 22. --wide 2.8 s, peak commit 8.9 MB. Usage: python firstreturn.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, QF, le # noqa: E402 from hull import Coords, hull, hull_set, eq # noqa: E402 from keyweld import forbidden, lattice_key, lt, stranded # noqa: E402 WIDE = "--wide" in sys.argv def abs_q(x): return x if x.sign() >= 0 else QF(0) - x def frac_up(n, r): """{-n r} = ceil(n r) - n r, exact, n > 0.""" y = QF(math.ceil(n * r.f)) - r * n if y.sign() <= 0: y = y + QF(1) elif not lt(y, QF(1)): y = y - QF(1) assert y.sign() > 0 and lt(y, QF(1)) return y def enum_side(r, L, B, up): """The least n in 1 .. floor(B) with {-n r} < L (up) or {n r} < L, else None (beyond B).""" for n in range(1, math.floor(B) + 1): y = frac_up(n, r) if not up: y = QF(1) - y if lt(y, L): return n return None def three_gap(F, t, L): """(n+, n-) from r_t's records, as derived by hand.""" r = F.r[t] assert math.floor(1 / r.f) == F.a(t + 1) th = {-1: QF(-1), 0: r} q = {-1: 0, 0: 1} k = 0 while not (lt(abs_q(th[k]), L) and lt(abs_q(th[k - 1]), L)): a = F.a(t + k + 1) th[k + 1] = th[k] * a + th[k - 1] q[k + 1] = q[k] * a + q[k - 1] assert lt(abs_q(th[k + 1]), abs_q(th[k])) assert th[k + 1].sign() == (-1) ** (k + 1) k += 1 th[k + 1] = th[k] * F.a(t + k + 1) + th[k - 1] out = [] for i0 in (0, -1): i = i0 while not lt(abs_q(th[i + 2]), L): i += 2 if lt(abs_q(th[i]), L): out.append(q[i]) continue num, den = abs_q(th[i]) - L, abs_q(th[i + 1]) j = math.floor(num.f / den.f) + 1 # exact floor + 1: while j > 1 and lt(num, den * (j - 1)): j -= 1 while le(den * j, num): j += 1 assert 1 <= j <= F.a(t + i + 2) out.append(q[i] + j * q[i + 1]) return out[0], out[1] def l_formula(F, t, m, c): """m (|theta_(c+1)| + |theta_(c+2)|) - |theta_2|, r_t's own theta's (theta_(-1) = -1, theta_0 = r_t): the unclipped zero-reply piece's length, derived after the run.""" th = {-1: QF(-1), 0: F.r[t]} for k in range(c + 2): th[k + 1] = th[k] * F.a(t + k + 1) + th[k - 1] return (abs_q(th[c + 1]) + abs_q(th[c + 2])) * m - abs_q(th[2]) def g_range(co, t, ya, yb, zlo, zhi): k = co.kap[t] return (math.floor(zlo.f - k.f * yb.f), math.ceil(zhi.f - k.f * ya.f)) def read_piece(F, co, t, pc, zlo, zhi, bmul=1): """Per end that is a lattice key: (side, E, G_E, B, h+, h-) by enumeration, None for a side beyond B; and the G-range.""" ya, yb, ca, cb = pc L = yb - ya glo, ghi = g_range(co, t, ya, yb, zlo, zhi) span = 4 * (zhi.f - zlo.f) + 4 r = F.r[t] ends = [] for side, y in (("a", ya), ("b", yb)): E = lattice_key(F, t, y) if E is None: continue GE = E[0] B = bmul * (max(abs(glo - GE), abs(ghi - GE)) + span) hp = hm = None if L.sign() > 0: # from E_a: h+ reads {-n r}, h- reads {n r}; E_b the mirror hp = enum_side(r, L, B, up=(side == "a")) hm = enum_side(r, L, B, up=(side == "b")) ends.append((side, E, GE, B, hp, None if hm is None else -hm)) return ends, (glo, ghi) def certified(F, co, t, pc, zlo, zhi, ends, grange, scale=1): """No key of the hull in the piece: no closed end in the hull, and some end's first-return window holds the G-range.""" ya, yb, ca, cb = pc for closed, y in ((ca, ya), (cb, yb)): if closed: E = lattice_key(F, t, y) if E is None: return False z = co.Z(*E, t) if le(zlo, z) and le(z, zhi): return False if not lt(ya, yb): return True glo, ghi = grange for side, E, GE, B, hp, hm in ends: lo_ok = hm is None or glo > GE + scale * hm hi_ok = hp is None or ghi < GE + scale * hp if lo_ok and hi_ok: return True return False def inside(y, pc): ya, yb, ca, cb = pc return ((le(ya, y) if ca else lt(ya, y)) and (le(y, yb) if cb else lt(y, yb))) def main(): t0 = time.time() maps = (2, 3, 4, 5) + ((6, 7, 8, 9) if WIDE else ()) pieces = cert_n = 0 unc, rows, per_cell = [], [], {} p2_read = p2_bad = p2_beyond = p2_beyond_bad = 0 lf_n = lf_bad = 0 sound_n = sound_bad = plant_hit = fault = 0 ctl_a = [] for name, per in PERIODIC: F = Field(per) p = F.p cname = name.split()[0] for m in maps: cinf = least(F, m, "pin") for c in range(cinf + 1): win = Window(F, m, c) st, miss = win.pin_starts() if miss: continue co = Coords(F, m, c) zhi, _ = hull(win, co, st) zlo, _ = hull(win, co, st, low=True) Hs = hull_set(win, co, zlo, zhi) strand = stranded(win, Hs) cert = {} for t in range(p): for f in (True, False): for d in win.replies(f, t): for pc in forbidden(win, t, f, d): zl, zh = zlo[(t, f)], zhi[(t, f)] ends, gr = read_piece(F, co, t, pc, zl, zh) ok = certified(F, co, t, pc, zl, zh, ends, gr) okp = certified(F, co, t, pc, zl, zh, ends, gr, scale=2) cert[(t, f, d, pc)] = (ok, okp) if c != cinf: continue pieces += 1 cert_n += ok key = f"{cname} x{m}" a0, b0 = per_cell.get(key, (0, 0)) per_cell[key] = (a0 + 1, b0 + ok) if not ok: unc.append((key, t, int(f), d)) L = pc[1] - pc[0] if d == 0: lf_n += 1 lf_bad += not eq(L, l_formula(F, t, m, c)) tg = (three_gap(F, t, L) if L.sign() > 0 else None) for side, E, GE, B, hp, hm in ends: if tg is not None: npl, nmi = tg w_p = nmi if side == "a" else npl w_m = -(npl if side == "a" else nmi) for h, w in ((hp, w_p), (hm, w_m)): if h is not None: p2_read += 1 p2_bad += h != w else: p2_beyond += 1 p2_beyond_bad += abs(w) <= B mhi = None if hp is None else GE + hp - gr[1] mlo = None if hm is None else gr[0] - GE - hm rows.append((key, t, int(f), d, round(pc[0].f, 5), round(L.f, 6), side, E, gr, round(B, 1), hm, hp, mlo, mhi, ok, tg)) if (key == "bronze x3" and t == 0 and d == 0 and abs(pc[0].f - 0.02012) < 1e-4): for side, E, GE, B, hp, hm in ends: if side == "b": ctl_a.append((int(f), E, round(B, 2), hp, hm)) for (G, H, f, t), d in strand: y = QF(H) - F.r[t] * G for (t2, f2, d2, pc), (ok, okp) in cert.items(): if (t2, f2, d2) != (t, f, d) or not inside(y, pc): continue sound_n += 1 sound_bad += ok plant_hit += okp fault += ok and c == cinf print(f" {name:20s} x{m} c_inf {cinf}", flush=True) print("== PIECES at c_inf: (cell, t, f, d, y_a, L, end, E, G-range, B, " "h-, h+, margin lo, margin hi, certified, three-gap (n+, n-))") for row in rows: print(" ", row) print("== CONTROLS") print(f" (a) bronze x3, first piece, end E_b (flag, E, B, h+, h-): " f"{ctl_a}") print(f" (b) SOUNDNESS: stranded (key, reply) pairs of H(c), c <= " f"c_inf, inside a piece: {sound_n}; in a certified one: " f"{sound_bad}") print(f" (c) THE PLANT (h+, h- doubled): stranded pairs in a piece " f"it certifies: {plant_hit}") print(f" instrument fault (a certified piece holding a key of " f"H(c_inf)): {fault}") print("== P1") print(f" per cell (pieces, certified): {per_cell}") print(f" uncertified: {unc}") print(f" KILL: uncertified pieces at c_inf: {pieces - cert_n} of " f"{pieces}") print("== P2") print(f" sides read inside B: {p2_read}; beyond B: {p2_beyond}, " f"three-gap |h| <= B there: {p2_beyond_bad}") print(f" KILL: three-gap h != enumerated h at " f"{p2_bad + p2_beyond_bad} sides") print("== THE PIECE LENGTH (derived after the run)") print(f" zero-reply pieces at c_inf whose L != m(|theta_(c+1)| + " f"|theta_(c+2)|) - |theta_2|, r_t's own theta's: {lf_bad} of " f"{lf_n}") checks = [ ctl_a == [(1, (99, 30), 242.67, 109, None), (0, (99, 30), 368.89, 109, -251)], sound_n > 0 and sound_bad == 0 and fault == 0, plant_hit > 0, pieces == 22 and cert_n == 22 and not unc, per_cell == {"golden x2": (2, 2), "silver x2": (4, 4), "bronze x3": (6, 6), "V1 x2": (6, 6), "V1 x3": (2, 2), "V2 x4": (2, 2)}, (p2_read, p2_beyond, p2_bad, p2_beyond_bad) == (80, 8, 0, 0), (lf_n, lf_bad) == (22, 0), ] print(f" {sum(checks)}/{len(checks)} checks as recorded, " f"{time.time() - t0:.1f} s") sys.exit(0 if all(checks) else 1) if __name__ == "__main__": main()