""" hulls.py -- a producer with a hull per string: does x y feed z·U past the threshold-miss law? QUESTION. chains.py's (7) predicts the two-unit chain x y -> z·U dead at (L1*, L2* - 1) wherever Lam2 - 1 > (Mh/w) min(S(L1*), room), on the budget (3), which puts one hull at each value. A level-n prefix of U is a digit STRING; its children are one per integer, but strings that share a value are distinct nodes, each covering its own fibre. Is the budget the law of that tree, or can a producer hand z·U narrower hulls? THE MODEL (frozen before this file). Level units, the deep limit made exact by bounding: every head image is at most d = 2 Mh w / b^L1 wide (level-n units), and z·U accepts every hull of width at most eta_max = (b^L2 (w - 1) - tau w)/Mh, tau = Mh^2, at any position: its image of a z box times the hull is at most (Mh |H| + tau w)/b^L2 wide in level n - L2 units (chains.py's (6)), and an interval no longer than w - 1 lies in a tile. z·U's verdict on a hull is a statement about the set alone (the tile lemma), never about the string or value holding it, and accepted hulls are downward closed, so a head image is homeless iff it is rejected as a hull. That needs tau w + Mh d > b^L2 (w - 1), at L2 = 1 Mh^2 (1 + 2/b^L1) > 1: never at Mh < 1, L1 >= 2. There the converse cannot rest on one image; it lives in the tree. A STATE (o, F) is a string whose fibre is held in [u + o, u + o + F] inside its box (-M- <= o, o + F <= M+), F <= eta. It is SUSTAINED when children e in D (one per integer, taken in increasing e), each a sustained state, cover [b o, b (o + F)] so that every window of width d lies in one child's interval. The greatest fixpoint of F(o) on a grid of offsets (step 1/G, G = (b - 1) K, so M+- are exact; d rounded up, eta down, the root range outward) is a certificate: a producer sending each (x, y) box to a child whose interval holds its image is legal and hands z·U hulls <= eta_max, so the chain lives. Children in increasing order and the grid only lose producers, never invent one. The certificate is re-verified by an exact checker over the recorded children. THE DRIFT (the estimate behind the prediction). Children at consecutive integers e_1 < ... < e_m have offsets o_(k+1) <= o_k + F_k - d - 1, so each drifts down by 1 + d - F_k inside a window of length w - F, and bF = sum_(k= 3; cells where eta* <= eta_max < 1 + d gain past (7). KILL. eta* >= 1 + d at every slack-1 product-fed cell, radices 3..40, Mh < 1: the budget is the tree's law. CONTROL, read first. At eta = 1 + d the narrowed reader's state (o = -M-, F = 1 + d) is in the fixpoint; at eta < d the root is not covered; the checker rejects a certificate with one child moved past its box. CC's 17 gaining cells certified at (2, 1) is read in the sweep's per-cell lines, not in the control. As run, against the frozen control: "at eta < d the fixpoint is empty" is read as "the root is not covered" (a state with no children keeps F = d//b, holding no image), and the narrowed state is read at o = -M- alone. H2 (designed after the record run, so the bare run checks the gain it found): (20, 8, 12) and its mirror at K = 200, (L1*, L2* - 1) = (2, 1), live at eta_max with 0 checker faults, where chains.two_unit's least is the naive sum. USAGE: python hulls.py [K [bmax]], K = 40 and bmax = 12 bare; the record run is python hulls.py 1000 40. Exit 1 if a control or an H2 check fails. FINDINGS (entered after the run; every number is a print, K = 1000). - The controls read as by hand: at (4, 2, 2) the narrowed state holds F = 1 + d (3334/3000) in one pass; at eta = d - 1/G the root is not covered; the checker passes the certificate at eta_max with 0 faults and finds 2 once one child is moved past its box. CC's 17 gaining cells are all certified, 0 faults. - THE KILL MISSED. eta* < 1 + d at 440 of the 441 cells (slack 1, product-fed, representable, Mh < 1, radices 3..40); level only at (10, 6, 4), where a-^2 = a+ (b - 1) puts the range's top on the box (M+ - hi = 0; that this is the cause is untested). The gap, in units of S/(b - 2): at least 0.6 at 438 cells, 0.435 at (4, 2, 2), 0.544 at (5, 2, 3), up to 0.947, tending up with b but not monotone in it. eta* is the grid greedy's least, an upper bound on the tree's. - A GAIN PAST (7): (20, 8, 12) and its mirror, at (L1*, L2*) - (0, 1) = (2, 1): eta* 19018/19000 <= eta_max = 1085/1083 < 1 + d = 19064/19000. x y -> z·U reads at 3 against the naive 4, which the threshold-miss law and the inset law both call dead. The certificate at eta_max is exact (0 faults, as at every one of the 19 live cells; eta* itself is not run through the checker); the K = 200 run finds the same pair, eta* 3804/3800, and nothing else. H2, run bare, prints both live at eta_max 1085/1083 with 0 checker faults, (7) reading 4. - The budget (chains.py's (3)) is not the law of the tree: it is the drift-free corner x = 0 of a producer whose strings each cover their own fibre. RUN RECORD: K = 40, radices 3..6, 0.4 s, 16.5 MB (the rehearsal); K = 200, radices 3..40, 18.2 s, 33.9 MB; K = 1000, 97.1 s, 112.4 MB (with the eta* side counts printed, 97.2 s, 112.1 MB: below 1 + d at 440, level at (10, 6, 4), live at 19); again with eta_max printed, 97.4 s, 112.4 MB, every verdict the same; all under a memory guard. Bare, with H2: 5/5 checks, 0.3 s, 22.0 MB. """ import os os.environ.setdefault("OPENBLAS_NUM_THREADS", "1") import math # noqa: E402 import sys # noqa: E402 import time # noqa: E402 from fractions import Fraction as Fr # noqa: E402 import numpy as np # noqa: E402 import chains # noqa: E402 import manystream as ms # noqa: E402 CHECKS = [] def check(name, ok, detail=""): CHECKS.append(bool(ok)) tail = f" ({detail})" if detail else "" print(f" {'PASS' if ok else 'FAIL'} {name}{tail}") class Grid: """A slack-1 product-fed cell at (L1, L2) on offsets of step 1/G.""" def __init__(self, cell, L1, L2, K): b = cell.b self.cell, self.b, self.G = cell, b, (b - 1) * K G = self.G self.Mm, self.Mp = cell.am * K, cell.ap * K self.N = self.Mm + self.Mp + 1 Mh, w = cell.Mh, cell.w tau = Mh ** 2 self.d_fr = 2 * Mh * w / Fr(b) ** L1 self.eta_fr = (Fr(b) ** L2 * (w - 1) - tau * w) / Mh self.d = math.ceil(self.d_fr * G) self.eta_max = math.floor(self.eta_fr * G) lo, hi = -cell.Mm * cell.Mp, Mh ** 2 self.lo, self.hi = math.floor(lo * G), math.ceil(hi * G) self.o = np.arange(-self.Mm, self.Mp + 1, dtype=np.int64) def greedy(self, F, start, record=False): """The furthest cover end from each start, children e in D in increasing order, each the state of largest top among offsets <= the limit. Vectorized over the starts.""" top = self.o + F PM = np.maximum.accumulate(top) if record: idx = np.where(top == PM, np.arange(self.N), 0) PA = np.maximum.accumulate(idx) me = start + self.d picks = [] for e in range(-self.cell.am, self.cell.ap + 1): j = me - self.d - e * self.G + self.Mm ok = j >= 0 jj = np.clip(j, 0, self.N - 1) cand = e * self.G + PM[jj] take = ok & (cand > me) if record: picks.append((e, np.where(take, PA[jj], -1))) me = np.where(take, cand, me) return (me, picks) if record else me def fixpoint(self, eta): F = np.minimum(eta, self.Mp - self.o) it = 0 while True: it += 1 me = self.greedy(F, self.b * self.o) new = np.minimum(F, (me - self.b * self.o) // self.b) if np.array_equal(new, F): return F, it F = new def live(self, eta): F, it = self.fixpoint(eta) me = self.greedy(F, np.array([self.b * self.lo])) return bool(me[0] >= self.b * self.hi), F, it def certificate(self, F): """Every state with its recorded children, and the root's.""" starts = np.concatenate([self.b * self.o, [self.b * self.lo]]) Fx = F me, picks = self.greedy(Fx, starts, record=True) cert = [] for s in range(len(starts)): kids = [(e, int(p[s])) for e, p in picks if p[s] >= 0] cert.append(kids) return cert def check(self, F, cert, eta, plant=None): """Exact, pure-integer: each state's interval (and the root's) is covered by its recorded children (a state with b F <= d holds no window and needs none), each a state of the set, inside its box, F <= eta, every window of width d in one.""" b, G, d = self.b, self.G, self.d Fl = [int(x) for x in F] bad = sum(x > eta for x in Fl) for s, kids in enumerate(cert): if s < self.N: o0 = s - self.Mm lo, hi = b * o0, b * (o0 + Fl[s]) else: lo, hi = b * self.lo, b * self.hi reach, last_e = lo + d, None for e, i in kids: oe = i - self.Mm Fe = Fl[i] if plant is not None and (s, e) == plant: oe += G if not (-self.cell.am <= e <= self.cell.ap): bad += 1 if last_e is not None and e <= last_e: bad += 1 if not (-self.Mm <= oe and oe + Fe <= self.Mp): bad += 1 st = e * G + oe if st > reach - d: bad += 1 reach = max(reach, st + Fe) last_e = e if reach < hi: bad += 1 return bad def eta_star(self, hi): """The least eta (grid) whose fixpoint covers the root.""" lo = self.d if not self.live(hi)[0]: return None while hi - lo > 1: mid = (lo + hi) // 2 if self.live(mid)[0]: hi = mid else: lo = mid return hi def cells1(bmin, bmax): for b in range(bmin, bmax + 1): for am in range(1, b): cell = ms.Cell(b, am, b - am) if chains.representable(cell) and cell.Mh < 1: yield cell def section_control(K): print("H0 controls") hand = ms.Cell(4, 2, 2) L1 = chains.floor_xy(hand) g = Grid(hand, L1, 1, K) narrow = g.G + g.d F, it = g.fixpoint(narrow) check("(4,2,2): at eta = 1 + d the state o = -M- has F = 1 + d", F[0] == narrow, f"L1 {L1}, d {g.d}/{g.G}, F {F[0]}, {it} passes") check("at eta = d - 1/G the root is not covered", not g.live(g.d - 1)[0]) lv, F, _ = g.live(g.eta_max) cert = g.certificate(F) bad = g.check(F, cert, g.eta_max) s = next(s for s, k in enumerate(cert) if len(k) >= 2 and F[s] >= g.d) planted = g.check(F, cert, g.eta_max, plant=(s, cert[s][0][0])) check("(4,2,2) live at eta_max, 0 checker faults, a fault once one " "child is moved past its box", lv and bad == 0 and planted > 0, f"faults {bad}, planted {planted}") def section_tree(K=200): """H2: the gain past (7), at (L1*, L2* - 1), checked bare.""" print(f"H2 (20, 8, 12) and its mirror, K {K}") for cell in (ms.Cell(20, 8, 12), ms.Cell(20, 12, 8)): L1 = chains.floor_xy(cell) naive, least, _, _ = chains.two_unit(cell, chains.xy_head) g = Grid(cell, L1, 1, K) lv, F, _ = g.live(g.eta_max) bad = g.check(F, g.certificate(F), g.eta_max) if lv else None check(f"({cell.b},{cell.am},{cell.ap}) at ({L1}, 1): the tree " f"lives where (7) reads the naive {naive}", lv and bad == 0 and least == naive and L1 + 1 == naive - 1, f"checker faults {bad}, eta_max {g.eta_fr}") def main(): K = int(sys.argv[1]) if len(sys.argv) > 1 else 40 bmax = int(sys.argv[2]) if len(sys.argv) > 2 else 12 t0 = time.time() section_control(K) if not all(CHECKS): print("CONTROL FAILED; nothing below is read") raise SystemExit(1) section_tree() print(f"H1 eta* against 1 + d, K {K}, radices 3..{bmax}") rows, side = [], [] for cell in cells1(3, bmax): L1 = chains.floor_xy(cell) lam2 = cell.Mh ** 2 + cell.Mh L2 = 1 if lam2 > 1 else 0 naive, least, _, S0 = chains.two_unit(cell, chains.xy_head) law = least < naive g = Grid(cell, L1, L2, K) lv, F, it = g.live(g.eta_max) if g.eta_max >= g.d else (False, None, 0) cap = g.G + g.d + 2 * g.G es = g.eta_star(min(cap, g.Mm + g.Mp)) S = cell.w - 1 - g.d_fr gap = None if es is None else (Fr(g.G + g.d - es, g.G)) / ( S / (cell.b - 2)) if cell.b > 2 else None bad = None if lv: bad = g.check(F, g.certificate(F), g.eta_max) rows.append((cell.b, cell.am, cell.ap, L1, L2, law, lv, bad, es, gap)) side.append(None if es is None else (es > g.G + g.d) - (es < g.G + g.d)) tag = "GAIN" if lv and not law else ("gain" if lv else "") print(f" ({cell.b},{cell.am},{cell.ap}) L1 {L1} L2 {L2}: law " f"{'gain' if law else 'none'}, model {'live' if lv else 'dead'}" f"{'' if bad is None else f' (faults {bad})'}; eta* " f"{es}/{g.G} vs 1+d {g.G + g.d}, eta_max {g.eta_fr}, gap/(S/(b-2)) " f"{'-' if gap is None else f'{float(gap):.3f}'} {tag}") print(f" eta* below 1 + d at {side.count(-1)}, level at " f"{[r[:3] for r, x in zip(rows, side) if x == 0]}, above at " f"{side.count(1)}, none at {side.count(None)}; model live at " f"{sum(1 for r in rows if r[6])}") past = [r[:3] for r in rows if r[6] and not r[5]] lost = [r[:3] for r in rows if r[5] and not r[6]] print(f" cells {len(rows)}; model live where (7) says none: {past}; " f"(7) gains the model misses: {lost}") print(f"{sum(CHECKS)}/{len(CHECKS)} checks passed, " f"{time.time() - t0:.1f} s") raise SystemExit(0 if all(CHECKS) else 1) if __name__ == "__main__": main()