dial.py
Checks: CLOCK: A block clock keeps at most one runaway per block theorem; CLOCK: Two blocks of a number ring never both run away theorem.
Cited on: CLOCK.
To run it: save dial.py, with limit.py, stop.py beside it; standard library only.
"""dial.py -- the block clock: how many runaways a greedy walk keeps when
items share a notch in blocks, and what decides which blocks run.
QUESTION. A number ring's places over one rational prime read the state
through one p-adic valuation, so they share a notch; places over different
primes do not. That is a BLOCK clock, strictly between the family's two
ends: the GLOBAL clock (one block) and the PER-ITEM clock (every item its
own block). Measured before: at a constant gap one item runs away however
the items are cut into blocks, at a growing ladder one item per block. Is
that stop.py's per-item theorem with the block as the item, and the
chain of limit.py read inside each block? And is "one runaway at a flat
cost" a law, or a tie-break's?
THE SCHEDULE is limit.py's with the notch made per block. An item is (d,
slot), of degree d; a partition names its BLOCK b(d, slot), and a ladder
function names its LADDER. Block b carries a notch T_b, starting at 1. A
CLOCK move on an item of block b at exponent a has door T_b + 1 - a,
lands at T_b + 1, and moves T_b to next(T_b + 1) along the MOVER's own
ladder; an unseated item of a covered degree enters by a clock move from
a = 0. An OPENING has door 1, lands at 1, and moves no notch. The degree's
covering is global (born {1}, nu = 1). One block is limit.py's global
clock; singleton blocks are stop.py's per-item clock. The HOLDER of a
clock move is the item it moves; an item's ENTRY DOOR r0 is the door of
its first move; the HIGH-WATER PRICE H is the largest price a walk pays.
A block is SINGLE-HOLDER when one item makes all its clock moves. Its
CROSSING PRICE is H_b = kappa(d, max(r0, sup)), d and r0 its holder's and
sup its holder's ladder's largest gap: the dearest price on the holder's
path, paid where the path crosses the head.
THE ARGUMENT (written before the engine).
(1) THE CHAIN, PER BLOCK. limit.py's proof reads only the one notch the
two holders share and the exponents under it. Take a clock move of
Y in block b whose block's previous clock move had holder Z != Y. Z
landed at t + 1 above the notch t it met, the notch went to
next(t + 1), and since only openings and other blocks' moves came
between -- neither touches T_b or raises an exponent of b above 1 --
Y's door is at least next(t + 1) + 1 - max(1, t), one more than Z's
next(t + 1) - t. Z was on the menu, so with kappa(d', r') > kappa(d, r)
whenever d' >= d and r' > r, d_Y < d_Z. The ladders need not agree:
the notch moved along Z's. So every change of holder inside a block
falls in degree, and a block clocked infinitely often has exactly
one runaway.
(2) A FROZEN BLOCK ONLY CHEAPENS. While b is not clocked, T_b and b's
exponents stand still; an opening in b adds an item at exponent 1,
door T_b, and a newly covered degree adds an entry at door T_b + 1.
So b's least pending price never rises while b is idle, and it is
finite once b has a seated item or a covered one.
(3) THE SINGLE HOLDER'S PATH (stop.py (2)). A single holder pays its
entry door and then its own ladder's consecutive gaps: its notch
stands at next(its landing), the landing one past a member. So its
pending price is at every step one its path pays, and every price
it pays is at most H_b.
(4) BOUNDED GAPS: THE CROSSING PRICE ADMITS, THE TAIL DECIDES. Let every
ladder's gaps be bounded and kappa(d, 1) tend to infinity. Some block is
clocked infinitely often (limit.py), its runaway's prices are
bounded, so H is finite and finitely many items ever move. Past the
last opening every block's pending price is fixed except the
blocks being clocked, and a runaway past its bend pays kappa(d, tail)
forever on a ladder whose gaps settle (on bounded gaps that never
settle it pays several prices forever). Let B be the largest price
paid infinitely often; greed pays the least price on the menu at
every step, so every idle block's pending price is at least B. If
every block is single-holder, (3) gives H = min_b H_b over the blocks
ever clocked: the runaway's path never prices above its H_b and is
always on the menu, and a block whose path must pass a dearer
price is left waiting at it. So a block whose TAIL is the cheapest
can be priced out by its HEAD: its crossing price above another
block's leaves it frozen at its bend. Two blocks run away only at
an exact tie of recurrent prices, and whether a tied block runs is
then the tie-break's.
(5) CLIMBING GAPS: EVERY BLOCK RUNS. Let the gaps be unbounded and kappa
unbounded in the door. A block clocked finitely often keeps a
pending price at most some P once it holds a seated item, by (2),
so every later price paid is at most P; a block clocked infinitely
often pays gaps without bound; and if no block were, infinitely
many openings would be paid at prices without bound. So every
block that ever holds a seated item is clocked infinitely often,
and by (1) holds exactly one runaway. Every opening is made
(stop.py), so every block with a supplied item runs: one runaway
per block.
(6) THE RING. A number ring's blocks are its rational primes and each place's
ladder steps by its finite e past the bend (clock.py), so its gaps are
bounded; but a ring's block ticks in counts and an opening can jump it,
which (4) does not model, so the ring rests on the lid (lid.py): a block
clocked forever becomes lidded, finitely many openings follow, and past
the last no count jumps. Its price is N(P)^r, so two blocks' recurrent
prices p^(fe) and q^(f'e') are powers of different primes, by unique
factorization, and never tie: a number ring keeps ONE runaway if the walk
locks and none otherwise (a walk that never locks clocks every block
finitely often, lid.py), and no tie-break is consulted across blocks
[ruled on audit (F7): proved between blocks only; within one prime the
chain is door.py's]. A function field's places all lie over p: one block,
the global clock, one runaway by (1). Two runaways at a climbing ladder
need two blocks with unbounded gaps, two characteristics each of equal
characteristic, which no domain has (F_2[t] x F_3[t] has them).
(7) THE WIDE PLACE. Two items of ONE degree in one block, on a gap-1
and a gap-h ladder, tie at their entry; by (1) whichever enters
first holds the block's clock forever, the other never passing
exponent 1. So "the narrow place is the runaway" at equal degree
is the tie-break at the entry, not a price: the wide item runs on
the branch where it enters first. At a real ring the two places
have different norms and no tie.
[Ruled since (F6): false; x^3 + 2x + 1 holds two places of norm 59
on gaps 1 and 2.]
HAND-ATTACK, at d r with two items per degree and the slot partition:
(a) gap 3 in block 0 against (2,2,3) = 1, 2, 4, 9, 11, ... in block
1. The block-0 rational item enters at door 2 and then pays 3
forever. The block-1 rational item pays 2, 1, 2 and then faces 5
at its bend: H_0 = 3 < H_1 = 5, so block 1 freezes there with its
tail price 2 cheaper than the runaway's 3. H = 3.
[Ruled after the run (F2): (2,2,3) is 1, 2, 7, 9, 11, ...; the item
pays 2, 1 and then faces 5.]
(b) gap 5 against (2,2,3): H_0 = 5 = H_1; both cross, the recurrent
prices 5 and 2 part, and block 1 runs. H = 5.
(c) gap 3 in both blocks: both rational items enter at 2 and bid 3.
Lowest exponent first, they leapfrog and both run; highest first,
the one ahead stays ahead and one runs.
(d) ring shape, one block, gap 1 and gap h for the two slots of every
degree: the rational slots tie at door 2 at notch 1. Wide first: it
lands at 2, the notch goes to 1 + h, it re-clocks at h and the
narrow item's entry costs h + 2. Narrow first: the notch stays at
2, it re-clocks at 1.
(e) the doubling ladder in a finite partition: a holder's price
doubles per clock and the price of the opening at the horizon
(the least uncovered supplied degree) grows about one per move,
so the last half of a walk sees each block
clocked about once; the doubling ladder is the marginal case of
PR5, the squares ladder the comfortable one.
PREDICTIONS, frozen before the engine, each naming what the run PRINTS.
Ladders: gap 1, 2, 3, 5; (p,e,w) ladders (2,1,1), (2,2,1), (2,2,3), (2,4,2),
(5,4,1), (2,8,4), (2,3,0) built by stop.py; doubling and squares for
the climbing side. Partitions: ONE, SLOT (b = slot), MOD2 ((d + slot)
mod 2), MOD3, ITEM. Prices d r, d^2 r, d + r. Two items per degree to
400, ties branched over the first 7 moves, each branch then walked
lowest-exponent-first (LOW) for 240 moves (480 at a climbing ladder).
PR1 THE LEMMA. Per cell: high-water lemma faults (stop.py's check).
KILL: one.
PR2 THE CHAIN PER BLOCK. Per cell: changes of holder inside a block,
and those not falling in degree. KILL: one not falling; or, at a
bounded ladder, a block with two items clocked in the last quarter.
PR3 BOUNDED. Per cell: branches; those whose last-quarter clock moves
pay more than one price, or leave an idle block's pending price
below it; single-holder branches, and those where H differs from
min H_b over clocked blocks or a last-quarter block has H_b != H.
KILL: any of these nonzero.
PR4 THE ADMISSION CELLS (a) and (b), printed: each block's holder, H_b,
tail price, last-quarter moves, and H. KILL: (a) block 1 clocked in
the last quarter or H != 3; (b) block 0 clocked there or H != 5.
PR5 CLIMBING. Per cell at doubling and squares over ONE, SLOT, MOD2,
MOD3: blocks holding a seated item, and those not clocked in the
last half. KILL: one not clocked, at squares; printed at doubling.
Per-item at a climbing ladder: items clocked in the last half,
printed without a prediction.
PR6 THE TIE (c) at gap 2, 3, 5 and at (2,2,3), SLOT: blocks clocked in
the last quarter, per branch, under LOW and under HIGH (highest
exponent first). KILL: a branch with one under LOW where both
rational items are seated, or with two under HIGH.
PR7 THE TWO CHARACTERISTICS, SLOT: doubling in block 0, tripling in
block 1. KILL: a branch whose last half clocks one block.
PR8 THE WIDE PLACE (d), h = 2, 3, 5 (printed as e): per branch, the
slot of the runaway. KILL: the wide slot the runaway on no
branch, or two items clocked in the last quarter on any branch.
CONTROLS, run first: ONE reproduces stop.py's global walk and ITEM its per-item
walk move for move at stop.py's ladders [ruled on audit: limit.py's seven]
(kind, degree, door, price); the chain checker fires on a planted log whose
holder change rises in degree; the equal-price checker fires on a planted last
quarter paying two prices.
FINDINGS (entered after the run, from its printed output).
F0 CONTROLS. ONE matches stop.py's global walk and ITEM its per-item
walk move for move at 7 ladders, 3360 moves; both planted checkers
fire.
F1 THE LEMMA, THE CHAIN, THE BOUNDED LAW (PR1, PR2, PR3 hit). 4096 branches
over 13 bounded ladders (the gaps 1, 2, 3, 5 and stop.py's nine place
ladders, (2,2,2) and (3,2,1) beside the slate's seven), 5 partitions and 3
prices: 0 lemma faults; 560 changes of holder inside a block, 0 not
falling; 0 blocks with two items clocked in the last quarter; 0 last
quarters paying two prices, 0 idle blocks pending below B; 3536
single-holder branches, 0 with H off min H_b or a late block's H_b off H.
911 branches keep more than one late block, all at gaps 2, 3, 5 and at
(2,3,0), where a rational item's crossing price is its recurrent price;
the exact ladder keeps one, its entry door 2 standing above its gap 1 as a
head does (F4).
F2 THE ADMISSION CELLS (PR4 KILLED at (a) and at (b), as frozen). The
hand-attack read one branch shape, degree 1 holding block 0 from the first
clock, and wrote (2,2,3) as 1, 2, 4, 9 where it is 1, 2, 7, 9
(doors 2, 1, 5, as stop.py prints). At gap 3 | (2,2,3), 9 of 25
branches read H 3 with block 0 running and block 1 frozen at its
bend, its tail price 2 below the runaway's 3, as predicted. On 4 a
degree-2 item takes block 0's clock first, its crossing price is 6,
and block 1 runs at H 5. On 12 that degree-2 item is a strand: the
rational item enters block 0 at door 5, ties block 1's crossing
price, pays it first, and recurs at 3 below block 1's pending 5, so
block 1, with the cheaper tail, never crosses. At gap 5 | (2,2,3),
44 of 56 branches run block 1 as (b) said and 12 run block 0, whose
rival there is a degree-2 holder at H_b 10. On every single-holder
branch of both cells H = min H_b, the clause the theorem claims;
the frozen PR4 is a claim about which block that is, and the branch
decides it.
F3 CLIMBING (PR5 hit). At doubling and squares under ONE, SLOT, MOD2
and MOD3, every block holding a seated item is clocked in the last
half of each walk (7 branched moves and 480 more), on all 207
branches, one item per block. Per
item: 1464 of 1488 and 1296 of 1512 seated items clocked in the last
half.
F4 THE TIE (PR6 hit at the gap ladders, KILLED at (2,2,3)). Under LOW
both blocks run on every branch seating both rational items, 22, 26
and 56 at gaps 2, 3, 5; under HIGH one runs on every branch. At
(2,2,3) one runs on all 16 branches under either rule: the first
rational item across the bend recurs at 2 and the other waits at 5
forever. READ AFTER THE RUN, and proved at any ladder: a runaway's
pending price is never more than the next price it pays (another
holder of its block can raise a waiting item's door, never lower
it), so when the later
of two runaways' last payments above B is made the other pends at
most B, which greed would pay first; so at most one runaway ever
pays above B. Checked on every branch of S1 and S4, counting a
late block whose crossing price exceeds B: 0 branches with two.
F5 TWO CHARACTERISTICS (PR7 hit). Doubling | tripling in two blocks
keeps both blocks clocked in the last half on all 20 branches; the
doubling ladder in one block keeps one on all 32.
F6 THE WIDE PLACE (PR8 hit). One block, gap 1 against gap h: the wide slot is
the runaway on 15, 18 and 40 of 25, 34 and 92 branches at h = 2, 3, 5, and
no branch clocks two items in the last quarter. Which slot runs is which
entered first. (door.py: the ring of x^3 + 2x + 1 holds two places of norm
59 on gaps 1 and 2, and a ring ticks in counts, where the wide place's
first tick leaves both pending 59^2; this reading is the depth engine's
and does not carry to that block.)
F7 THE RING, SETTLED ON AUDIT. Argument (6)'s "a number ring keeps ONE
runaway" is proved between blocks only: no two rational primes both
run away. One place over that prime is the chain, which needs the
ring's door to be this engine's T + 1 - a in one unit, the door
identity's step and not this file's.
RUN RECORD. One process, CPython, no numpy: 1282652 checks, 98.5 s,
peak commit 17.5 MB under a memory guard; the frozen kills PR4 and PR6
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
CHECKS = [0]
def check(cond, msg):
CHECKS[0] += 1
if not cond:
raise SystemExit("FAIL: " + msg)
# ---------------------------------------------------------------------------
# a cell: a price, a partition into blocks, and a ladder per item
class Cell:
def __init__(self, name, price, block, ladder):
self.name, self.price = name, price
self.block, self.ladder = block, ladder
self.S = L.Sched(name, None, price) # born {1}, nu 1
PARTS = {"ONE": lambda d, s: 0, "SLOT": lambda d, s: s,
"MOD2": lambda d, s: (d + s) % 2, "MOD3": lambda d, s: (d + s) % 3,
"ITEM": lambda d, s: (d, s)}
class St:
"""T: block -> notch; seat: item -> (exponent, entry door); last: block
-> the item its last clock move moved."""
__slots__ = ("T", "seat", "opens", "nseat", "last")
def __init__(self):
self.T, self.seat, self.last = {}, {}, {}
self.opens, self.nseat = Counter(), Counter()
def copy(self):
s = St()
s.T, s.seat, s.last = dict(self.T), dict(self.seat), dict(self.last)
s.opens, s.nseat = Counter(self.opens), Counter(self.nseat)
return s
def key(self):
return (tuple(sorted(self.T.items(), key=repr)),
tuple(sorted(self.seat.items())),
tuple(sorted(self.opens.items())),
tuple(sorted(self.last.items(), key=repr)))
def notch(C, st, it):
return st.T.get(C.block(*it), 1)
def moves(C, st, sup, b_only=None):
"""Every move on the menu, (price, type), a type (kind, d, a, r0, slot).
With b_only, the clock moves of that block alone, openings excluded."""
out = []
for (d, s), (a, r0) in st.seat.items():
if b_only is not None and C.block(d, s) != b_only:
continue
r = notch(C, st, (d, s)) + 1 - a
out.append((C.price(d, r, False), ("c", d, a, r0, s)))
for d in sup:
if b_only is None and out and C.price(d, 1, True) > min(out)[0]:
break
for s in range(sup[d]):
if (d, s) in st.seat:
continue
if b_only is not None and C.block(d, s) != b_only:
continue
if not L.covered(C.S, st, d):
if b_only is None:
out.append((C.price(d, 1, True), ("o", d, 0, 1, s)))
else:
r = notch(C, st, (d, s)) + 1
out.append((C.price(d, r, True), ("u", d, 0, r, s)))
return out
def menu(C, st, sup):
ms = moves(C, st, sup)
best = min(p for p, _ in ms)
return best, [t for p, t in ms if p == best]
def apply(C, st, t):
"""(state after, door paid, block moved or None, item)."""
kind, d, a, r0, s = t
n = st.copy()
it = (d, s)
if kind == "o":
n.seat[it] = (1, 1)
n.opens[d] += 1
n.nseat[d] += 1
return n, 1, None, it
b = C.block(d, s)
T = st.T.get(b, 1)
r = T + 1 - a
if kind == "u":
check(r == r0, "an unseated item's entry door")
n.nseat[d] += 1
n.seat[it] = (T + 1, r0 if kind == "c" else r)
n.T[b] = C.ladder(d, s).next(T + 1)
n.last[b] = it
return n, r, b, it
def canon_low(types):
return min(types, key=lambda t: (t[0] == "o", t[1], t[2], t[3], t[4]))
def canon_high(types):
return min(types, key=lambda t: (t[0] == "o", t[1], -t[2], t[3], t[4]))
def step(C, st, t, price, log):
s2, r, b, it = apply(C, st, t)
check(C.price(t[1], r, t[0] != "c") == price, "the menu's price")
prev = st.last.get(b) if b is not None else None
log.append((t[0], t[1], r, price, b, it, prev))
return s2
def run(C, sup, n, st=None, log=None, choose=canon_low):
st = st if st is not None else St()
log = [] if log is None else log
for _ in range(n):
best, types = menu(C, st, sup)
st = step(C, st, choose(types), best, log)
return st, log
def branches(C, sup, k, n, choose=canon_low, cap=6000):
front = {St().key(): (St(), [])}
for _ in range(k):
nxt = {}
for st, log in front.values():
best, types = menu(C, st, sup)
for t in types:
lg = list(log)
s2 = step(C, st, t, best, lg)
nxt.setdefault(s2.key(), (s2, lg))
front = nxt
check(len(front) <= cap, "the branch cap")
return [run(C, sup, n, st, list(log), choose) for st, log in
front.values()]
# ---------------------------------------------------------------------------
# readings
def chain_faults(log):
"""(changes of holder inside a block, those not falling in degree)."""
ch = bad = 0
for kind, d, r, p, b, it, prev in log:
if b is not None and prev is not None and prev != it:
ch += 1
bad += not d < prev[0]
return ch, bad
def late(log, frac):
"""block -> {item: [prices]} over the clock moves of the last part."""
out = {}
for kind, d, r, p, b, it, prev in log[int(len(log) * (1 - frac)):]:
if b is not None:
out.setdefault(b, {}).setdefault(it, []).append(p)
return out
def lemma_faults(C, st, sup, H):
bad = 0
for d in sup:
if not sup[d] or d in C.S.born:
continue
p1 = C.price(d, 1, True)
if p1 < H and not L.covered(C.S, st, d) and st.nseat[d] < sup[d]:
bad += 1
if p1 > H and st.opens[d]:
bad += 1
u = min(d for d in sup if sup[d] and not L.covered(C.S, st, d))
bad += C.price(u, 1, True) < H
return bad
def holders(log):
"""block -> list of distinct clock movers in order, with each one's
entry door (the door of its first clock move, or 1 if opened)."""
out, first = {}, {}
for kind, d, r, p, b, it, prev in log:
if kind == "o":
first.setdefault(it, 1)
if b is None:
continue
first.setdefault(it, r)
hs = out.setdefault(b, [])
if not hs or hs[-1] != it:
hs.append(it)
return out, first
def crossing(C, it, r0):
s, _ = SP.sup_tail(C.ladder(*it))
return C.price(it[0], max(r0, s), False)
def bounded_reading(C, st, log, sup):
"""The PR3 observables for one branch."""
H = max(x[3] for x in log)
lt = late(log, 0.25)
prices = {p for b in lt for ps in lt[b].values() for p in ps}
B = max(prices)
two_price = len(prices) > 1
idle_below = 0
for b in {C.block(*it) for it in st.seat}:
if b in lt:
continue
pend = [p for p, _ in moves(C, st, sup, b_only=b)]
idle_below += bool(pend) and min(pend) < B
hs, first = holders(log)
single = all(len(set(v)) == 1 for v in hs.values())
off = None
if single:
Hb = {b: crossing(C, v[0], first[v[0]]) for b, v in hs.items()}
off = (H != min(Hb.values())
or any(Hb[b] != H for b in lt))
two_late = sum(len(v) > 1 for v in lt.values())
headed = sum(crossing(C, hs[b][-1], first[hs[b][-1]]) > B for b in lt)
return dict(H=H, B=B, two_price=two_price, idle_below=idle_below,
single=single, off=off, two_late=two_late, late=lt, hs=hs,
first=first, headed=headed)
PRICES = SP.PRICES
SUP = L.wide(2, 400)
K, N, NC = 7, 240, 480
PR4_KILLED = {3: 16, 5: 12}
def bounded_ladders():
return SP.ladders()
def climbing_ladders():
return [L.ladder_b(2), L.Ladder("squares",
lambda t: (L.isqrt(t) + 1) ** 2, False)]
def common(lad):
return lambda d, s: lad
def by_slot(l0, l1):
return lambda d, s: l0 if s == 0 else l1
# ---------------------------------------------------------------------------
# the sections
def section_control():
print("S0 CONTROLS")
moves_read = 0
for lad in L.LADDERS:
S = L.Sched(lad.name, lad, L.price_power(1))
for part, glob in (("ONE", True), ("ITEM", False)):
_, ref = SP.run(S, SUP, glob, N)
C = Cell(lad.name, L.price_power(1), PARTS[part], common(lad))
_, mine = run(C, SUP, N)
check([(t[0], t[1], r, p) for t, r, p, *_ in ref]
== [x[:4] for x in mine],
f"{part} parts from stop.py at {lad.name}")
moves_read += len(ref)
print(f" ONE matches stop.py's global walk and ITEM its per-item walk "
f"move for move at {len(L.LADDERS)} ladders, {moves_read} moves")
planted = [("c", 1, 2, 2, 0, (1, 0), None),
("c", 2, 1, 2, 0, (2, 0), (1, 0))]
check(chain_faults(planted) == (1, 1), "the chain checker did not fire")
C = Cell("gap 3", L.price_power(1), PARTS["SLOT"],
common(L.ladder_gap(3)))
st, log = run(C, SUP, N)
check(not bounded_reading(C, st, log, SUP)["two_price"],
"a clean walk's last quarter")
log2 = list(log)
k, d, r, p, b, it, prev = log2[-1]
log2[-1] = (k, d, r, p + 1, b, it, prev)
check(bounded_reading(C, st, log2, SUP)["two_price"],
"the equal-price checker did not fire")
print(" the chain checker fires on a planted rising change; the "
"equal-price checker on a planted second price")
def section_bounded():
print(f"S1 BOUNDED (PR1-PR3): 2 items per degree to 400, born {{1}}, "
f"ties branched over {K} moves, {N} more LOW")
print(" price ladder part branches lemma chg/rise 2late | "
"2price idle<B single off >1 late block")
tot = Counter()
for pname, price in PRICES:
for lad in bounded_ladders():
for part in PARTS:
C = Cell(lad.name, price, PARTS[part], common(lad))
row = Counter()
for st, log in branches(C, SUP, K, N):
rd = bounded_reading(C, st, log, SUP)
row["br"] += 1
row["lemma"] += lemma_faults(C, st, SUP, rd["H"])
ch, bad = chain_faults(log)
row["chg"] += ch
row["rise"] += bad
row["2late"] += rd["two_late"]
row["2price"] += rd["two_price"]
row["idle"] += rd["idle_below"]
row["single"] += rd["single"]
row["off"] += bool(rd["off"])
row["multi"] += len(rd["late"]) > 1
row["headed"] += rd["headed"] > 1
tot += row
print(f" {pname:6s} {lad.name:9s} {part:5s} {row['br']:5d} "
f"{row['lemma']:5d} {row['chg']:4d}/{row['rise']:<3d} "
f"{row['2late']:4d} | {row['2price']:5d} "
f"{row['idle']:6d} {row['single']:6d} {row['off']:3d}"
f" {row['multi']:4d}")
print(f" totals: {tot['br']} branches; lemma faults {tot['lemma']}; "
f"{tot['chg']} changes of holder, {tot['rise']} not falling; "
f"{tot['2late']} blocks with two late items; {tot['2price']} "
f"two-price quarters, {tot['idle']} idle blocks below B; "
f"{tot['single']} single-holder, {tot['off']} off min H_b; "
f"{tot['multi']} branches with more than one late block, "
f"{tot['headed']} with two headed late blocks")
for key in ("lemma", "rise", "2late", "2price", "idle", "off",
"headed"):
check(tot[key] == 0, f"PR1-PR3: {key}")
def describe(C, st, log):
rd = bounded_reading(C, st, log, SUP)
parts = []
for b, hs in sorted(rd["hs"].items(), key=repr):
it = hs[-1]
s, tl = SP.sup_tail(C.ladder(*it))
Hb = crossing(C, it, rd["first"][it])
nl = sum(len(v) for v in rd["late"].get(b, {}).values())
parts.append(f"block {b}: holder {it} H_b {Hb} tail price "
f"{C.price(it[0], tl, False)} late moves {nl}")
return rd, parts
def section_admission():
"""PR4, killed as frozen: the census of every branch, with the clause
the theorem does claim -- H = min H_b on a single-holder branch --
checked on each."""
print("S2 THE ADMISSION CELLS (PR4): d r, SLOT, LOW, every branch")
psi = SP.place_ladder(2, 2, 3)
for c in (3, 5):
fired = 0
C = Cell(f"gap {c} | (2,2,3)", L.price_power(1), PARTS["SLOT"],
by_slot(L.ladder_gap(c), psi))
seen, shown = Counter(), {}
for st, log in branches(C, SUP, K, N):
rd, parts = describe(C, st, log)
if rd["single"]:
check(not rd["off"], f"H = min H_b at gap {c}")
fired += rd["H"] != c or (1 if c == 3 else 0) in rd["late"]
k = (rd["H"], tuple(sorted(rd["late"], key=repr)), rd["single"])
seen[k] += 1
shown.setdefault(k, parts)
print(f" gap {c} | (2,2,3): {sum(seen.values())} branches; PR4 "
f"KILLED as frozen on {fired}")
check(fired == PR4_KILLED[c], f"PR4's frozen kill as recorded, "
f"gap {c}")
for k, n in sorted(seen.items(), key=repr):
print(f" H {k[0]}, late blocks {list(k[1])}, single-holder "
f"{k[2]}: {n} branches")
for line in shown[k]:
print(" " + line)
def section_climbing():
print(f"S3 CLIMBING (PR5): d r, {NC} moves, blocks with a seated item "
f"and those not clocked in the last half")
total = 0
for lad in climbing_ladders():
for part in PARTS:
C = Cell(lad.name, L.price_power(1), PARTS[part], common(lad))
miss, blocks, br, per_late = 0, 0, 0, 0
for st, log in branches(C, SUP, K, NC):
br += 1
seated = {C.block(*it) for it in st.seat}
lt = late(log, 0.5)
blocks += len(seated)
if part == "ITEM":
per_late += len(lt)
continue
miss += len(seated - set(lt))
check(all(len(v) == 1 for v in lt.values()),
"two late items in a block, climbing")
if part == "ITEM":
print(f" {lad.name:8s} ITEM {br} branches, items clocked "
f"in the last half {per_late} of {blocks} seated")
continue
total += br
check(miss == 0, f"PR5 at {lad.name} {part}")
print(f" {lad.name:8s} {part:5s} {br} branches, blocks seated "
f"{blocks}, not clocked late {miss}")
print(f" {total} branches under the four coarser partitions")
def section_tie():
print("S4 THE TIE (PR6): SLOT, one ladder in both blocks, d r")
fired = 0
for lad in (L.ladder_gap(2), L.ladder_gap(3), L.ladder_gap(5),
SP.place_ladder(2, 2, 3)):
C = Cell(lad.name, L.price_power(1), PARTS["SLOT"], common(lad))
out = {}
for nm, ch in (("LOW", canon_low), ("HIGH", canon_high)):
cnt = Counter()
for st, log in branches(C, SUP, K, N, ch):
rd = bounded_reading(C, st, log, SUP)
nb = len(rd["late"])
both = (1, 0) in st.seat and (1, 1) in st.seat
cnt[(nb, both)] += 1
check(rd["headed"] <= 1, f"two headed runaways {lad.name}")
if nm == "LOW" and lad.bounded and lad.name.startswith("("):
fired += both and nb == 1
continue # PR6 killed here: the head breaks the tie
if nm == "LOW":
check(not (both and nb == 1), f"PR6 LOW at {lad.name}")
else:
check(nb == 1, f"PR6 HIGH at {lad.name}")
out[nm] = dict(cnt)
print(f" {lad.name:8s} (late blocks, both rational seated): "
f"LOW {out['LOW']} HIGH {out['HIGH']}")
print(f" PR6 KILLED as frozen at (2,2,3) under LOW on {fired} branches")
check(fired == 8, "PR6's frozen kill as recorded, (2,2,3) LOW")
def section_two_chars():
print("S5 TWO CHARACTERISTICS (PR7): SLOT, doubling | tripling, d r")
C = Cell("2 | 3", L.price_power(1), PARTS["SLOT"],
by_slot(L.ladder_b(2), L.ladder_b(3)))
cnt = Counter()
for st, log in branches(C, SUP, K, NC):
nb = len(late(log, 0.5))
check(nb == 2, "PR7: one block clocked late")
cnt[nb] += 1
print(f" late-half blocks per branch: {dict(cnt)}")
C = Cell("2", L.price_power(1), PARTS["ONE"], common(L.ladder_b(2)))
cnt = Counter(len(late(log, 0.5)) for _, log in branches(C, SUP, K, NC))
print(f" one block, doubling: late-half blocks per branch {dict(cnt)}")
def section_wide():
print("S6 THE WIDE PLACE (PR8): ONE block, slot 0 on gap 1, slot 1 on "
"gap e, d r")
for e in (2, 3, 5):
C = Cell(f"1 | {e}", L.price_power(1), PARTS["ONE"],
by_slot(L.ladder_gap(1), L.ladder_gap(e)))
cnt = Counter()
for st, log in branches(C, SUP, K, N):
(items,) = late(log, 0.25).values()
check(len(items) == 1, f"PR8 two late items at e = {e}")
(it,) = items
cnt[(it, max(x[3] for x in log))] += 1
check(any(it[1] == 1 for it, _ in cnt), f"PR8 wide never runs, {e}")
print(f" e = {e}: (runaway, H): branches {dict(cnt)}")
def main():
t0 = time.time()
section_control()
section_bounded()
section_admission()
section_climbing()
section_tie()
section_two_chars()
section_wide()
print(f"ALL CHECKS PASS: {CHECKS[0]} checks, {time.time() - t0:.1f} s")
if __name__ == "__main__":
main()