strand.py
Cited on: FLUSH.
To run it: save strand.py, with anchors.py, classform.py, decide.py, firstreturn.py, flush.py, gaps.py, hull.py, hullform.py, induct.py, keyweld.py, ostrowski.py, slackbar.py, tie.py, widestep.py beside it; standard library only.
"""
strand.py -- the class step one c below the window's: at c = c_ov - 2,
does some zero-reply piece hold a hull key, and where?
QUESTION. (TRANSPLANT: the hull's bounds are hullform.forms', its ends
a rule at the 136 only; here they are read at the 881 new cells.)
widestep.py reads c_inf in {c_ov - 1, c_ov} at 1001 cells; c_inf >=
c_ov - 1 is not derived. LOW's test fails at c_ov - 2 for free
(D2 below), so its failure proves nothing: the content is a STRANDED
HULL KEY at c_ov - 2, a valid key in a zero-reply gap with Z in the
hull's [Z_lo, Z_hi] (then the closure's ends, open, make it reachable).
DERIVED BY HAND (before the engine).
Notation (slackbar.py's): phase t, a_k = a_(t+k), P_k = |theta_k| of
r_t (P_(-1) = 1, P_0 = r_t), q_k = U_k, K_k = (q_k, p_k), y(K_k) =
(-1)^(k+1) P_k, Z = G + kappa_t y. Gap length at c, phase t:
L(c, t) = m (P_(c+1) + P_(c+2)) - P_2 (classform's convention, read off
pieces(): E_a = m K_E - K_2 + e K_1, E_b = m K_O + e K_1, O/E the odd/
even of c+1, c+2; y_b - y_a = m (P_O + P_E) - P_2). c_ov = least c with
L(c, t) <= 0 at every t (equivalent over phases to keyweld.c_ov).
Let c = c_ov - 2 >= 0 and t a phase with L(c+1, t) > 0 (one exists, c+1
< c_ov). Write lam = L(c, t).
(D1) lam > P_(c+1). Proof: lam = L(c+1, t) + m (P_(c+1) - P_(c+3)) =
L(c+1, t) + m a_(c+3) P_(c+2) > 2 a_(c+3) P_(c+2) >= a_(c+3) P_(c+2) +
P_(c+3) = P_(c+1), using m >= 2, P_(c+3) < P_(c+2), and P_(c+1) =
a_(c+3) P_(c+2) + P_(c+3). (theorem, by hand)
(D2) So every unclipped piece at (t, full) fails the LOW test. From
E_b: K_O has y = +P_O < lam, so {-q_O r} = P_O < lam and n-(lam) <=
q_O; G_b - n- >= (m - 1) q_O + e a_1 >= 1, while the full flag's G_lo
is -(a_1 + 1) + d, d in {-1, 0, 1}, <= -a_1 <= -1. From E_a: K_E has y
= -P_E, so n+(lam) <= q_E; G_a - n+ >= (m - 1) q_E - q_2 + e a_1 >= 0
> G_lo, as E >= 2. Both ends' margins are negative. (theorem, by hand)
So LOW's failure at c_ov - 2 is free, and LOW failing is no proof of
loss: it says the certificate is silent, not that a hull key sits in a
gap. The content of c_inf >= c_ov - 1 is a STRANDED HULL KEY at c_ov - 2
(and then the closure's ends, already open, to make it reachable).
Hand case, golden x3 (c_ov 5, c = 3, phase 0, full flag; r = 1/phi,
P_k = phi^-(k+1), q = 1, 1, 2, 3, 5, 8). lam = 3 P_3 - P_2 = 0.2016 >
P_4 = 0.0902 (D1). a_2 = 1: e = 0 only. E_b = 3 K_5 = (24, 15), y_b =
3 P_5 = 0.1672; E_a = 3 K_4 - K_2 = (13, 8), y_a = -0.0344. Window
(full, c odd: lo = m K_c - K_1, hi = m K_(c+1) - K_0): lo = (8, 5), y =
3 P_3 - P_1 = 0.0557; hi = (14, 9), y = 0.3475. The piece is (0.0557,
0.1672), its lower end closed at (8, 5). Hull G-range on the full flag:
-2 .. 9 (Z_lo = -Z(2, 1), Z_hi = Z(3 K_3) = Z(9, 6)). Keys inside: G = 3,
H = 2: K_3 = (3, 2), y = P_3 = 0.1459, in the piece and the hull. The
closed end (8, 5): Z = 8 + kappa 0.0557 < Z_hi, in the hull. Two
stranded hull keys, one interior (K_c) and one closed end (the window's
lower end).
The closed end in general: c odd, lo = m K_c - K_1, G = m q_c - a_1, Z
= Z_hi - a_1 - kappa P_1 < Z_hi and Z - Z_lo = m q_c + 1 + kappa (m P_c
- P_0) > 0: the full window's lower end is ALWAYS a hull key at c odd.
It is stranded iff it lies inside a gap: (e + 1) P_1 in (m a_(c+2)
P_(c+1), m (P_c + P_(c+1)) - P_2), an interval of length lam, for some
e + 1 in 1 .. a_2. Not forced by lam alone. TRANSPLANT from golden.
QUESTION. At c = c_ov - 2 (>= 0, pinned moves), does some zero-reply
piece hold a hull key, and where?
CELLS: widestep.py's W (1001) and decide.py's 136, deduplicated (1017).
Per cell: c_ov (keyweld), c = c_ov - 2; skip (counted apart) c < 0 and
c without pinned moves (Window.pin_starts misses). Per (t, f), the
pieces (classform.pieces), the hull bounds (hullform.forms); a HULL KEY
IN A PIECE: an integer key (G, H) with y = H - G r_t in the open
(y_a, y_b), or a closed end, with Z in [Z_lo, Z_hi] (exact, QF / lt /
le), G enumerated over floor(Z_lo - kappa y_b) .. ceil(Z_hi - kappa
y_a).
PREDICTIONS.
(D1) lam > P_(c+1) at every (cell, phase) with L(c+1, t) > 0: a proof,
its print a control of the engine's indices.
(D2) LOW fails at every unclipped full-flag piece at those phases:
a proof, likewise.
(H1) at every read cell, some piece at c_ov - 2 holds a hull key.
(H2) at every read cell, some such key lies in a full-flag piece at a
phase with L(c+1, t) > 0 (the named place).
KILL (printed as): "D1 fails at n of N phases"; "D2 fails at n of N
pieces"; "no hull key in any piece at c_ov - 2 at n of N cells" (H1);
"no hull key at the named place at n of N cells" (H2). n > 0 kills
each; D1 or D2 firing is an index fault (the proofs hold), read first.
Printed beside, no kill: per cell the kind of the stranded keys (closed
end; interior; K_c or -K_c or the window's lower end among them) and
counts of each over the read cells; the cells skipped for c < 0 and for
no pinned moves.
CONTROLS (read before the verdicts).
(a) golden x3 at c = 3, phase 0, full flag: the piece (0.0557, 0.1672)
closed below at (8, 5), the hull keys in it exactly {(3, 2), (8, 5)}.
(b) the enumerator's none-direction: at c = c_ov - 1 on the arm (c_inf =
c_ov - 1, every piece passes FORM, so no hull key in any piece), the
enumerator finds 0 hull keys at every arm cell.
(c) beside it, the class step at W: at c_ov - 1 off the arm with pinned
moves (c_inf = c_ov), the cells where no piece holds a hull key,
printed (0 at the 48 by the class step's rule; read, not a kill).
(d) THE PLANT: Z_hi lowered to Z_lo on every flag (the hull a sliver):
H1's line must fire at most cells.
FINDINGS (copied from the run's prints).
CONTROLS. (a) golden x3, c 3, phase 0, full: the piece (0.0557,
0.1672) closed below at (8, 5), hull keys {(3, 2), (8, 5)}: held.
(b) the arm at c_ov - 1: 109 cells, hull keys in pieces at 0.
(c) off the arm with pinned moves at c_ov - 1: 579 cells, no hull
key in any piece at 0: the class step reads c_inf at all 688
cells with pinned moves at c_ov - 1. (d) Z_hi := Z_lo: H1's line
fires at 27 of 115, not "most" as frozen: at the other 88 the
hull's lower end key itself lies in a piece. The line can fire.
CELLS. 1017; c_ov - 2 < 0 at 0; no pinned moves at c_ov - 2 at 902;
read 115. c_inf - c_ov in {-1, 0} at all 1017.
D1, D2: 0 of 152 phases, 0 of 133 pieces (37 cells have no unclipped
full piece at a hot phase): the indices are the proofs'.
H1, H2, KILLS MISSED: a hull key in a piece at c_ov - 2 at all 115, and
at the named place (full flag, hot phase) at all 115.
KINDS. Every read cell holds both a closed end and an interior key in
the hull; +-K_c among them at 23.
AFTER THE RUN (derived by hand from those prints, then printed).
T1 (theorem, by hand; printed apart at 0 of 4018 (cell, c), c = c_ov
- 3 .. c_ov). The pinned key (0, 0) at phase t has the moves (-e, 0),
e = 0 .. a_1, at y = e P_0. The full window is [m P_(c+1) - P_1, P_0
- m P_c] at c even and [m P_c - P_1, P_0 - m P_(c+1)] at c odd
(win_keys' ends), whose top is below P_0, so only e = 0 can be valid:
pinned moves at c iff 0 lies in V(t, full) at every phase, i.e. m
P_(c+1) <= P_1 and m P_c <= P_0 (c even), m P_c <= P_1 and m P_(c+1)
<= P_0 (c odd), at every t.
T2 (theorem). c odd with pinned moves has c >= c_ov - 1. Phase t + 1's
m P_c <= P_1 reads m P_(c+1) <= P_2 in t's scale (P^(t+1)_k = P_(k+1)
/ P_0); then L(c + 1, t) = m (P_(c+2) + P_(c+3)) - P_2 <= m P_(c+1) -
P_2 <= 0, as P_(c+2) + P_(c+3) <= P_(c+1), at every t: c + 1 >= c_ov.
Printed: odd c with pinned moves sit at c - c_ov in {-1, 0}.
T3. At c even the full window's upper end E_h = m K_c - K_0 is a hull
key (theorem): G = m q_c - 1, Z(E_h) = Z_hi - 1 + kappa_t P_0 < Z_hi,
and Z(E_h) - Z_lo = m q_c + a_1 + kappa_t (P_1 - m P_c) > 0, as m P_c
<= P_0 < 1 (T1) and 0 < kappa_t < 1. It lies in the gap e = a_2 - j
iff j P_1 lies in (m a_(c+2) P_(c+1), m (P_c + P_(c+1)) - P_2), an interval of length
L(c, t) (theorem); some phase has such a j at all 115 (rule, verified
at the 115; printed: no phase at 0). Not derived: why a phase must.
A hot phase t places the top j = a_(t+4) under the interval's top
at phase t + 2 (m (P_(c+2) + P_(c+3)) - P_4 > P_2 - P_4 = a_4 P_3 in
t's scale), the bottom unproved; t + 2 strands for some hot t at 78
of the 115 (printed).
So c_inf >= c_ov - 1 reduces to: T3's phase at c_ov - 2 even, and a
stranded hull key forcing a loss (the closure's ends). Printed
beside: every closed end in the hull is the full window's upper end
(others at 0), and the engine's closed-end finds agree with T3's
interval at every (cell, phase).
RUN RECORD. 23.3 s, peak commit 20.8 MB. The engine was written whole
after the freeze, rehearsed on 40 cells, then run once; T1 to T3 and
the closed-end flag line were added after that run, from its prints,
and the whole rerun printed every frozen line unchanged; a review added
the t + 2 count, the closed-end identity and T3's agreement with the
engine. Changed from the freeze: the kinds print as counts over cells,
not per cell, and (c) reads all 1017 cells, not W alone. On shipping,
the verdicts were made the exit code: 0 iff (a) held, (b) at 0 of 109,
(c) at 0 of 579, (d) at 27 of 115, the cells as counted, c_inf -
c_ov in {-1, 0}, D1 to H2 at 0
(of 152 phases, 133 pieces, 115 cells), T1 apart at 0 of 4018 with odd
c at c - c_ov in {-1, 0}, T3's phase at all 115, and the closed-end
lines at 0, 0 and 78 hold as printed.
Usage: python strand.py
"""
import math
import os
import sys
import time
os.environ.setdefault("OPENBLAS_NUM_THREADS", "1")
from flush import PERIODIC # noqa: E402
from decide import FRESH # noqa: E402
from induct import Field, Window, least # noqa: E402
from hull import Coords # noqa: E402
from keyweld import c_ov, lt # noqa: E402
from induct import le, QF # noqa: E402
from firstreturn import l_formula # noqa: E402
from hullform import forms, uv # noqa: E402
from classform import pieces, win_keys, ykey # noqa: E402
from slackbar import low_margin # noqa: E402
from widestep import necklaces # noqa: E402
TOL = 1e-7
def P(F, t, k):
"""P_k = |theta_k| of r_t, exact."""
zero = QF(0)
th = {-1: QF(-1), 0: F.r[t]}
for j in range(k):
th[j + 1] = th[j] * F.a(t + j + 1) + th[j - 1]
x = th[k]
return x if lt(zero, x) else zero - x
def hull_keys(F, co, t, pc, zlo, zhi):
"""[(key, kind)]: hull keys in the piece, kind 'closed' or 'in'."""
ya, yb, ca, cb, Ea, Eb = pc
out = []
for closed, E in ((ca, Ea), (cb, Eb)):
z = co.Z(*E, t)
if closed and le(zlo, z) and le(z, zhi):
out.append((tuple(E), "closed"))
if not lt(ya, yb):
return out
k, r = co.kap[t].f, F.r[t].f
glo = math.floor(zlo.f - k * yb.f) - 1
ghi = math.ceil(zhi.f - k * ya.f) + 1
yaf, ybf, zlf, zhf = ya.f, yb.f, zlo.f, zhi.f
for G in range(glo, ghi + 1):
H = math.floor(yaf + G * r) + 1
for h in (H - 1, H, H + 1):
y = h - G * r
if y < yaf - TOL or y > ybf + TOL:
continue
z = G + k * y
if z < zlf - TOL or z > zhf + TOL:
continue
yq = ykey(F, t, (G, h))
if not (lt(ya, yq) and lt(yq, yb)):
continue
zq = co.Z(G, h, t)
if le(zlo, zq) and le(zq, zhi):
out.append(((G, h), "in"))
return out
def read_c(F, m, c, plant=False):
"""None without pinned moves; else the hull keys in pieces and the
D1, D2 reads at the hot phases (L(c + 1, t) > 0)."""
win = Window(F, m, c)
_st, miss = win.pin_starts()
if miss:
return None
co = Coords(F, m, c)
keys, d1, d2, named, nunc = [], [], [], [], 0
for t in range(F.p):
l1 = l_formula(F, t, m, c + 1)
hot = lt(QF(0), l1)
if hot:
d1.append(lt(P(F, t, c + 1), l_formula(F, t, m, c)))
fm = forms(F, co, m, c, t)
Kc = uv(F, t, c)
lo_full = tuple(win_keys(F, t, m, c, True)[0])
for f in (True, False):
zlo, zhi = fm[(f, True)], fm[(f, False)]
if plant:
zhi = zlo
for pc in pieces(F, t, m, c, f):
for key, kind in hull_keys(F, co, t, pc, zlo, zhi):
tag = kind
if key == tuple(Kc):
tag += "+Kc"
elif key == (-Kc[0], -Kc[1]):
tag += "-Kc"
if f and key == lo_full:
tag += "+lo"
keys.append((t, f, key, tag))
if hot and f:
named.append(key)
if hot and f and not pc[2] and not pc[3]:
nunc += 1
me = low_margin(F, co, t, m, c, f, pc, zlo)
d2.append(me is not None and me <= 0)
return dict(keys=keys, d1=d1, d2=d2, named=named, nunc=nunc)
def zero_in(F, m, c):
"""(T1) V(t, full) holds y = 0 at every phase, by its ends' y."""
for t in range(F.p):
lo, hi = ((c + 1, 1), (c, 0)) if c % 2 == 0 else ((c, 1), (c + 1, 0))
for k, j in (lo, hi):
if not le(P(F, t, k) * m, P(F, t, j)):
return False
return True
def strands_hi(F, m, c, t):
"""(T3) the j in 1 .. a_2 with j P_1 in (m a_(c+2) P_(c+1), m (P_c +
P_(c+1)) - P_2): the full window's upper end m K_c - K_0 in gap
e = a_2 - j, c even."""
A = P(F, t, c + 1) * (m * F.a(t + c + 2))
B = (P(F, t, c) + P(F, t, c + 1)) * m - P(F, t, 2)
return [j for j in range(1, F.a(t + 2) + 1)
if lt(A, P(F, t, 1) * j) and lt(P(F, t, 1) * j, B)]
def cells():
out = {}
for _name, per in list(PERIODIC) + list(FRESH):
for m in range(2, 10):
out[(tuple(per), m)] = None
for per in necklaces():
for m in range(2, 13):
out[(tuple(per), m)] = None
return list(out)
def control_a():
F = Field((1,))
co = Coords(F, 3, 3)
fm = forms(F, co, 3, 3, 0)
got = [(round(pc[0].f, 4), round(pc[1].f, 4), pc[2], tuple(pc[4]),
sorted(hull_keys(F, co, 0, pc, fm[(True, True)],
fm[(True, False)])))
for pc in pieces(F, 0, 3, 3, True)]
print(f" (a) golden x3, c 3, phase 0, full: {got}")
return got == [(0.0557, 0.1672, True, (8, 5),
[((3, 2), "in"), ((8, 5), "closed")])]
def main():
t0 = time.time()
print("== CONTROLS")
ok_a = control_a()
only = int(sys.argv[1]) if len(sys.argv) > 1 else None
rows = []
for per, m in cells()[:only]:
F = Field(per)
cov = c_ov(F, m)
cinf = least(F, m, "pin")
row = dict(per=per, m=m, cov=cov, cinf=cinf, two=None, one=None,
plant=None)
if cov - 2 >= 0:
row["two"] = read_c(F, m, cov - 2)
if row["two"] is not None:
row["plant"] = read_c(F, m, cov - 2, plant=True)
if cov - 1 >= 0:
row["one"] = read_c(F, m, cov - 1)
row["t1"] = []
for c in range(max(cov - 3, 0), cov + 1):
pin = not Window(F, m, c).pin_starts()[1]
row["t1"].append((c, pin, pin == zero_in(F, m, c)))
c = cov - 2
if row["two"] is not None and c % 2 == 0:
row["t3"] = [t for t in range(F.p) if strands_hi(F, m, c, t)]
rows.append(row)
t1 = time.time()
N = len(rows)
arm = [x for x in rows if x["cinf"] == x["cov"] - 1]
b = [x for x in arm if x["one"] is None or x["one"]["keys"]]
print(f" (b) arm at c_ov - 1: {len(arm)} cells; hull keys found (or no "
f"pinned moves) at {len(b)}: {[(x['per'], x['m']) for x in b[:6]]}")
off = [x for x in rows if x["cinf"] == x["cov"] and x["one"] is not None]
cc = [x for x in off if not x["one"]["keys"]]
print(f" (c) off the arm with pinned moves at c_ov - 1: {len(off)}; no "
f"hull key in any piece at {len(cc)}: "
f"{[(x['per'], x['m']) for x in cc[:8]]}")
read = [x for x in rows if x["two"] is not None]
neg = [x for x in rows if x["cov"] - 2 < 0]
nopin = [x for x in rows if x["cov"] - 2 >= 0 and x["two"] is None]
dp = [x for x in read if not x["plant"]["keys"]]
print(f" (d) THE PLANT Z_hi := Z_lo: H1's line fires at {len(dp)} of "
f"{len(read)}")
print(f"== CELLS: {N}; c_ov - 2 < 0 at {len(neg)}; no pinned moves at "
f"c_ov - 2 at {len(nopin)}; read {len(read)}")
print(f" c_inf - c_ov over all: "
f"{sorted(set(x['cinf'] - x['cov'] for x in rows))}")
d1 = [v for x in read for v in x["two"]["d1"]]
d2 = [v for x in read for v in x["two"]["d2"]]
print("== VERDICTS")
print(f" D1 KILL: D1 fails at {d1.count(False)} of {len(d1)} phases")
print(f" D2 KILL: D2 fails at {d2.count(False)} of {len(d2)} pieces; "
f"cells with no unclipped full piece at a hot phase: "
f"{sum(x['two']['nunc'] == 0 for x in read)}")
h1 = [x for x in read if not x["two"]["keys"]]
print(f" H1 KILL: no hull key in any piece at c_ov - 2 at {len(h1)} of "
f"{len(read)} cells: {[(x['per'], x['m']) for x in h1[:8]]}")
h2 = [x for x in read if not x["two"]["named"]]
print(f" H2 KILL: no hull key at the named place at {len(h2)} of "
f"{len(read)} cells: {[(x['per'], x['m']) for x in h2[:8]]}")
kinds = {}
for x in read:
for tg in set(k[3] for k in x["two"]["keys"]):
kinds[tg] = kinds.get(tg, 0) + 1
print(f"== KINDS (cells holding each tag): {dict(sorted(kinds.items()))}")
noclosed = [x for x in read
if not any(k[3].startswith("closed") for k in x["two"]["keys"])]
nokc = [x for x in read
if not any("Kc" in k[3] for k in x["two"]["keys"])]
both = [x for x in noclosed if x in nokc]
print(f" no closed end in the hull at {len(noclosed)}; no +-K_c at "
f"{len(nokc)}; neither at {len(both)}: "
f"{[(x['per'], x['m']) for x in both[:10]]}")
print("== AFTER THE RUN (derived by hand from the first prints)")
tt = [v for x in rows for v in x["t1"]]
print(f" T1: pinned moves iff V(t, full) holds 0 at every phase, apart "
f"at {sum(not v[2] for v in tt)} of {len(tt)} (cell, c), c = c_ov "
f"- 3 .. c_ov")
odd = sorted(set(v[0] - x["cov"] for x in rows for v in x["t1"]
if v[1] and v[0] % 2))
print(f" T2: odd c with pinned moves sit at c - c_ov in {odd}")
ev = [x for x in read if (x["cov"] - 2) % 2 == 0]
print(f" T3: read cells with c_ov - 2 even {len(ev)} of {len(read)}; "
f"no phase stranding the full window's upper end at "
f"{sum(not x.get('t3') for x in ev)}")
oth, apart, n2 = 0, 0, 0
for x in ev:
F, m, c = Field(x["per"]), x["m"], x["cov"] - 2
hot = [t for t in range(F.p)
if lt(QF(0), l_formula(F, t, m, c + 1))]
n2 += any((t + 2) % F.p in x["t3"] for t in hot)
for t in range(F.p):
hi = tuple(win_keys(F, t, m, c, True)[1])
cl = [k for k in x["two"]["keys"]
if k[0] == t and k[3].startswith("closed")]
oth += sum(not (k[1] and k[2] == hi) for k in cl)
apart += bool(cl) != (t in x["t3"])
print(f" closed hull keys other than the full window's upper end: "
f"{oth}; engine's closed finds apart from T3's interval at "
f"{apart} (cell, phase); t + 2 strands for some hot t at {n2} "
f"of {len(ev)}")
checks = [
ok_a,
(len(arm), len(b), len(off), len(cc)) == (109, 0, 579, 0),
(len(dp), len(read)) == (27, 115),
(N, len(neg), len(nopin)) == (1017, 0, 902),
sorted(set(x["cinf"] - x["cov"] for x in rows)) == [-1, 0],
(d1.count(False), len(d1), d2.count(False), len(d2))
== (0, 152, 0, 133),
(len(h1), len(h2)) == (0, 0),
sum(not v[2] for v in tt) == 0 and len(tt) == 4018
and odd == [-1, 0],
(len(ev), sum(not x.get("t3") for x in ev)) == (115, 0),
(oth, apart, n2) == (0, 0, 78),
]
print(f" {sum(checks)}/{len(checks)} checks as recorded; cells "
f"{t1 - t0:.1f} s, all {time.time() - t0:.1f} s")
sys.exit(0 if all(checks) else 1)
if __name__ == "__main__":
main()