manystream.py
Checks: REDUNDANT: The many-stream theorem theorem.
Cited on: REDUNDANT.
To run it: save manystream.py, with redundant.py beside it; standard library only.
"""
manystream.py -- the least lookahead of a smooth map of several
signed-digit streams, read against the affine criterion.
QUESTION. redundant.py gives the exact least lookahead of every
weighted sum of streams: the affine criterion, a count of lattice
points in one interval. Its LENGTH TEST, the same interval measured
against a period with the lattice dropped, is within one digit of it.
What does a map that is NOT affine cost? The claim carried here: a
C^2 map of any number of streams is read at exactly the length test
taken at its steepest tangent, the sup over the root box of its
gradient's L1 norm, unless it is affine on the root box. Curvature
forfeits the lattice and nothing else. And is the sup the gradient's
own, or the gradient BOX's (each partial's sup taken apart)?
THE READER. Streams are infinite strings of the digits D = {-a-, ...,
a+} in radix b, a+- >= 0, SLACK rho = a- + a+ + 1 - b >= 1. Write
M+- = a+-/(b - 1), w = M- + M+ and |I| = a- + a+, so w = |I|/(b - 1)
and w - 1 = rho/(b - 1). A stream's value lies in [-M-, M+]; after n
digits, with u the integer the n digits write, it lies in the BOX
[(u - M-)/b^n, (u + M+)/b^n], and every integer u of
[-a- R_n, a+ R_n], R_n = (b^n - 1)/(b - 1), is some prefix. A map f of
d streams is written as y = sum_j e_j b^(o - j), e_j in D, with a LEAD
o in Z: after t output digits of value Q the output lies in the TILE
[(Q - M-) b^(o - t), (Q + M+) b^(o - t)]. The REAL READER, the reader
of infinite streams this script builds, at lookahead c commits output
digit t once it has read n = t + c digits of every stream (before
reading any, when c < 0), and must keep f of the current box inside
the current tile. The lead is the least o whose root tile
[-M- b^o, M+ b^o] holds f's range; the count that carries the law is
L = c + o.
THE ARGUMENT (written before this script).
(1) THE TILE LEMMA. In units b^(o - t) the level-t tiles are
[p - M-, p + M+], p an integer, and consecutive ones overlap in
the ZONE [p + 1 - M-, p + M+] of length w - 1 > 0. An interval
[lo, hi] lies in some tile iff an integer lies in
[hi - M+, lo + M-], and otherwise it STRICTLY CONTAINS a zone,
the one at p = ceil(hi - M+) - 1. If the committed tile of
value Q holds the interval, its children bQ + e, e in D, run
over the integers of [bQ - a-, bQ + a+], and the interval's
ends put hi - M+ <= bQ + a+ and lo + M- >= bQ - a-, so an
integer of [hi - M+, lo + M-] clamped into the children's range
stays in it: some CHILD tile holds the interval. So the reader
is dead at L iff some box of some depth n, with t = n - c >= 1,
has an image strictly containing a level-t zone. That is a
property of the streams alone: the reader has no strategy, and
every legal digit is as good as another. In absolute units the
level-t zone has length (w - 1) b^(L - n).
(2) THE WIDTH RATE. A depth-n box has side w/b^n in every
coordinate, so by the mean value theorem its image is at most
Lam_B w/b^n wide, Lam_B the sup over the box of
|grad f|_1 = sum_i |d_i f|. It cannot strictly contain a zone
when Lam_B <= Lam_law = (w - 1) b^L / w, a bound free of the
depth, and a sub-box's sup is at most its box's. So only boxes
of the EXCESS REGION, Lam_B > Lam_law, can kill, and a scan
confined to them loses no kill.
(3) THE MARGIN LAW. With Lam the sup of |grad f|_1 over the root box,
f is read at L whenever Lam <= Lam_law, that is
b^L rho >= Lam |I|,
the region then being empty. Let L* be the least such L.
(4) THE LENGTH TEST AT THE STEEPEST TANGENT. For an affine map with
weights lam_i of either sign, redundant.py's injection bounds
add to M+ + M- = |I| sum_i |lam_i|, so its interval
[-eps-, eps+] has length eps+ + eps- = |I| (b^c - Lam)/(b - 1),
Lam = sum_i |lam_i|, and the length test eps+ + eps- >= b^c is
b^c rho >= Lam |I|: the margin law at L = c. Signs do not enter.
So (3) reads f at the length test of its tangent map at the
point where the gradient's L1 norm is largest.
(5) NECESSITY. Below L* the law's excess xi = Lam w/b^L - (w - 1) is
positive. If f is not affine on the root box, the component C of
{|grad f|_1 > (Lam + Lam_law)/2} holding the peak carries a
point of nonzero Hessian: a vanishing Hessian on C makes the
gradient constant on C, a boundary point of C inside the root box
would then read the midpoint, so C is the root box and f is
affine. Round that point, a small ball B has every partial of
one sign or identically zero, an integer direction V with
V^T H V one-signed, H the Hessian, and at least zeta > 0 in
size, and sum_i inf_B |d_i f| above the midpoint. On B the image
of a box runs between the two opposite corners the signs name, so
every box there has excess at least xi/2, and along the prefix
line u + i V, u a prefix and i an integer, the image's lower end,
read modulo the zone grid, is a C^2 phase in i whose second
derivative is one-signed and of size
at least zeta/b^(n+L). By van der Corput's second-derivative
estimate and the Erdos-Turan inequality (Kuipers and
Niederreiter, Uniform Distribution of Sequences, 1974) these
phases are equidistributed as n grows, so one of them falls in
the dead arc of length xi/2 at some depth: the reader is dead.
An affine map has no such line; its lower ends sit on a lattice
and redundant.py's criterion decides it, reading at L* or one
below it.
(6) THE SUMS. For x_1 + ... + x_k the image of a box is fixed by
the prefix sum s, which runs over every integer of
[-k a- R_n, k a+ R_n], so the box's image is
[(s - k M-)/b^n, (s + k M+)/b^n]. The stream reader of
redundant.py, its signed-digit reader of integers, at lookahead
c and this reader at L = c should be one reader: that stream
reader's clause "0 lies in J", b^c >= k, is the real reader's
lead, b^o >= k. (As frozen, and it holds: the lead o is the least o with b^o >= k, so the clause at c = L, b^L >= k, holds iff L >= o.)
(7) THE BOX IS NOT THE GRADIENT. f = x(1 - y^2) has d_x = 1 - y^2,
d_y = -2xy. With Mh = max(M-, M+) <= 1, |1 - y^2| + 2 Mh |y|
rises in |y| on the root box, so Lam = 1 + Mh^2 at |x| = |y| = Mh,
while the partials' separate sups add to 1 + 2 Mh^2: d_x peaks
at y = 0, where d_y vanishes. The law read on the gradient box
asks for b^L rho >= (1 + 2 Mh^2)|I|.
THE DESIGN, frozen before the engine.
Exact rationals throughout. A map is its image over a box, exact:
intervals of distinct variables multiply exactly, an even power of
an interval holding 0 starts at 0, x^2 + x y takes its corners and
its edge minima at x = -y/2, and x(1 - y^2) is the product of the
independent intervals x and 1 - y^2. Its width rate over a box is an
interval-arithmetic bound on each partial, summed in absolute value:
never below the true sup, so pruning by it keeps every kill. Lam is
derived per map in closed form and checked against the width rate
over the whole root box, which is exact for every map but x(1 - y^2).
The lead is the least o in Z whose root tile holds the exact range.
THE SCAN at L: depth by depth from the root box, the children of a box
u being b u + e, e in D, per coordinate, only boxes of the excess
region kept; at each depth n with t = n - c >= 1 every kept box is
tested by (1). It stops at the first kill, at depth NMAX, or past
BUDGET boxes.
THE MAPS: x^2, x^3, x y, x^2 + y, x y + z, x^2 + x y, x^2 y, x y z and
x(1 - y^2), at the 20 cells b = 2..5, 1 <= a+- <= b - 1, rho >= 1.
Their laws: x^2 and x y at Lam = 2 Mh; x^3, x^2 y and x y z at 3 Mh^2;
x^2 + y and x y + z at 2 Mh + 1; x^2 + x y at 4 Mh (|2x + y| + |x| at
the corner of largest magnitude with x = y); x(1 - y^2) at
1 + Mh^2 by (7).
THE SUMS: k = 1, 2, 3 at every cell b = 2..5, 0 <= a+- <= b,
rho >= 1, M+ > 0 and M- > 0; the lead the least o with b^o >= k;
redundant.py's stream reader's least lookahead from its game,
sum_game_c_min at unit weights and phase 0.
THE ARITHMETIC: at b = 2..12, 0 <= a+- <= 12, rho >= 1, k = 1..4,
L = 0..4, the real reader's k-sum clause, dead iff an integer lies in
((b^L - k) M+, b^L - (b^L - k) M-), against redundant.py's
sum_criterion at unit weights, phase 0, c = L; and at the same cells
with the weight vectors of redundant.py's grid, the margin at the
vector's L1 norm against the length of sum_interval's unclipped
interval.
PREDICTIONS.
MA the controls, read first: x y at (2, 1, 1) at L* = 2 and dead at
1; x^2 + y at (2, 1, 1) at L* = 3, lead 1; x at (2, 1, 1) alive
at L = 0 to NMAX; x + y at (2, 1, 1) dead at L = 1.
ML the margin law at a weight vector's L1 norm is the length test at
every arithmetic cell, every c and every vector, both signs.
MS at every map and cell the region is empty at L*, and the width
rate over the root box equals the closed-form Lam at every map but
x(1 - y^2).
MN at every map and cell the scan at L* - 1 finds a kill, at output
depth at most 6 (the cube's at the least-excess cell (5, 3, 3)
the deepest, a transplant from the cube's earlier census).
MB x(1 - y^2): the scan at L* finds no kill to depth NMAX at every
cell; the box law's L is above L* at some cells, among them
(2, 1, 1), (4, 3, 3) and (5, 4, 4), and at those the scan at L*
is clean too.
MK for k = 1, 2, 3 at every sum cell the scan at L = c_min - 1 kills
(when c_min - 1 >= o) and at L = c_min finds nothing to depth
NMAX, c_min redundant.py's stream reader's.
MC the k-sum clause is redundant.py's criterion at every arithmetic
cell.
MW at every census cell with a+ = b - 1 >= a- (so x y's steepest
tangent is x + y), L*(x y) - c_min(X + Y) is 0 or 1, and 1
exactly on the addition wedge.
KILLS, as what the script prints.
K1 an MA line off: the reader's convention is wrong; nothing below
is read.
K2 an ML cell off: (4) is false.
K3 a nonempty region at L*, or a root-box rate off its closed form:
the map's Lam or its interval bound is wrong.
K4 an MN pair with no kill: necessity is unread there (the scan's
reach, or (5)).
K5 an MB kill at L*: (7)'s Lam is wrong or (3) fails.
K6 an MK or MC line off: (6)'s identification of the two readers is
false.
K7 an MW line off: the wedge does not transfer.
POSITIVE CONTROL: MA, read before any verdict line.
FINDINGS (entered after the run; every number is a print).
- MA holds: x y at (2, 1, 1) at L* = 2, dead at 1 at output depth 2;
x^2 + y at L* = 3 with lead 1; the identity clean at L = 0; x + y
dead at L = 1 at output depth 1. K1 did not fire.
- ML holds: the margin at the L1 norm is the length test at all
334950 (cell, weight vector, c), both signs.
- MS holds: the root-box rate is the closed-form Lam at the eight
maps and 1 + 2 Mh^2 at x(1 - y^2).
- MN holds: all 180 (map, cell) pairs are dead at L* - 1, each by an
exact box whose image strictly contains a zone. Output depth 1 at
114 pairs, 2 at 56, 3 at 6, 4 at 3 (x^2 at (4, 2, 2), x^2 y and
x y z at (5, 3, 3)) and 6 at one, x^3 at (5, 3, 3), as the
transplant said. Of the kills at depth 4 or more, whose boxes
print, x y z at (5, 3, 3) read the most, 17879.
- MB holds: the box law asks one more digit than L* at 6 cells,
(2, 1, 1), (4, 3, 3), (5, 3, 3), (5, 3, 4), (5, 4, 3) and
(5, 4, 4). At the four radix-5 cells the excess region is EMPTY by
depth 2 at L* (printed per cell), so the scan's bound certifies
survival outright; at
(2, 1, 1) and (4, 3, 3), where Lam = Lam_law exactly, the corner
boxes' bound never falls to the threshold and the scan is clean to
depth 12 and 8, the theorem's sufficiency doing the rest.
- MK holds: at all 132 (cell, k), k = 1, 2, 3, the real reader of
the k-sum is alive at c_min, c_min the stream reader's least
lookahead in redundant.py, and dead at c_min - 1 at every pair
where c_min - 1 reaches the lead (56 of the 132); below the lead its
first digit must hold the whole range. The two readers are one.
- On audit: ML re-types sum_interval's eps+- rather than calling it,
so it reads the identity's exact arithmetic; MS's empty region at
L* followed from the rate check and the definition of L*, and is
cut, the rates kept.
- MC holds at all 17400 (cell, k, L): the k-sum clause is the
criterion.
- MW holds at 10 cells: x y reads one digit after addition at
(3, 2, 2), (4, 2, 3) and (5, 2, 4), the wedge cells, and with it
elsewhere. Curvature pays exactly the lattice's discount.
- Two changes after the first run, neither touching a verdict. The
sum scan as frozen ran to depth NMAX; in zone units the image is
[(s - k M-)/b^L, (s + k M+)/b^L], free of n and periodic in s with
period b^L, so the scan now stops at the first depth whose prefix
sums cover a period, in integers, and its survival side is
decided rather than budgeted (MK read the same at both). The
arithmetic grid is b, a+- <= 10, not 12, for the wall.
- (5) as frozen says an affine map reads "at L* or one below it".
Only "at or below" holds for every affine map, by (3); the one
digit is the length bound's, proved for positive weights at total
rate at least 1, and MK carries it to the real reader of unit
sums alone. The lead never binds at the 180 pairs: L* is the
law's L at each.
RUN RECORD: 11/11 checks, 30.0 s, peak commit 104.9 MB under a memory guard;
after an audit, 11/11, 27.9 s, 104.9 MB.
"""
import math
import time
from fractions import Fraction as Fr
import redundant as rd
CHECKS = []
NMAX = 12
BUDGET = 300_000
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 repunit(b, j):
return (b ** j - 1) // (b - 1)
# ---- intervals, exact ----
def imul(p, q):
c = (p[0] * q[0], p[0] * q[1], p[1] * q[0], p[1] * q[1])
return (min(c), max(c))
def iadd(*ps):
return (sum(p[0] for p in ps), sum(p[1] for p in ps))
def ipow(p, k):
lo, hi = p
if k % 2 == 1:
return (lo ** k, hi ** k)
if lo <= 0 <= hi:
return (Fr(0), max(lo ** k, hi ** k))
return (min(lo ** k, hi ** k), max(lo ** k, hi ** k))
def iscale(s, p):
return (min(s * p[0], s * p[1]), max(s * p[0], s * p[1]))
def isup(p):
return max(abs(p[0]), abs(p[1]))
ONE = (Fr(1), Fr(1))
# ---- the maps: (name, d, image, partials, Lam of Mh) ----
def img_x2_xy(B):
(x0, x1), (y0, y1) = B
vals = [x * (x + y) for x in (x0, x1) for y in (y0, y1)]
for y in (y0, y1):
if x0 <= -y / 2 <= x1:
vals.append(-y * y / 4)
return (min(vals), max(vals))
def one_minus_sq(p):
return iadd(ONE, iscale(-1, ipow(p, 2)))
MAPS = [
("x^2", 1, lambda B: ipow(B[0], 2),
lambda B: [iscale(2, B[0])], lambda M: 2 * M),
("x^3", 1, lambda B: ipow(B[0], 3),
lambda B: [iscale(3, ipow(B[0], 2))], lambda M: 3 * M * M),
("x y", 2, lambda B: imul(B[0], B[1]),
lambda B: [B[1], B[0]], lambda M: 2 * M),
("x^2 + y", 2, lambda B: iadd(ipow(B[0], 2), B[1]),
lambda B: [iscale(2, B[0]), ONE], lambda M: 2 * M + 1),
("x y + z", 3, lambda B: iadd(imul(B[0], B[1]), B[2]),
lambda B: [B[1], B[0], ONE], lambda M: 2 * M + 1),
("x^2 + x y", 2, img_x2_xy,
lambda B: [iadd(iscale(2, B[0]), B[1]), B[0]], lambda M: 4 * M),
("x^2 y", 2, lambda B: imul(ipow(B[0], 2), B[1]),
lambda B: [iscale(2, imul(B[0], B[1])), ipow(B[0], 2)],
lambda M: 3 * M * M),
("x y z", 3, lambda B: imul(imul(B[0], B[1]), B[2]),
lambda B: [imul(B[1], B[2]), imul(B[0], B[2]), imul(B[0], B[1])],
lambda M: 3 * M * M),
("x(1 - y^2)", 2, lambda B: imul(B[0], one_minus_sq(B[1])),
lambda B: [one_minus_sq(B[1]), iscale(-2, imul(B[0], B[1]))],
lambda M: 1 + M * M),
]
BOXLAW = {"x(1 - y^2)": lambda M: 1 + 2 * M * M}
def census():
return [(b, am, ap) for b in range(2, 6) for am in range(1, b)
for ap in range(1, b) if am + ap + 1 - b >= 1]
class Cell:
def __init__(self, b, am, ap):
self.b, self.am, self.ap = b, am, ap
self.rho = am + ap + 1 - b
self.I = am + ap
self.Mm, self.Mp = Fr(am, b - 1), Fr(ap, b - 1)
self.w = self.Mm + self.Mp
self.Mh = max(self.Mm, self.Mp)
def box(self, u, n):
s = Fr(1, self.b ** n)
return ((u - self.Mm) * s, (u + self.Mp) * s)
def lam_law(self, L):
return (self.w - 1) * Fr(self.b) ** L / self.w
def law_L(self, lam):
L = -40
while Fr(self.b) ** L * self.rho < lam * self.I:
L += 1
return L
def lead(self, rng):
o = -40
while not (rng[0] >= -self.Mm * Fr(self.b) ** o
and rng[1] <= self.Mp * Fr(self.b) ** o):
o += 1
return o
def kills(self, img, n, L):
"""(1): does the image strictly contain a zone at depth n?"""
e = Fr(self.b) ** (L - n)
lo, hi = img[0] / e, img[1] / e
return math.floor(lo + self.Mm) < hi - self.Mp
def rate(parts):
return sum(isup(p) for p in parts)
def digit_tuples(D, d):
if d == 1:
return [(e,) for e in D]
return [(e,) + r for e in D for r in digit_tuples(D, d - 1)]
def scan(cell, mp, L, o):
"""Least output depth of a kill at L, or None; and boxes read."""
name, d, image, partials, _ = mp
c = L - o
law = cell.lam_law(L)
tuples = digit_tuples(range(-cell.am, cell.ap + 1), d)
level = [(0,) * d]
read = 0
for n in range(0, NMAX + 1):
kept = []
for u in level:
B = [cell.box(ui, n) for ui in u]
read += 1
if rate(partials(B)) <= law:
continue
if n - c >= 1 and cell.kills(image(B), n, L):
return n - c, read
kept.append(u)
scan.reached, scan.emptied = n, not kept
if not kept or read > BUDGET:
return None, read
level = [tuple(cell.b * ui + e for ui, e in zip(u, es))
for u in kept for es in tuples]
return None, read
def root_box(cell, d):
return [(-cell.Mm, cell.Mp)] * d
def law_of(cell, mp):
name, d, image, partials, lamf = mp
lam = lamf(cell.Mh)
o = cell.lead(image(root_box(cell, d)))
return lam, o, max(cell.law_L(lam), o)
# ---- sums of streams ----
def sum_scan(cell, k, L, o):
"""(6): the k-sum's boxes are indexed by the prefix sum s. In zone
units the image is [(s - k M-)/b^L, (s + k M+)/b^L], free of the
depth and periodic in s with period b^L, so the first depth whose
prefix sums cover a period decides the reader."""
c = L - o
b, q, B = cell.b, cell.b - 1, cell.b ** L
for n in range(max(0, c + 1), NMAX + 1):
R = repunit(b, n)
s0, s1 = -k * cell.am * R, k * cell.ap * R
for s in range(s0, min(s1, s0 + B - 1) + 1):
X = s * q - k * cell.am + cell.am * B
Y = s * q + k * cell.ap - cell.ap * B
if (X // (q * B)) * q * B < Y:
return n - c
if s1 - s0 + 1 >= B:
return None
raise RuntimeError("the prefix sums never covered a period")
def sum_lead(b, k):
o = 0
while b ** o < k:
o += 1
return o
def clause_dead(b, am, ap, k, L):
Mm, Mp = Fr(am, b - 1), Fr(ap, b - 1)
lo, hi = (b ** L - k) * Mp, b ** L - (b ** L - k) * Mm
return math.floor(lo) + 1 < hi
# ---- the sections ----
def section_ma():
print("MA the controls")
xy, x2y = MAPS[2], MAPS[3]
cell = Cell(2, 1, 1)
lam, o, Ls = law_of(cell, xy)
k, _ = scan(cell, xy, 1, o)
check(f"x y at (2, 1, 1): L* = {Ls}, dead at 1 at output depth {k}",
Ls == 2 and k is not None, "recorded L* = 2")
lam, o, Ls = law_of(cell, x2y)
check(f"x^2 + y at (2, 1, 1): L* = {Ls}, lead {o}",
Ls == 3 and o == 1, "recorded 3, lead 1")
k1 = sum_scan(cell, 1, 0, 0)
check(f"x at (2, 1, 1), L = 0: kill {k1}", k1 is None,
"the identity reads at 0")
k2 = sum_scan(cell, 2, 1, sum_lead(2, 2))
check(f"x + y at (2, 1, 1), L = 1: kill at output depth {k2}",
k2 is not None, "addition reads at 2")
def arith_cells():
for b in range(2, 11):
for am in range(11):
for ap in range(11):
if am + ap + 1 - b >= 1:
yield b, am, ap
def section_ml():
print("ML the margin at the L1 norm is the length test")
bad = tot = 0
vectors = list(rd.weight_vectors())
for (b, am, ap) in arith_cells():
rho, I = am + ap + 1 - b, am + ap
for lams in vectors:
Lam = sum(abs(l) for l in lams)
Mp = sum(abs(l) * (ap if l > 0 else am) for l in lams)
Mm = sum(abs(l) * (am if l > 0 else ap) for l in lams)
for c in range(5):
ep = (Fr(ap * b ** c) - Mp) / (b - 1)
em = (Fr(am * b ** c) - Mm) / (b - 1)
tot += 1
if (ep + em >= b ** c) != (b ** c * rho >= Lam * I):
bad += 1
check("ML margin == length test", bad == 0,
f"{tot} (cell, vector, c), {bad} off")
def section_mapped():
print("MS, MN, MB the nine maps at the 20 cells")
t0 = time.time()
off = 0
nokill, deepest, reads = [], 0, 0
box_above, box_clean = [], 0
for mp in MAPS:
name, d, image, partials, lamf = mp
Lv, ov, kd = set(), set(), {}
for (b, am, ap) in census():
cell = Cell(b, am, ap)
lam, o, Ls = law_of(cell, mp)
Lv.add(Ls)
ov.add(o)
wr = rate(partials(root_box(cell, d)))
want = BOXLAW[name](cell.Mh) if name in BOXLAW else lam
if wr != want:
off += 1
k, r = scan(cell, mp, Ls - 1, o)
reads += r
if k is None:
nokill.append((name, b, am, ap))
else:
kd[k] = kd.get(k, 0) + 1
deepest = max(deepest, k)
if k >= 4:
print(f" {name} at ({b}, {am}, {ap}): output "
f"depth {k}, {r} boxes")
if name in BOXLAW:
kL, r = scan(cell, mp, Ls, o)
reads += r
Lbox = max(cell.law_L(BOXLAW[name](cell.Mh)), o)
if Lbox > Ls:
box_above.append(((b, am, ap), Ls, Lbox,
scan.reached, scan.emptied))
if kL is None:
box_clean += 1
if kL is not None:
nokill.append((name + " killed at L*", b, am, ap))
print(f" {name}: L* in {sorted(Lv)}, leads {sorted(ov)}, "
f"kills at L* - 1 by output depth {dict(sorted(kd.items()))}")
check("MS the root-box rates match their closed forms", off == 0,
f"{off} rates off")
check("MN a kill at L* - 1 at every map and cell, depth <= 6",
not nokill and deepest <= 6,
f"{len(MAPS) * len(census())} pairs, deepest {deepest}, "
f"missing {nokill}")
print(f" x(1 - y^2): the box law above L* at {len(box_above)} "
f"cells (cell, L*, box L, depth the scan at L* reached, "
f"the excess region emptied there): "
f"{box_above}")
need = {(2, 1, 1), (4, 3, 3), (5, 4, 4)}
check("MB x(1 - y^2) clean at L*; the box law asks more",
need <= {c for c, _, _, _, _ in box_above}
and box_clean == len(box_above),
f"clean at {box_clean} of {len(box_above)}")
print(f" {reads} boxes read, {time.time() - t0:.1f} s")
def sum_cells():
for b in range(2, 6):
for am in range(1, b + 1):
for ap in range(1, b + 1):
if am + ap + 1 - b >= 1:
yield b, am, ap
def section_mk():
print("MK the k-sum: the real reader against redundant.py's stream reader")
bad, tot, below = [], 0, 0
for (b, am, ap) in sum_cells():
cell = Cell(b, am, ap)
for k in (1, 2, 3):
cm = rd.sum_game_c_min(b, am, ap, (Fr(1),) * k, Fr(0))
o = sum_lead(b, k)
tot += 1
if sum_scan(cell, k, cm, o) is not None:
bad.append((b, am, ap, k, "kill at c_min"))
if cm - 1 >= o:
below += 1
if sum_scan(cell, k, cm - 1, o) is None:
bad.append((b, am, ap, k, "none at c_min - 1"))
check("MK the real reader of x_1 + .. + x_k reads at c_min",
not bad, f"{tot} (cell, k), dead below read at {below}, "
f"off {bad}")
def section_mc():
print("MC the k-sum clause is the affine criterion")
bad = tot = 0
for (b, am, ap) in arith_cells():
for k in range(1, 5):
for L in range(5):
tot += 1
crit = rd.sum_criterion(b, am, ap, (Fr(1),) * k,
Fr(0), L)
if clause_dead(b, am, ap, k, L) == crit:
bad += 1
check("MC clause dead iff the criterion fails", bad == 0,
f"{tot} (cell, k, L), {bad} off")
def wedge(b, am, ap):
rho = am + ap + 1 - b
return (b >= 3 and rho == 2 and min(am, ap) != 1) or \
(b == 3 and rho == 3)
def section_mw():
print("MW x y against its steepest tangent x + y")
bad, gaps = [], []
for (b, am, ap) in census():
if not ap == b - 1 >= am:
continue
_, _, Ls = law_of(Cell(b, am, ap), MAPS[2])
cm = rd.sum_game_c_min(b, am, ap, (Fr(1), Fr(1)), Fr(0))
g = Ls - cm
gaps.append(((b, am, ap), g))
if g not in (0, 1) or (g == 1) != wedge(b, am, ap):
bad.append((b, am, ap, Ls, cm))
print(f" L*(x y) - c_min(X + Y): {gaps}")
check("MW one digit exactly on the wedge", not bad,
f"{len(gaps)} cells, off {bad}")
def main():
t0 = time.time()
section_ma()
if not all(CHECKS):
print("\nCONTROL FAILED: nothing below is read.")
raise SystemExit(1)
section_ml()
section_mapped()
section_mk()
section_mc()
section_mw()
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()