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