""" chains.py -- what a chain of on-line units pays: the inset law, the threshold-miss law, the matching law, and the led stream spent in one hop. QUESTION. manystream.py prices ONE reader of signed-digit streams: a map f is read at the least L with b^L rho >= Lam |I|. A datapath wires readers in series, the first unit's output digits being the next unit's input stream. The literature prices a series by adding the units' on-line delays (Usman, Ercegovac and Lee, Low-Latency Online Multiplier with Reduced Activities and Minimized Interconnect for Inner Product Arrays, J. Signal Processing Systems 95, 2023, section 4.2.2: "for a series of online operations, the overall latency is the sum of online delays of the corresponding operation"). Four questions. Can the first unit's choice among legal digits buy the second a lower delay, or is the sum a floor? Where the sum is beaten, by what law? What does a chain of many units pay? And when the first unit runs AHEAD (poles.py: the reciprocal emits before it reads), does the lead pass down the chain? THE SETTING. Radix b, digits D = {-a-, ..., a+}, 1 <= a+- <= b - 1, slack rho = a- + a+ + 1 - b >= 1, M+- = a+-/(b - 1), w = M- + M+, w - 1 = rho/(b - 1), Mh = max(M-, M+). Every stream is a D-stream of value in [-M-, M+]; after n digits it is confined to a BOX of width w/b^n. The PRODUCER is x y read at lead 0. Its range is [-M- M+, max(M-^2, M+^2)], which the root tile at lead 0 holds iff M-^2 <= M+, that is a-^2 <= a+ (b - 1): the REPRESENTABLE cells. Its floor L1* is the least L with b^L (w - 1) >= 2 Mh w (manystream: Lam = 2 Mh). The CONSUMER reads the producer's stream U and a fresh stream z. Units in series are ALIGNED: the consumer reads digit n of U and of z together, and a chain at (L1, L2) pays L1 + L2 in the inputs. THE ARGUMENT (written before the engine). (1) THE HULL. The consumer sees a prefix of U. What it knows of x y is the FIBRE: every value the producer's selector sends to that prefix. Its output tiles are intervals, so a tile holds the fibre plus a z box iff it holds the fibre's HULL plus that box. The hull is an interval inside U's own box, INSET by alpha from the box's bottom and beta from its top (in units of the box's level). So the producer's selector reaches the consumer only through its insets. The step uses that a tile is an interval and nothing else; it is the floor's whole scope. (2) THE INSET CLAUSE. By manystream's tile lemma the sum consumer U + z at delay L2 is dead iff some image strictly contains a zone. With U's hull shortened by (alpha, beta) the k = 2 clause becomes: dead iff an integer lies in ((b^L2 - 2) M+ + beta, b^L2 - (b^L2 - 2) M- - alpha). Its ESCAPE COST E(L2) is the least alpha + beta that empties the interval: 0 when it is empty, and otherwise, with the integers j_1 < ... < j_r inside, the least over splits of (j_i - lo) + (hi - j_(i+1)). (3) THE BUDGET. At level n + L1 the product images of the (x, y) prefixes have widths up to 2 Mh w / b^L1 in level-n units near the product's corner x = y = +-Mh, where their starts are dense, and each must sit inside the hull its prefix is sent to. Hulls sit at unit spacing, so hulls there must overlap by the widest image in the limit of depth: alpha + beta <= S(L1) = (w - 1) - 2 Mh w / b^L1, nonnegative exactly from L1* on. This is an argument: it puts one hull at each value, while past level 1 digit strings that share a value carry hulls of their own and beat it (hulls.py). (4) THE INSET LAW predicts the chain dead at (L1, L2) when E(L2) > S(L1). For the adder it is proved without (3), by the ALIGNED UNIT. At L2 = 1 the clause at a hull [h0, h1] of the box at 0 is dead iff an integer lies in (a+ - h1, b - a- - h0), so a hull is permitted iff it lies in [k, k + rho] for an integer k: at slack 1, an aligned unit of its level. The clause's length is 2 - rho (b - 2)/(b - 1) at L2 = 1 and 2w - b^L2 (w - 1) <= 0 at L2 >= 2, so it bites only at L2 = 1 and slack 1 (at rho = 2 the ends' fractions are s/(b - 1) and (s + 2)/(b - 1), s = b - 1 - a+ <= b - 3), where the adder's floor is 2. There x y hands it, at prefix level 1 and every L1, an image with 1 strictly inside: y in the top box at depth 1 + L1, x in the boxes below with lower ends X >= 0, whose starts step less than each width (w > 1), the union running from below 1 to b Mh^2 >= b^3/(4 (b - 1)^2) > 1. That image is HOMELESS: no permitted hull at any value holds it, however many prefixes share one. So (L1, 1) is dead at every L1 and the chain's floor is the naive sum at every representable cell (a+- <= b - 1, which the rho >= 2 steps use), (L1*, L2*) living by (5) at zero insets. (5) THE NARROWED READER (sufficiency, by the tile lemma). A reader into tiles [q - M- + alpha, q + M+ - beta] is a reader on the tiles narrowed by alpha below and beta above, with the same integer digits, whose children still cover their parent since a+- >= (b - 1)(M+- - inset). Its zones have length w - 1 - alpha - beta, so it reads f wherever b^L (w - 1 - alpha - beta) >= Lam w, the input boxes unchanged. A producer so narrowed hands its consumer a hull inset by (alpha, beta). (6) A PRODUCT CONSUMER z U, U of TOP tau = sup |U| (tau = Mh^2 behind a product, 2 Mh/b behind a sum read at lead 1), reading U through a hull inset by eta in total: its image of a z box times a hull is at most (tau w + Mh (w - eta))/b^n wide, so by (5) it reads at L2 wherever tau w + Mh (w - eta) <= b^L2 (w - 1), and keeps for the next unit the LEFTOVER S2(L2, eta) = (w - 1) - (Lam2 w - Mh eta)/b^L2, Lam2 = tau + Mh. Its escape cost is its own threshold's miss read in the producer's coordinate: E2(L2) = max(0, Lam2 w - b^L2 (w - 1))/Mh. (7) THE THRESHOLD-MISS LAW. At slack 1, w - 1 = w/b, so the consumer's floor is 1 when Lam2 <= 1 and 2 when Lam2 > 1, and the only pair that can beat the sum is (L1*, L2* - 1). The chain reads one below the sum if 0 < Lam2 - 1 <= (Mh / w) min(S(L1*), room), the threshold missed by at most the producer's budget, bounded by its range's room (the audit note below; corrected after the run). The survival side is (5) and (6), a proof. The death side rested on (3) and is false: hulls.py's tree of hulls reads (20, 8, 12) one below the sum. The root Lam2(Mh) = 1 is 1/phi behind a product (Lam2 = Mh + Mh^2) and the rational b/(b + 2) behind a sum (Lam2 = Mh (1 + 2/b)); the sum head's budget is (w - 1) - (2w - 1)/b^L1, its images on a lattice of pitch 1/b^L1. (8) THE MATCHING LAW. A chain of units, a head reading fresh streams alone, then product consumers numbered from 2, each consumer j of top tau_(j-1) = tau_1 Mh^(j-2) and Lam_j = Mh + tau_(j-1), priced by (6) link by link: a consumer below its floor spends its producer's leftover, and one at its floor passes on its own. The least total over every assignment is an UPPER bound on the chain's floor, proved by (5); that the floor reaches it rested on (3) and fails at the two-unit chain at (20, 8, 12). At slack 1 three steps, each proved at every radix. GREEDY. Of two states (t, v) and (t + d, v'), d >= 1, the first answers a move of the second at L with one at L + 1 (at L* + 1 against L* + 2) and keeps as much: keep(L + 1, v) - keep(L, v') = ((b - 1) Lam w - b Mh v' + Mh v)/b^(L+1) >= 0, as v' <= w - 1 = w/b and Lam >= Mh; then it dominates. So the least total is the greedy one, each unit at the least delay alive on what its producer hands it. THE FIRST GAIN. A GAIN is a link (j - 1, j) at which unit j reads one below its floor on the FLOOR CHAIN's leftover, every unit at its floor; PAIRWISE if on its producer's at zero inset; CROSSED if a gain and not pairwise. A gain needs Lam_j > 1, so every consumer above it sits at floor 2, keeping A_j + Mh eta/b^2. Each consumer scales its producer's range by Mh, so the ROOMS rise along the chain; with Lam falling so does A_j, capped by its room, and either head's budget at its floor is below every A_j (behind a product L1* = 2 and Lam_j <= 2 Mh; behind a sum L1* <= 2 and (2w - 1)/b^L1* >= Lam_j w/b^2), all at Mh < 1; at Mh = 1 no link gains, every miss w (Lam_j - 1)/Mh exceeding w - 1. So a crossed gain's miss m_j = w (Lam_j - 1)/Mh lies within Mh w/b^3 of the miss of any gain above it, while consecutive misses differ by more than w (1 - Mh)^2/Mh^2 >= w/(Mh^2 (b - 1)^2): a crossed gain is its chain's first gain. THE LAW. Outside the ADJACENT range (two units below their floors side by side, which needs the second's miss under about Mh^2/b^2) the least total is the naive sum less nu, a MAXIMUM MATCHING of the path's gains. Upper: matched downstream units one below, the rest at their floors; a crossed gain is the first, so its producer reads the floor chain. Lower: a low unit keeps less than Mh w/b^2 <= A_j; charge it to the nearest unit above it not at its floor when that one is high, which nothing else charges; otherwise its producer hands it at most the floor chain's leftover, so its link is a gain, and these links are disjoint. (9) A LED STREAM IS SPENT IN ONE HOP. Let a unit multiply a fresh stream z by a stream r >= 0 (corrected after the run) whose range has top tau > 0 (so the map's range is [-M- tau, M+ tau] and its scale K = tau). The least lead o has b^(o - 1) < tau, so a level-1 cell, of length w b^(o - 1), is shorter than the range's w tau. At a negative lookahead the first digit is committed before any digit of z, and must hold the whole range: dead. So such a unit reads at c >= 0 whatever r's producer did, and its own output is an ordinary stream. The reciprocal's lead is not lost, though: a consumer reading r as deep as the reciprocal runs ahead, d = -c1* digits past z, sees r's box b^d times narrower, and by (5) reads wherever (tau + Mh b^-d) w <= b^L (w - 1), against (tau + Mh) w for the aligned consumer. THE DESIGN, frozen before the engine. CA THE CONTROLS. (i) The inset clause at zero insets equals manystream.clause_dead at k = 2 at the 20 cells of radices 2..5 (manystream.census) and L2 = 0..3. (ii) The inset clause against an exact zone scan: U's hulls nested (a prefix's hull its own inset box cut to its parent's), every (U, z) prefix pair to depth 4 at radices 2..4, L2 in {1, 2}, insets on a grid of sixths and tenths of the slack w - 1; the scan's death verdict equals the clause's at every triple. (iii) The narrowed reader (5) at zero insets reproduces manystream's product floor at the representable cells. CB THE INSET LAW at the 20 cells. Per cell: L1*, L2* (the k = 2 clause), the naive sum, the inset law's least L1 + L2 over L1 in [L1*, L1* + 5], L2 in [0, 5], and the FUSED floor of x y + z (manystream's law, Lam = 2 Mh + 1, at its own lead). The aligned unit (4) (designed after the record run, in place of a covering search with one hull at each value, exact at n = 1 where a prefix is one digit, not past it): at every cell of radices 2..60, every escape option's hull at L2 = 1 at slack 1 inside an aligned unit, the clause empty at slack 2 or more and at L2 = 2, 3; at every representable slack-1 cell and L1 = L1*..L1* + 3, the straddling image of the row, checked homeless against every option hull at every value. Controls, printed first, not gating the sweep: (2, 1, 1) at L1 = 2, whose straddler by hand is the image 15/16..7/4 of i = 1, and aligned halves [j/2, (j + 1)/2], never homeless. CC THE THRESHOLD-MISS LAW at every slack-1 cell of radices 2..40, both consumers, each at its representable cells (the product consumer where Mh^2 fits the root tile at lead 0; the sum-fed where 2 Mh^2 <= b M+ and its mirror): the least L1 + L2 by (6) over L1 in [L1*, L1* + 5], L2 in [0, 5], against the criterion (7). And every cell of slack 2 or more to radix 40 read the same way. CD THE MATCHING LAW. A dynamic programme over a chain's units, keeping the largest leftover at each (total, below-floor run) state (every verdict is monotone in the inset), at slack 1, radices 3..40, n = 3..12, both heads; and at radices 3..24 along each finite run of floor-2 consumers. Printed: where the greedy total differs from the programme's least, and the chains where the least differs from naive - nu, inside the adjacent range or out. CG THE CROSSED LINKS, every prefix (designed after the record run). Every slack-1 product-head chain, representable, Mh < 1, its whole floor-2 run plus one unit, radices 3..60 (3..200 with --cg200), and every prefix of 3 units or more, priced greedily: the crossed links, any gain above one (ABOVE), the prefixes outside the adjacent range where greedy differs from naive - nu (OFF), and the arm with the floor chain removed, nu read on the pairwise links. Control, read first: three chains the full programme prices, (31, 3, 28) n = 34 at 67, (29, 2, 27) n = 74 at 147 and (24, 3, 21) n = 23 at 46. CE THE LED STREAM at every reciprocal pair of poles.py (the 20 cells, h = j/(b - 1), j in 1, 2, 4, 8, 32, 128) with c1* < 0: tau = b^-o1 / h; the consumer's lead from its range; its aligned and eager L by (9); c2 = L - o2; and the fused divider z/(s + x) from poles.Divider, in the consumer's output scale. PREDICTIONS. PA (i), (ii), (iii) agree everywhere. PB the inset law's floor equals the naive sum at all 20 cells; no aligned-unit line off to radix 60; representable at 13 of 20; the fused floor below the chain at 9 of those 13 and equal at the 4 with L1* = 1. PC the search equals the criterion at every slack-1 cell of both consumers; the product-fed gains at 17 cells, all at (2, 1): (4,2,2), (9,4,5), (12,5,7), (17,7,10), (22,9,13), (25,10,15), (30,12,18), (33,13,20), (38,15,23) and the mirrors of all but the symmetric first; the sum-fed gains at (b, 2, b - 2) and its mirror at every radix 5..40 and nowhere else; no cell of slack 2 or more gains to radix 40. PD greedy is the least total at every chain; outside the adjacent range the programme reads naive - nu at every cell; the five-unit sum-fed chain at (9, 2, 7) reads 7 against the matching's 8, an adjacent pair; the sum-fed four-unit chain at (b, 2, b - 2) reads naive - 2 at every radix 8..40. PG (its counts a TRANSPLANT from an earlier sweep of the same chains by a footprint engine) ABOVE and OFF empty; the crossed links at (29, 2, 27) j = 74, (31, 3, 28) j = 34, (46, 2, 44) j = 140 and, past radix 60, (91, 3, 88) j = 152; the pairwise arm off by one at 27 prefixes to radix 60 and 36 to radix 200. PE c2 >= 0 at every pair; the eager L below the aligned at 25 of the 40 pairs; the fused divider at or below the chain at all 40. KILLS, as what the script prints. K1 a CA line off: the clause or the scan is wrong; nothing below is read. K2 the inset law's floor below the naive sum at some cell, or an "AU OFF" line: (4) is wrong. K3 a slack-1 cell where the search and the criterion disagree: (7) is wrong. K4 a cell outside the adjacent range where the programme is not naive - nu, a CD chain where greedy is not the least, or an ABOVE or OFF line non-empty: (8) is wrong. K5 c2 < 0 at a pair: (9) is wrong. POSITIVE CONTROL: CA, read before any verdict line. FINDINGS (entered after the run; every number is a print). - PA holds: the inset clause at zero insets is the k = 2 clause at 80 of 80 (cell, L); the zone scan agrees with the clause at 500 of 500 (cell, L2, insets); the narrowed reader at zero insets is the product's floor at every representable cell. K1 did not fire. - PB holds. The inset law's floor equals the naive sum at 20 of 20 cells. The aligned unit holds to radix 60: 1770 slack-1 cells, every option hull in an aligned unit and the adder's floor 2; 34220 cells of slack 2 or more, the clause empty at L2 = 1; none biting at L2 = 2, 3; 4364 representable (cell, L1) pairs, each with a homeless image at prefix level 1. The controls read as by hand. A scratch break (every hull widened by 10^-6 at its top) prints AU OFF from radix 13 on, where the straddle is thinner. Representable at 13; the fused x y + z (lead 1) reads below the chain at 9 of the 13 and level at 4, the cells with L1* = 1; at the 7 cells where U needs a lead, below at 6 and level at 1. K2 did not fire. - PC holds: the search equals the criterion at every slack-1 cell of both consumers. The product-fed consumer gains at the 17 predicted cells, 9 radices; the sum-fed at 72 cells, (b, 2, b - 2) and its mirror at all 36 radices 5..40; no cell of slack 2 or more gains (no head skipped for want of budget). K3 did not fire. - PD holds: 12242 chains read; greedy is the least at all of them; the programme differs from naive - nu at 49, every one inside the adjacent range and every one by 1. The five-unit sum-fed chain at (9, 2, 7) reads 7 against naive 10 and the matching's 8; the four-unit sum-fed chain reads naive - 2 at every radix 8..40. K4 did not fire. - PE holds: 40 pairs; the eager consumer's L below the aligned at 25; the fused divider at or below the eager chain at 40, equal at 33. c2 >= 0 held by construction (the L of (9) is the sufficiency law's, which puts b^L above the range's scale), so K5 could never fire; it is now argued, not checked: a multiplied stream's first digit must hold its whole range. The least c2 is printed: 1 at the aligned consumer, 0 at the eager. - Two changes after the first run, no verdict touched. The whole-run read first built each chain to 400 units, which at Mh = 1 (where every consumer's Lam exceeds 1 and the run never ends) read 400-unit chains and cost 350 s; the run is now read only at Mh < 1, and the 76 (cell, head) with Mh = 1 are read at n <= 12, where every consumer's miss is the same and nothing bunches. And the programme now prices every length of a chain in one pass. - Settled at the audit, after the record run: (5) holds only while the narrowed root tile still holds the unit's range at lead 0, so every budget and leftover is now bounded by that ROOM, (M- + lo) + (M+ - hi) for a range [lo, hi]. The room binds at the head's floor at 3539 (cell, head) of the product head and 1 of the sum head, and moves no verdict: every PC and PD line reprints unchanged. CB's inset law keeps the raw budget, its least total the naive sum at every cell either way. - As run, against the frozen design: CA(i) reads L = 1..4, CA(ii)'s scan reaches depth 3 with insets 0, 1/10, 1/6, 1/3 and 1/2 of the slack, CB's L2 runs 1..5 (the sum's lead is 1), and CD keys its states by total alone. PC's "all at (2, 1)" is not read out: the 17 cells are. CA(iii) is a cross-engine control, chains.narrowed_L against manystream.law_of. - PG holds. The control reads 67, 147 and 46, each equal to the full programme's least. To radix 200, 264787 prefixes, 486 inside the adjacent range: ABOVE 0, OFF 0; the crossed links are the four predicted, each its chain's only crossed link; the pairwise arm is off by one at 36 prefixes, all at those four cells (27 at the three to radix 60): the floor chain is the whole correction. K4 did not fire. RUN RECORD: 15/15 checks, 12.1 s, peak commit 12.8 MB under a memory guard; after an audit (CE's c2 check, which held by construction, cut), 14/14, 12.5 s, 14.5 MB; with CG at radix 60, 20/20, 14.7 s, 13.2 MB; with --cg200, 20/20, 126.0 s, 19.6 MB; with the aligned unit in CB for the covering search, 22/22, 15.2 s, 10.9 MB. """ import math import sys import time from fractions import Fraction as Fr import manystream as ms import poles 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 cells(bmin, bmax, slack=None): for b in range(bmin, bmax + 1): for am in range(1, b): for ap in range(1, b): rho = am + ap + 1 - b if rho >= 1 and (slack is None or rho == slack): yield ms.Cell(b, am, ap) def representable(cell): return cell.am ** 2 <= cell.ap * (cell.b - 1) # ---- (2) the inset clause and its escape cost ---- def clause_ends(cell, L2): B = Fr(cell.b) ** L2 return (B - 2) * cell.Mp, B - (B - 2) * cell.Mm def clause_dead(cell, L2, alpha, beta): lo, hi = clause_ends(cell, L2) lo, hi = lo + beta, hi - alpha return math.floor(lo) + 1 < hi def escape_options(cell, L2): """The minimal (alpha, beta) emptying the clause; [(0, 0)] when it is already empty.""" lo, hi = clause_ends(cell, L2) ints = [j for j in range(math.floor(lo) + 1, math.ceil(hi)) if lo < j < hi] if not ints: return [(Fr(0), Fr(0))] opts = [] for i in range(len(ints) + 1): beta = ints[i - 1] - lo if i > 0 else Fr(0) alpha = hi - ints[i] if i < len(ints) else Fr(0) opts.append((alpha, beta)) return opts def escape_cost(cell, L2): return min(a + c for a, c in escape_options(cell, L2)) def sum_floor(cell): L = 1 while clause_dead(cell, L, 0, 0): L += 1 return L # ---- (3) the budgets, (5) the narrowed reader ---- def budget_xy(cell, L1): return cell.w - 1 - 2 * cell.Mh * cell.w / Fr(cell.b) ** L1 def budget_sum(cell, L1): return cell.w - 1 - (2 * cell.w - 1) / Fr(cell.b) ** L1 def floor_xy(cell): L = 0 while budget_xy(cell, L) < 0: L += 1 return L def narrowed_L(cell, lam, inset): """(5): least L with b^L (w - 1 - inset) >= lam w, or None.""" z = cell.w - 1 - inset if z <= 0: return None L = -40 while Fr(cell.b) ** L * z < lam * cell.w: L += 1 return L # ---- the zone scan of the inset clause ---- def zone_scan_dead(cell, L2, alpha, beta, nmax=3): """Every nested hull of U to depth nmax plus every z box over a period of prefix values: does an image strictly contain a zone?""" b, Mm, Mp = cell.b, cell.Mm, cell.Mp D = range(-cell.am, cell.ap + 1) level = {(0, (-Mm + alpha, Mp - beta))} period = b ** L2 for n in range(1, nmax + 1): s = Fr(1, b ** n) new = set() for p, (plo, phi) in level: for e in D: q = b * p + e lo = max((q - Mm + alpha) * s, plo) hi = min((q + Mp - beta) * s, phi) if lo < hi: new.add((q, (lo, hi))) level = new if n < L2: continue hulls = {h for _, h in level} umin = -cell.am * poles_repunit(b, n) for (hlo, hhi) in hulls: for u in range(umin, umin + period + 1): img = (hlo + (u - Mm) * s, hhi + (u + Mp) * s) if cell.kills(img, n, L2): return True return False def poles_repunit(b, n): return (b ** n - 1) // (b - 1) # ---- (4) the aligned unit ---- def homeless(cell, opts, img): """True iff the level-1 image fits no hull [q - M- + a, q + M+ - c] at any integer q under any option (a, c): a death however many prefixes share a value.""" u, v = img for q in range(math.floor(v - cell.Mp) - 1, math.ceil(u + cell.Mm) + 2): if any(q - cell.Mm + a <= u and v <= q + cell.Mp - c for a, c in opts): return False return True def straddler(cell, L1): """(4)'s witness at prefix level 1, in level-1 units: y in the top box at depth 1 + L1, x in the box of lower end X = Mh - (w + i) s' with i the least whose image starts below 1 (mirrored to the positive corner when M- > M+). Returns (i, image).""" s = Fr(1, cell.b ** (1 + L1)) top = cell.Mh - cell.w * s i = max(0, math.floor((cell.Mh - 1 / (cell.b * top)) / s - cell.w) + 1) while cell.b * (cell.Mh - (cell.w + i) * s) * top >= 1: i += 1 X = cell.Mh - (cell.w + i) * s return i, (cell.b * X * top, cell.b * (X + cell.w * s) * (top + cell.w * s)) # ---- (6), (7) a product consumer ---- def consumer_escape(cell, A, L2): lam2 = A + cell.Mh miss = lam2 * cell.w - Fr(cell.b) ** L2 * (cell.w - 1) return max(Fr(0), miss) / cell.Mh def xy_head(cell): """(the largest magnitude tau_1, the head's floor, its budget bounded by its room, its range) behind a product.""" rng = (-cell.Mm * cell.Mp, max(cell.Mm, cell.Mp) ** 2) r = room(cell, rng) return (cell.Mh ** 2, floor_xy(cell), lambda L: min(budget_xy(cell, L), r), rng) def sum_head(cell): rng = (-2 * cell.Mm / cell.b, 2 * cell.Mp / cell.b) r = room(cell, rng) return (2 * cell.Mh / cell.b, sum_floor(cell), lambda L: min(budget_sum(cell, L), r), rng) def room(cell, rng): """The most a narrowed reader may inset in total and still hold the range [lo, hi] in its root tile at lead 0.""" return (cell.Mm + rng[0]) + (cell.Mp - rng[1]) def times_z(cell, rng): c = [z * p for z in (-cell.Mm, cell.Mp) for p in rng] return (min(c), max(c)) def sum_fed_ok(cell): return 2 * cell.Mh ** 2 <= cell.b * cell.Mp def two_unit(cell, head): """(naive, least, the consumer's Lam2, the head's floor budget).""" A, L1s, S, _ = head(cell) lam2 = A + cell.Mh L2s = 0 while consumer_escape(cell, A, L2s) > 0: L2s += 1 least = L1s + L2s for L1 in range(L1s, L1s + 6): for L2 in range(0, 6): if consumer_escape(cell, A, L2) <= S(L1): least = min(least, L1 + L2) return L1s + L2s, least, lam2, S(L1s) # ---- (8) the chain programme ---- def chain_units(cell, head, n): A1, L1s, S, rng = head(cell) lams = [cell.Mh + A1 * cell.Mh ** (j - 2) for j in range(2, n + 1)] rooms = [] for _ in lams: rng = times_z(cell, rng) rooms.append(room(cell, rng)) return L1s, S, lams, rooms def leftover(cell, lam, L, inset): scale = Fr(cell.b) ** L return cell.w - 1 - (lam * cell.w - cell.Mh * inset) / scale def unit_floor(cell, lam): L = 0 while leftover(cell, lam, L, 0) < 0: L += 1 return L def pareto(states): """Drop every (total, leftover) another beats on both.""" out, best = {}, Fr(-1) for t in sorted(states): if states[t] > best: out[t] = best = states[t] return out def links(cell, head, n): """Per consumer j = 2..n: (its floor, GAIN: it reads one below its floor on the floor chain's leftover, PAIRWISE: on its producer's at zero inset).""" L1s, S, lams, rooms = chain_units(cell, head, n) v0 = A = S(L1s) out = [] for lam, rm in zip(lams, rooms): Ls = unit_floor(cell, lam) def low(eta): return Ls >= 1 and leftover(cell, lam, Ls - 1, min(eta, cell.w - 1)) >= 0 out.append((Ls, low(v0), low(A))) v0 = min(leftover(cell, lam, Ls, min(v0, cell.w - 1)), rm) A = min(leftover(cell, lam, Ls, 0), rm) return out def matchings(flags): """The maximum matching of the flagged links (j - 1, j) along a path, for every prefix: m[i] within consumers 2..i + 2.""" take, skip, out = -1, 0, [] for g in flags: take, skip = (skip + 1 if g else -1), max(take, skip) out.append(max(take, skip)) return out def adjacent_from(cell, lams): """The least chain length whose units carry an adjacent-range pair, or None.""" w, Mh, b = cell.w, cell.Mh, cell.b for j in range(len(lams) - 1): l1, l2 = lams[j], lams[j + 1] keep = Mh * (Mh * (w - 1) - w * (l1 - 1)) / b if l1 > 1 and l2 > 1 and w * (l2 - 1) < keep: return j + 3 return None def programme_all(cell, head, nmax, full=True): """For every chain length n = 3..nmax, the prefix of one chain: {n: (naive, the matching, the least total, greedy, the pairwise matching, inside the adjacent range)}. A chain of n units is the first n units of the chain of nmax, so one pass prices every length. GREEDY sets each unit at the least delay alive on what its producer hands it, the head at L1*; full=False skips the programme (least total None).""" L1s, S, lams, rooms = chain_units(cell, head, nmax) ls = links(cell, head, nmax) nu = matchings([g for _, g, _ in ls]) nu2 = matchings([p for _, _, p in ls]) first = adjacent_from(cell, lams) states = {} for L1 in range(L1s, L1s + 3): if S(L1) >= 0: states[L1] = max(S(L1), states.get(L1, Fr(-1))) states = pareto(states) naive, greedy = L1s, (L1s, S(L1s)) out = {} for j, (lam, (Ls, _, _)) in enumerate(zip(lams, ls)): if full: new = {} for t, v in states.items(): for L in range(max(0, Ls - 1), Ls + 3): r = leftover(cell, lam, L, min(v, cell.w - 1)) if r >= 0: r = min(r, rooms[j]) if r >= 0 and r > new.get(t + L, Fr(-1)): new[t + L] = r states = pareto(new) t, v = greedy for L in range(max(0, Ls - 1), Ls + 3): r = leftover(cell, lam, L, min(v, cell.w - 1)) if r >= 0: greedy = (t + L, min(r, rooms[j])) break naive += Ls n = j + 2 if n >= 3: out[n] = (naive, naive - nu[j], min(states) if full else None, greedy[0], naive - nu2[j], first is not None and n >= first) return out def programme(cell, head, n): return programme_all(cell, head, n)[n] def run_units(cell, A1): """A chain's whole floor-2 run plus one unit, at least 3 units.""" run, top = 0, A1 while cell.Mh + top > 1: run, top = run + 1, top * cell.Mh return max(3, run + 2) # ---- the sections ---- def section_ca(): print("CA the controls") off = 0 for cell in cells(2, 5): for L in range(1, 5): off += clause_dead(cell, L, 0, 0) != ms.clause_dead( cell.b, cell.am, cell.ap, 2, L) check("CA(i) the inset clause at zero insets is the k = 2 clause", off == 0, f"80 (cell, L), {off} off") fr = [Fr(0), Fr(1, 10), Fr(1, 6), Fr(1, 3), Fr(1, 2)] tot, off, where = 0, 0, [] for cell in cells(2, 4): for L2 in (1, 2): for fa in fr: for fb in fr: a, c = fa * (cell.w - 1), fb * (cell.w - 1) tot += 1 if zone_scan_dead(cell, L2, a, c) != clause_dead( cell, L2, a, c): off += 1 where.append((cell.b, cell.am, cell.ap, L2, str(fa), str(fb))) check("CA(ii) the zone scan equals the inset clause", off == 0, f"{tot} triples, {off} off {where[:4]}") off = 0 for cell in cells(2, 5): if representable(cell): lam, o, Ls = ms.law_of(cell, ms.MAPS[2]) off += narrowed_L(cell, 2 * cell.Mh, 0) != Ls - o check("CA(iii) the narrowed reader at zero insets is the product's " "floor", off == 0, f"{off} off") def section_cb(): print("CB the inset law at the 20 cells") below, fused_cmp, rep = [], {}, 0 for cell in cells(2, 5): L1s, L2s = floor_xy(cell), sum_floor(cell) naive = L1s + L2s least = naive for L1 in range(L1s, L1s + 6): for L2 in range(1, 6): if escape_cost(cell, L2) <= budget_xy(cell, L1): least = min(least, L1 + L2) if least < naive: below.append((cell.b, cell.am, cell.ap)) lam, o, Lf = ms.law_of(cell, ms.MAPS[4]) tag = "rep" if representable(cell) else "led" rep += tag == "rep" rel = "below" if Lf < naive else ( "equal" if Lf == naive else "above") fused_cmp.setdefault(tag, {}).setdefault(rel, 0) fused_cmp[tag][rel] += 1 print(f" ({cell.b},{cell.am},{cell.ap}) {tag}: L1* {L1s}, " f"L2* {L2s}, naive {naive}, inset law {least}, fused " f"{Lf} (lead {o})") print(f" fused against the chain: {fused_cmp}; representable " f"{rep}") check("CB the inset law never below the naive sum", not below, f"below at {below}") print("CB the aligned unit (4): controls, then radices 2..60") hand = ms.Cell(2, 1, 1) i, img = straddler(hand, 2) o1 = escape_options(hand, 1) fine = [(Fr(j, 2), Fr(j + 1, 2)) for j in range(-4, 6)] print(f" (2,1,1) L1 2: i {i}, image {img[0]}..{img[1]} (by hand " f"i 1, 15/16..7/4), homeless {homeless(hand, o1, img)}; the " f"aligned halves [j/2, (j+1)/2]: homeless at " f"{sum(homeless(hand, o1, im) for im in fine)} of {len(fine)}") check("CB control: the hand straddler, homeless", (i, img) == (1, (Fr(15, 16), Fr(7, 4))) and homeless(hand, o1, img)) check("CB control: aligned images are never homeless", not any(homeless(hand, o1, im) for im in fine)) off, s1, s2, pairs, worst_i = [], 0, 0, 0, 0 for cell in cells(2, 60): for L2 in (2, 3): if escape_options(cell, L2) != [(Fr(0), Fr(0))]: off.append(("bites at L2", L2, cell.b, cell.am, cell.ap)) opts = escape_options(cell, 1) if cell.am + cell.ap + 1 - cell.b >= 2: s2 += 1 if opts != [(Fr(0), Fr(0))]: off.append(("bites at slack 2+", cell.b, cell.am, cell.ap)) continue s1 += 1 for a, c in opts: h0, h1 = -cell.Mm + a, cell.Mp - c if h1 > math.floor(h0) + 1: off.append(("hull past its unit", cell.b, cell.am, cell.ap)) if sum_floor(cell) != 2: off.append(("adder floor", cell.b, cell.am, cell.ap)) if not representable(cell): continue L1s = floor_xy(cell) for L1 in range(L1s, L1s + 4): pairs += 1 i, img = straddler(cell, L1) worst_i = max(worst_i, i) X = cell.Mh - (cell.w + i) * Fr(1, cell.b ** (1 + L1)) if not (X >= 0 and img[0] < 1 < img[1] and homeless(cell, opts, img)): off.append(("no homeless image", cell.b, cell.am, cell.ap, L1)) for o in off[:12]: print(f" AU OFF {o}") print(f" slack-1 cells {s1}, every option hull in an aligned unit, " f"adder floor 2; slack-2+ cells {s2}, clause empty at L2 = 1; " f"no cell bites at L2 = 2, 3; representable (cell, L1) pairs " f"{pairs}, each with a homeless image at n = 1 (largest i " f"{worst_i}); off {len(off)}") check("CB the aligned unit and its homeless image", not off and pairs, f"{len(off)} off") def section_cc(): print("CC the threshold-miss law, radices 2..40") off, gains, deep = [], {"xy": [], "sum": []}, [] bound = {"xy": 0, "sum": 0} unfunded = 0 for cell in cells(2, 40): for name, head, ok in (("xy", xy_head, representable), ("sum", sum_head, sum_fed_ok)): if not ok(cell): continue naive, least, lam2, S0 = two_unit(cell, head) if S0 < 0: unfunded += 1 continue _, L1s, _, rng = head(cell) raw = (budget_xy if name == "xy" else budget_sum)(cell, L1s) if room(cell, rng) < raw: bound[name] += 1 if cell.rho >= 2: if least < naive: deep.append((name, cell.b, cell.am, cell.ap)) continue law = 0 < lam2 - 1 <= cell.Mh / cell.w * S0 if law != (least < naive): off.append((name, cell.b, cell.am, cell.ap)) if least < naive: gains[name].append((cell.b, cell.am, cell.ap)) for name, g in gains.items(): more = " ..." if len(g) > 12 else "" print(f" {name}-fed: {len(g)} gaining cells at " f"{len({c[0] for c in g})} radices: {g[:12]}{more}") print(f" the range's room below the budget at the head's floor: " f"{bound}; heads with no budget at their floor, skipped: " f"{unfunded}") check("CC the search equals the criterion at every slack-1 cell", not off, f"off at {off[:6]}") want = [(4, 2, 2)] for b, am, ap in ((9, 4, 5), (12, 5, 7), (17, 7, 10), (22, 9, 13), (25, 10, 15), (30, 12, 18), (33, 13, 20), (38, 15, 23)): want += [(b, am, ap), (b, ap, am)] check("CC the product-fed gains are the 17 predicted cells", sorted(gains["xy"]) == sorted(want), f"read {len(gains['xy'])}") want = sorted([(b, 2, b - 2) for b in range(5, 41)] + [(b, b - 2, 2) for b in range(5, 41)]) check("CC the sum-fed gains are (b, 2, b - 2) and mirrors, 5..40", sorted(gains["sum"]) == want, f"read {len(gains['sum'])}") check("CC no cell of slack >= 2 gains", not deep, f"at {deep[:6]}") def section_cd(): print("CD the matching law") t0 = time.time() outside, inside, greedy_off, reads, unending = [], {}, [], 0, 0 for cell in cells(3, 40, slack=1): for name, head, ok in (("xy", xy_head, representable), ("sum", sum_head, sum_fed_ok)): if not ok(cell): continue A1, L1s, S, _ = head(cell) if S(L1s) < 0: continue ns = set(range(3, 13)) if cell.Mh == 1: unending += 1 elif cell.b <= 24: ns.add(run_units(cell, A1)) every = programme_all(cell, head, max(ns)) for n in sorted(ns): naive, match, least, greedy, _, adj = every[n] reads += 1 key = (name, cell.b, cell.am, cell.ap, n) if greedy != least: greedy_off.append(key + (least, greedy)) if least != match: if adj: inside[key] = match - least else: outside.append(key + (naive, match, least)) print(f" {reads} chains read, {time.time() - t0:.1f} s; whole run " f"unread at {unending} (cell, head) with Mh = 1") print(f" window 0 (greedy against the programme) off at " f"{len(greedy_off)} {greedy_off[:4]}") print(f" off the matching inside the adjacent range at " f"{len(inside)}, by {sorted(set(inside.values()))}") check("CD greedy is the least total at every chain", not greedy_off) check("CD naive - nu outside the adjacent range", not outside, f"off at {outside[:4]}") naive, match, least, *_, adj = programme(ms.Cell(9, 2, 7), sum_head, 5) print(f" (9, 2, 7) sum-fed, five units: naive {naive}, matching " f"{match}, least {least}, adjacent {adj}") check("CD the witness reads 7 against the matching's 8, adjacent", (match, least, adj) == (8, 7, True)) off = [] for b in range(8, 41): for cell in (ms.Cell(b, 2, b - 2), ms.Cell(b, b - 2, 2)): naive, match, least, *_ = programme(cell, sum_head, 4) if least != naive - 2: off.append((b, cell.am, cell.ap, naive, least)) check("CD the sum-fed four-unit chain reads naive - 2, radices 8..40", not off, f"off at {off[:4]}") def section_ce(): print("CE the led stream") rows = [] for cell, h in poles.pairs(): u = poles.Recip(cell, h) c1 = u.law_L() - u.lead() if c1 >= 0: continue R = Fr(1) / (Fr(cell.b) ** u.lead() * h) o2 = poles.least_pow(cell.b, R) La = narrowed_L(cell, R + cell.Mh, 0) Le = narrowed_L(cell, R + cell.Mh / Fr(cell.b) ** (-c1), 0) dv = poles.Divider(cell, h) cd = dv.law_L() - dv.lead() rows.append((La - o2, Le - o2, cd)) eb = sum(1 for a, e, _ in rows if e < a) fz = sum(1 for _, e, c in rows if c <= e) fe = sum(1 for _, e, c in rows if c == e) print(f" {len(rows)} pairs; eager below aligned at {eb}; the fused " f"divider at or below the eager chain at {fz}, equal at {fe}") print(f" least c2 over the pairs: aligned " f"{min(a for a, _, _ in rows)}, eager {min(e for _, e, _ in rows)}" " (at least 0 by the sufficiency law, printed, not checked)") check("CE 40 pairs, eager below aligned at 25", len(rows) == 40 and eb == 25, f"read {len(rows)}, {eb}") check("CE the fused divider at or below at every pair", fz == len(rows)) def section_cg(bmax): print(f"CG the crossed links, every prefix, radices 3..{bmax}") for b, am, ap, n, want in ((31, 3, 28, 34, 67), (29, 2, 27, 74, 147), (24, 3, 21, 23, 46)): cell = ms.Cell(b, am, ap) naive, match, least, greedy, pair, adj = programme(cell, xy_head, n) print(f" ({b},{am},{ap}) n = {n}: naive {naive}, least {least}, " f"greedy {greedy}, matching {match}, pairwise {pair}") check(f"CG control ({b},{am},{ap}) n = {n} reads {want}", least == greedy == match == want and not adj) if not all(CHECKS): return t0 = time.time() crossed, above, off, pair_off = [], [], [], [] reads = adj = 0 for b in range(3, bmax + 1): for cell in cells(b, b, slack=1): if not representable(cell) or cell.Mh == 1: continue A1, L1s, S, _ = xy_head(cell) if S(L1s) < 0: continue n = run_units(cell, A1) ls = links(cell, xy_head, n) gains = [j for j, (_, g, _) in enumerate(ls, 2) if g] for j, (_, g, p) in enumerate(ls, 2): if g and not p: crossed.append((b, cell.am, cell.ap, j)) above += [(b, cell.am, cell.ap, i, j) for i in gains if i < j] for m, (naive, match, _, greedy, pair, a) in programme_all( cell, xy_head, n, full=False).items(): reads += 1 if a: adj += 1 continue key = (b, cell.am, cell.ap, m) if greedy != match: off.append(key + (match, greedy)) if greedy != pair: pair_off.append(key + (pair - greedy,)) print(f" {reads} prefixes, {adj} inside the adjacent range, " f"{time.time() - t0:.1f} s") print(f" crossed links {crossed}") print(f" ABOVE {above[:6]} ({len(above)})") print(f" OFF {off[:6]} ({len(off)})") print(f" the pairwise reading off at {len(pair_off)} prefixes, by " f"{sorted({d for *_, d in pair_off})}, at cells " f"{sorted({k[:3] for k in pair_off})}") check("CG no gain above a crossed link", not above) check("CG greedy is naive - nu at every prefix outside the adjacent " "range", not off) return crossed, pair_off def main(): t0 = time.time() section_ca() if not all(CHECKS): print("\nCONTROL FAILED: nothing below is read.") raise SystemExit(1) section_cb() section_cc() section_cd() section_ce() section_cg(200 if "--cg200" in sys.argv else 60) 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()