""" floor.py -- the private zone: a floor under every producer of x y feeding z·U, and the threshold-miss pair priced by it. QUESTION. hulls.py's tree certifies (x y)·z live at (L1*, L2* - 1) where its least hull eta* <= eta_max, but its dead verdicts price nothing. Is there a floor every producer obeys, and which cells does it decide? THE FLOOR (derived before this file). A string's children are one per digit e, child e's hull inside [e - M-, e + M+] in the parent's scaled frame, so the window starts e can hold lie in [e - M-, e + M+ - d]. Those of e and e + 2 are separated by 2 - w + d > 0 (b >= 3), so every window starting between them goes to e + 1. Near the product's corner the images are dense (every window of width d(1 - eps) lies in one, at every level past some n0 and within some delta of the corner), and a string holding every image on a start interval of length >= 2 - w + d hands its children every sub-image on b times it, which holds such a zone again. So every producer has, at infinitely many deep levels, a fibre holding an interval of width 1 + d - S - o(1), S = w - 1 - d, near the point the held zones track: the corner itself only where the tracked zones never leave it (tracked at width d they leave it at 151 of the 274 dead L2 = 1 cells; see FINDINGS). The consumer's half: a fixed distance below the corner, z near its extreme sweeps the start of z box times that interval through every position modulo the zones, so a fibre wider than eta_max by a margin kills z·U by the tile lemma; at the corner the sweep is bounded, and THE FAR REGIME moves the chain a fixed distance below. The derivation's verdict, dead wherever eta_max < 1 + d - S, is NOT carried: FINDINGS derive dead the 148 cells at L2 = 0 and live the 19 where eta_max >= eta*, and dead the 274 dead L2 = 1 cells by THE FAR REGIME on THE HONEST TRACKING, its gaps and widths at fixed delta derived and printed at toy scale (THE FIXED DELTA). (G) in full: at level n, x and y boxes a and c steps below the top value at depth t = n + L1, the image starts (level-n units) at Mh^2 b^n - Mh (a + c + 2w)/b^L1 + (a + w)(c + w)/b^(n + 2 L1), its width (|x| + |y|) w/b^L1 + O(b^-n). At absolute distance delta below the corner s = a + c is about delta b^t/Mh; within one s the starts step by at most s/b^(n + 2 L1) = (delta/Mh^2) p and spread over about s^2/(4 b^(n + 2 L1)), past a pitch once delta >~ 2 Mh^(3/2) b^(-t/2). One image's sub-images are the 2b + 1 windows b s + k p, k = 0..2b, spanning b d (b + w = b w): density comes from many images. (C) in full: a fibre J at U level m and z at depth m near its extreme give z box times J of width ((Mh - delta')|J| + (Mh^2 - delta) w)/b^L2 in level-(m - L2) units; it strictly contains a zone iff its start lies in an open set of length W - (w - 1) per period, and the start moves by J_lo/b^L2 per z step, J_lo = Mh^2 - delta_J, drifting on each residue class of Z mod (b - 1)^2 b^L2 by (b - 1)^2 delta_J per period. Over the usable z boxes (eps < eps_c below the extreme) the drift totals eps_c delta_J b^m/b^L2: dense only where delta_J b^m is large, a fixed distance below the corner, and O(1) at the corner itself. PREDICTIONS (frozen, with the derivation). (FP1) 1 + d - S <= eta* at every cell. (FP2) 19 live, 407 dead, 15 open over the 441 representable slack-1 cells with Mh < 1, radices 3..40 (read off hulls.py's prints before the freeze; a reproduction). (FP3) the dense limit: at (4, 2, 2) and (7, 3, 4), images x, y boxes a, c <= S0 steps below the top at depth t = n + L1, on the start band of s = a + c in [S0/4, S0/2]: largest gap between starts <= (delta/Mh^2) p, least width >= d (1 - delta/Mh^2), delta = Mh S0/(2 b^t), p = Mh/b^L1. (FP4) at the dead cell (5, 2, 3) the zone's interval near the corner is killed by some z box near the extreme, and a hull of width eta_max at the same start by none. KILL. The dead set is withdrawn if FP1 fails at any cell or FP4 finds no killing z box; FP3 failing at the deepest level withdraws the dense limit as proved. THE ZONE CHAIN (frozen after the record run of FP1-FP4, before its arm). Between consecutive private zones P_j, P_(j+1) lies an overlap O_j of length S that only the ranges of j and j + 1 reach, so if a parent holds every start on k consecutive zones and the overlaps between them, child j's hull is at least |P_j| + d + x_j + y_(j-1), x_j + y_j >= S, and some hull is at least 1 + d - S/k. Only the ranges' convex hulls enter, so fibres may interleave or have gaps. A fully held zone hands its children every start on an interval of length b (2 - w) + (2b - 1) d, which holds k >= b - 2 such zones: every producer has near the corner a hull >= 1 + d - S/(b - 2). [Narrowed: only the core [b P.lo + 2bp, b P.hi] is held in full, since starts below b P.lo + 2bp also come from images below P; its length is b (2 - w) + d, which still holds k = b - 2 zones with exactly one unit of alignment to spare. At the corner even that fails: the held range below the corner is the core cut at the corner's start, b (r - P.lo) long, and may hold fewer than b - 2 complete zones.] (FP5) that floor <= eta* at every cell (a violation kills the argument). (FP6) no open cell: 19 live, 422 dead. THE TRACKED CORNER (the control at width d). Track the corner through held zones, every window d wide: at level n the frame's corner start x, the digit j whose zone holds it, the offset r = x - j, the next start b r + (b - 1) d. It exits where x falls into an overlap or below the held core, or cycles. (FP7) by hand at (5, 2, 3): r = -0.2625, -0.0125, 0.2375, 0.4875, then -0.2625 again. THE FAR REGIME (frozen before its arm). In a held range [lo, x] the top complete zone e has its top e + 1 - M- a distance D below the corner end x + d; its child holds the core [b P.lo + 2bp, b P.hi], whose top is the zone's top, and the core's top complete zone has its top there too: c1 - 1 + M- = b - 1 - a- is an integer (as in FP18), so the nested zones share one top and shrink onto it. Zone tops do not depend on the image width (P.hi = e + 1 - M- is where e + 1 starts), so the chain's point is delta* = D/b^l below the corner, l the first zone's level: at an overlap exit the zone below the overlap holding x, or back up the tracked levels while it is not complete. (As frozen, delta* carried a term g/(b - 1) with g = c1 - (e1 + 1 - M-), which is 0 at every cell.) At a cycling cell the chain starts at any cycle level with a complete zone below the corner, so delta* -> 0 along the cycle, each delta* > 0 a far regime of its own (m -> oo after l is fixed): dead iff the margin's limit at delta -> 0+ is positive. At delta below the corner: an image whose top is x_hi y_hi has width (x_hi + y_hi) w/b^L1 - w^2/b^(n + 2 L1) >= d_min = d sqrt(1 - delta/Mh^2) in the limit, since x_hi + y_hi >= 2 sqrt(x_hi y_hi); along a diagonal a + c = s the starts step by s - 2a - 1 units of b^-(n + 2 L1), and Mh u - u^2/4 <= delta for u = (s + 2w)/b^t, so the gaps are at most gamma = 2 (1 - sqrt(1 - delta/Mh^2)) p once the diagonals overlap (true at fixed delta). With zones private for windows d_min wide, a child taking starts l_j..h_j has hull >= h_j + d_min - l_j and no start lies in (h_j, l_(j+1)), so over k zones some hull is at least F = 1 + d_min - (w - 1 - d_min)/k - (1 + 1/k) gamma. The consumer, z near its extreme and J's low end delta below the corner, kills iff |J| > eta_max(delta) = eta_max + delta w/Mh, its sweep dense once eps_c delta b^m/b^L2 passes sigma. k = k_core, the complete zones of a full core. (FP17) the 163 exits are overlap exits, levels 1 to 37. (FP18, amended after its first run, which found b - 1 at every cell: the core's bounds a+ - b + 1 + (b - 1)(d - d_min) and b - 1 - a- are integers at d_min = d) k_core is b - 1 at d_min = d and b - 2 while 0 < (b - 1)(d - d_min) <= 1. (FP19) F - eta_max <= 0 at every live cell, which FP5 makes structural once k_core is right (an over-count by one and a tripled delta term both pass it, scratch copies, run). (FP20) the limit margin 1 + d - S/(b - 2) - eta_max > 0 at all 123 cycling dead cells, (7, 3, 4) among them. (FP21, a lean) exits at levels 1 and 2 fail, most of the 151 die. (FP22, the consumer's control) at (5, 2, 3), delta = 1/10, m 6: an interval eta_max(delta) + 0.05 wide is killed by some z box, one 0.05 narrower by none (a threshold of eta_max - delta w/Mh fails it). (FP22-, the consumer's - side, frozen before its arm at the mirror (5, 3, 2), which is not representable, then moved after its first run to (7, 4, 3)) the same where the - side binds (Mh = M-): z from its least value up, each image [z_lo J_hi, z_hi J_lo], its width |z_lo| |J| + J_lo w/b^m as on the + side. KILL (frozen): a cell is dead here iff its printed far margin F(delta*) - eta_max(delta*) exceeds 1e-9; FP19 or FP22 or FP22- failing withdraws the regime. THE HONEST TRACKING (frozen before its arm). Level n, t = n + L1, u = b^-t; a box a steps in from an extreme M has |hi| = M - a u, so a pair (a, c) at the extremes M, M (M = Mh, or when a- != a+ the other extreme Ml, both factors of its sign) starts (M - (a + w) u)(M - (c + w) u) and is (2M - s u) w u - w^2 u^2 wide, s = a + c, scaled by b^n: the width depends on s alone and falls with it, and on a diagonal the start is highest at a = floor(s/2). So the least width of the windows starting at or above a frame point sigma0 is the width at the largest s whose balanced start reaches sigma0, over both extremes (W_z, exact, by bisection on s). The frame: the corner end E_n is exact (E_1 = b Mh^2, E_(n+1) = b (E_n - j_n)), and so is it at width d (x + d); j_n = ceil(E_n - M+), the least digit whose range reaches the corner end, is a function of E_n alone, so the two trackings take the same digits and part only at a test. The corner window is d - eps_n wide, eps_n = w^2/b^(n + 2 L1): it exits into the overlap iff E_n - d + eps_n >= j_n + 1 - M-. Zone j's honest bottom is sigma_j = j - 1 + M+ - W_z(j - 1 + M+ - d) (every window starting above it overhangs j - 1's range, since W_z bounds their widths); it is complete iff sigma_j >= lo_n, the held range's low end; lo_(n+1) = b (max(sigma_j, lo_n) - j_n) + 2bp (an incomplete zone passes on the part it holds; the spread of a window's sub-image starts is 2bp - (2w - 1) b/b^(n + 2 L1) <= 2bp). At width d the completeness margin sigma_j - lo_n is the integer j_n + a- - 1, since (b - 1) d = 2bp, so a level at margin 0 fails honestly. The far start: at an exit the zone e = floor(x_n - 1 + M-) if complete, else back up the levels taking j - 1. A cycling cell's E cycles exactly; past level N the honest deficits (eps_n, the zone bottoms' d (1 + d)/(Mh^2 b^n) + eps_n) fall by about b a level and the low end's excess by a cycle (a margin-0 level multiplies it by b), so its tail is read from the last cycle's prints. (FP23, step (0), a lean) at level 1 alone (the root holds every image, no tracking) the far margin at delta*_1 = D_1/b is positive at fewer than half of the 274 dead L2 = 1 cells: D_1 is spread over [d, 1 + d) and the margin falls about w/Mh per unit of delta. (FP24, control) a brute scan of every box pair at levels 1 and 2 (3 at b <= 5) at (4, 2, 2), (5, 2, 3), (5, 3, 2), (7, 3, 4), (7, 4, 3) gives W_z exactly at the three zone bottoms below the corner. (FP25) the margin j_n + a- - 1 prints as an integer at every tracked level. (FP26, a lean) the honest paths part from the width-d paths at a few cells, at margin-0 levels and where the other extreme reaches the level-1 zone; a far margin is unchanged wherever its far start is. KILL (frozen): a dead L2 = 1 cell is dead iff, on the honest tracking, its exit's far margin at the honest delta* prints above 1e-9, or it cycles through level N with no honest exit, eps_N below the cycle's least overlap margin (printed), the low end's excess below 1, a complete zone wholly below the corner start at some cycle level, and its limit margin above 1e-9; every other dead L2 = 1 cell is open. FP24 or FP25 failing stops the verdicts. THE FIXED DELTA (frozen before its arm). THE FAR REGIME's gaps and widths at a fixed absolute delta are derived; here they are printed. At level n, every pair at both extremes whose start lies within h = 4p/b^n of delta below the corner, exactly (int64 while ((b - 1) b^t)^2 Mh^2 fits). The diagonals overlap once delta >= 2 Mh^(3/2) b^(-t/2) ((G)), from a level n_ov. (FP27) the largest gap between consecutive starts is at most gamma(delta + h) at every level from n_ov on (a ratio printed per level, falling with n); (FP28, by AM-GM, a check of the code) the least width is at least d sqrt(1 - (delta + h)/Mh^2) - eps_n. Run at delta*_1 = D_1/b of (5, 2, 3), (7, 4, 3), (10, 6, 4) and (28, 11, 17), levels 1 to the last under 4 million pairs. KILL: a gap above gamma(delta + h) at a level past n_ov withdraws the gap bound as derived, and with it every far verdict (by the exit status; the verdicts print before it). CONTROL, read first: FP4's two arms and FP7 stop the run before the sweep; FP1 stops it before THE FAR REGIME and F2; FP22 and FP22- stop every far verdict. USAGE: python floor.py [K [bmax]], K = 40 and bmax = 12 bare; the record run is python floor.py 200 40. Exit 1 if a check fails. FINDINGS (entered after the run; every number is a print of K = 200, or of a scratch copy named with it). - The controls read as derived: a hull of width eta_max at (5, 2, 3) is killed by none of 3000 z boxes; the zone's interval, of width 1 + d - S = 9/10, by 20 of them. The floor is below eta* at all 441 cells. - FP2 reproduced: 19 live, 407 dead, 15 open, every open cell with eta_max < 1: (7, 3, 4), (10, 4, 6), (10, 6, 4), (15, 6, 9), (18, 7, 11), (23, 9, 14), (28, 11, 17), (31, 12, 19), (36, 14, 22), (39, 15, 24) and the mirrors of five of them. - The zone chain's floor 1 + d - S/(b - 2) is below eta* at all 441 cells (FP5) and above eta_max at all 422 the tree does not certify (FP6), 148 of them at L2 = 0 where eta_max < 0 needs no floor (the largest eta_max there printed, -0.3867). eta* sits above the chain floor by 0.069 to 1.015 of S/(b - 2). - THE TRACKED CORNER, at width d: the hand cycle at (5, 2, 3) reproduces (FP7), and the completeness margin is j + a- - 1 at all 7185 tracked levels (FP25). The corner stays in zones forever at 123 of the 274 dead L2 = 1 cells, the witness (5, 2, 3) among them; at the other 151 it falls into an overlap at some level, and the held zones then stop a fixed distance below it, where the images are narrower than d and eta_max is larger. The 19 live cells stand on the tree's certificate either way (7 reach the corner, 12 exit). All 163 exits are overlap exits (FP17), at levels 1 to 37 (none at 36), 5 at level 1 and 7 at level 2. - THE HONEST TRACKING. w_z equals the brute scan of every box pair at 38 zone bottoms (one more lies below 0, where w_z refuses), the other extreme setting the least at 4 of them (FP24). Level 1 alone: the far margin at delta*_1 = D_1/b is positive at 260 of the 274 dead cells (FP23's lean falsified: the limit margins have median 0.5289, and the margin falls 1.054 to 1.835 per unit of delta); the 14 it misses are the plain floor's 15 open cells less (10, 6, 4); D_1 runs 0.0039 to 0.9771, the width deficit d - W_z at the zone 1.66e-05 to 1.65e-02, and the level-2 core holds its top zone complete at every cell. Tracked honestly no path parts from the width-d paths (FP26's lean falsified); at 5 of the 151 exits the exit zone sits at margin 0, fails honestly, and the far start backs up a level ((11, 4, 7): level 7, D = 19/100, for level 8, D = 9/100). The 123 cycling dead cells pass the tail: eps_N at most 1e-7 of the least overlap margin, the low end's excess at most 0.00013 (0.00131 a cycle before), a complete zone below the corner start at all 123. Read after the run: each far start's child holds its core's top zone complete, at all 163 exits and at every held cycle level of the 130 cycling cells, and each cycling cell's excess is no larger than a cycle before. - THE FAR REGIME, on the honest tracking: the far margin is positive at all 151 exiting dead cells, at every first-zone level (FP21's lean falsified), least 0.00620 at (28, 11, 17), first zone at level 6, every delta* at most 1/(9b); the limit margin is positive at all 123 cycling dead cells, least 0.02290, (7, 3, 4) at 0.03254 with k_core 5 (FP20). k_core is b - 1 at d_min = d and b - 2 just below at every L2 = 1 cell (FP18 as amended); far_margin's closed zone count k (not k_core) is b - 2 at every dead exit's delta*. The consumer's control: at delta = 1/10, eta_max(delta) = 0.8958, 3 of 3000 z boxes kill the wider interval and none the narrower (FP22), and on the - side at (7, 4, 3), eta_max(delta) = 1.1472, 6 and none (FP22-; it fails with the + side's image ends, with z from the top, or at eta_max - delta w/Mh, scratch copies, run). By the frozen kill all 274 dead L2 = 1 cells are dead, none open; the far margin is at most 0 at the 19 live cells (FP19), a margin read at each of them. - The dense limit, at the deepest level run: at (4, 2, 2), n = 6, the largest start gap is 0.0095 p against the bound 0.0239 and the least width 0.98796 d against the checked bound 1 - delta/Mh^2 = 0.976; at (7, 3, 4), n = 4, 0.0071 p against 0.0178, width 0.99103 d. Gaps shrink by about b every two levels (4 at b = 4, 6.8 at b = 7), as the band's design (delta shrinking with n) makes them; the gap against its bound holds near 0.35 to 0.4. A check to n <= 6 does not prove the limit, nor measures a fixed delta. - THE FIXED DELTA, at delta*_1: the band enumerator equals the outer product of every box pair at (5, 2, 3) and (7, 4, 3), levels 1 and 2. Past the overlap the largest gap against gamma(delta + h) is at most 0.708 at (5, 2, 3) (n 2 to 7, falling to 0.002), 0.379 at (7, 4, 3) (n 1 to 5, to 0.001), 0.937 at (10, 6, 4) (n 2 to 5, to 0.006) and 0.347 at (28, 11, 17) (n 1 and 2, to 0.026) (FP27); before it, at n 1, the gap is 5.760 and 30.224 gammas at (5, 2, 3) and (10, 6, 4). At fixed delta gamma is fixed in level-n units and the starts fill in, so the bound loosens with depth. The least width is at or above d sqrt(1 - (delta + h)/Mh^2) - eps_n at every level (FP28). Toy scale: four cells, at most 1.4 million pairs a level. RUN RECORD: bare (K = 40, radices 3..12), 0.5 s; K = 200, radices 3..40, 17.5 s, 152.8 MB with the chain arm; with THE FAR REGIME, 17.9 s, 156.8 MB; with THE HONEST TRACKING, 20.6 s, 157.8 MB; with THE FIXED DELTA, 21.0 s, 158.2 MB; one tracker, the corner's own arms cut, 20.8 s, 156.8 MB; with FP22- at (7, 4, 3), 20.8 s, 156.0 MB; with the L2 = 0 eta_max and FP19's margins printed, 20.9 s, 157.5 MB; under a memory guard. """ 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 hulls # 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}") def numbers(cell): """(L1, L2, d, S, the floor 1 + d - S, eta_max), exact.""" b, Mh, w = cell.b, cell.Mh, cell.w L1 = chains.floor_xy(cell) L2 = 1 if Mh ** 2 + Mh > 1 else 0 d = 2 * Mh * w / Fr(b) ** L1 S = w - 1 - d eta_max = (Fr(b) ** L2 * (w - 1) - Mh ** 2 * w) / Mh return L1, L2, d, S, 1 + d - S, eta_max def zone_kills(cell, m, delta_J, R, width=None, side=1): """Kills of z box times J at the consumer's level m - L2, z at depth m from the top value down R steps (side -1: from the least value up); J the private zone's interval at U level m (or an interval of the given width at its start).""" b, Mm, Mp = cell.b, cell.Mm, cell.Mp L1, L2, d, S, fl, em = numbers(cell) B = Fr(b) ** m v = math.floor((cell.Mh ** 2 - delta_J) * B) lo = v - (1 - Mp + d) hi = v + 1 - Mm + d if width is None else lo + width Jlo, Jhi = lo / B, hi / B Zmax = cell.ap * (b ** m - 1) // (b - 1) Zmin = -cell.am * (b ** m - 1) // (b - 1) n = m - L2 kills = 0 Zs = range(Zmax, Zmax - R, -1) if side == 1 else range(Zmin, Zmin + R) for Z in Zs: if side == 1: ilo = (Z - Mm) / B * Jlo * Fr(b) ** n ihi = (Z + Mp) / B * Jhi * Fr(b) ** n else: ilo = (Z - Mm) / B * Jhi * Fr(b) ** n ihi = (Z + Mp) / B * Jlo * Fr(b) ** n k = math.floor(ilo + Mm) if k + Mp < ihi and k + 1 - Mm > ilo: kills += 1 return kills, hi - lo def section_witness(): print("F0 the consumer's half at the dead cell (5, 2, 3)") cell = ms.Cell(5, 2, 3) L1, L2, d, S, fl, em = numbers(cell) k0, wd0 = zone_kills(cell, 6, Fr(1, 100), 3000, width=em) check("a hull of width eta_max is never killed", k0 == 0, f"width {wd0}, kills {k0} of 3000 z boxes") k1, wd1 = zone_kills(cell, 6, Fr(1, 100), 3000) check("the private zone's interval is killed by some z box", k1 > 0, f"width {wd1} = 1 + d - S {fl}, kills {k1} of 3000") lvl, kind, lv = honest_track(cell, honest=False, extra=0) i0 = next(i for i, t in enumerate(lv) if t[1] == lv[-1][1]) got = [float(x - j) for _, _, j, x, *_ in lv[i0:-1]] \ if kind == "cycle" else (lvl, kind) want = [-0.2625, -0.0125, 0.2375, 0.4875] check("FP7: at width d the corner's offsets x - j cycle as by hand", got == want, f"{got}") def band_pairs(cell, n, delta, h, cap=None): """Every pair at both extremes whose start lies in [Mh^2 - delta - h, Mh^2 - delta + h] at level n: (starts, widths) as int64 over ((b - 1) b^t)^2, or None past int64 or the cap.""" L1 = numbers(cell)[0] b, am, ap, Mh = cell.b, cell.am, cell.ap, cell.Mh t = n + L1 q = (b - 1) * b ** t if (q * q) * Mh ** 2 * 4 >= 2 ** 63: return None lo_s = math.ceil((Mh ** 2 - delta - h) * q * q) hi_s = math.floor((Mh ** 2 - delta + h) * q * q) ext = (b - 1) * (ap * (b ** t - 1) // (b - 1)) - am, \ (b - 1) * (am * (b ** t - 1) // (b - 1)) - ap # |lo| at a = 0 sts, wds = [], [] total = 0 for L0 in ext: A = max(0, (L0 - math.ceil(lo_s / L0)) // (b - 1)) + 1 a = np.arange(A, dtype=np.int64) La = L0 - (b - 1) * a a, La = a[La > 0], La[La > 0] clo = -((-(L0 - hi_s // La)) // (b - 1)) # ceil clo = np.maximum(clo, 0) chi = (L0 - (-((-lo_s) // La))) // (b - 1) # floor cnt = np.maximum(chi - clo + 1, 0) total += int(cnt.sum()) if cap is not None and total > cap: return None ai = np.repeat(a, cnt) off = np.arange(int(cnt.sum()), dtype=np.int64) - np.repeat( np.cumsum(cnt) - cnt, cnt) ci = np.repeat(clo, cnt) + off Lx, Ly = L0 - (b - 1) * ai, L0 - (b - 1) * ci st = Lx * Ly sts.append(st) wds.append((Lx + b) * (Ly + b) - st) # |hi| = |lo| + (b - 1) w return np.concatenate(sts), np.concatenate(wds), q def section_fixed(): print("F6 the gaps and widths at fixed delta") bad = [] for c in ((5, 2, 3), (7, 4, 3)): cell = ms.Cell(*c) L1 = numbers(cell)[0] b, am, ap = cell.b, cell.am, cell.ap for n in (1, 2): t = n + L1 q = (b - 1) * b ** t dl, h = Fr(1, 3 * b), 4 * cell.Mh / Fr(b) ** (L1 + n) X = np.arange(-am * (b ** t - 1) // (b - 1), ap * (b ** t - 1) // (b - 1) + 1, dtype=np.int64) lo, hi = (b - 1) * X - am, (b - 1) * X + ap out = [] for s in (1, -1): ml, mh = (lo, hi) if s == 1 else (-hi, -lo) keep = ml * int(ml.max()) >= (cell.Mh ** 2 - dl - h) * q * q ml, mh = ml[keep], mh[keep] st = np.outer(ml, ml).ravel() wd = np.outer(mh, mh).ravel() - st sel = (st >= math.ceil((cell.Mh ** 2 - dl - h) * q * q)) & \ (st <= math.floor((cell.Mh ** 2 - dl + h) * q * q)) out.append(np.stack([st[sel], wd[sel]])) brute = np.concatenate(out, axis=1) st, wd, _ = band_pairs(cell, n, dl, h) fast = np.stack([st, wd]) bo = brute[:, np.lexsort(brute[::-1])] fo = fast[:, np.lexsort(fast[::-1])] if bo.shape != fo.shape or not (bo == fo).all(): bad.append((c, n, bo.shape[1], fo.shape[1])) check("the band enumerator equals every box pair's outer product", not bad, f"(5, 2, 3), (7, 4, 3) at levels 1, 2, delta 1/(3b); " f"differs at {bad}") if bad: return worst = [] for c in ((5, 2, 3), (7, 4, 3), (10, 6, 4), (28, 11, 17)): cell = ms.Cell(*c) L1, L2, d, S, fl, em = numbers(cell) b, Mh, w = cell.b, cell.Mh, cell.w p = Mh / Fr(b) ** L1 n1, E, j, x, *_ = honest_track(cell, extra=0)[2][0] e = math.floor(x - 1 + cell.Mm) dl = (E - (e + 1 - cell.Mm)) / b rows = [] for n in range(1, 40): t = n + L1 ov = 2 * float(Mh) ** 1.5 * b ** (-t / 2) <= float(dl) h = 4 * p / Fr(b) ** n got = band_pairs(cell, n, dl, h, cap=4 * 10 ** 6) if got is None: break st, wd, q = got st.sort() scale = Fr(b) ** n / (q * q) gap = int(np.diff(st).max()) * scale if st.size > 1 else None qq = float((dl + h) / Mh ** 2) gam = 2 * (qq / (1 + math.sqrt(1 - qq))) * float(p) wmin = int(wd.min()) * scale wlb = float(d) * math.sqrt(1 - qq) - float( w * w / Fr(b) ** (n + 2 * L1)) rows.append((n, st.size, ov, None if gap is None else float(gap) / gam, float(wmin) / wlb)) print(f" {c} delta*_1 b = {float(dl * b):.4f}: " + "; ".join( f"n {r[0]} {r[1]} pairs{' ov' if r[2] else ''} gap/gamma " f"{r[3]:.3f} width/bound {r[4]:.5f}" for r in rows)) past = [r for r in rows if r[2]] worst.append((c, max((r[3] for r in past), default=None), min(r[4] for r in rows), rows[-1][0])) check("FP27: the gap is at most gamma(delta + h) at every level past " "the overlap", all(t[1] is not None and t[1] <= 1 for t in worst), f"largest ratio past n_ov per cell {[(t[0], t[1]) for t in worst]}") check("FP28: the least width is at least d sqrt(1 - (delta + h)/Mh^2) " "- eps_n", all(t[2] >= 1 for t in worst), f"least ratio {[(t[0], round(t[2], 5)) for t in worst]}") def section_geometry(): print("F2 the dense limit near the corner") for cell, levels in ((ms.Cell(4, 2, 2), (2, 4, 6)), (ms.Cell(7, 3, 4), (2, 4))): b, am, ap = cell.b, cell.am, cell.ap L1 = chains.floor_xy(cell) Mh = cell.Mh for n in levels: t = n + L1 S0 = int(10 * math.sqrt(float(Mh)) * b ** (t / 2)) Xmax = ap * (b ** t - 1) // (b - 1) # integer starts and ends scaled by (b - 1)^2 b^(2t - n) X = (b - 1) * (Xmax - np.arange(S0 + 1, dtype=np.int64)) lo_x, hi_x = X - am, X + ap st = np.outer(lo_x, lo_x) s = np.add.outer(np.arange(S0 + 1), np.arange(S0 + 1)) band_hi = st[s == S0 // 4].max() band_lo = st[s == S0 // 2].min() del s sel = (st >= band_lo) & (st <= band_hi) wa = np.outer(hi_x, hi_x) wa -= st wid = int(wa[sel].min()) del wa scale = (b - 1) ** 2 * b ** (2 * t - n) P = max(am, ap) * (b - 1) * b ** t # the pitch p, scaled starts = np.sort(st[sel]) gap = int(np.diff(starts).max()) delta = Mh * S0 / (2 * Fr(b) ** t) dsc = 2 * Mh * cell.w / Fr(b) ** L1 * scale gap_p = Fr(gap, P) wid_d = wid / dsc check(f"({b},{am},{ap}) n {n}: gap <= (delta/Mh^2) p, width >= " f"d (1 - delta/Mh^2)", gap_p <= delta / Mh ** 2 and wid_d >= 1 - delta / Mh ** 2, f"S0 {S0}, {starts.size} starts, gap {float(gap_p):.4f} p " f"vs {float(delta / Mh ** 2):.4f}, width " f"{float(wid_d):.5f} d") del st, sel, starts def k_core(cell, dm): """The complete zones of a full core, zones private for windows at least dm wide.""" b, Mm, Mp = cell.b, cell.Mm, cell.Mp L1 = numbers(cell)[0] lo = b * (Mp - dm - 1) + 2 * b * (cell.Mh / Fr(b) ** L1) e_lo = math.ceil(lo + 1 - Mp + dm) e_hi = math.floor(b * (1 - Mm) - 1 + Mm) return max(0, e_hi - e_lo + 1) def far_margin(cell, delta): """(F(delta) - eta_max(delta), k_core), floats: the zone chain's floor with narrow images and gaps, less the consumer's threshold, delta below the corner (THE FAR REGIME).""" L1, L2, d, S, fl, em = numbers(cell) b, Mh, w = cell.b, float(cell.Mh), float(cell.w) q = float(delta / cell.Mh ** 2) sq = q / (1 + math.sqrt(1 - q)) # 1 - sqrt(1 - q), no cancellation dm = float(d) * (1 - sq) p = Mh / b ** L1 gam = 2 * sq * p # the core's lower bound is a+ - b + 1 + (b - 1)(d - d_min), its upper # b - 1 - a-, both integers at d_min = d (FP18): b - 2 zones while # 0 < (b - 1)(d - d_min) <= 1, fewer past it k = b - 2 - math.floor((b - 1) * float(d) * sq) # delta -> 0+: b - 2 if k <= 0: return None, 0 F = 1 + dm - (w - 1 - dm) / k - (1 + 1 / k) * gam return F - (float(em) + float(delta) * w / Mh), k def extremes(cell): """The extremes whose pairs reach the product's top: Mh, and the other one when a- != a+ (both factors of the same sign).""" lo = min(cell.Mm, cell.Mp) return (cell.Mh,) if lo == cell.Mh else (cell.Mh, lo) def w_z(cell, n, E, sigma0, honest=True, top_only=False): """The least width of the level-n windows whose frame start is at least sigma0, the frame's corner end at E (THE HONEST TRACKING), exactly; d when not honest; over Mh's pairs alone if top_only.""" L1, L2, d, S, fl, em = numbers(cell) if not honest: return d b, w, Mh = cell.b, cell.w, cell.Mh u = Fr(1, b ** (n + L1)) Bn = Fr(b) ** n if Mh ** 2 - (E - sigma0) / Bn <= 0: # a start at or below 0 admits unbalanced and mixed-sign pairs raise ValueError("w_z: the threshold reaches 0") best = None for M in extremes(cell)[:1 if top_only else 2]: def start(s): a = s // 2 return E - Bn * (Mh ** 2 - (M - (a + w) * u) * (M - (s - a + w) * u)) if start(0) < sigma0: continue top = 2 * math.floor(M / u - w) - 1 # both factors positive lo, hi = 0, 1 while hi <= top and start(hi) >= sigma0: lo, hi = hi, 2 * hi hi = min(hi, top + 1) while hi - lo > 1: # start(lo) >= sigma0 mid = (lo + hi) // 2 if start(mid) >= sigma0: lo = mid else: hi = mid wd = Bn * ((2 * M - lo * u) * w * u - w * w * u * u) best = wd if best is None or wd < best else best return best def brute_wz(cell, n, E, sigma0): """w_z by every box pair at depth n + L1 whose product reaches sigma0, in integers: the control.""" L1, L2, d, S, fl, em = numbers(cell) b, am, ap, Mh = cell.b, cell.am, cell.ap, cell.Mh t = n + L1 q = (b - 1) * b ** t dmax = (E - sigma0) / Fr(b) ** n # absolute depth below Mh^2 thr = Mh ** 2 - dmax # least start, absolute xmax = ap * (b ** t - 1) // (b - 1) xmin = -am * (b ** t - 1) // (b - 1) X = np.arange(xmin, xmax + 1, dtype=np.int64) lo, hi = (b - 1) * X - am, (b - 1) * X + ap best = None for s in (1, -1): mag_hi = hi if s == 1 else -lo mag_lo = lo if s == 1 else -hi # a start >= thr needs |lo| >= thr/Mh; |hi| >= it keeps a superset keep = (mag_lo > 0) & (mag_hi >= math.floor(thr * q / Mh)) a_lo, a_hi = mag_lo[keep], mag_hi[keep] st = np.outer(a_lo, a_lo) wd = np.outer(a_hi, a_hi) - st tq = math.ceil(thr * q * q) sel = st >= tq if sel.any(): v = int(wd[sel].min()) best = v if best is None or v < best else best return None if best is None else Fr(best, q * q) * Fr(b) ** n def honest_track(cell, honest=True, extra=2): """Track the corner with honest widths (THE HONEST TRACKING), or with every window d wide (honest False, an incomplete zone an exit there). Returns (exit level or None, kind, levels), each level (n, E, j, x, sigma_j, lo, lo_d, complete), lo_d the low end at width d; a cycle runs `extra` cycles past E's first repeat.""" L1, L2, d, S, fl, em = numbers(cell) b, Mm, Mp = cell.b, cell.Mm, cell.Mp w = cell.w p = cell.Mh / Fr(b) ** L1 E, lo, lo_d = b * cell.Mh ** 2, None, None seen, levels, stop = {}, [], None for n in range(1, 400): eps = w * w / Fr(b) ** (n + 2 * L1) if honest else 0 j = math.ceil(E - Mp) x = E - d + eps if x >= j + 1 - Mm: levels.append((n, E, j, x, None, lo, lo_d, None)) return n, "overlap", levels sg = j - 1 + Mp - w_z(cell, n, E, j - 1 + Mp - d, honest) comp = lo is None or sg >= lo levels.append((n, E, j, x, sg, lo, lo_d, comp)) if not comp and not honest: return n, "core", levels if E in seen and stop is None: stop = n + extra * (n - seen[E]) seen.setdefault(E, n) if stop is not None and n >= stop: return None, "cycle", levels zl = j - 1 + Mp - d lo_d = b * (max(zl, lo_d) - j) + 2 * b * p if lo_d is not None \ else b * (zl - j) + 2 * b * p lo = b * (max(sg, lo) - j) + 2 * b * p if lo is not None \ else b * (sg - j) + 2 * b * p E = b * (E - j) raise RuntimeError(f"honest_track: no cycle in 400 levels at {cell.b}") def honest_start(cell, levels, honest=True): """The first fully held zone of the far chain on an honest track: (level, D below the corner end, the zone's honest bottom, the zone, the level's low end, its corner end), from the last level, backing up while its zone is not complete; None if none.""" L1, L2, d, S, fl, em = numbers(cell) Mm, Mp = cell.Mm, cell.Mp n, E, j, x, sg, lo, lo_d, comp = levels[-1] e = math.floor(x - 1 + Mm) for i in range(len(levels) - 1, -1, -1): n, E, j, x, sg, lo, lo_d, comp = levels[i] if i < len(levels) - 1: e = j - 1 se = e - 1 + Mp - w_z(cell, n, E, e - 1 + Mp - d, honest) if lo is None or se >= lo: return n, E - (e + 1 - Mm), se, e, lo, E return None def section_far(rows): print("F4 the far regime: nested held zones a fixed distance below") cell = ms.Cell(5, 2, 3) L1, L2, d, S, fl, em = numbers(cell) dl = Fr(1, 10) emd = em + dl * cell.w / cell.Mh k_hi, _ = zone_kills(cell, 6, dl, 3000, width=emd + Fr(1, 20)) k_lo, _ = zone_kills(cell, 6, dl, 3000, width=emd - Fr(1, 20)) check("FP22: at delta 1/10, eta_max(delta) + 0.05 is killed by some z " "box, eta_max(delta) - 0.05 by none", k_hi > 0 and k_lo == 0, f"eta_max(delta) {float(emd):.4f}, kills {k_hi} and {k_lo} of " f"3000 at m 6") mir = ms.Cell(7, 4, 3) L1, L2, d, S, fl, em = numbers(mir) emd = em + dl * mir.w / mir.Mh k_hi, _ = zone_kills(mir, 6, dl, 3000, width=emd + Fr(1, 20), side=-1) k_lo, _ = zone_kills(mir, 6, dl, 3000, width=emd - Fr(1, 20), side=-1) check("FP22-: the same on the - side at (7, 4, 3), z from " "its least value up", mir.Mh == mir.Mm and k_hi > 0 and k_lo == 0, f"eta_max(delta) {float(emd):.4f}, kills {k_hi} and {k_lo} of " f"3000 at m 6") if not all(CHECKS[-2:]): return False tally = {} for r in rows: if r[1] == 1 and r[9][0] is not None: key = (r[9][1], r[9][0]) tally[key] = tally.get(key, 0) + 1 print(" FP17: the exits by kind and level: " + ", ".join(f"{k} {lv}: {n}" for (k, lv), n in sorted(tally.items()))) eps = Fr(1, 10 ** 12) bad18 = [(r[0].b, r[0].am, r[0].ap) for r in rows if r[1] == 1 and (k_core(r[0], numbers(r[0])[2]) != r[0].b - 1 or k_core(r[0], numbers(r[0])[2] * (1 - eps)) != r[0].b - 2)] check("FP18 (amended): k_core is b - 1 at d_min = d, its ends " "integers, and b - 2 just below, at every L2 = 1 cell", not bad18, f"differs at {bad18}") gz = [(r[0].b, r[0].am, r[0].ap) for r in rows if r[1] == 1 and math.floor(r[0].b * (1 - r[0].Mm) - 1 + r[0].Mm) != r[0].b * (1 - r[0].Mm) - 1 + r[0].Mm] check("the core's top complete zone has the core's top (g = 0) at " "every L2 = 1 cell, an identity: b - 1 - a- is an integer", not gz, f"g > 0 at {gz}") return True def tag(cell): return (cell.b, cell.am, cell.ap) def core_holds(cell, n, E, e, se, lo): """Does zone e's child, holding [max(se, lo), e + 1 - M-] at level n, hold its core's top zone complete at level n + 1 (honest widths)?""" L1, L2, d, S, fl, em = numbers(cell) b, Mm, Mp = cell.b, cell.Mm, cell.Mp p = cell.Mh / Fr(b) ** L1 low = se if lo is None else max(se, lo) clo = b * (low - e) + 2 * b * p e2 = b * (1 - Mm) - 1 + Mm s2 = e2 - 1 + Mp - w_z(cell, n + 1, b * (E - e), e2 - 1 + Mp - d) return s2 >= clo def section_honest(rows): print("F5 the honest tracking") l2 = [r for r in rows if r[1] == 1] ints, total = [], 0 for r in l2: for n, E, j, x, sg, lo, lo_d, comp in honest_track( r[0], honest=False)[2]: if lo is not None and sg is not None: total += 1 if sg - lo != j + r[0].am - 1: ints.append((tag(r[0]), n)) check("FP25: at width d the completeness margin is j + a- - 1", not ints, f"{total} levels, differs at {ints[:5]}") agree, other, cases, skip = 0, 0, 0, 0 for c in ((4, 2, 2), (5, 2, 3), (5, 3, 2), (7, 3, 4), (7, 4, 3)): cell = ms.Cell(*c) Mp, d = cell.Mp, numbers(cell)[2] lv = honest_track(cell)[2] for n, E, j, x, sg, lo, lo_d, comp in lv[:3 if cell.b <= 5 else 2]: for jj in (j, j - 1, j - 2): s0 = jj - 1 + Mp - d if cell.Mh ** 2 - (E - s0) / Fr(cell.b) ** n <= 0: skip += 1 continue got, bru = w_z(cell, n, E, s0), brute_wz(cell, n, E, s0) cases += 1 agree += got == bru if len(extremes(cell)) > 1: other += w_z(cell, n, E, s0, top_only=True) != got check("FP24: w_z equals the brute scan of every box pair", agree == cases, f"{agree} of {cases} (levels 1-2, 3 at b <= 5, three zone " f"bottoms each, {skip} below 0 skipped); the other extreme " f"sets the least at {other}") if not all(CHECKS[-2:]): print("CONTROL FAILED; no honest verdict is read") return None # step (0): level 1 alone print(" step (0), level 1 alone (the root holds every image):") lvl1 = {"live": [], "dead": []} for r in l2: if r[7] == "open": continue cell = r[0] L1, L2, d, S, fl, em = numbers(cell) b, Mm, Mp = cell.b, cell.Mm, cell.Mp p = cell.Mh / Fr(b) ** L1 n, E, j, x, sg, lo, lo_d, comp = honest_track(cell, extra=0)[2][0] e = math.floor(x - 1 + Mm) wz = w_z(cell, 1, E, e - 1 + Mp - d) se = e - 1 + Mp - wz D = E - (e + 1 - Mm) mg, k = far_margin(cell, D / b) lo2, E2 = b * (se - e) + 2 * b * p, b * (E - e) e2 = b * (1 - Mm) - 1 + Mm s2 = e2 - 1 + Mp - w_z(cell, 2, E2, e2 - 1 + Mp - d) k = k_core(cell, d * (1 - Fr(1, 10 ** 12))) m0 = float(1 + d - S / k - em) lvl1[r[7]].append((cell, D, mg, d - wz, s2 >= lo2, m0, (m0 - mg) / float(D / b))) dd = lvl1["dead"] pos = [t for t in dd if t[2] is not None and t[2] > 1e-9] print(f" FP23: the level-1 far margin > 0 at {len(pos)} of {len(dd)} " f"dead L2 = 1 cells; D_1 from {float(min(t[1] for t in dd)):.4f} " f"to {float(max(t[1] for t in dd)):.4f}; the width deficit " f"d - W_z at the zone from {float(min(t[3] for t in dd)):.2e} to " f"{float(max(t[3] for t in dd)):.2e}") m0s = sorted(t[5] for t in dd) print(f" the limit margin over the dead: median " f"{m0s[len(m0s) // 2]:.4f}; the fall per unit of delta from " f"{min(t[6] for t in dd):.3f} to {max(t[6] for t in dd):.3f}; " f"missed at level 1: " f"{[tag(t[0]) for t in dd if not (t[2] is not None and t[2] > 1e-9)]}") nc = [tag(t[0]) for t in dd + lvl1["live"] if not t[4]] print(f" the level-2 core holds its top zone complete at all but " f"{nc}") lpos = [tag(t[0]) for t in lvl1["live"] if t[2] is not None and t[2] > -1e-9] print(f" live cells with level-1 margin > 0: {lpos}") # step (1): the honest tracking print(" step (1), the honest tracking:") res = {"live": [], "dead": []} parted = [] for r in l2: if r[7] == "open": continue cell = r[0] L1, L2, d, S, fl, em = numbers(cell) b, Mm = cell.b, cell.Mm lvl, kind, lv = honest_track(cell) lvl0, kind0, lv0 = honest_track(cell, honest=False) if (lvl, kind) != (lvl0, kind0): parted.append((tag(cell), (kind0, lvl0), (kind, lvl))) if kind == "overlap": st = honest_start(cell, lv) st0 = honest_start(cell, lv0, honest=False) \ if kind0 == "overlap" else None if st is None: res[r[7]].append((cell, "exit", lvl, None, None, st0, False)) continue ds = st[1] / Fr(b) ** st[0] mg, k = far_margin(cell, ds) res[r[7]].append((cell, "exit", st[0], ds, mg, st0, core_holds(cell, st[0], st[5], st[3], st[2], st[4]), k)) continue N = lv[-1][0] Lc = next(q for q in range(1, len(lv)) if lv[-1 - q][1] == lv[-1][1]) cyc = lv[-Lc:] ov = min((j + 1 - Mm) - (E - d) for _, E, j, *_ in cyc) epsN = cell.w ** 2 / Fr(b) ** (N + 2 * L1) exc = max(lo - lo_d for *_, lo, lo_d, _ in cyc) exc2 = max(lo - lo_d for *_, lo, lo_d, _ in lv[-2 * Lc:-Lc]) cyc0 = lv[-2 * Lc:-Lc] held, cores = False, True for n, E, j, x, sg, lo, lo_d, comp in cyc: e = math.floor(x - 1 + Mm) se = e - 1 + cell.Mp - w_z(cell, n, E, e - 1 + cell.Mp - d) if se >= lo: held = True cores &= core_holds(cell, n, E, e, se, lo) k = k_core(cell, d * (1 - Fr(1, 10 ** 12))) m0 = 1 + d - S / k - em ok = epsN < ov and exc < 1 and held fall = exc <= max(lo - lo_d for *_, lo, lo_d, _ in cyc0) res[r[7]].append((cell, "cycle", N, (ov, epsN, exc, exc2, held), float(m0) if ok else None, Lc, cores, fall)) print(f" paths parted from width d's at {len(parted)}: " f"{parted[:12]}") for v in ("live", "dead"): for kind in ("cycle", "exit"): rs = [t for t in res[v] if t[1] == kind] pos = [t for t in rs if t[4] is not None and t[4] > 1e-9] print(f" {v} {kind}: {len(rs)}, dead by the kill at " f"{len(pos)}") lk = [tag(t[0]) for t in res["live"] if t[4] is not None and t[4] > -1e-9] nm = sum(1 for t in res["live"] if t[4] is None) check("FP19 on the honest tracking: the far margin is <= 0 at every " "live cell", not lk, f"not below at {lk}; no margin at {nm}") cy = [t for t in res["dead"] if t[1] == "cycle"] if cy: print(f" cycling dead: least overlap margin / eps_N " f"{float(min(t[3][0] / t[3][1] for t in cy)):.3g}, largest " f"excess {float(max(t[3][2] for t in cy)):.3g} (the cycle " f"before: {float(max(t[3][3] for t in cy)):.3g}), a complete " f"zone below at {sum(t[3][4] for t in cy)} of {len(cy)}; " f"least limit margin " f"{min(t[4] for t in cy if t[4] is not None):.5f}") t734 = [(t[4], k_core(t[0], numbers(t[0])[2] * (1 - Fr(1, 10 ** 12)))) for t in cy if tag(t[0]) == (7, 3, 4)] print(f" (7, 3, 4): limit margin, k_core {t734}") ext = [t for t in res["dead"] if t[1] == "exit"] byl = {} for t in ext: a = byl.setdefault(t[2], [0, 0]) a[0] += 1 a[1] += t[4] is not None and t[4] > 1e-9 print(" exiting dead cells dead by the kill, by first-zone level: " + ", ".join(f"l {lv}: {a[1]}/{a[0]}" for lv, a in sorted(byl.items()))) ks = {} for t in ext: ks[t[7] - (t[0].b - 2)] = ks.get(t[7] - (t[0].b - 2), 0) + 1 print(f" far_margin's k - (b - 2) at delta*, exiting dead: {ks}; " f"largest " f"delta* b {max(t[3] * t[0].b for t in ext if t[3])} (exact)") same = sum(1 for t in ext if t[5] is not None and t[3] is not None and (t[2], t[3] * Fr(t[0].b) ** t[2]) == t[5][:2]) back = [(tag(t[0]), (t[2], t[3] * Fr(t[0].b) ** t[2]), t[5][:2], t[5][3] + t[0].am - 1) for t in ext if t[5] is not None and t[3] is not None and (t[2], t[3] * Fr(t[0].b) ** t[2]) != t[5][:2]] print(" far starts moved (honest (l, D), width d's, the width-d zone's " "margin j + a- - 1): " + "; ".join( f"{c} {h} {o} {m}" for c, h, o, m in back)) allx = [t for v in ("live", "dead") for t in res[v]] print(f" read after the run: the far start's child holds its core's " f"top zone complete at " f"{sum(1 for t in allx if t[1] == 'exit' and t[6])} of " f"{sum(1 for t in allx if t[1] == 'exit' and t[3] is not None)} " f"exits, and at every held cycle level of " f"{sum(1 for t in allx if t[1] == 'cycle' and t[6])} of " f"{sum(1 for t in allx if t[1] == 'cycle')} cycling cells; the " f"low end's excess no larger than a cycle before at " f"{sum(1 for t in allx if t[1] == 'cycle' and t[7])} of them") print(f" exiting dead: far start as at width d at " f"{same} of {len(ext)}") fails = [t for t in res["dead"] if not (t[4] is not None and t[4] > 1e-9)] print(f" open by the kill ({len(fails)}): " + ", ".join(f"{tag(t[0])} {t[1]} l {t[2]} margin " f"{None if t[4] is None else round(t[4], 5)}" for t in fails[:20])) ex_ok = [t for t in ext if t[4] is not None and t[4] > 1e-9] if ex_ok: lt = min(ex_ok, key=lambda t: t[4]) print(f" least exit margin {lt[4]:.5f} at {tag(lt[0])} l {lt[2]}") return res def section_sweep(K, bmax): print(f"F1 the floor against the tree, K {K}, radices 3..{bmax}") rows = [] for cell in hulls.cells1(3, bmax): L1, L2, d, S, fl, em = numbers(cell) g = hulls.Grid(cell, L1, L2, K) assert g.eta_fr == em and g.d_fr == d lv = g.eta_max >= g.d and g.live(g.eta_max)[0] cap = g.G + g.d + 2 * g.G es = g.eta_star(min(cap, g.Mm + g.Mp)) es = None if es is None else Fr(es, g.G) verdict = "live" if lv else ("dead" if em < fl else "open") fl2 = 1 + d - S / (cell.b - 2) v2 = "live" if lv else ("dead" if em < fl2 else "open") ex = honest_track(cell, honest=False, extra=0)[:2] \ if L2 == 1 else None rows.append((cell, L2, fl, em, es, verdict, fl2, v2, S, ex)) if verdict == "open": print(f" ({cell.b},{cell.am},{cell.ap}) L2 {L2}: floor " f"{float(fl):.5f} <= eta_max {float(em):.5f} < eta* " f"{float(es):.5f}") bad = [r[0] for r in rows if r[4] is not None and r[2] > r[4]] check("FP1: the floor <= eta* at every cell", not bad, f"{len(rows)} cells, above at {[(c.b, c.am, c.ap) for c in bad]}") print(" (dead below = under the floor, not a derived verdict)") for v in ("live", "dead", "open"): print(f" {v}: {sum(1 for r in rows if r[5] == v)}") print(" the zone chain, 1 + d - S/(b - 2):") bad2 = [r[0] for r in rows if r[4] is not None and r[6] > r[4]] check("FP5: the chain floor <= eta* at every cell", not bad2, f"above at {[(c.b, c.am, c.ap) for c in bad2]}") print(" (dead below = under the chain floor, not a derived verdict)") for v in ("live", "dead", "open"): print(f" {v}: {sum(1 for r in rows if r[7] == v)}") check("FP6: no open cell", not any(r[7] == "open" for r in rows)) rel = [float((r[4] - r[6]) / (r[8] / (r[0].b - 2))) for r in rows if r[4] is not None] print(f" eta* above the chain floor by {min(rel):.3f} to " f"{max(rel):.3f} of S/(b - 2)") print(" the corner tracked through held zones (L2 = 1 only):") for v in ("live", "dead"): n_in = sum(1 for r in rows if r[1] == 1 and r[7] == v and r[9][0] is None) n_ex = sum(1 for r in rows if r[1] == 1 and r[7] == v and r[9][0] is not None) print(f" {v}: reaches the corner {n_in}, exits into an overlap " f"{n_ex}") z0 = [r[3] for r in rows if r[1] == 0] print(f" L2 = 0 (eta_max < 0, no floor needed): {len(z0)}, the " f"largest eta_max there {max(map(float, z0)) if z0 else None}") return rows 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_witness() if not all(CHECKS[:3]): print("CONTROL FAILED; nothing below is read") raise SystemExit(1) rows = section_sweep(K, bmax) if not CHECKS[3]: print("CONTROL FAILED; nothing below is read") raise SystemExit(1) if section_far(rows): section_honest(rows) else: print("CONTROL FAILED; no far verdict is read") section_fixed() section_geometry() 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()