keyweld.py
Cited on: FLUSH.
To run it: save keyweld.py, with flush.py, hull.py, induct.py, ostrowski.py, tie.py beside it; standard library only.
"""
keyweld.py -- the key window of the integer reader of x m against the
affine criterion of a radix reader: which steps of the criterion's
sufficiency carry to the keys, and what carries the one that does not.
QUESTION. The affine criterion's sufficiency has three steps: the
admissible moves form a run (the window is an interval), the endpoint
bound keeps the run inside the digit range, and the window meets every
class of the state lattice modulo the move's step, of which there are
P, so P consecutive points suffice. The integer reader's key (G, H, f,
t) at a purely periodic alpha has offset y = H - G r_t, and a reply d
then a move e send it to y' = -y / r_t + m d W_t + e r_(t+1) (hull.py's
HULL-WI), G's coefficient 0, so validity reads y alone and the run
carries. (Q1) With the lattice dropped, the offset real, is the window
inductive exactly from the overlap reader's c_ov, so the lattice's
whole gain is c_ov - c_inf? (Q2) On the lattice the classes of the move
step r_(t+1) are the integers H, not finitely many, and the hull set
cuts them by Z = lambda_t G + kappa_t H. Is Z kappa_t times the
tentative conjugate u = G zeta'_t + H (flush.py's conj_ratios), so the
hull set is a cut-and-project set, and does the norm form of the module
Z + Z r_t then carry the class step: a lattice key strictly inside a
reply's gap differs from each of the gap's ends, themselves lattice
keys, by a vector v with |y(v) Z(v)| = kappa_t |N| >= mu_t?
DERIVED BY HAND (before the engine).
THE CONJUGATE. kappa = s / (1 + r s), lambda = 1 / (1 + r s), so
lambda / kappa = 1 / s and Z = kappa (H + G / s); zeta'_t = 1 / s_t
(both [a_t; a_(t-1), ...] at a purely periodic alpha), so Z = kappa_t
u. Galois: r_t's conjugate is -1 / s_t, so y(v) u(v) is the norm of
x = dH - dG r_t, and with N(x) = dH^2 - 2A dG dH + C dG^2 (r_t = A +
B sqrt D, C = A^2 - B^2 D), den N(x) is a nonzero integer, den the lcm
of 2A's and C's denominators: mu_t = kappa_t / den. (G, H) -> (y, Z)
has determinant -(r kappa + lambda) = -1: unimodular.
THE REAL LINE (TRANSPLANT of the endpoint and class steps). The
reply-d image of V(t, f), -V / r_t + m d W_t, must lie in the union
over e = 0 .. a_(t+2) of V(t+1, f') - e r_(t+1), f' = (d = 0);
consecutive translates leave an open gap of r_(t+1) - len V(t+1, f')
when that is positive. At s = 0 the window is I_(t+1), whose members
overlap by |theta_(t+2)| = ov_(t+1), and a full sub-cylinder has width
w_(t+1), so len V(t+1, F) >= r_(t+1) is w_(t+1) <= ov_(t+1): the
overlap reader's bar. Sufficiency at c_ov is derived here for that
gap step alone; the endpoint step and the reduced flag are owed by
the overlap reader's induction, not written; that the real window
fails below c_ov needs room to straddle an overlap, not derived.
THE CERTIFICATE. A forbidden interval (y_a, y_b) of V(t, f) under reply
d, of length L, its ends lattice keys E_a, E_b at Z_a, Z_b: a key at
y_a + x, 0 < x < L, has |Z - Z_a| >= mu / x and |Z - Z_b| >= mu / (L -
x). With x_1 = mu / (Z_a - Z_lo), x_2 = mu / (Z_b - Z_lo), no such key
has Z >= Z_lo below both exclusions iff x_1 + x_2 > L, or Z_a <= Z_lo,
or Z_b <= Z_lo; the mirror at Z_hi; and no key lies between the
exclusions when 4 mu / L > |Z_b - Z_a|. A closed end (clipped at V's
end) is read directly. Golden x2 at c = 3, phase 0, full flag, the
zero reply (induct.py's gap (phi^-6, 2 phi^-6)): ends (8, 5) and
(16, 10), mu = 1 / sqrt 5, L = phi^-6, so Z_b - Z_a = mu / L =
8.0249 < 4 mu / L, and the low side needs Z_lo > Z_a - phi mu / L =
-4.9597, exactly Z(-5, -3): the bound is attained at golden.
(Exact values, recomputed after the run; the frozen text read 8.03,
12.99, -4.97 and -4.96.)
DESIGN (frozen before the engine). Cells: flush.py's PERIODIC, m = 2 ..
5 (--wide: to 9), (s, s_0) = (0, 1), Window, Coords and the exact
fixed points Z_lo, Z_hi from induct.py and hull.py, c_inf =
induct.least(F, m, "pin"). C_REAL: the least c with each pinned key's
valid move and, at every (t, f) and reply d, the reply image of the
real V(t, f) inside the union of V(t+1, f')'s move translates, exact.
C_OV: the least c with m (P(c) + P(c+1)) <= P(1) at every phase, P(k)
= |theta_(t+k) / theta_(t-1)|, and w_0 <= alpha. The forbidden
intervals at c: per (t, f, d), V(t, f) less the preimages of the
translates. THE CERTIFICATE as derived, exact in Q(sqrt D).
PREDICTIONS (frozen). (P1) Z = kappa_t u at every key of H(c_inf), and
conj(r_t) = -1 / s_t at every phase, all cells. (P2) c_real = c_ov at
every cell, c_inf < c_real at some. (P3) every forbidden interval at
c_inf at every cell is certified, ends integral. KILL: "c_real != c_ov
at n cells" (Q1) and "uncertified forbidden intervals at c_inf: n at k
cells" (Q2), n > 0 on either. A cell with c_real > c_ov, or a
certified interval holding a key of H, is an instrument fault (the
certificate proved, c_real <= c_ov derived in its gap step), printed
apart. (Frozen as c_real < c_ov, the unproved
side; corrected after the run, the print with it: 0 either way.)
CONTROLS (read before the verdict). (a) golden x2 .. x9: c_ov against
the closed form, the least c with m phi^-c <= phi^-2 (4, 5, 5, 6, 6, 7,
7, 7); (b) the real window at golden x2, c = 3, fails at the zero reply
with the gap (phi^-6, 2 phi^-6) at phase 0; (c) SOUNDNESS: at every c
from the first with pinned moves to c_inf, every key of H(c) inside a
forbidden interval (enumerated directly, as hull.py's wi) lies in an
uncertified one, and the direct enumeration at c_inf finds none
(hull.py's HULL-WI verdict); (d) THE PLANT, in the direction it pushes:
mu inflated 4-fold must certify some interval holding a key of H at
some c below c_inf, so (c) can fire.
FINDINGS (the --wide run, copied from its prints; the bare run, m = 2
.. 5, prints the same Q2 rows and 24 of the cells).
CONTROLS. (a) golden x2 .. x9: c_ov [4, 5, 5, 6, 6, 7, 7, 7], the
closed form's. (b) the open gap (phi^-6, 2 phi^-6) is among the
forbidden pieces at golden x2, c = 3, phase 0, full, the zero
reply. (c) 1165 stranded (key, reply) pairs of H(c), c <= c_inf,
lie in forbidden pieces, 0 in a certified one; 0 stranded at
c_inf by direct enumeration (hull.py's HULL-WI). (d) mu x 4
certifies pieces holding 30 stranded pairs: (c) can fire. (e) the
forbidden pieces and the direct enumeration rule 0 (key, reply)
pairs of H(c), c <= c_inf, apart.
P1. conj(r_t) = -1/s_t at every phase; |1/s_t - zeta'_t| at most
4.4e-16 against flush.conj_ratios; Z = kappa_t u at every key of
H(c_inf), 0 off (an identity once zeta'_t = 1/s_t, so that print
cannot fire): the hull set is the cut-and-project set of the
module Z + Z r_t with the window V(t, f) in y and [Z_lo, Z_hi] in
kappa_t u.
Q1, KILL MISSED. c_real != c_ov at 0 of 48 cells, c_real > c_ov at 0:
with the lattice dropped the affine criterion's three steps hold
exactly from c_ov, the overlap reader's lookahead. c_inf < c_real
at 6 of 48, each by 1: golden x2 (3 against 4), silver x2 (2, 3),
bronze x3 (2, 3), V1 x2 (3, 4), V1 x3 (4, 5), V2 x4 (4, 5); none at
m = 5 .. 9. The lattice's whole gain over the real window is those
six cells' one step.
Q2, KILL FIRED. Uncertified forbidden pieces at c_inf: 15 of 22, at 4
cells (bronze x3, V1 x2, V1 x3, V2 x4); per cell (pieces,
certified): golden x2 (2, 2), silver x2 (4, 4), bronze x3 (6, 0),
V1 x2 (6, 1), V1 x3 (2, 0), V2 x4 (2, 0); every end integral. The least
low-side margin (x1 + x2) / L is 0.1458 (1 is the bar). No key of
H(c_inf) lies in any of the 22 (control c), so the norm form's
minimum alone carries the class step at golden x2 and silver x2
and at no other cell whole: what keeps H out of bronze x3's gaps,
(0.02012, 0.02521) and two more at phase 0 on both flags after
the zero reply, is not the norm bound at the gap's two ends.
RUN RECORD. Bare 0.8 s, --wide 2.3 s, peak commit 8.8 MB. The engine
was written whole after the freeze and run once bare, once --wide,
nothing changed between. C_OV's frozen "and w_0 <= alpha" is not
evaluated: at s = 0 it follows from the phase-0 bar, P(1) < P(0). A
review after the run added control (e), the zeta' read and the
per-cell print, and turned the fault print's direction; --wide then
4.7 s, every earlier line unchanged. On shipping, the verdicts were
made the exit code: 0 iff the controls, P1 and Q1 hold as printed and
Q2's kill fires as recorded, 15 of 22 pieces uncertified at the four
cells named, the per-cell table and the least margin as printed (the
bare run's cells hold every piece).
Usage: python keyweld.py [--wide] (--wide adds m = 6 .. 9)
"""
import math
import os
import sys
import time
from fractions import Fraction as Fr
os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
from flush import PERIODIC, conj_ratios # noqa: E402
from induct import Field, Window, least, QF, le # noqa: E402
from hull import Coords, hull, hull_set, inv, eq, back_ratio # noqa: E402
WIDE = "--wide" in sys.argv
def lt(x, y):
return not le(y, x)
def conj(x):
return QF(x.a, -x.b)
def lattice_key(F, t, y):
"""(G, H) with H - G r_t = y, or None if not integral."""
r = F.r[t]
G = -y.b / r.b
H = y.a + G * r.a
if G.denominator != 1 or H.denominator != 1:
return None
return int(G), int(H)
def mu_of(F, co, t):
"""kappa_t / den: a lower bound on |y(v) Z(v)| over lattice v != 0."""
r = F.r[t]
A, B = r.a, r.b
C = A * A - B * B * QF.D
den = math.lcm((2 * A).denominator, C.denominator)
return co.kap[t] * QF(Fr(1, den))
def W_of(win, t):
U, V = win.UV[t]
return QF(V) - win.F.r[(t + 1) % win.F.p] * U
def forbidden(win, t, f, d):
"""The offsets y of V(t, f) with no valid move after reply d:
[(lo, hi, lo_closed, hi_closed)]."""
F, m, p = win.F, win.m, win.F.p
t1 = (t + 1) % p
f1 = d == 0
lo1, hi1 = win.V[(t1, f1)]
r1 = F.r[t1]
a = F.a(t1 + 1)
# open pieces of the y1 line outside every translate [lo1 - e r1,
# hi1 - e r1], e = 0 .. a; None stands for an infinite end
pieces = [(None, lo1 - r1 * a), (hi1, None)]
for e in range(a):
g0, g1 = hi1 - r1 * (e + 1), lo1 - r1 * e
if lt(g0, g1):
pieces.append((g0, g1))
lo, hi = win.V[(t, f)]
if lt(hi, lo):
return []
rt = F.r[t]
base = QF(m * d) * W_of(win, t)
out = []
for A1, B1 in pieces:
# y = r_t (base - y1) reverses the piece
ya = rt * (base - B1) if B1 is not None else None
yb = rt * (base - A1) if A1 is not None else None
ca = cb = False
if ya is None or lt(ya, lo):
ya, ca = lo, True
if yb is None or lt(hi, yb):
yb, cb = hi, True
if lt(ya, yb) or (ca and cb and eq(ya, yb)):
out.append((ya, yb, ca, cb))
return out
def certify(F, co, t, ya, yb, ca, cb, zlo, zhi, mu):
"""(certified, integral ends, low margin): no key of the hull at
(t, f) lies in the piece, by the norm form."""
Ea, Eb = lattice_key(F, t, ya), lattice_key(F, t, yb)
if Ea is None or Eb is None:
return False, False, None
Za, Zb = co.Z(*Ea, t), co.Z(*Eb, t)
L = yb - ya
for closed, Zc in ((ca, Za), (cb, Zb)):
if closed and le(zlo, Zc) and le(Zc, zhi):
return False, True, None
if le(L, QF(0)):
return True, True, None
marg = None
if le(Za, zlo) or le(Zb, zlo):
low = True
else:
s = mu * inv(Za - zlo) + mu * inv(Zb - zlo)
low = lt(L, s)
marg = s.f / L.f
if le(zhi, Za) or le(zhi, Zb):
high = True
else:
high = lt(L, mu * inv(zhi - Za) + mu * inv(zhi - Zb))
gap = Zb - Za if le(Za, Zb) else Za - Zb
mid = lt(gap, QF(4) * mu * inv(L))
if not mid:
z0, z1 = (Za, Zb) if le(Za, Zb) else (Zb, Za)
m0, m1 = z0 + mu * inv(L), z1 - mu * inv(L)
mid = lt(zhi, m0) or lt(m1, zlo)
return low and high and mid, True, marg
def c_ov(F, m, cmax=20):
p = F.p
for c in range(cmax + 1):
ok = True
for t in range(p):
P = [QF(1)]
for i in range(c + 2):
P.append(P[-1] * F.r[(t + i) % p])
# P[k + 1] = |theta_(t+k) / theta_(t-1)|
ok &= le(QF(m) * (P[c + 1] + P[c + 2]), P[2])
if ok:
return c
return None
def real_ok(win):
p = win.F.p
for t in range(p):
for f in (True, False):
for d in win.replies(f, t):
if forbidden(win, t, f, d):
return False
return True
def stranded(win, Hs):
"""[(key, d)]: keys of the hull with no valid move after reply d."""
p = win.F.p
out = []
for G, H, f, t in sorted(Hs):
for d in win.replies(f, t):
G1, H1 = win.pre(G, H, t, d)
if not win.moves(G1, H1, d == 0, (t + 1) % p):
out.append(((G, H, f, t), d))
return out
def main():
t0 = time.time()
maps = (2, 3, 4, 5) + ((6, 7, 8, 9) if WIDE else ())
n = kill_ov = fault_ov = gain = 0
p1_bad = conj_bad = 0
pieces_inf = cert_inf = unint = 0
unc_cells, unc_list = [], []
margins = []
sound_bad = sound_n = plant_hit = direct_inf = 0
ctl_a, ctl_b = [], None
zeta_off, enum_off, per_cell = 0.0, 0, {}
for name, per in PERIODIC:
F = Field(per)
p = F.p
s_all = [back_ratio(F, t) for t in range(p)]
for t in range(p):
conj_bad += not eq(conj(F.r[t]), QF(0) - inv(s_all[t]))
zeta_off = max(zeta_off,
abs(inv(s_all[t]).f - conj_ratios(per)[t]))
for m in maps:
n += 1
cinf = least(F, m, "pin")
cov = c_ov(F, m)
creal = None
for c in range(16):
win = Window(F, m, c)
if win.pin_starts()[1]:
continue
if real_ok(win):
creal = c
break
kill_ov += creal != cov
fault_ov += (creal is not None and cov is not None
and creal > cov)
gain += creal is not None and cinf < creal
if name.startswith("golden"):
ctl_a.append(cov)
if m == 2:
pcs = forbidden(Window(F, 2, 3), 0, True, 0)
ctl_b = any(eq(a, QF(9, -4)) and eq(b, QF(18, -8))
and not ca and not cb
for a, b, ca, cb in pcs)
for c in range(cinf + 1):
win = Window(F, m, c)
st, miss = win.pin_starts()
if miss:
continue
co = Coords(F, m, c)
zhi, _b1 = hull(win, co, st)
zlo, _b2 = hull(win, co, st, low=True)
Hs = hull_set(win, co, zlo, zhi)
mus = [mu_of(F, co, t) for t in range(p)]
strand = stranded(win, Hs)
if c == cinf:
direct_inf += len(strand)
for G, H, f, t in Hs:
u = QF(G) * inv(s_all[t]) + QF(H)
p1_bad += not eq(co.Z(G, H, t), co.kap[t] * u)
cert = {}
for t in range(p):
for f in (True, False):
for d in win.replies(f, t):
for pc in forbidden(win, t, f, d):
args = (F, co, t) + pc + (zlo[(t, f)],
zhi[(t, f)])
ok, integ, mg = certify(*args, mus[t])
okp = certify(*args, mus[t] * QF(4))[0]
cert[(t, f, d, pc)] = (ok, okp)
if c != cinf:
continue
pieces_inf += 1
cert_inf += ok
key = f"{name.split()[0]} x{m}"
a0, b0 = per_cell.get(key, (0, 0))
per_cell[key] = (a0 + 1, b0 + ok)
unint += not integ
if mg is not None:
margins.append(mg)
if not ok:
cell = f"{name.split()[0]} x{m}"
if cell not in unc_cells:
unc_cells.append(cell)
if len(unc_list) < 6:
unc_list.append(
(cell, t, f, d,
round(pc[0].f, 5),
round(pc[1].f, 5)))
sset = set(strand)
for (G, H, f, t) in Hs:
y = QF(H) - F.r[t] * G
for d in win.replies(f, t):
inn = any((le(ya, y) if ca else lt(ya, y)) and
(le(y, yb) if cb else lt(y, yb))
for ya, yb, ca, cb in
forbidden(win, t, f, d))
enum_off += inn != (((G, H, f, t), d) in sset)
for (G, H, f, t), d in strand:
y = QF(H) - F.r[t] * G
for (t2, f2, d2, pc), (ok, okp) in cert.items():
if (t2, f2, d2) != (t, f, d):
continue
ya, yb, ca, cb = pc
if ((le(ya, y) if ca else lt(ya, y)) and
(le(y, yb) if cb else lt(y, yb))):
sound_n += 1
sound_bad += ok
plant_hit += okp
print(f" {name:20s} x{m} c_inf {cinf} c_real {creal} "
f"c_ov {cov}", flush=True)
print("== CONTROLS")
print(f" (a) golden: c_ov {ctl_a} against the closed form "
f"{[4, 5, 5, 6, 6, 7, 7, 7][:len(ctl_a)]}")
print(f" (b) golden x2, c = 3, phase 0, full, zero reply: the open "
f"gap (phi^-6, 2 phi^-6) among the forbidden pieces: {ctl_b}")
print(f" (c) SOUNDNESS: stranded (key, reply) pairs of H(c), c <= "
f"c_inf, inside a forbidden piece: {sound_n}; in a certified "
f"piece: {sound_bad}; stranded at c_inf (direct): {direct_inf}")
print(f" (e) (key, reply) pairs of H(c), c <= c_inf, the "
f"forbidden pieces and the direct enumeration rule apart: "
f"{enum_off}")
print(f" (d) THE PLANT (mu x 4): stranded pairs in a piece it "
f"certifies: {plant_hit}")
print("== P1: THE CONJUGATE")
print(f" conj(r_t) != -1/s_t at {conj_bad} phases; keys of H(c_inf) "
f"with Z != kappa_t u: {p1_bad}; |1/s_t - zeta'_t| "
f"(flush.conj_ratios) at most {zeta_off:.1e}")
print("== Q1: THE REAL LINE")
print(f" c_real > c_ov (instrument fault) at {fault_ov} cells; "
f"c_inf < c_real at {gain} of {n} cells")
print(f" KILL: c_real != c_ov at {kill_ov} of {n} cells")
print("== Q2: THE CERTIFICATE at c_inf")
print(f" forbidden pieces {pieces_inf}, certified {cert_inf}, ends "
f"not integral {unint}")
if margins:
print(f" low-side margin (x1 + x2) / L where read: least "
f"{min(margins):.4f}, over {len(margins)} pieces")
print(f" per cell (pieces, certified): {per_cell}")
print(f" uncertified, first ones: {unc_list}")
print(f" KILL: uncertified forbidden intervals at c_inf: "
f"{pieces_inf - cert_inf} at {len(unc_cells)} cells "
f"({', '.join(unc_cells) or '-'})")
checks = [
ctl_a == [4, 5, 5, 6, 6, 7, 7, 7][:len(ctl_a)], ctl_b,
sound_bad == 0 and direct_inf == 0, enum_off == 0, plant_hit > 0,
conj_bad == 0 and p1_bad == 0 and zeta_off < 1e-12,
kill_ov == 0 and fault_ov == 0, gain == 6,
(pieces_inf, cert_inf, unint) == (22, 7, 0),
unc_cells == ["bronze x3", "V1 x2", "V1 x3", "V2 x4"],
per_cell == {"golden x2": (2, 2), "silver x2": (4, 4),
"bronze x3": (6, 0), "V1 x2": (6, 1),
"V1 x3": (2, 0), "V2 x4": (2, 0)},
bool(margins) and round(min(margins), 4) == 0.1458,
]
print(f" {sum(checks)}/{len(checks)} checks as recorded, "
f"{time.time() - t0:.1f} s")
sys.exit(0 if all(checks) else 1)
if __name__ == "__main__":
main()