census.py
Checks: CLOCK: The admission census is the high-water lemma, item by item theorem.
Cited on: CLOCK.
To run it: save census.py, with dial.py, limit.py, stop.py beside it; standard library only.
"""census.py -- the admission census: which items a greedy walk strands,
read off the menu's prices with no walk run.
QUESTION. stop.py proves the high-water lemma: at the step that pays the
walk's largest price H every move on the menu costs at least H, so the
openings made are those priced below H. It proves that under a per-item
clock H is the runaway's crossing price. Read before, the items a headed
ladder's transient strands were counted by a formula: an item strands iff
its entry and every climb door price under the runaway's crossing price,
resting at the first rung whose exit prices at or above it. That count
held at every per-item cell read, under three hypotheses on the price
found by deleting each. Is it the high-water lemma read item by item, so
that the census is a count of menu prices below H with no walk in it?
And was the reading beside it right, that a coarser clock only raises
doors and so seats nothing the per-item census excludes?
THE SCHEDULE is limit.py's, walked by stop.py (per-item and global
clocks) and by dial.py (any partition into blocks), imported. Born {1},
nu = 1, two items per degree to 400. A ladder is HEADED when its sup
exceeds its tail, which by clock.py is a place with w >= 1. The price
kappa(d, r) is nondecreasing in d at every door and strictly increasing in
the door, kappa(d, 1) tending to infinity; a tie goes to a clock before an
opening and to the lower degree first.
An item's PATH is the sequence of (price, depth landed at) its moves would have
if it alone were clocked, read off the ladder: an opening pays kappa(d, 1)
and lands at 1; an item of a covered degree enters at door 2 and lands
at 2; an opened item, at depth 1 = x_1, pays kappa(d, 1) again and lands
at 2; from one past a member x_j (the ladder's members are x_1 = 1, x_2,
... in order) it pays kappa(d, x_(j+1) - x_j), x_(j+1) the next member, and
lands at x_(j+1) + 1. A degree d is not born and not yet opened: its
first item's path starts with the opening and its other items' with the
entry at door 2; a born degree's items all start with the entry. THE
CENSUS at a bar rho: a degree opens iff kappa(d, 1) < rho, its other
items enter iff kappa(d, 2) < rho, and every entered item rests at the
depth landed at before the first price on its path at or above rho. A
STRAND is an entered item other than the runaway resting above depth 1.
THE ARGUMENT (written before the engine).
(1) H IS kappa(1, sup), PER-ITEM. Let sup >= 2. A degree-1 item pends its
next path price at every step, and every price on its path is at
most kappa(1, sup): the entry door is 2 and each gap at most the sup.
Greed pays the least price on the menu, so every price paid is at
most kappa(1, sup). The runaway X pays kappa(d_X, max(r0, sup)) >=
kappa(1, sup) (stop.py). So H = kappa(1, sup), with no walk read.
(2) THE FIRST STEP PAYING H. There every move on the menu costs at
least H (the lemma) and a degree-1 item pends at most H, so it
pends exactly H; the tie goes to the lower degree, so a degree-1
item pays it, at its crossing, the one gap of a headed ladder equal
to the sup. After it that item pays kappa(1, tail) < H forever, and
every other item's pending price stands at or above H: under a
per-item clock an item's pending price changes only when it moves,
or rises once from kappa(d, 1) to kappa(d, 2) when its degree is covered.
So nothing but the runaway moves again.
[Ruled after the run (F1): the first step paying H is the crossing
only with the sup above the entry door 2; at sup = 2, Z_2, a
second degree-1 item pays H at its entry first.]
(3) THE CENSUS. Before that step every price paid is below H, and at
it every item pends at or above H, so every item has paid every
price of its path before its first price at or above H and none
after. That is the census at H = kappa(1, sup): the resting place of
every item is a function of the ladder, the price and the supply.
Each strand rests one past a ladder member at or below the bend,
since its path stops at a price at or above kappa(1, sup) and the
crossing gap is the sup: the old RUNG LAW (rest at p^j + 1) is a
corollary.
(4) THE CLOSED FORM AT (2, 4). The ladder (p, e, w) =
(2, 4, w), w free, is 1, 2, 4, 4 + 4 + w, then gap 4: gaps 1, 2, 4 + w,
4, 4, ... At kappa = d r, H = 4 + w. A degree-1 item enters at
2 and pays 1, 2 (rest 5 if not the runaway). A degree d >= 2
opens iff d < H and pays d, d, d, 2d:
rest 5 if 2d < H, else 3. Its second item enters iff 2d < H and
rests at 5. So the strands number 1 + (w + 2) + #{d >= 2 : 2d < 4
+ w} = w + 3 + ceil(w/2): 5, 6, 8, 9, 12, 15, 21, 27, 39 at w = 1,
2, 3, 4, 6, 8, 12, 16, 24, the series recorded by walking, and
every strand rests at 3 or 5.
(5) A COARSER CLOCK CAN RAISE H. Under dial.py's block clock a single holder
pays its own path (dial.py (3)), so on a branch where every block has one
holder and H = kappa(1, sup) each holder rests where the census puts it,
and every other item has at most opened: the branch seats nothing beyond
the census. But the global clock's floor can be exceeded (stop.py).
HAND-RUN, global clock, kappa = d r, the ladder (2, 2, 3) = 1, 2, 7, 9,
11, ...: open degree 2 at the void tie kappa(2, 1) = 2 = kappa(1, 2),
clock it at door 1 (price 2) to 2, notch 2, again at door 1 (price 2) to
3, notch 7. Now it bids kappa(2, 5) = 10, a degree-1 entry
kappa(1, 8) = 8, and the openings of degrees 3 to 7 are cheaper and made.
A degree-1 item takes the clock at 8 and runs away. H = 8 against the
census's kappa(1, 5) = 5, and degrees 5, 6 and 7 are open, which the
per-item census never opens. The old containment is a theorem on
single-holder branches at H = kappa(1, sup) and false off them.
[Ruled after the run (F3): a theorem there only with no TIE and
sup > 2; a move at price H at a degree above 1 can seat beyond.]
PREDICTIONS, frozen before the engine, each naming what the run PRINTS.
Ladders: stop.py's headed place ladders (2,1,1), (2,2,1), (2,2,2),
(2,2,3), (3,2,1), (2,4,2), (5,4,1), (2,8,4); prices d r, d^2 r, d + r.
PR1 PER-ITEM. Printed per cell: branches (ties followed over the
first moves, then walked clock-first), H against kappa(1, sup), the
branches where a move at price H went to a degree above 1 (TIE),
and the non-TIE branches whose final seating, the runaway removed,
differs from the census at H = kappa(1, sup). KILL: one such branch,
or H off kappa(1, sup) on a non-TIE branch.
PR2 THE CLOSED FORM. Printed at (2, 4, w), w = 1, 2, 3, 4, 6, 8, 12,
16, 24, kappa = d r: the census's strand count, its rest depths, w + 3
+ ceil(w/2), and the canonical per-item walk's strand count. KILL:
any of the three counts apart, or a rest depth other than 3 and 5.
PR3 COARSER CLOCKS. Partitions ONE, SLOT, MOD2, MOD3 over the same
cells, branches as PR1 [ruled: ties followed over 7 moves, where
PR1's code follows 9, then lowest-first]. Printed per partition:
branches, those single-holder with H = kappa(1, sup), and among
them the branches seating an item beyond the census (an item
seated the census leaves unseated, or resting deeper than the
census rest). KILL: one. Printed without a prediction: the other
branches, how many carry H above kappa(1, sup), and how many seat
beyond the census.
PR4 THE EXCESS WITNESS. The hand-run at (2, 2, 3), global clock, d r,
two moves forced. Printed: H, the runaway's degree, the degrees
opened that the census leaves shut. KILL: H = 5, or no such degree.
CONTROLS, run first: the census reproduces stop.py's canonical per-item
walk at the exact width series' first cell by hand (A(1): strands 5, at
depths 3 and 5, read off (4)); the census comparator fires on a walk
state with one item planted a rung deeper and on one with an extra
opening; the TIE detector fires on a planted log paying H at degree 2.
S0 sets the census against the hand count A(1); the
walk meets it in S2.
FINDINGS (entered after the run, from its printed output).
F0 CONTROLS. The census at (2, 4, 1), d r, H 5 reads 5 strands at
depths 3 and 5, as the hand count; the comparator fires on a planted
deeper item and on a planted extra opening; the TIE detector fires.
F1 PER-ITEM (PR1 KILLED as frozen, at one ladder). 58 branches, 24 of
them TIE. Every non-TIE branch has H = kappa(1, sup), and every one sits
on the census except at (2, 1, 1), off at all three prices, one
branch each. There the sup is 2, the entry door itself: a second
degree-1 item pays H at its entry before the first crosses, so
whether it is seated is a tie among degree-1 items, and step (2)'s
"the first step paying H is the crossing" needs the sup above the
entry door. The ladder (2, 1, 1) is the one place with e + w = 2,
Z_2. With sup > 2 the census holds on every non-TIE branch. All 24
TIE branches seat beyond the census (printed at the audit, the
deepest item taken as the runaway).
F2 THE CLOSED FORM (PR2 hit). At all nine widths the census, w + 3 +
ceil(w/2) and the walk agree: 5, 6, 8, 9, 12, 15, 21, 27, 39, every
strand at depth 3 or 5.
F3 COARSER CLOCKS (PR3 KILLED as frozen). Of the single-holder branches
at H = kappa(1, sup), 204, 206, 206 and 158 under ONE, SLOT, MOD2 and
MOD3 seat beyond the census. Read after the kill: each is a TIE
branch, a move at price exactly H made at a degree above 1, or sits
at (2, 1, 1), since the rest print zero beyond.
The slate conditioned PR1 on the tie and forgot to condition PR3 on
it. With no TIE and sup > 2, 218, 176, 176 and 156 branches, none
beyond. Printed without a prediction: under ONE, 578 of 1006
branches are not single-holder at kappa(1, sup), all 578 with H above
it and 576 of them seating beyond the census; under SLOT, MOD2 and
MOD3 every branch is single-holder at kappa(1, sup).
F4 THE EXCESS WITNESS (PR4 hit). H 8 against kappa(1, sup) = 5, runaway
degree 1, degrees 5, 6 and 7 opened that the census leaves shut.
RUN RECORD. One process, CPython, no numpy: 67 checks, 2.9 s, peak
commit 16.9 MB under a memory guard; the two frozen kills are held to
their recorded counts.
"""
import os
import sys
import time
from collections import Counter
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import limit as L # noqa: E402
import stop as SP # noqa: E402
import dial as D # noqa: E402
CHECKS = [0]
def check(cond, msg):
CHECKS[0] += 1
if not cond:
raise SystemExit("FAIL: " + msg)
# ---------------------------------------------------------------------------
# the census, read off the ladder, the price and the supply
def path(lad, price, d, opener):
"""(price, depth landed at) of an item's moves were it alone clocked."""
out = [(price(d, 1, True), 1)] if opener else [(price(d, 2, True), 2)]
a = out[0][1]
for _ in range(60):
t = lad.next(a)
out.append((price(d, t + 1 - a, False), t + 1))
a = t + 1
return out
def rest(pth, H):
"""The landing before the first price at or above H; 0 if none paid."""
a = 0
for p, land in pth:
if p >= H:
return a
a = land
raise SystemExit("FAIL: a path never reaching H")
def census(lad, price, sup, H, born=(1,)):
"""(degree, rest, entry door) -> count, every entered item."""
out = Counter()
for d, n in sup.items():
if not n:
continue
if d not in born and price(d, 1, True) >= H:
continue
roles = [False] * n if d in born else [True] + [False] * (n - 1)
for opener in roles:
a = rest(path(lad, price, d, opener), H)
if a:
out[(d, a, 1 if opener else 2)] += 1
return out
def strands(cen):
"""Entered items resting above depth 1, less the one runaway."""
return sum(n for (d, a, r0), n in cen.items() if a > 1) - 1
def fits(walk, cen):
"""Items a walk seats beyond the census: per (degree, role), the
walk's exponents against the census rests, both sorted down."""
def group(items):
g = {}
for (d, a, r0), n in items:
g.setdefault((d, r0 == 1), []).extend([a] * n)
return {k: sorted(v, reverse=True) for k, v in g.items()}
gw, gc = group(walk), group(cen.items())
bad = 0
for k, ws in gw.items():
cs = gc.get(k, [])
bad += max(0, len(ws) - len(cs))
bad += sum(w > c for w, c in zip(ws, cs))
return bad
def is_tie(log, H):
"""A move at price H made at a degree above 1 (a stop.py log)."""
return any(p == H and t[1] > 1 for t, r, p, *_ in log)
HEADED = [(2, 1, 1), (2, 2, 1), (2, 2, 2), (2, 2, 3), (3, 2, 1), (2, 4, 2),
(5, 4, 1), (2, 8, 4)]
PRICES = SP.PRICES
SUP = L.wide(2, 400)
K, KB, N = 9, 7, 240
PR3_KILLED = {"ONE": 204, "SLOT": 206, "MOD2": 206, "MOD3": 158}
def lad_of(pew):
return SP.place_ladder(*pew)
# ---------------------------------------------------------------------------
# the sections
def section_control():
print("S0 CONTROLS")
lad = lad_of((2, 4, 1))
price = L.price_power(1)
cen = census(lad, price, SUP, 5)
depths = {a for (d, a, r0) in cen if a > 1}
check(strands(cen) == 5 and depths == {3, 5}, "the hand census A(1)")
print(f" (2,4,1) d r at H 5: {strands(cen)} strands at depths "
f"{sorted(depths)}, as the hand count")
items = list(cen.items())
print(f" the comparator on the census itself: {fits(items, cen)} "
f"(zero by construction)")
(d, a, r0), n = next(x for x in items if x[0][1] == 3)
deeper = [x for x in items if x[0] != (d, a, r0)] + [((d, 5, r0), 1)]
if n > 1:
deeper.append(((d, a, r0), n - 1))
extra = items + [((40, 1, 1), 1)]
f1, f2 = fits(deeper, cen), fits(extra, cen)
check(f1 > 0 and f2 > 0, "the comparator did not fire")
print(f" the comparator fires on an item planted a rung deeper ({f1}) "
f"and on an extra opening ({f2})")
planted = [(("o", 2, 0, 1), 1, 5, (2, 1, 1), False)]
check(is_tie(planted, 5) and not is_tie(planted, 4),
"the TIE detector did not fire")
print(" the TIE detector fires on a planted move at price H, degree 2")
def section_per_item():
"""PR1."""
print(f"S1 PER-ITEM (PR1): ties followed over {K} moves, {N} more "
f"clock-first; census at H = kappa(1, sup)")
print(" price ladder sup kappa(1,sup) branches H off TIE off")
tot = Counter()
for pname, price in PRICES:
for pew in HEADED:
lad = lad_of(pew)
s, tl = SP.sup_tail(lad)
check(s > tl, f"headed {pew}")
S = L.Sched(lad.name, lad, price)
H0 = price(1, s, False)
cen = census(lad, price, SUP, H0)
# the runaway's census entry; none when its entry is its
# crossing, the entry door being the sup
run1 = max((k for k in cen if k[0] == 1), key=lambda k: k[1],
default=None)
want = cen - Counter({run1: 1}) if run1 else cen
row = Counter()
for st, log in SP.branches(S, SUP, False, K, N):
row["n"] += 1
H = max(x[2] for x in log)
if is_tie(log, H):
row["tie"] += 1
# beyond the census, the deepest item taken as the
# runaway (added at the audit)
top = max(st.seat, key=lambda k: k[1])
rest_ = st.seat - Counter({top: 1})
row["tie_beyond"] += fits(rest_.items(), want) > 0
continue
row["Hoff"] += H != H0
top = max((k for k in st.seat if k[0] == 1),
key=lambda k: k[1])
got = st.seat - Counter({top: 1})
row["off"] += got != want
# the frozen kill is printed, not raised, where the entry door
# 2 reaches the sup: step (2) of the argument missed that case
if s > 2:
check(row["Hoff"] == 0 and row["off"] == 0,
f"per-item census at {pname} {pew}")
elif row["Hoff"] or row["off"]:
tot["killed"] += 1
tot += row
print(f" {pname:6s} {lad.name:9s} {s:3d} {H0:13d} {row['n']:9d} "
f"{row['Hoff']:6d} {row['tie']:4d} {row['off']:4d}")
print(f" totals: {tot['n']} branches, {tot['tie']} TIE, off the "
f"census {tot['off']}, H off {tot['Hoff']}; cells off with the "
f"sup at the entry door 2: {tot['killed']}; TIE branches "
f"seating beyond the census {tot['tie_beyond']}")
print(f" PR1 KILLED as frozen, at the sup 2 only: {tot['killed']} cells")
check(tot["killed"] == 3, "PR1's frozen kill as recorded: (2, 1, 1) at "
"each of the three prices")
def section_closed():
"""PR2."""
print("S2 THE CLOSED FORM (PR2): (2,4,w), d r, per-item")
price = L.price_power(1)
for w in (1, 2, 3, 4, 6, 8, 12, 16, 24):
lad = lad_of((2, 4, w))
H = price(1, 4 + w, False)
cen = census(lad, price, SUP, H)
depths = sorted({a for (d, a, r0) in cen if a > 1})
form = w + 3 + (w + 1) // 2
S = L.Sched(lad.name, lad, price)
st, log = SP.run(S, SUP, False, 400)
walked = sum(n for (d, a, r0), n in st.seat.items() if a > 1) - 1
check(strands(cen) == form == walked and depths == [3, 5],
f"the closed form at w = {w}")
print(f" w {w:2d}: census {strands(cen):2d}, w + 3 + ceil(w/2) "
f"{form:2d}, walk {walked:2d}, depths {depths}")
def section_coarse():
"""PR3."""
print(f"S3 COARSER CLOCKS (PR3): ties followed over {KB} moves, {N} "
f"more lowest-first")
print(" part branches | 1-holder at kappa(1,sup) beyond | other "
"H above beyond")
for part in ("ONE", "SLOT", "MOD2", "MOD3"):
row = Counter()
for pname, price in PRICES:
for pew in HEADED:
lad = lad_of(pew)
s, _ = SP.sup_tail(lad)
H0 = price(1, s, False)
cen = census(lad, price, SUP, H0)
C = D.Cell(lad.name, price, D.PARTS[part], D.common(lad))
for st, log in D.branches(C, SUP, KB, N):
row["n"] += 1
H = max(x[3] for x in log)
hs, _ = D.holders(log)
single = all(len(set(v)) == 1 for v in hs.values())
lt = D.late(log, 0.25)
runners = {it for b in lt for it in lt[b]}
walk = Counter()
for it, (a, r0) in st.seat.items():
if it not in runners:
walk[(it[0], a, r0)] += 1
bad = fits(walk.items(), cen)
if single and H == H0:
row["pred"] += 1
row["pred_bad"] += bool(bad)
# read after the frozen kill: the tie at H
tie = any(x[3] == H and x[1] > 1 for x in log)
clean = not tie and s > 2
row["clean"] += clean
row["clean_bad"] += clean and bool(bad)
else:
row["other"] += 1
row["above"] += H > H0
row["other_bad"] += bool(bad)
check(row["clean_bad"] == 0, f"single-holder containment, {part}")
print(f" PR3 KILLED as frozen under {part}: {row['pred_bad']} "
f"single-holder branches beyond")
check(row["pred_bad"] == PR3_KILLED[part],
f"PR3's frozen kill as recorded, {part}")
print(f" {part:5s} {row['n']:9d} | {row['pred']:20d} "
f"{row['pred_bad']:7d} | {row['other']:5d} {row['above']:8d} "
f"{row['other_bad']:7d}")
print(f" of the single-holder branches, no TIE and sup > 2: "
f"{row['clean']}, beyond {row['clean_bad']}")
def section_excess():
"""PR4."""
print("S4 THE EXCESS WITNESS (PR4): (2,2,3), global clock, d r, open "
"degree 2 and clock it, then clock-first")
lad = lad_of((2, 2, 3))
price = L.price_power(1)
S = L.Sched(lad.name, lad, price)
st, log = SP.run(S, SUP, True, N, first=[("o", 2, 0, 1),
("c", 2, 1, 1)])
H = max(x[2] for x in log)
s, _ = SP.sup_tail(lad)
H0 = price(1, s, False)
(dX, _), = SP.late(log)
shut = sorted(d for d in st.opens if st.opens[d]
and d not in S.born and price(d, 1, True) >= H0)
check(H != H0 and shut, "the excess witness")
print(f" H {H} against kappa(1, sup) {H0}; runaway degree {dX}; degrees "
f"opened the census leaves shut: {shut}")
def main():
t0 = time.time()
section_control()
section_per_item()
section_closed()
section_coarse()
section_excess()
print(f"ALL CHECKS PASS: {CHECKS[0]} checks, {time.time() - t0:.1f} s")
if __name__ == "__main__":
main()