rider.py
Checks: ELEMENT: The element lid theorem.
Cited on: ELEMENT.
To run it: save rider.py, with dial.py, door.py, limit.py, race.py, stop.py, winner.py beside it; standard library only.
"""rider.py -- the lid when every move must be principal: what a greedy
walk over a number ring pays once it has locked, when each move buys a
core together with the minimal rider that makes it an element.
QUESTION. lid.py proves, for walks whose moves are ideals, that a block
whose last mover sits one tail gap below the next count and whose count
has outgrown the mover's tail price stays so forever, every later
price at most the lid, N^e of its last mover (N the norm, e the
ramification index); and that four statements about a walk are one:
it reaches such a state, some block is clocked infinitely often, it
makes finitely many openings, its prices are bounded infinitely often.
That proof reads places one at a time. In the ELEMENT world a move is a
principal ideal, and its least form is a CORE Q^r at Q's door r together
with a RIDER, a least ideal of the class -r c_Q (element_ring.py): one
move deepens several places, some possibly over the core's own prime.
Does the lid carry, with what price in place of N^e, and does the
four-way equivalence carry with it?
THE OBJECTS. A place Y over p has residue field of N = p^f elements,
ramification e, ladder x_1 = 1 < x_2 < ..., column c(b) = #{j : x_j <
b}, m_Y(j) = x_j + 1, gap G_Y(j) = m_Y(j + 1) - m_Y(j), tail index t_Y
(door.py). Its class in the class group is c_Y. mu(x) is the least norm
of an integral ideal of class x, mu(0) = 1, and a LEAST IDEAL of class x
is one attaining it. The PRICE of Y at door k is
pi_Y(k) = N^k * mu(-k c_Y),
and Y's TAIL PRICE is Lambda_Y = pi_Y(e_Y). A block is the set of
places over p; its count is V = v_p(L). A HOLDER of the block is a
seated place over p at column exactly V. A CREEPER over p is a place Y
over p that some least ideal contains with multiplicity strictly
between 0 and e_Y: a rider can move it less than one column.
THE ARGUMENT (written before the engine).
(0) THE BARE DOOR BOUND (element_ring.py (3)), read for every place of
a vehicle and not only its core: a principal J with v_Y(J) = k
has N(J) >= pi_Y(k), since J Y^(-k) is integral of class -k c_Y;
and pi_Y is nondecreasing, since a least ideal of class -(k+j) c_Y
times Y^j is an integral ideal of class -k c_Y. The least moves at
a state are the cores at their doors times least ideals, so the
menu's price is min over Y of pi_Y(door_Y).
(1) A HOLDER PENDS AT MOST ITS TAIL PRICE. At column V its depth
a satisfies m(V) <= a < m(V + 1), so its door m(V + 1) - a is at
most G(V), which is e once V >= t_Y; by (0) the move costs at most
Lambda_Y, and greed pays no more than any move on its menu.
(2) THE ELEMENT LID. Call the block over p LIDDED when it has a holder,
V >= t_Y for every place Y over p, and p^(V+1) >= B, where
B = max(Lambda over the holders, Lambda over the creepers
over p).
Its LID is the largest Lambda over its holders. Then:
(a) No jump is affordable. Raising V without deepening a place
over p needs a newly seated place Q (core or rider) with
p^(V+1) | N(Q) - 1, and any vehicle holding Q costs at least
N(Q) > p^(V+1) >= B, while a holder pends at most B by (1).
Deepening a seated place over another prime adds no p-part.
(b) Every new holder was a holder, is a creeper, or has Lambda at
most the price that made it. Let a move deepen Y by k and
leave it in the top column. If k >= e_Y, (0) applied to Y
inside the vehicle gives Lambda_Y <= pi_Y(k) <= the price paid
<= the lid. If k < e_Y and Y is the core, it moved at its
door, so it crossed the count from column V: it was a holder.
If k < e_Y and Y rides, Y is a creeper. So a holder's Lambda
never exceeds B, the lid never exceeds B, and with no creeper
over p the lid never rises; V only grows, keeping p^(V+1) >= B
and the tails.
THE ELEMENT LID THEOREM: a lidded block stays lidded, and every
price the walk pays afterwards is at most its lid at that moment,
which is at most B. With no creeper over p the lid never rises.
(3) THE QUADRATIC CASE. Over an imaginary quadratic field the places
over one prime share Lambda: a split pair is conjugate with
inverse classes and mu(x) = mu(-x); an inert or ramified prime has
one place. So each block has ONE tail price and its lid is
constant once lidded:
split p: p * mu(c_P), p when P is principal;
ramified p: p^2 (2 c_P = 0);
inert p: p^2.
The ramified place is a creeper (a least ideal holds it at most
once, P^2 = (p) being principal), but it is alone in its block, so
B is its own Lambda. The ideal lid is the principal case; the
element lid differs from it exactly at the split non-principal
places, by the factor mu(c_P) = the leading coefficient of the
class's reduced form.
(4) THE LOCK. The four statements stay one. Lidded implies every
later price at most B; each opening costs at least the norm of
the place it seats as core, and only finitely many places are
riders, so finitely many openings follow. Prices bounded
infinitely often bring cores of bounded norm, each opened once,
so some seated core crosses its door infinitely often and some
block's count rises by deepening infinitely often; the count then
passes every tail and the finitely many Lambda over p, and at the
state after such a rise the crosser is a holder, so the block is
lidded. Finitely many openings leave finitely many seated places,
one of which is a core infinitely often. What is NOT carried: that
the walk then repeats ONE vehicle forever. The ideal proof of one
runaway reads single places; here a rider can lag its block by a
growing number of columns and still move, and whether that can
keep the vehicle sequence from settling is left open.
THE CLASS GROUP. Gauss's reduced forms of discriminant D (known): a
place over a split or ramified p is the form (p, b, (b^2 - D)/(4p)) with
b^2 = D mod 4p, its conjugate negating b; an inert place is principal;
composition is Dirichlet's (Cohen, A Course in Computational Algebraic
Number Theory, algorithm 5.4.7), then reduction. mu(x) is the leading
coefficient of the reduced form of x (known: the least value a reduced
form properly represents), and it is re-derived here as a shortest path
over the places' classes in (min, x) and by brute enumeration.
PREDICTIONS, frozen before the engine, each naming what the run PRINTS.
PE0 CONTROL (read first; KILL of the engine). (a) Per field: the
composition of reduced forms is closed, has the principal form as
identity and (a, -b, c) as inverse, is associative over every
triple, and has h elements; every split place times its conjugate
is principal. (b) mu by the (min, x) path equals the leading
coefficient and the brute minimum over every ideal of norm up to
max mu. (c) At Q(sqrt -5) and Q(sqrt -23) the void's tree holds
the paths 4, 4, 9, 6, 4, ... and 6, 6, 6, 4, ... (element_ring.py
and its predecessor). (d) At every field of class number 1 the
element tree's set of price sequences equals the ideal tree's
(race.py).
PE1 THE ELEMENT LID. Over every imaginary quadratic field Q(sqrt m),
-200 <= m <= -1 squarefree, the void walked 40 moves with every tie
branched and equal states merged, at every state of every end:
a lidded block stays lidded, its lid never rises, every price paid
after a lidded state is at most that state's lid (the least over
its lidded blocks), no jump lands on a lidded block, and every
holder pends at most its Lambda. Printed: fields, ends, states,
lidded ends and each violation count. KILL: any count above 0.
PE2 THE RIDER IS LOAD-BEARING (a measurement, no kill). The prices
after a lidded state that exceed the IDEAL lid of their state
(the least, over its lidded blocks, of the largest N^e among a
block's holders), the element lid being larger. Predicted: some, all at
fields where a split place of a lidded block is non-principal.
PE3 THE REACH (a measurement, no kill). Every end lidded within 40
moves. Printed: the first lidded move's distribution.
PE4 THE LOCK AND ITS RIDER'S PRIME (a measurement, no kill; a
question element_ring.py leaves open, its locks each lying over
one prime by observation). Every end's last 10 moves repeat one
vehicle. Printed: the ends that do not, and the lock vehicles
whose support lies over two primes. Predicted from the void:
none over two primes, since the block over 2 has Lambda at most 4
(split: 2 * mu(c) = 4 or 2; inert or ramified: 4) and a vehicle
over two primes costs at least 6. From the principal seeds of norm
at most 40, walked on one path each, printed without prediction.
TRANSPLANTS, marked. From the ideal world: lid.py's whole argument,
which (2) re-derives with (0) in place of the single-place door. From
element_ring.py: the bare door and the menu as cores times riders,
proved there and re-used here for every place of a vehicle.
FINDINGS (entered after the run, from its output).
F1 THE CONTROLS (PE0 hit, read first). 122 fields, class numbers 1 to
20 (9 fields of h = 1, 27 of h = 4, 21 of h = 8, one of h = 20);
every group closed, associative, with identity and inverses, every
split pair principal, mu equal to the leading coefficient and the
brute minimum at every class. The void's trees at Q(sqrt -5) and
Q(sqrt -23) hold 4, 4, 9, 6, 4, ... and 6, 6, 6, 4, .... At the 9
fields of class number 1, 150 states, the element menu equals the
ideal menu at every one.
F2 THE ELEMENT LID (PE1 hit). 207 ends, 8487 states, 7762 prices paid
after a lidded state: no lid lost, risen or over B, no price over
the lid, no jump on a lidded block, no holder over its Lambda. The
1206 principal seeds of norm at most 40, one path each, the same:
0 violations.
F3 THE RIDER IS LOAD-BEARING (PE2 as predicted). 3567 prices exceed
the ideal lid N^e of their state, at 13 fields: -5, -15, -23, -31,
-39, -47, -71, -95, -111, -119, -143, -167, -191. By (3) the two
lids differ only at a split non-principal place, so these are the
fields where such a block is lidded before a cheaper one; at
Q(sqrt -5) the split place over 3 lids at 3 * mu(c) = 6.
F4 THE REACH (PE3). Every end lidded by move 4: move 1 on 2 ends, 2
on 119, 3 on 66, 4 on 20.
F5 THE LOCK (PE4, one part missed). 189 of 207 void ends repeat one
vehicle over their last 10 moves; the 18 that do not are all
Q(sqrt -15), where the price is 4 at every move of every end. Its
class of the places over 2 has order 2, so both places lie in it
and it has TWO least ideals, P2 and P2': the vehicles P2^2 and P2
P2' tie at 4 forever and the tree follows every interleaving. A
least ideal need not be unique over a number ring. Void lock
prices 2, 3, 4, 9, 13, 25; seed lock prices 2 to 47. No lock
vehicle lies over two primes, from the void or from any seed.
THE SECOND SITTING: WHERE A LOCK'S RIDER CAN SIT. element_ring.py
leaves open whether a lock's rider can lie over another prime than its
core. F5 found none. Is that forced?
THE ARGUMENT (written before its engine).
(5) Over an imaginary quadratic field, a vehicle W that a walk repeats
forever lies over one prime. Let S over p be a core of W at door
r, W = S^r R with R a least ideal of class -r c_S. Then N(R) <=
p^r: S's conjugate S' (S itself when ramified) has class -c_S, so
S'^r is an integral ideal of class -r c_S; an inert S is
principal and R = (1). Suppose R has a place over q != p. Once W
repeats, only W's places move, so the places of W over q grow
without bound, the q-count is the largest of their columns and
rises infinitely often, and at each rise a place Y of W over q is
a holder, past its tail once the count is. By (1) it pends at most
Lambda_Y, and by (3) Lambda_Y <= q^2 (split: q * mu(c_Y) <= q * q,
Y itself lying in c_Y; ramified or inert: q^2). But N(W) = p^r
N(R) >= p^r N(Y): if N(Y) = q then q <= N(R) <= p^r and N(W) >=
q^2, with equality only if p^r = q, impossible; if Y is inert,
N(W) >= p^r q^2 > q^2. So Y pends strictly below N(W), and W is
not a least move at that state. Hence W has no place over q.
THEOREM: a lock's rider lies over its core's prime.
The quadratic field enters twice. Once in Lambda_Y <= q^2, which in
a field of degree n reads only q^n; and once in the bound
N(R) <= p^r: over a field of higher degree S's class need not be
cancelled by a power of the places over p, and the question stays
open there.
PREDICTIONS, frozen before the engine, each naming what the run PRINTS.
PR1 THE TABLE (proof check of (3), read first). At every field, the
places over each prime share one Lambda, and it equals p mu(c)
for a split place, p^2 for a ramified or inert one. Printed: the
blocks read, the mismatches, and Q(sqrt -5)'s table. KILL: one.
PR2 WHERE THE THEOREM BITES. Every split non-principal place S of norm
at most 60 whose least rider R = MINREP(-c_S) lies over another
prime is seeded at W^j, W = S R, j = 1, 2, 3, and walked 40 moves
on one path. Printed: the seeds, how many take W at least once as
a move (the POSITIVE CONTROL: at least one, or the test is
vacuous and says so), how many repeat one vehicle over their last
10 moves, the lid violations, and the lock vehicles over two
primes. KILL: a lock over two primes, or a lid violation.
FINDINGS OF THE SECOND SITTING (entered after the run, from its output).
F6 THE TABLE (PR1 hit). 5234 blocks over the primes with a place of
norm <= 400, 0 mismatches; (3)'s creeper clause holds for a
non-principal ramified place, a principal one lying in no least
ideal. Q(sqrt -5): the
ramified place over 2 at 4, the split pair over 3 at 6 each, the
ramified place over 5 at 25, the places over 7 at 14.
F7 WHERE THE THEOREM BITES (PR2 hit, positive control met). 1354
pairs of a split non-principal place and a least rider over another
prime, 4062 seeds: 100 take the two-prime vehicle W at least once,
and every one leaves it. Q(sqrt -5), core over 3 with the ramified
place over 2 riding, from W: 4, 6, 6, 4, 4, ..., W taken at the
second and third moves. All 4062 lock, 0 lid violations, and no
lock vehicle lies over two primes; lock prices from 4 to 121.
RUN RECORD (both sittings). One process, CPython, no numpy: 784,441
checks, 28.5 s, peak working set 78.6 MB.
"""
import os
import sys
import time
from collections import Counter
from math import gcd
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import door as DR # noqa: E402
import race as RC # noqa: E402
import winner as WN # noqa: E402
CHECKS = [0]
N_W = 40 # moves per walk
LOCK_R = 10 # a lock: the last LOCK_R moves repeat one vehicle
SEED_N = 40 # principal seeds up to this norm, one path each
CAP = 20000 # states per step of a tree
def check(cond, msg):
CHECKS[0] += 1
if not cond:
raise SystemExit("FAIL: " + msg)
# ---------------------------------------------------------------------------
# the class group by reduced forms
def reduce_form(a, b, c):
D = b * b - 4 * a * c
while True:
k = (b + a - 1) // (2 * a)
b -= 2 * a * k
c = (b * b - D) // (4 * a)
if a > c:
a, b, c = c, -b, a
continue
if a == c and b < 0:
b = -b
return a, b, c
def reduced_forms(D):
out, a = [], 1
while 3 * a * a <= -D:
for b in range(-a + 1, a + 1):
if (b * b - D) % (4 * a) == 0:
c = (b * b - D) // (4 * a)
if c >= a and not (a == c and b < 0) and \
gcd(gcd(a, abs(b)), c) == 1:
out.append((a, b, c))
a += 1
return sorted(out)
def xgcd(a, b):
"""(u, v, d) with u a + v b = d = gcd(a, b) >= 0."""
x0, y0, x1, y1 = 1, 0, 0, 1
while b:
q = a // b
a, b = b, a - q * b
x0, x1 = x1, x0 - q * x1
y0, y1 = y1, y0 - q * y1
if a < 0:
a, x0, y0 = -a, -x0, -y0
return x0, y0, a
def compose(f1, f2, D):
"""Dirichlet composition (Cohen 5.4.7), reduced."""
(a1, b1, c1), (a2, b2, c2) = f1, f2
if a1 > a2:
(a1, b1, c1), (a2, b2, c2) = (a2, b2, c2), (a1, b1, c1)
s = (b1 + b2) // 2
n = b2 - s
if a2 % a1 == 0:
y1, d = 0, a1
else:
u, v, d = xgcd(a2, a1)
y1 = u
if s % d == 0:
y2, x2, d1 = -1, 0, d
else:
u, v, d1 = xgcd(s, d)
x2, y2 = u, -v
v1, v2 = a1 // d1, a2 // d1
r = (y1 * y2 * n - x2 * c2) % v1
b3 = b2 + 2 * v2 * r
a3 = v1 * v2
check((b3 * b3 - D) % (4 * a3) == 0, "composition off discriminant")
return reduce_form(a3, b3, (b3 * b3 - D) // (4 * a3))
class Group:
"""The class group as indices into the reduced forms, 0 principal."""
def __init__(self, D):
self.D = D
self.forms = reduced_forms(D)
self.h = len(self.forms)
self.ix = {f: i for i, f in enumerate(self.forms)}
check(self.forms[0][0] == 1, "the principal form first")
self.mul = [[self.ix[compose(f, g, D)] for g in self.forms]
for f in self.forms]
self.inv = [self.ix[reduce_form(a, -b, c)] for a, b, c in self.forms]
self.ords = []
for x in range(self.h):
k, y = 1, x
while y != 0:
y = self.mul[y][x]
k += 1
self.ords.append(k)
def power(self, x, k):
y = 0
for _ in range(k % self.ords[x]):
y = self.mul[y][x]
return y
def of_form(self, a, b, c):
return self.ix[reduce_form(a, b, c)]
def group_control(G):
"""PE0 (a) at one discriminant."""
h, mul = G.h, G.mul
for x in range(h):
check(mul[0][x] == x and mul[x][0] == x, "identity")
check(mul[x][G.inv[x]] == 0, "inverse")
for y in range(h):
check(mul[x][y] == mul[y][x], "commutative")
for z in range(h):
check(mul[mul[x][y]][z] == mul[x][mul[y][z]], "associative")
# ---------------------------------------------------------------------------
# a field: its places with their classes, mu and the least ideals
class Field:
def __init__(self, m):
self.m = m
self.D = m if m % 4 == 1 else 4 * m
self.pls = WN.field(m)
self.G = G = Group(self.D)
group_control(G)
cls, seen = [], Counter()
for q in self.pls:
if q.f == 2 and q.e == 1:
cls.append(0)
continue
p = q.p
b = [b for b in range(0, 2 * p)
if (b * b - self.D) % (4 * p) == 0][0]
sign = -1 if seen[p] else 1
seen[p] += 1
cls.append(G.of_form(p, sign * b, (b * b - self.D) // (4 * p)))
self.cls = cls
for i, q in enumerate(self.pls):
if q.e == 1 and q.f == 1 and seen[q.p] == 2 and \
i + 1 < len(self.pls) and self.pls[i + 1].p == q.p:
check(G.mul[cls[i]][cls[i + 1]] == 0,
f"Q(sqrt {m}): a split pair's product not principal")
least = {}
for q in self.pls:
c = cls[q.idx]
if c not in least or q.N < least[c]:
least[c] = q.N
INF = float("inf")
mu = [INF] * G.h
mu[0] = 1
changed = True
while changed:
changed = False
for x in range(G.h):
if mu[x] < INF:
for c, n in least.items():
y = G.mul[x][c]
if mu[x] * n < mu[y]:
mu[y] = mu[x] * n
changed = True
self.mu = mu
self.least = self.least_ideals(max(mu))
self.lam_rec = [self.price(q, q.e) for q in self.pls]
self.creep = set()
for ids in self.least:
for I in ids:
for i, k in I:
if 0 < k < self.pls[i].e:
self.creep.add(i)
def ideals(self, top):
"""Every integral ideal of norm <= top: (norm, ((idx, k), ...))."""
small = [q for q in self.pls if q.N <= top]
out = []
def rec(j, n, ideal):
out.append((n, tuple(ideal)))
for t in range(j, len(small)):
q = small[t]
k, nn = 1, n * q.N
while nn <= top:
rec(t + 1, nn, ideal + [(q.idx, k)])
k += 1
nn *= q.N
rec(0, 1, [])
return out
def least_ideals(self, top):
"""Per class the ideals of least norm, PE0 (b) checked."""
best = {}
for n, I in self.ideals(top):
best.setdefault(self.cls_of(I), []).append((n, I))
least = []
for x in range(self.G.h):
ns = best.get(x, [])
check(ns, f"Q(sqrt {self.m}): class {x} has no ideal <= {top}")
lo = min(n for n, I in ns)
check(lo == self.mu[x], f"Q(sqrt {self.m}): brute mu at {x}")
check(lo == self.G.forms[x][0],
f"Q(sqrt {self.m}): mu is not the leading coefficient")
least.append([I for n, I in ns if n == lo])
return least
def cls_of(self, I):
x = 0
for i, k in I:
x = self.G.mul[x][self.G.power(self.cls[i], k)]
return x
def rider_class(self, q, r):
return self.G.inv[self.G.power(self.cls[q.idx], r)]
def price(self, q, r):
return q.N ** r * self.mu[self.rider_class(q, r)]
def state(self, I):
st = St()
for i, k in I:
st.a[i] = k
lam = self.pls[i].lam(k)
st.L = st.L * lam // gcd(st.L, lam)
return st
def fields():
for m in range(-1, -201, -1):
if RC.squarefree(m):
yield Field(m)
# ---------------------------------------------------------------------------
# the element walk
class St:
__slots__ = ("a", "L")
def __init__(self, a=None, L=1):
self.a, self.L = dict(a or {}), L
def key(self):
return tuple(sorted(self.a.items()))
def emenu(F, st):
"""(best price, [vehicle]); a vehicle is ((core idx, door), (idx, k),
...), its places sorted after the core."""
best, out = None, []
for q in F.pls:
if best is not None and q.N > best:
break
r = DR.door_lcm(q, st.a.get(q.idx, 0), st.L)
pr = F.price(q, r)
if best is None or pr < best:
best, out = pr, []
if pr == best:
for I in F.least[F.rider_class(q, r)]:
v = Counter({q.idx: r})
for i, k in I:
v[i] += k
out.append(((q.idx, r),) + tuple(sorted(v.items())))
check(best is not None and best < F.pls[-1].N, "the supply ran out")
return best, out
def apply(F, st, veh):
n = St(st.a, st.L)
for i, k in veh[1:]:
n.a[i] = n.a.get(i, 0) + k
lam = F.pls[i].lam(n.a[i])
n.L = n.L * lam // gcd(n.L, lam)
check(n.L != st.L, "a vehicle that does not raise lambda")
return n
class Path:
__slots__ = ("st", "vehs", "paid")
def __init__(self, st, vehs, paid):
self.st, self.vehs, self.paid = st, vehs, paid
def etree(F, st0, n, tally=None):
"""Every tie branched, equal states merged (the first path kept); at
class number 1 every state's menu is read against race.py's."""
front = {st0.key(): Path(st0, [], [])}
for _ in range(n):
nxt = {}
for path in front.values():
best, vehs = emenu(F, path.st)
succ = set()
for v in vehs:
s2 = apply(F, path.st, v)
k = s2.key()
succ.add(k)
if k not in nxt:
nxt[k] = Path(s2, path.vehs + [v], path.paid + [best])
if tally is not None and F.G.h == 1:
ideal_control(F, path.st, best, succ, tally)
front = nxt
check(len(front) <= CAP, "the branch cap")
return list(front.values())
def ideal_control(F, st, best, succ, tally):
"""PE0 (d): at class number 1 the element menu is race.py's."""
rs = DR.RSt()
rs.a, rs.L = dict(st.a), st.L
b2, types = RC.menu(F.pls, rs, Counter(), True)
s2 = set()
for t in types:
n = DR.rstep(F.pls, rs, t, b2, [], [], Counter())
s2.add(n.key())
tally["ctl_states"] += 1
check(b2 == best and s2 == succ, f"Q(sqrt {F.m}): element and ideal"
f" menus part at {st.key()}")
def canon_path(F, st0, n):
st, vehs, paid = st0, [], []
for _ in range(n):
best, vs = emenu(F, st)
v = min(vs)
st = apply(F, st, v)
vehs.append(v)
paid.append(best)
return Path(st, vehs, paid)
# ---------------------------------------------------------------------------
# the element lid read off a state
def tail(q):
return DR.tail_index(q.lad)[0]
def holders(F, st, p):
V = DR.vp(st.L, p)
return V, [q for q in F.pls if q.p == p and st.a.get(q.idx, 0) >= 1
and DR.column(q.lad, st.a[q.idx]) == V]
def block_read(F, st, p):
"""(lidded, lid, B, holders) of the block over p at st."""
V, hold = holders(F, st, p)
if not hold:
return False, None, None, hold
over = [q for q in F.pls if q.p == p]
lid = max(F.lam_rec[q.idx] for q in hold)
B = max([lid] + [F.lam_rec[q.idx] for q in over if q.idx in F.creep])
ok = all(V >= tail(q) for q in over) and p ** (V + 1) >= B
return ok, lid, B, hold
def read_path(F, st0, path, tot):
"""PE1 and PE2 along one path: the first lidded move, or None."""
states = [st0]
for v in path.vehs:
states.append(apply(F, states[-1], v))
lidded, first = {}, None
for t, st in enumerate(states):
tot["states"] += 1
now = {}
for p in {F.pls[i].p for i in st.a}:
ok, lid, B, hold = block_read(F, st, p)
if ok:
now[p] = (lid, B, hold)
for q in hold:
r = DR.door_lcm(q, st.a[q.idx], st.L)
tot["holder_over"] += F.price(q, r) > F.lam_rec[q.idx]
tot["lid_lost"] += sum(p not in now for p in lidded)
for p, (lid, B, hold) in now.items():
if p in lidded:
tot["lid_rise"] += lid > lidded[p][0]
tot["over_B"] += lid > lidded[p][1]
lidded[p] = (lid, lidded[p][1])
else:
lidded[p] = (lid, B)
if t > 0:
before = states[t - 1]
for p in lidded:
V, hold = holders(F, st, p)
tot["jump_on_lid"] += V > DR.vp(before.L, p) and not hold
if not now:
continue
if first is None:
first = t
cur = min(lid for lid, B, hold in now.values())
ideal = min(max(q.N ** q.e for q in hold)
for lid, B, hold in now.values())
if t < len(path.paid):
tot["paid_after"] += 1
tot["over"] += path.paid[t] > cur
if path.paid[t] > ideal:
tot["over_ideal"] += 1
tot.setdefault("over_ideal_at", set()).add(F.m)
return first
def lock_read(F, path, tot, key):
tail_v = path.vehs[-LOCK_R:]
if len({v[1:] for v in tail_v}) != 1:
tot[key + "_unlocked"] += 1
tot.setdefault(key + "_unlocked_at", []).append(F.m)
return
v = tail_v[0]
tot[key + "_locked"] += 1
tot.setdefault(key + "_prices", Counter())[path.paid[-1]] += 1
if len({F.pls[i].p for i, k in v[1:]}) > 1:
tot.setdefault(key + "_two", []).append(
(F.m, path.paid[-1], [(F.pls[i].name, k) for i, k in v[1:]]))
# ---------------------------------------------------------------------------
# the sections
def section_control(Fs):
print("PE0 CONTROLS")
hs = Counter(F.G.h for F in Fs)
print(f" {len(Fs)} fields; class numbers (h: fields) "
f"{sorted(hs.items())}; every group closed, associative, with "
f"identity and inverses; every split pair principal; mu equal to "
f"the leading coefficient and the brute minimum at every class")
by = {F.m: F for F in Fs}
for m, want in ((-5, [4, 4, 9, 6] + [4] * 8), (-23, [6, 6, 6] + [4] * 9)):
ends = etree(by[m], St(), len(want))
seqs = {tuple(pth.paid) for pth in ends}
check(tuple(want) in seqs, f"PE0 (c) at {m}")
print(f" Q(sqrt {m}): the void's tree holds {want[:5]} ...; "
f"{len(ends)} end(s)")
tally = Counter()
for F in Fs:
if F.G.h == 1:
etree(F, St(), 12, tally)
print(f" class number 1: {tally['ctl_states']} states, element menu "
f"equal to the ideal menu at every one")
def section_lid(Fs):
print("PE1 - PE4 THE ELEMENT LID FROM THE VOID")
tot, reach, t0 = Counter(), Counter(), time.time()
for F in Fs:
tot["fields"] += 1
for path in etree(F, St(), N_W):
tot["ends"] += 1
first = read_path(F, St(), path, tot)
if first is None:
tot["unlidded"] += 1
else:
reach[first] += 1
lock_read(F, path, tot, "void")
print(f" {tot['fields']} fields, {tot['ends']} ends, {tot['states']} "
f"states, {tot['paid_after']} prices paid after a lidded state "
f"({time.time() - t0:.1f} s)")
print(f" PE1 violations: lid lost {tot['lid_lost']}, lid risen "
f"{tot['lid_rise']}, lid over B {tot['over_B']}, price over the "
f"lid {tot['over']}, jump on a lidded block {tot['jump_on_lid']},"
f" holder over its Lambda {tot['holder_over']}")
for k in ("lid_lost", "lid_rise", "over_B", "over", "jump_on_lid",
"holder_over"):
check(tot[k] == 0, "PE1: " + k)
at = sorted(tot.get("over_ideal_at", set()))
print(f" PE2 prices over the ideal lid N^e: {tot['over_ideal']}, at "
f"{len(at)} fields {at}")
print(f" PE3 ends lidded {tot['ends'] - tot['unlidded']}, not "
f"{tot['unlidded']}; first lidded move (move: ends) "
f"{sorted(reach.items())}")
print(f" PE4 locked ends {tot['void_locked']}, not "
f"{tot['void_unlocked']} {tot.get('void_unlocked_at', [])}; lock "
f"prices {sorted(tot.get('void_prices', Counter()).items())}; "
f"over two primes {tot.get('void_two', [])}")
check(not tot.get("void_two"), "F5: the void's lock lies over two primes")
return tot
def section_seeds(Fs):
print("PE4 THE PRINCIPAL SEEDS, ONE PATH EACH")
tot, t0 = Counter(), time.time()
for F in Fs:
for n, I in F.ideals(SEED_N):
if not I or F.cls_of(I) != 0:
continue
st0 = F.state(I)
path = canon_path(F, st0, N_W)
tot["seeds"] += 1
if read_path(F, st0, path, tot) is None:
tot["unlidded"] += 1
lock_read(F, path, tot, "seed")
print(f" {tot['seeds']} seeds ({time.time() - t0:.1f} s); lid "
f"violations {sum(tot[k] for k in ('lid_lost', 'lid_rise', 'over_B', 'over', 'jump_on_lid', 'holder_over'))},"
f" unlidded {tot['unlidded']}")
for k in ("lid_lost", "lid_rise", "over_B", "over", "jump_on_lid",
"holder_over"):
check(tot[k] == 0, "PE1 at the seeds: " + k)
print(f" locked {tot['seed_locked']}, not {tot['seed_unlocked']} "
f"{tot.get('seed_unlocked_at', [])}; lock prices "
f"{sorted(tot.get('seed_prices', Counter()).items())}")
two = tot.get("seed_two", [])
print(f" lock vehicles over two primes: {len(two)}; the first "
f"{two[:6]}")
check(not two, "F5: a seed's lock vehicle lies over two primes")
def section_table(Fs):
print("PR1 THE TABLE")
blocks = bad = 0
for F in Fs:
for p in sorted({q.p for q in F.pls if q.N <= 400}):
over = [q for q in F.pls if q.p == p]
want = set()
for q in over:
if q.e == 1 and q.f == 1:
want.add(p * F.mu[F.cls[q.idx]])
else:
want.add(p * p)
got = {F.lam_rec[q.idx] for q in over}
blocks += 1
bad += len(got) != 1 or got != want
print(f" {blocks} blocks, mismatches {bad}")
check(bad == 0, "PR1: the table")
F = [F for F in Fs if F.m == -5][0]
print(f" Q(sqrt -5): " + ", ".join(
f"{q.name} Lambda {F.lam_rec[q.idx]}" for q in F.pls[:5]))
def section_bite(Fs):
print("PR2 WHERE THE THEOREM BITES")
tot, t0 = Counter(), time.time()
for F in Fs:
for q in F.pls:
if q.N > 60 or q.e != 1 or q.f != 1 or F.cls[q.idx] == 0:
continue
for R in F.least[F.rider_class(q, 1)]:
if all(F.pls[i].p == q.p for i, k in R):
continue
W = Counter({q.idx: 1})
for i, k in R:
W[i] += k
places = tuple(sorted(W.items()))
tot["places"] += 1
for j in (1, 2, 3):
st0 = F.state(tuple((i, j * k) for i, k in places))
path = canon_path(F, st0, N_W)
tot["seeds"] += 1
took = [t for t, v in enumerate(path.vehs)
if v[1:] == places]
tot["took"] += bool(took)
if took and "took_ex" not in tot:
tot["took_ex"] = (F.m, q.name, j, path.paid[:8],
took[:5])
if read_path(F, st0, path, tot) is None:
tot["unlidded"] += 1
lock_read(F, path, tot, "bite")
print(f" {tot['places']} (place, rider) pairs, {tot['seeds']} seeds "
f"({time.time() - t0:.1f} s); taking W at least once {tot['took']}"
f"; example (field, core, j, prices, moves taking W) "
f"{tot.get('took_ex')}")
check(tot["took"] >= 1, "no seed takes W: the bite test is vacuous")
viol = sum(tot[k] for k in ("lid_lost", "lid_rise", "over_B", "over",
"jump_on_lid", "holder_over"))
print(f" locked {tot['bite_locked']}, not {tot['bite_unlocked']}; lid "
f"violations {viol}, unlidded {tot['unlidded']}; lock prices "
f"{sorted(tot.get('bite_prices', Counter()).items())}; locks over "
f"two primes {tot.get('bite_two', [])}")
check(viol == 0, "PR2: the lid")
check(tot["bite_unlocked"] == 0, "PR2: every seed locks")
check(not tot.get("bite_two"), "PR2: a lock over two primes")
def main():
t0 = time.time()
Fs = list(fields())
section_control(Fs)
section_lid(Fs)
section_seeds(Fs)
section_table(Fs)
section_bite(Fs)
print(f"\n{CHECKS[0]} checks, {time.time() - t0:.1f} s")
if __name__ == "__main__":
main()