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