chains.py
Checks: REDUNDANT: The relative-gradient law property; rule; REDUNDANT: The chained delay theorem; REDUNDANT: The threshold-miss law rule; pattern; REDUNDANT: The matching law rule.
Cited on: REDUNDANT.
To run it: save chains.py, with manystream.py, poles.py, redundant.py beside it; standard library only.
"""
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()