costs.py
Checks: LEARNER: Of the per-kind prices, only the rank's keeps one level criterion.
Cited on: LEARNER.
To run it: save costs.py, with learner.py, rationed.py beside it; standard library only.
"""costs.py -- which move costs keep the greedy spend-all readers of the
straddle cover on one level.
QUESTION. Give the cover's moves a cost other than the rank they gain:
which costs keep the four greedy spend-all readers on one level, a
grading g rising strictly under containment whose trace they share?
BY HAND.
(S) SUFFICIENT (repaired before any engine: an earlier (G'), the
cheapest step's cost a function of phi alone, is not enough; levels
0 -> 1 -> 2 -> 5 and 0 -> 3 -> 4 at costs 1, 1, 3 and 3, 1 meet it
and part at 4 units, 2 against 4). Let c(M -> M') = phi(M') -
phi(M) for an integer phi rising strictly under strict containment
among the members holding J, and (G) from every member above the
bottom let some legal move cost exactly 1 (a chain move truncated to
k + 1 counts), a chain move truncating to any index it can pay for. Then the common rank's
proof runs with phi for rank: every holder contains the bottom, so
phi(M) <= phi*(J) with equality only at the bottom; a route's cost
is the phi it gains; above the bottom, with a unit left, a move of
cost 1 is open, so every greedy spend-all reader stops at
min(phi*, phi_0 + units), whatever its route. phi = f(rank), f
strictly increasing, passes by its own argument: every holder of
rank r above the bottom has a legal +1-rank step costing f(r+1) - f(r), the same
ladder for all, so each stops at the largest rank <= rank* it can
pay for.
(F) THE PER-KIND FAMILY: tree move a, chain move e [k = 0] + b (k' -
k), integers a, b >= 1, e >= 0. It is a potential iff a = b and e = 0: chain
gives phi(T_i, k) = phi(T_i) + e + b k for k >= 1, tree from T_i
gives phi(T_i) = phi_0 + a i on a path, and tree from (T_i, k),
k >= 1, to T_(i+k+1) then needs (a - b) k = e for k = 1 and 2.
(W) THE WITNESS: a sketch of the straight run at the root, superseded
by THE GENERAL WITNESS below (cut after the run, a change to frozen
text; its K = 20 worked case and its walks did not survive), its
worked case run as C4.
PREDICTION. Under every cost of the family a, b in {1, 2}, e in {0, 1}
other than (1, 1, 0) and (2, 2, 0), on the nine rows at the 16
settings scaled to the cost (income B max(a, b), cap W max(a, b), B =
1..4, W = 0, 2, 4, 8), two of the four greedy spend-all readers commit
strictly nested members at some step.
KILL (frozen; repaired before any engine). Printed per cost: NESTED,
the (row, setting, step, pair) sites where two of the four commit
strictly nested members, and RANKDIFF, those where their ranks differ.
NESTED > 0 proves a break under every grading rising strictly under
containment. A route-dependent cost (a != b or e > 0) with NESTED = 0
and RANKDIFF = 0 at every row and setting keeps one level on the rows,
the rank, and kills "a route-dependent cost breaks it" there; NESTED =
0 with RANKDIFF > 0 is undecided, incomparable members at different
ranks: at a != b the witness (W) on its constructed image decides
whether the cost breaks the common level in general, not on the rows;
at a = b, e > 0 nothing decides it yet, and it is recorded undecided.
CONTROLS (read first, four). (1, 1, 0) reproduces rationed.py's rank and bank
traces at all 16 settings, NESTED = 0; (2, 2, 0) at income 2B and cap 2W gives
the same traces (the f(rank) argument, f = 2r: no move costs 1); a planted nesting, the refuser beside U, is counted by
the NESTED counter. (W)'s worked case: the constant image J = (0.951,
0.96), clear of every endpoint (k_0* = 19, T_m holds it for m <= 20, so
K = 19 and the window is spends 21 to 39, by hand, re-derived first) at
(2, 1, 0), setting (B, W) = (2, 0) scaled, income 4 a step, prints the
pair chain first at both and tree first at both nested at the steps
whose cumulative spend falls in the window, and nowhere outside it.
RE-DERIVED before the engine: the root's straddle S_k = (k/(k+1),
(k+1)/k) holds J iff k <= 19; T_m = ((m-1)/m, 1) holds it iff m <= 20,
and T_20's vertex 20/21 lies inside J, so I* = T_20 and r* = 20; no
straddle at T_m, m <= 20, holds J (its right end (m+1)/(m+2) < 0.96);
T_m lies inside S_k iff m >= k + 1. At income 4 and W = 0, tree first
at both sits at T_(2n+2) to step 9 (spend 4(n+1)); chain first at both
sits at S_(4n+4) to step 3, at S_19 at step 4 (a unit lost, the tree
move costing 2), at T_20 from step 5. So the pair is nested at steps 5
to 8 exactly (spends 24 to 36, inside 21 to 39) and incomparable
before. Tree first at tiles never enters a straddle here, so (0, 0)
and (0, 1) run one trace; U, truncated to S_4 at step 0, turns down to
T_6 at step 1 and walks T_(2n+4), nested against tree first at both
at steps 1 to 8 and against chain first at both at steps 5 to 7.
FINDINGS (copied from the run's print).
Controls: C1 46,800 runs, 0 off; C2 46,800 runs, 0 off; C3 1,074
sites at (2, 2), a plant caught by construction (the refuser's root
contains every member); C4 prints the walks as re-derived ((0, 0)
and (0, 1) T2 .. T20, (1, 0) S4 S8 S12 S16 S19 T20, (1, 1) S4 T6 ..
T20), the pair nested at steps 5 to 8, U at 1 to 8 and 5 to 7, and
the kill's own counter (pair_counts, added after the frozen run)
reads NESTED 27 and RANKDIFF 43 on those traces, counted by hand;
with "contains" dropped from it in a copy of the script it reads
NESTED 3 and fails.
Kill, NESTED / RANKDIFF: (1, 1, 0) 0 / 0 and (2, 2, 0) 0 / 0; (1, 1,
1) 13,724 / 13,773; (1, 2, 0) 15,065 / 15,154; (1, 2, 1) 12,584 /
12,676; (2, 1, 0) 19,552 / 19,829; (2, 1, 1) 15,830 / 16,129; (2, 2,
1) 12,729 / 12,845. Each route-dependent cost is nested at 27 to 39
of the 144 (setting, row) cells and at 14 to 16 of the 16 settings.
The prediction holds and no cost reads undecided. RANKDIFF exceeds
NESTED at every breaking cost: some pairs of different rank are
incomparable.
THE GENERAL WITNESS (derived by hand after the frozen run; its arm
frozen before its code). Let J_K = (x, y) with x = (2K+1)/(2K+3) and
y = (K+2)/(K+3), K >= 1. Then K/(K+1) < x < (K+1)/(K+2) < y < 1, so
the root's S_k holds J_K iff k <= K, T_m = ((m-1)/m, 1) iff m <= K + 1,
T_(K+1)'s vertex (K+1)/(K+2) lies inside J_K (I* = T_(K+1), r* = K +
1), and no straddle at T_m, m <= K + 1, holds it: S_1(T_m) has right
end (m+1)/(m+2) <= y, and at m = K + 1 left end (2K+1)/(2K+3) = x. A
tree move from T_m goes to T_(m+1), a chain at the root enters S_k,
k <= K, and a tree move from S_k goes to T_(k+1); an unaffordable
preferred move yields to the other kind, so each case below reads its
walk off its budget. One step from the root, income I:
b < a: K = floor(e/(a-b)) + 1, so K(a - b) > e; I = e + K b + a <
(K + 1) a. Chain first at both: S_K, then T_(K+1), the
bottom. Tree first at both: T_floor(I/a), floor(I/a) <= K,
strictly containing T_(K+1).
b > a: K = a, I = e + K b. Chain first at both: S_K, nothing left.
Tree first at both: I >= (K + 1) a as K(b - a) >= a, so it
stops at the bottom T_(K+1), strictly inside S_K.
a = b, e > 0: c = ceil(e/a), m = c + 1, K = m, I = m a. Chain first
at both: S_1 (m a - e >= a, and m a - e - a = c a - e < a, so
no second unit of chain and no tree). Tree first at both:
T_m, m >= 2, strictly inside S_1.
So at every cost of the family with a != b or e > 0, at one income and
any cap, chain first at both and tree first at both commit strictly
nested members at step 0, and no grading rising strictly under
containment carries the four on one level. With (S) at a = b, e = 0:
the four greedy spend-all readers (patiences 0, delta = INF) share one
level at every income, cap and stream iff the cost is the rank scaled,
a = b and e = 0, a criterion over the family.
ARM (frozen before its code): for a, b in 1..6 and e in 0..6, every
route-dependent cost (246), the run at step 0 prints the two members
named above, strictly nested; CONTROL: at the 6 costs a = b, e = 0, on
J_K for K = 1..6 at every income 1 .. 3(K+1)a, the four are never
nested. PRINTED: 246 costs, 0 off; the control 1,701 (a, K, I), 0
nested.
RUN RECORD. 7 checks, 78.5 s, peak commit 7.8 MB; C1 and C2 take most
of it; 8 once the counter's control was added, the kill's print
unchanged; moved beside its citation, 8 checks, 78.9 s, peak 7.7 MB.
Exact integers throughout. No prediction was changed; the general
witness and its arm came after the frozen run, by hand first.
THE ENGINE: rationed.py::run_rationed with three
changes: a move is legal only if affordable (the tree move only at rem
>= a); the chain truncates to k + floor((rem - e [k = 0]) / b), capped
at the largest index holding the reference; rem falls by the move's
cost. The reader moves in its preferred order among legal affordable
moves, so an unaffordable preferred move yields to the other kind,
until none is left.
"""
import sys
from learner import INF, ROOT, add, le, span, holds, index_max
from rationed import (ROWS9, N_MAIN, INCOMES, CAPS, images9, run_rationed,
rank, relation, space5)
COSTS = [(a, b, e) for a in (1, 2) for b in (1, 2) for e in (0, 1)]
SIGMAS = ((0, 0), (0, 1), (1, 0), (1, 1))
QUARTET = [sg + (0, 0, INF) for sg in SIGMAS]
U = (1, 1, 0, 0, INF)
REFUSER = (0, 0, INF, INF, INF)
CHAIN_BOTH, TREE_BOTH = (1, 0), (0, 1)
J_W = ((951, 1000), (96, 100))
CHECKS = []
def check(name, ok, detail=""):
CHECKS.append(bool(ok))
print(f" {'PASS' if ok else 'FAIL'} {name}" +
(f" ({detail})" if detail else ""))
def run_costed(Js, pol, B, W, cost):
"""run_rationed with a tree move costing a and a chain move from k
to k' costing e [k = 0] + b (k' - k); a move is legal only if
affordable, the chain truncated to what is left."""
a, b, e = cost
s_tile, s_str, pt, pc, dl = pol
C = ROOT
bank = 0
out, banks = [], []
for n, J in enumerate(Js):
rt = Js[n - pt] if pt is not INF and n - pt >= 0 else None
rc = Js[n - pc] if pc is not INF and n - pc >= 0 else None
avail = B + bank
spend = avail if dl is INF else min(avail, B + dl)
rem = spend
while rem > 0:
l, r, k, d = C
v = add(l, r)
lo, hi = span(C)
tree = chain = None
if rt is not None and rem >= a:
for ch in ((lo, v, 0, d + k + 1), (v, hi, 0, d + k + 1)):
if holds(ch, rt):
tree = ch
break
entry = e if k == 0 else 0
if rc is not None and rem - entry >= b:
k2 = min(index_max(l, r, rc), k + (rem - entry) // b)
if k2 > k:
chain = (l, r, k2, d)
if tree is None and chain is None:
break
prefer_chain = (s_tile == 1) if k == 0 else (s_str == 0)
if chain is not None and (tree is None or prefer_chain):
rem -= entry + b * (chain[2] - k)
C = chain
else:
rem -= a
C = tree
bank = min(W, avail - (spend - rem))
if not (le(span(C)[0], J[0]) and le(J[1], span(C)[1])):
raise AssertionError("a commitment lost the image")
out.append(C)
banks.append(bank)
return out, banks
def nested_steps(t1, t2):
return [n for n in range(len(t1))
if relation(t1[n], t2[n]) in ("inside", "contains")]
def pair_counts(trs):
"""The kill's counter over a list of traces: NESTED and RANKDIFF
pair-steps, and the first nested site (step, i, j)."""
nested = rankdiff = 0
first = None
for n in range(len(trs[0])):
for i in range(len(trs)):
for j in range(i + 1, len(trs)):
x, y = trs[i][n], trs[j][n]
if relation(x, y) in ("inside", "contains"):
nested += 1
if first is None:
first = (n, i, j)
if rank(x) != rank(y):
rankdiff += 1
return nested, rankdiff, first
def settings(cost):
m = max(cost[0], cost[1])
return [(B * m, W * m) for B in INCOMES for W in CAPS]
def controls(imgs):
print("C CONTROLS (read first)")
# C1: the unit cost is rationed.py's reader, every policy, every setting
off = runs = 0
for B in INCOMES:
for W in CAPS:
for row in ROWS9:
for p in space5(W):
runs += 1
off += (run_costed(imgs[row], p, B, W, (1, 1, 0)) !=
run_rationed(imgs[row], p, B, W))
check("C1 (1, 1, 0) reproduces rationed.py's traces and banks",
off == 0, f"{runs} runs, {off} off")
# C2: (2, 2, 0) at doubled budgets and drawdowns, the same members
off = runs = 0
for B in INCOMES:
for W in CAPS:
for row in ROWS9:
for p in space5(W):
p2 = p[:4] + ((INF if p[4] is INF else 2 * p[4]),)
t1, b1 = run_costed(imgs[row], p, B, W, (1, 1, 0))
t2, b2 = run_costed(imgs[row], p2, 2 * B, 2 * W,
(2, 2, 0))
runs += 1
off += t1 != t2 or b2 != [2 * x for x in b1]
check("C2 (2, 2, 0) at 2B, 2W, 2 delta: same members, banks doubled",
off == 0, f"{runs} runs, {off} off")
# C3: a planted nesting, the refuser beside U, through the counter
sites = 0
for row in ROWS9:
tu, _ = run_costed(imgs[row], U, 2, 2, (1, 1, 0))
tr, _ = run_costed(imgs[row], REFUSER, 2, 2, (1, 1, 0))
sites += len(nested_steps(tu, tr))
check("C3 the refuser beside U is counted nested", sites > 0,
f"{sites} sites at (2, 2)")
# C4: (W)'s worked case, constant image, (2, 1, 0) at (B, W) = (4, 0)
Js = [J_W] * 12
tr = {sg: run_costed(Js, sg + (0, 0, INF), 4, 0, (2, 1, 0))[0]
for sg in SIGMAS}
for sg in SIGMAS:
print(f" {sg}: " + " ".join(
f"{'T' if c[2] == 0 else 'S'}{rank(c) if c[2] == 0 else c[2]}"
for c in tr[sg]))
pairs = {}
for i in range(4):
for j in range(i + 1, 4):
s, t = SIGMAS[i], SIGMAS[j]
pairs[(s, t)] = nested_steps(tr[s], tr[t])
print(f" nested {s} {t}: steps {pairs[(s, t)]}")
check("C4 (W): chain first at both against tree first at both, "
"nested at steps 5 to 8 exactly",
pairs[(TREE_BOTH, CHAIN_BOTH)] == [5, 6, 7, 8])
check("C4 (W): U against tree first at both 1 to 8, against chain "
"first at both 5 to 7; (0, 0) and (0, 1) one trace",
pairs[(TREE_BOTH, (1, 1))] == list(range(1, 9)) and
pairs[(CHAIN_BOTH, (1, 1))] == [5, 6, 7] and
tr[(0, 0)] == tr[(0, 1)])
nst, rkd, _ = pair_counts([tr[sg] for sg in SIGMAS])
check("C4 the kill's counter on these traces: NESTED 27, RANKDIFF 43, "
"counted by hand", nst == 27 and rkd == 43,
f"NESTED {nst}, RANKDIFF {rkd}")
def kill(imgs):
print()
print("K THE KILL: NESTED and RANKDIFF per cost, the quartet, all steps")
verdicts = {}
for cost in COSTS:
nested = rankdiff = 0
where, first = set(), None
for B, W in settings(cost):
for row in ROWS9:
trs = [run_costed(imgs[row], p, B, W, cost)[0]
for p in QUARTET]
nst, rkd, f = pair_counts(trs)
nested += nst
rankdiff += rkd
if nst:
where.add((B, W, row))
if f is not None and first is None:
n, i, j = f
first = ((B, W), row, n, SIGMAS[i], SIGMAS[j],
trs[i][n], trs[j][n])
a, b, e = cost
dep = a != b or e > 0
if nested > 0:
v = "BREAKS"
elif rankdiff == 0:
v = "ONE LEVEL (kill)" if dep else "ONE LEVEL"
else:
v = "UNDECIDED"
verdicts[cost] = v
print(f" {cost}: NESTED {nested}, RANKDIFF {rankdiff}, "
f"nested at {len(where)} (setting, row) of 144, "
f"{len({w[:2] for w in where})} settings: {v}")
if first is not None:
(B, W), row, n, s, t, x, y = first
print(f" first: setting {(B, W)}, row {row}, step {n}, "
f"{s} {t}: rank {rank(x)} {x} / rank {rank(y)} {y}")
return verdicts
def j_k(K):
return ((2 * K + 1, 2 * K + 3), (K + 2, K + 3))
def t_m(m):
return ((m - 1, m), (1, 1), 0, m)
def s_root(k):
return ((0, 1), (1, 0), k, 0)
def witness(a, b, e):
"""(K, I, chain first at both's member, tree first at both's)."""
if b < a:
K = e // (a - b) + 1
I = e + K * b + a
return K, I, t_m(K + 1), t_m(I // a)
if b > a:
K = a
return K, e + K * b, s_root(K), t_m(K + 1)
m = -(-e // a) + 1
return m, m * a, s_root(1), t_m(m)
def general():
print()
print("G THE GENERAL WITNESS, one step from the root on J_K")
cases = bad = 0
for a in range(1, 7):
for b in range(1, 7):
for e in range(0, 7):
if a == b and e == 0:
continue
K, I, want_c, want_t = witness(a, b, e)
Js = [j_k(K)]
c = run_costed(Js, CHAIN_BOTH + (0, 0, INF), I, 0,
(a, b, e))[0][0]
t = run_costed(Js, TREE_BOTH + (0, 0, INF), I, 0,
(a, b, e))[0][0]
cases += 1
ok = (c == want_c and t == want_t and
relation(c, t) in ("inside", "contains"))
if not ok:
bad += 1
print(f" miss {(a, b, e)}: K {K}, I {I}, {c} / {t}")
check("G the two members named, strictly nested, at every "
"route-dependent cost", bad == 0 and cases == 246,
f"{cases} costs, {bad} off")
runs = nested = 0
for a in range(1, 7):
for K in range(1, 7):
Js = [j_k(K)]
for I in range(1, 3 * (K + 1) * a + 1):
ms = [run_costed(Js, p, I, 0, (a, a, 0))[0][0]
for p in QUARTET]
runs += 1
nested += any(relation(ms[i], ms[j]) in ("inside",
"contains")
for i in range(4) for j in range(i + 1, 4))
check("G control: (a, a, 0) never nested on J_K", nested == 0 and
runs > 0, f"{runs} (a, K, I), {nested} nested")
def main():
imgs = images9(N_MAIN)
controls(imgs)
if not all(CHECKS):
print("controls failed: no verdict is read")
sys.exit(1)
verdicts = kill(imgs)
general()
print()
pred = all((verdicts[c] == "BREAKS") == (c not in ((1, 1, 0), (2, 2, 0)))
for c in COSTS)
print(f"PREDICTION (NESTED > 0 exactly off (1, 1, 0) and (2, 2, 0)): "
f"{'holds' if pred else 'misses'}")
print(f"{sum(CHECKS)}/{len(CHECKS)} checks passed")
sys.exit(0 if all(CHECKS) else 1)
if __name__ == "__main__":
main()