"""check_proof.py for #16 1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA (proof.md, stage informal_proof).

Every section re-checks claims of proof.md by EXACT simulation of the machine (pure Python, bytearray tape) or by
exact integer arithmetic; nothing is read from earlier output files.  Exhaustive small boxes plus random large ones.
Sections (proof.md section in brackets):
  A  [1]   rule table; TM5 of FractalType4.v is this table with states renamed (A..F -> B,C,D,E,A,F)
  B  [3.1] shift rules (single block, exhaustive) and their n-fold forms (random n)
  C  [3.3] staircase: P(a) (TM5's P, renamed) holds exactly for a in the level set S, for a <= AMAX; TM5's
           Inc1/Incs1 renamed; the 9-step start gadget after P(S)
  D  [3.2] one-trip lemmas BounceE / BounceP with exact step formulas: next left-turn frame, exhaustive box + random
  E  [4]   soundness of the whole macro rule set (scripts/macro_sim3.py): from every frame of a small grammar box
           (and random larger frames) the exact run visits the next K macro frames in order, without halting
  F  [7]   initial segment: blank -> base hub 0^inf <A (10)^85 (011010)^7 (10)^46 0^inf in exactly 46,734 steps
  G  [5]   invariant H*c4 (scripts/inv4.py Hc4): from blank; random long orbits and random short seeds (narrow
           generators, supporting evidence only)
  H  [5.3] G-step algebra: zipper families are swapped by B'(k) = 2 tau - B(k-1) (exhaustive small + random)
  I  [6]   halting: the only halting precursor (eat of an odd (10)-run) halts; negative controls of E are not met
  J  [5.2] skeptic round 1 repairs: the counterexamples to H*c3 are outside H*c4; Hc4 is total; CP on orbits
  K  [5.5] EXHAUSTIVE back-solved closure boxes (every zipper tail, both modes, clean/level/top): long E and long
           P (CP) right ends must close in one step (PASS required); short right ends are reported as OPEN
           (the short-regime clause Hs_K is a look-ahead and is not inductive: proof.md section 8, G1)
  L  [4.4, 5.5, 8] skeptic round 2 (scripts/round2.py): the window start formula (exact), what follows it (exact where
           ruled; the unruled corners and the glued wall are OPEN); long boxes at S = 168; the short kinds on wider boxes
           (E1w, P1w, Pt1 OPEN; Et1, Eseg must close); the Reflect-into-top chain (OPEN).  Leak counts are lower bounds.
  M  [4.4] round 2: RightEndP with P = 2 at a wall = RightEndP to P = 0 + Absorb0 (exact, with a negative control)
OPEN lines document known gaps (they are not counted as PASS or FAIL); SUMMARY lists them.
usage: nice -n 10 .venv/bin/python -B check_proof.py [quick]      (quick = smaller boxes)"""
import sys, os, random, itertools, time, collections
HERE = os.path.dirname(os.path.abspath(__file__))
SC = os.path.join(HERE, 'scripts')
sys.path.insert(0, SC)
sys.set_int_max_str_digits(0)
QUICK = len(sys.argv) > 1 and sys.argv[1] == 'quick'
TMS = '1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA'
TM5 = '1RB0RE_1RC0RF_0LD---_1LA1LE_1RA0LB_1LC1RE'      # verify/FractalType4.v Module TM5

def table(s):
    T = []
    for row in s.split('_'):
        r = []
        for j in range(2):
            x = row[3 * j:3 * j + 3]
            r.append(None if x == '---' else (int(x[0]), 1 if x[1] == 'R' else -1, 'ABCDEF'.index(x[2])))
        T.append(r)
    return T
T = table(TMS)
RES = collections.OrderedDict()
EVS1 = collections.Counter()      # event names met in E1 (used by E2)
def report(name, ok, detail='', open_=False):
    RES[name] = (ok, detail, open_)
    print('%-58s %s  %s' % (name, ('OPEN' if ok else 'FAIL(open item changed)') if open_ else ('PASS' if ok else 'FAIL'), detail), flush=True)

# ---------------------------------------------------------------- configurations
def parse(s):
    """'0^inf (10)^3 <A (011010)^2 010 0^inf' -> (cells, head index, state); <S: head on the last cell of the left
    part; S>: head on the first cell of the right part"""
    cells = []; head = None; st = None
    for tk in s.split():
        if tk == '0^inf': continue
        if tk[0] == '<': st = 'ABCDEF'.index(tk[1]); head = len(cells) - 1; continue
        if tk[-1] == '>': st = 'ABCDEF'.index(tk[0]); head = len(cells); continue
        if tk[0] == '(':
            w, n = tk[1:].split(')^') if ')^' in tk else (tk[1:-1], 1)
            cells += [int(c) for c in w] * int(n)
        else: cells += [int(c) for c in tk]
    return cells, head, st

def key(t, p):
    a = t.find(1); b = t.rfind(1)
    a = min(a, p) if a >= 0 else p; b = max(b, p)
    return bytes(t[a:b + 1]), p - a

def frame_key(s):
    cells, head, st = parse(s)
    pad = 8; t = bytearray(pad) + bytearray(cells) + bytearray(pad + 2)
    return key(t, head + pad)

def visit_seq(start, targets, cap, first_only=False):
    """exact run from start; at every standard left-turn frame (A reads 0 after a left move, cell p-2 = 0) compare with
    the next target (trimmed tape + head offset).  Returns ('ok', steps at each target) / ('halt', n) /
    ('cap', number matched) / ('miss', number matched) (first_only: the first standard frame must be the target)."""
    cells, head, st = parse(start)
    tk = [frame_key(x) for x in targets]
    pad = min(2 * len(cells) + 400 + cap // 40, 4 * 10 ** 6)
    t = bytearray(pad) + bytearray(cells) + bytearray(pad); p = pad + head
    lastL = any(x.startswith('<') for x in start.split())
    lo = min(pad, p); hi = max(pad + len(cells), p)
    i = 0; n = 0; at = []
    TT = T
    while n < cap:
        if st == 0 and lastL and t[p] == 0 and t[p - 2] == 0 and n > 0:
            w = t[lo:hi + 1]; a = w.find(1); b = w.rfind(1)
            a = min(a + lo, p) if a >= 0 else p; b = max(b + lo, p)
            if (p - a) == tk[i][1] and t[a:b + 1] == tk[i][0]:
                at.append(n); i += 1
                if i == len(tk): return ('ok', at)
            elif first_only:
                return ('miss', i)
        tr = TT[st][t[p]]
        if tr is None: return ('halt', n)
        t[p] = tr[0]; p += tr[1]; st = tr[2]; n += 1; lastL = tr[1] < 0
        if p < lo:
            lo = p
            if p < 3: return ('cap', i)
        elif p > hi:
            hi = p
            if p > len(t) - 3: return ('cap', i)
    return ('cap', i)

# ---------------------------------------------------------------- A
def sec_A():
    T5 = table(TM5); ren = {0: 1, 1: 2, 2: 3, 3: 4, 4: 0, 5: 5}     # TM5 A..F -> #16 B,C,D,E,A,F
    ok = True
    for s5 in range(6):
        for r in range(2):
            a, b = T5[s5][r], T[ren[s5]][r]
            if a is None or b is None: ok &= (a is None and b is None)
            else: ok &= (a[0], a[1], ren[a[2]]) == b
    report('A1 TM5 (FractalType4.v) = #16 under A..F -> B,C,D,E,A,F', ok)
    und = [(s, r) for s in range(6) for r in range(2) if T[s][r] is None]
    report('A2 one undefined transition, D1', und == [(3, 1)], str(und))
    # A3: every halting run of length <= 3 from any state/window passes B reading 0, then C reading 0, then D reading 1
    # (D is entered only by C0 and F0; F only by C1, which writes the 0 that F0 sends D back to; C by A1, which writes
    # the 0 that C0 sends D onto, or by B0).  So the only halting pattern is  B> 0 0 1.
    seqs = set(); n = 0
    for st in range(6):
        for w in itertools.product([0, 1], repeat=7):
            t = list(w); p = 3; s_ = st; hist = []
            for k in range(2):
                tr = T[s_][t[p]]
                if tr is None: break
                hist.append(('ABCDEF'[s_], t[p])); t[p] = tr[0]; p += tr[1]; s_ = tr[2]
            if len(hist) == 2 and T[s_][t[p]] is None: seqs.add(tuple(hist)); n += 1
    ok = seqs == {(('B', 0), ('C', 0))}
    preds = sorted({('ABCDEF'[s_], r) for s_ in range(6) for r in range(2) if T[s_][r] and T[s_][r][2] == 3})
    report('A3 halting needs B> 0 0 1 (D entered by C0/F0 only)', ok and preds == [('C', 0), ('F', 0)],
           'D entered by %s; every 2-step history before D1 is %s (%d windows)' % (preds, sorted(seqs), n))

# ---------------------------------------------------------------- B
def run_window(w, st, pos, nmax=10 ** 5):
    w = list(w); n = 0
    while 0 <= pos < len(w):
        tr = T[st][w[pos]]
        if tr is None: return None
        w[pos] = tr[0]; pos += tr[1]; st = tr[2]; n += 1
        if n > nmax: return None
    return ('R' if pos >= len(w) else 'L', st, w, n)

SHIFTS = [   # (direction, state in, word, word out, state out, steps)   proof.md 3.1
    ('R', 'A', '01', '10', 'A', 2), ('R', 'B', '10', '01', 'B', 2), ('R', 'B', '011010', '101101', 'B', 6),
    ('L', 'A', '01', '10', 'A', 4), ('L', 'E', '110110', '011010', 'E', 14), ('L', 'A', '101101', '100110', 'A', 14),
]
def sec_B():
    ok = True; bad = []
    for d, si, w, wo, so, ns in SHIFTS:
        wl = [int(c) for c in w]; s = 'ABCDEF'.index(si)
        r = run_window(wl, s, 0 if d == 'R' else len(wl) - 1)
        good = r is not None and r[0] == d and r[1] == 'ABCDEF'.index(so) and ''.join(map(str, r[2])) == wo and r[3] == ns
        ok &= good
        if not good: bad.append((d, si, w))
        # n-fold form, random n, inside random context (context must not matter: window never left)
        for n in [1, 2, 3, 7, random.randint(8, 60)]:
            r = run_window(wl * n, s, 0 if d == 'R' else len(wl) * n - 1)
            good = r is not None and r[0] == d and ''.join(map(str, r[2])) == wo * n and r[3] == ns * n
            ok &= good
            if not good: bad.append((d, si, w, n))
    report('B1 shift rules (6 rules, single block + n-fold)', ok, '%d rules %s' % (len(SHIFTS), bad[:2]))
    # B2 right turn: x B> 010 010 -->(5) x <A 101010, for any cell x (5 steps B0 C1 F0 D0 E1, D reads the 0 C1 wrote)
    ok = True
    for x in (0, 1):
        t = [x, 0, 1, 0, 0, 1, 0]; p = 1; st = 1
        for k in range(5):
            tr = T[st][t[p]]; t[p] = tr[0]; p += tr[1]; st = tr[2]
        ok &= p == 0 and st == 0 and t == [x, 1, 0, 1, 0, 1, 0]
    report('B2 right turn  x B> 010 010 -->(5) x <A 101010', ok)

# ---------------------------------------------------------------- C
def levels(n):
    S = [0]
    while S[-1] <= n: S.append(2 * S[-1] + (3 if S[-1] % 2 == 0 else 2))
    return S

def P_holds(a, ctx, cap=10 ** 7):
    """TM5's P a renamed: l (01)^a B> 0^inf -->* l <C 01 (010)^a 0^inf, with the run never reading l"""
    lc = list(ctx); pad = 4
    t = [0] * pad + lc + [0, 1] * a + [0] * (3 * a + 60); lo = pad + len(lc); p = lo + 2 * a; st = 1; n = 0
    while n < cap:
        tr = T[st][t[p]]
        if tr is None: return ('halt', n)
        t[p] = tr[0]; p += tr[1]; st = tr[2]; n += 1
        if p < lo:
            if st == 2 and p == lo - 1 and t[lo:lo + 2 + 3 * a] == [0, 1] + [0, 1, 0] * a and not any(t[lo + 2 + 3 * a:]):
                return ('ok', n)
            return ('left', n)
    return ('cap', n)

def S1(a, b, c, d):      # TM5 S1 l a b c d = l (01)^a <A 1 (011010)^b (10)^c 0 (100)^d 0^inf; TM5 A = #16 B
    return '0^inf 1 (01)^%d <B 1 (011010)^%d (10)^%d 0 (100)^%d 0^inf' % (a, b, c, d)

def sec_C():
    AMAX = 60 if QUICK else 130
    L = levels(AMAX); hold = [a for a in range(AMAX + 1) if P_holds(a, [1, 1, 0, 1])[0] == 'ok']
    report('C1 P(a) holds exactly for a in S = {0,3,8,19,40,83,...}, a<=%d' % AMAX, hold == [x for x in L if x <= AMAX], str(hold))
    ok = True
    for S in [x for x in levels(2000) if x <= 1400]:
        for ctx in ([], [1], [1, 0, 1], [0, 1, 1, 0, 1, 0]):
            ok &= P_holds(S, ctx, cap=10 ** 8)[0] == 'ok'
    report('C2 P(S) for S in levels <= 1400, 4 left contexts (l never read)', ok)
    # Inc1 renamed: S1 l (2+a) b c (2+d) -->* S1 l a (1+b) (2+c) d
    ok = True; cnt = 0
    box = itertools.product(range(0, 4), range(0, 3), range(0, 3), range(0, 4)) if True else []
    for a, b, c, d in box:
        r = visit_any(S1(2 + a, b, c, 2 + d), S1(a, 1 + b, 2 + c, d), 'C', 10 ** 5); ok &= r; cnt += 1
    for _ in range(20 if QUICK else 60):
        a, b, c, d = [random.randint(0, 40) for _ in range(4)]; n = random.randint(1, 30)
        r = visit_any(S1(2 * n + a, b, c, 2 * n + d), S1(a, n + b, 2 * n + c, d), 'C', 10 ** 7); ok &= r; cnt += 1
    report('C3 TM5 Inc1 / Incs1 renamed (box 4x3x3x4 + random n)', ok, '%d instances' % cnt)
    # start gadget: l (01)^m <C 01 (010)^S 0^inf -->(9) l (10)^(m-2) <A (10)(011010)(010)^(S-1) 0^inf, m >= 2
    ok = True; cnt = 0
    for S in [x for x in levels(500) if x >= 1 and x <= 400]:
        for m in list(range(2, 8)) + [random.randint(8, 300)]:
            st = '0^inf 1 (01)^%d <C 01 (010)^%d 0^inf' % (m, S)
            tg = '0^inf 1 0 (10)^%d <A (10) (011010) (010)^%d 0^inf' % (m - 2, S - 1)
            r = visit_seq(st, [tg], 50, first_only=True); ok &= r[0] == 'ok' and r[1] == [9]; cnt += 1
    report('C4 start gadget after P(S): 9 steps to the fresh bouncer', ok, '%d instances' % cnt)

def visit_any(start, target, st_letter, cap):
    """run until the configuration (tape key + head + state) equals target's (any state letter)"""
    c0, h0, s0 = parse(start); c1, h1, s1 = parse(target)
    pad = 400 + cap // 20; pad = min(pad, 2 * 10 ** 6)
    t = bytearray(pad) + bytearray(c0) + bytearray(pad); p = pad + h0; st = s0
    t1 = bytearray(pad) + bytearray(c1) + bytearray(pad); k1 = key(t1, pad + h1)
    n = 0
    while n < cap:
        tr = T[st][t[p]]
        if tr is None: return False
        t[p] = tr[0]; p += tr[1]; st = tr[2]; n += 1
        if st == s1 and t[p] == t1[pad + h1] and key(t, p) == k1: return True
    return False

# ---------------------------------------------------------------- D
def ystr(Y):
    s = ' (10)^%d' % Y[0] if Y[0] else ''
    for i in range(1, len(Y), 2): s += ' (011010)^%d' % Y[i] + (' (10)^%d' % Y[i + 1] if Y[i + 1] else '')
    return s
ZS = ['', ' (011010)^1 (10)^2 (010)^1', ' (10)^2 (010)^3', ' (011010)^2 (10)^4 (010)^2 (011010)^1 (10)^2 (010)^1']
XS = ['', ' (10)^2 (101)^2', ' (10)^5 (101)^3 (10)^4 (101)^4']

def bounceE(Y, d, Z):
    B = sum(Y[1::2]); A = sum(Y[0::2])
    st = '0^inf <A' + ystr(Y) + ' (010)^%d' % (d + 2) + Z + ' 0^inf'
    Y2 = list(Y); Y2[0] += 2; Y2[-1] += 2
    tg = '0^inf <A' + ystr(Y2) + (' (010)^%d' % d if d else '') + Z + ' 0^inf'
    return st, tg, 10 + 20 * B + 6 * A

def bounceP(X, P, Y, d, Z):
    B = sum(Y[1::2]); Ap = sum(Y[2::2])
    st = '0^inf' + X + ' (10)^%d <A' % (P + 2) + ystr(Y) + ' (010)^%d' % (d + 2) + Z + ' 0^inf'
    Y2 = list(Y); Y2[1] += 1; Y2[-1] += 2
    tg = '0^inf' + X + ' (10)^%d <A' % P + ystr(Y2) + (' (010)^%d' % d if d else '') + Z + ' 0^inf'
    return st, tg, 22 + 20 * B + 6 * Ap

def ys(nseg, vals, a0vals, akvals):
    for a0 in a0vals:
        for k in range(1, nseg + 1):
            for inner in itertools.product(vals, repeat=2 * k - 1):
                bs = inner[0::2]; ais = inner[1::2]
                for ak in akvals:
                    Y = [a0]
                    for j in range(k):
                        Y += [bs[j], ais[j] if j < k - 1 else ak]
                    yield Y

def sec_D():
    vals = [1, 2] if QUICK else [1, 2, 3]
    ok = True; cnt = 0; bad = []
    for Y in ys(2, vals, [1, 2, 3, 4], [0, 1, 2, 3]):
        for d in [0, 1, 2, 3]:
            for Z in ZS[:3]:
                st, tg, ns = bounceE(Y, d, Z)
                r = visit_seq(st, [tg], ns + 5, first_only=True); g = r[0] == 'ok' and r[1] == [ns]
                ok &= g; cnt += 1
                if not g and len(bad) < 3: bad.append((Y, d, Z, r))
    for _ in range(30 if QUICK else 100):
        Y = [random.randint(1, 200)]
        for j in range(random.randint(1, 4)): Y += [random.randint(1, 200), 2 * random.randint(1, 100)]
        Y[-1] = random.randint(0, 200); d = random.randint(0, 300); Z = random.choice(ZS)
        st, tg, ns = bounceE(Y, d, Z)
        r = visit_seq(st, [tg], ns + 5, first_only=True); g = r[0] == 'ok' and r[1] == [ns]; ok &= g; cnt += 1
        if not g and len(bad) < 3: bad.append((Y, d, Z, r))
    report('D1 BounceE: next frame, steps 10+20B+6A', ok, '%d instances %s' % (cnt, bad[:1]))
    ok = True; cnt = 0; bad = []
    for Y in ys(2, vals, [1], [0, 1, 2, 3]):
        for P in [2, 3, 4, 5]:
            for d in [0, 1, 2, 3]:
                for Z in ZS[:3]:
                    for X in XS[:2]:
                        st, tg, ns = bounceP(X, P, Y, d, Z)
                        r = visit_seq(st, [tg], ns + 5, first_only=True); g = r[0] == 'ok' and r[1] == [ns]
                        ok &= g; cnt += 1
                        if not g and len(bad) < 3: bad.append((X, P, Y, d, Z, r))
    for _ in range(30 if QUICK else 100):
        Y = [1]
        for j in range(random.randint(1, 4)): Y += [random.randint(1, 200), 2 * random.randint(1, 100)]
        Y[-1] = random.randint(0, 200); d = random.randint(0, 300); Z = random.choice(ZS); X = random.choice(XS)
        P = random.randint(2, 300)
        st, tg, ns = bounceP(X, P, Y, d, Z)
        r = visit_seq(st, [tg], ns + 5, first_only=True); g = r[0] == 'ok' and r[1] == [ns]; ok &= g; cnt += 1
        if not g and len(bad) < 3: bad.append((X, P, Y, d, Z, r))
    report('D2 BounceP: next frame, steps 22+20B+6A\'', ok, '%d instances %s' % (cnt, bad[:1]))

# ---------------------------------------------------------------- E
import macro_sim3 as MS
from corner_hybrid import mtostr

def macro_targets(m0, K, maxev=400):
    """the next macro frames after m0 (K non-bounce events, every frame recorded)"""
    ev = []; out = []; m = m0; n = 0
    for _ in range(maxev):
        m = MS.step(m, ev)
        out.append(m)
        if ev[-1] not in ('BounceP', 'BounceE'): n += 1
        if n >= K: break
    return out, ev

def standard(m):
    return (m.edge or m.P >= 2 or (m.P == 1 and not m.X)) and all(p >= 0 for p, q in m.X)

def box_frames(quick):
    v = [1, 2] if quick else [1, 2, 3]
    Ys = list(ys(2, v, [1], [0, 1, 2, 4]))
    Zs = [[], [([1, 2], 1)], [([1, 2], 0)], [([2, 4], 2)], [([1, 2], 2), ([1, 2], 1)]]
    Xs = [[], [(2, 2)], [(3, 3)], [(4, 2)], [(1, 1)], [(2, 2), (5, 3)]]
    for X in Xs:
        for P in [1, 2, 3, 4, 5, 6]:
            for Y in Ys:
                for d in [0, 1, 2, 3, 4, 5]:
                    for Z in Zs:
                        yield MS.M(False, X, P, Y, d, Z)
    for a0 in [1, 2, 3, 5]:
        for Y in Ys:
            for d in [0, 1, 2, 3, 4]:
                for Z in Zs:
                    Y2 = [a0] + Y[1:]
                    yield MS.M(True, [], 0, Y2, d, Z)

def check_macro(m0, K, cap):
    try: tg, ev = macro_targets(m0, K)
    except (MS.Unruled, ValueError, IndexError) as e: return 'unruled', str(e)[:30], None   # outside every rule's domain
    tgs = [x for x in tg if standard(x)]
    if not tgs: return 'skip', None, None
    strs = [mtostr(x) for x in tgs]
    if sum(len(s) for s in strs) > 20000: return 'skip', None, None
    r = visit_seq(mtostr(m0), strs, cap)
    return r[0], tuple(e for e in ev if e not in ('BounceP', 'BounceE')), strs

def sec_E():
    K = 3; cnt = collections.Counter(); evs = collections.Counter(); bad = []; t0 = time.time()
    for m0 in box_frames(QUICK):
        if not m0.edge and m0.Y[0] != 1: continue
        r, ev, strs = check_macro(m0, K, 3 * 10 ** 6)
        cnt[r] += 1
        if r == 'ok':
            for e in ev: evs[e] += 1
        elif r not in ('unruled', 'skip') and len(bad) < 4: bad.append((repr(m0), r, ev))
    ok = cnt['ok'] > 0 and all(k in ('ok', 'unruled', 'skip') for k in cnt)
    report('E1 macro rules sound on the small box (K=%d events)' % K, ok,
           '%s (%.0f s) %s' % (dict(cnt), time.time() - t0, bad[:2]))
    print('    event counts in E1:', dict(evs.most_common()))
    EVS1.update(evs)
    # random larger frames with walls / chunks, both modes, values up to 60
    cnt = collections.Counter(); bad = []; evs2 = collections.Counter(); t0 = time.time(); n = 0
    while n < (150 if QUICK else 600):
        edge = random.random() < 0.3
        Y = [random.choice([1, 3, 5, 2 * random.randint(1, 30) + 1]) if edge else 1]
        for j in range(random.choice([1, 1, 2, 3])): Y += [random.randint(1, 30), 2 * random.randint(1, 15)]
        Y[-1] = random.randint(0, 40)
        X = []
        if not edge:
            for j in range(random.choice([0, 0, 1, 2])):
                q = random.randint(1, 30); X.append((q % 2 + 2 * random.randint(1, 15), q))
        Z = []
        for j in range(random.choice([0, 0, 1, 2])):
            L = [random.randint(1, 10), 2 * random.randint(1, 8)]
            if random.random() < 0.3: L += [random.randint(1, 10), 2 * random.randint(1, 8)]
            Z.append((L, random.randint(1, 20)))
        m0 = MS.M(edge, X, 0 if edge else random.randint(2, 60), Y, random.randint(0, 60), Z)
        r, ev, strs = check_macro(m0, 3, 3 * 10 ** 7)
        if r == 'skip': continue
        n += 1; cnt[r] += 1
        if r == 'ok':
            for e in ev: evs2[e] += 1
        elif r != 'unruled' and len(bad) < 4: bad.append((repr(m0), r, ev))
    for _ in range(60 if QUICK else 300):      # rare families: EatChunkP (P large, d = 1), EatLast, V1 with d = 1
        kind = random.choice(['eatP', 'eatlast', 'v1d1'])
        Y = [1, random.randint(1, 9), random.randint(0, 9)]
        if kind == 'eatP':
            L = [random.randint(1, 5), 2 * random.randint(1, 5)]; B, A = L
            m0 = MS.M(False, random.choice([[], [(4, 2)]]), 4 * B + 2 * A + 2 + random.randint(0, 9), Y, 1, [(L, random.randint(1, 9))])
        elif kind == 'eatlast':
            L = [random.randint(1, 5), 2 * random.randint(1, 5) - 1]; B, A = L
            m0 = MS.M(False, [], 4 * B + 2 * A + 2 + random.randint(0, 9), Y, 1, [(L, 0)])
        else:
            q = random.randint(1, 12); m0 = MS.M(False, [(q + 3 + random.randint(0, 9), q)], 3, Y, 3, [])
        r, ev, strs = check_macro(m0, 3, 3 * 10 ** 7)
        if r == 'skip': continue
        cnt[r] += 1
        if r == 'ok':
            for e in ev: evs2[e] += 1
        elif r != 'unruled' and len(bad) < 4: bad.append((repr(m0), r, ev))
    ok = all(k in ('ok', 'unruled') for k in cnt)
    report('E2 macro rules sound on random frames (values <= 60)', ok, '%s (%.0f s) %s' % (dict(cnt), time.time() - t0, bad[:2]))
    print('    event counts in E2:', dict(evs2.most_common()))
    # negative controls: perturb the first target by one unit; the exact run must not visit it (same budget)
    random.seed(7); nn = 0; hit = 0
    for m0 in box_frames(True):
        if nn >= (20 if QUICK else 60): break
        if not m0.edge and m0.Y[0] != 1: continue
        try: tg, ev = macro_targets(m0, 1)
        except (MS.Unruled, ValueError, IndexError): continue
        tgs = [x for x in tg if standard(x)]
        if not tgs or random.random() < 0.7: continue
        m1 = tgs[-1].copy(); m1.Y[-1] += 1
        nn += 1; r = visit_seq(mtostr(m0), [mtostr(m1)], 2 * 10 ** 5); hit += r[0] == 'ok'
    report('E3 negative controls (target ak+1) not reached', hit == 0, '%d/%d reached' % (hit, nn))

# ---------------------------------------------------------------- F
def sec_F():
    target = '0^inf <A (10)^85 (011010)^7 (10)^46 0^inf'
    r = visit_seq('0^inf A> 0^inf', [target], 50000)
    # exactness: blank start has lastL False; first standard frame equal to the hub must be at 46,734
    report('F1 blank -> base hub [85,7,46] at step 46,734', r[0] == 'ok' and r[1] == [46734], str(r))
    # the macro orbit from the base hub against exact simulation: first right ends, in order
    m = MS.M(True, [], 0, [85, 7, 46], 0, []); ev = []; fr = []
    while len(fr) < (40 if QUICK else 120):
        m = MS.step(m, ev)
        if standard(m): fr.append(mtostr(m))
        if sum(len(x) for x in fr[-1:]) > 30000: break
    cap = 10 ** 7 if QUICK else 6 * 10 ** 7
    r = visit_seq('0^inf <A (10)^85 (011010)^7 (10)^46 0^inf', fr, cap)
    got = len(r[1]) if r[0] == 'ok' else r[1]
    report('F2 macro orbit from the base hub = exact run, in order', r[0] in ('ok', 'cap') and got >= 25,
           '%d of %d macro frames met in order within %d steps (%s)' % (got, len(fr), cap, r[0]))

# ---------------------------------------------------------------- G
def sec_G():
    os.environ.setdefault('LOOKK', '4')
    import seed_clause as SCL, hubinv_H, inv4
    t0 = time.time()
    o = SCL.orbit((True, [], 0, [85, 7, 46]), 600 if QUICK else 2000)
    bad = [i for i, (x, e) in enumerate(o) if inv4.Hc4(x)]
    report('G1 H*c4 at every right end from blank (%d)' % len(o), not bad, '(%.0f s) %s' % (time.time() - t0, bad[:3]))
    for smax, seed in ((5459, 11), (1e30, 12)):
        random.seed(seed); n = 0; leaks = collections.Counter(); t0 = time.time(); nre = 0
        N = 150 if QUICK else 600
        while n < N:
            R = hubinv_H.rnd_R(random.choice(['Rc', 'Rt']), 0, smax)
            if R is None or hubinv_H.H(R) is not None: continue
            n += 1
            try: oo = SCL.orbit(R, 20)
            except MS.Unruled as e: leaks['unruled ' + str(e)[:30]] += 1; continue
            for x, ev in oo[1:]:
                nre += 1; h = inv4.Hc4(x)
                if h: leaks[h] += 1; break
        report('G2 rnd_R long orbits (narrow generator), 20 trav., S<=%g' % smax, not leaks,
               '%d orbits, %d right ends, leaks %s (%.0f s)' % (N, nre, dict(leaks), time.time() - t0))
    for smax, seed in ((5459, 13), (1e30, 14)):
        random.seed(seed); n = 0; leaks = collections.Counter(); t0 = time.time(); kinds = collections.Counter()
        N = 150 if QUICK else 600
        while n < N:
            r = SCL.rnd_short(smax)
            if r is None: continue
            kind, R = r
            if inv4.Hc4(R): continue
            n += 1; kinds[kind] += 1
            try: oo = SCL.orbit(R, 20)
            except MS.Unruled as e: leaks['unruled ' + str(e)[:30]] += 1; continue
            for x, ev in oo[1:]:
                h = inv4.Hc4(x)
                if h: leaks[h] += 1; break
        report('G3 rnd_short seeds in H*c4 (narrow generator), S<=%g' % smax, not leaks,
               '%d seeds %s, leaks %s (%.0f s)' % (N, dict(kinds), dict(leaks), time.time() - t0))

# ---------------------------------------------------------------- J
def sec_J():
    """skeptic round 1: counterexamples to H*c3 (all in H*c3, all outside H*c4); totality; CP on orbits"""
    import seed_clause as SCL, inv4
    cases = [  # (R, clause of H*c4 that rejects it, what the skeptic found)
        ((True, [], 0, [9, 20, 24, 2, 24, 20, 39]), "H2t'", 'next right end [73,4,40,12,4,12,79] is a window'),
        ((True, [], 0, [35, 13, 30, 14, 18, 2, 40]), 'HL', 'gives a P-mode right end with walls'),
        ((True, [], 0, [79, 2, 40, 1, 40]), 'HL', 'unruled RightEndP P=2 with walls'),
        ((False, [], 5, [1, 27, 28, 15, 14, 1, 41]), 'CP', 'next E hub [257,2,104] has b1 even'),
        ((False, [], 1, [1, 41, 40, 1, 41]), 'CP', 'unruled V1 d=1 at the p=-1 wall'),
        ((False, [], 23, [1, 9, 8, 1, 9]), 'CP', 'unruled EatLast runs out of P')]
    ok = True; det = []
    for R, cl, why in cases:
        h3 = SCL.Hc3(R); h4 = inv4.Hc4(R)
        good = h3 is None and h4 is not None and h4.startswith(cl)
        ok &= good; det.append('%s:%s' % (cl, 'ok' if good else (h3, h4)))
    report('J1 skeptic counterexamples: in H*c3, rejected by H*c4', ok, ' '.join(map(str, det)))
    # totality: Hc4 never raises on a small box of short right ends, incl. the E hub [12,2,2] (Hc3 raised TypeError)
    n = 0; err = []; old_err = 0
    for ak in range(1, 23):
        for b1 in range(1, 9):
            for a in range(1, 25):
                for R in ((True, [], 0, [a, b1, ak]), (False, [], a, [1, b1, ak])):
                    n += 1
                    try: inv4.Hc4(R)
                    except Exception as e: err.append((R, type(e).__name__))
                    try: SCL.Hc3(R)
                    except TypeError: old_err += 1
                    except Exception: pass
    report('J2 Hc4 is total (no exception) on a box of short right ends', not err and old_err > 0,
           '%d right ends, %d exceptions (Hc3 raised TypeError on %d of them)' % (n, len(err), old_err))
    # round 2: fuzz with degenerate tuples (ak <= 0, segment-less [0], negative entries, walls, P <= 0)
    rs = random.getstate(); random.seed(11); err = []; cnt = collections.Counter()
    def rv(): return random.choice([0, 1, 2, 3, random.randrange(-1, 12), random.randrange(1, 400), 2 * random.randrange(1, 200)])
    for i in range(10000 if QUICK else 60000):
        edge = random.random() < 0.5; k = random.choice([0, 0, 1, 1, 2, 3, 5])
        Y = [rv() for _ in range(2 * k + 1)]
        X = [] if random.random() < 0.9 else [(rv(), rv())]
        P = 0 if edge else random.choice([0, 1, 2, 3, rv()])
        try: h = inv4.Hc4((edge, X, P, Y)); cnt['member' if h is None else ('degenerate' if h.startswith('H0 degen') else 'rejected')] += 1
        except Exception as e: err.append(((edge, X, P, Y), type(e).__name__))
    random.setstate(rs)
    report('J2b Hc4 total on fuzzed tuples incl. degenerate ones', not err, '%s, %d exceptions %s' % (dict(cnt), len(err), err[:2]))
    c = inv4.cp_test(31, 100 if QUICK else 300, 5459)
    report('J3 CP: every long P-mode right end on orbits has P = 2B(3)-2tau+3', c['CP holds'] == c['long P-mode right ends'] > 0,
           '%d/%d (blank 1,500 right ends + rnd_R orbits x 40)' % (c['CP holds'], c['long P-mode right ends']))

# ---------------------------------------------------------------- K
def sec_K():
    """exhaustive back-solved boxes: every tail of the zipper at the given levels, every length up to MMAX pairs"""
    import inv4, io, contextlib
    def quiet(f, *a):
        buf = io.StringIO()
        with contextlib.redirect_stdout(buf): r = f(*a)
        return r
    t0 = time.time(); c, lk = quiet(inv4.box, 'E', [3, 8, 19, 40], 8)
    report('K1 long E hubs, S<=40, <=8 pairs: next right end in H*c4', c['members'] > 20000 and not lk,
           '%d members of %d candidates, next in H*c4 %d, leaks %d %s (%.0f s)' % (c['members'], c['candidates'], c['next in H*c4'], sum(lk.values()), dict(lk), time.time() - t0))
    t0 = time.time(); c, lk = quiet(inv4.box, 'P', [3, 8, 19, 40], 6)
    report('K2 long P-mode right ends (P from CP), S<=40: next in H*c4', c['members'] > 15000 and not lk,
           '%d members of %d candidates, next in H*c4 %d (all next short: %d), leaks %d %s (%.0f s)' % (c['members'], c['candidates'], c['next in H*c4'], c['next short'], sum(lk.values()), dict(lk), time.time() - t0))
    if not QUICK:
        t0 = time.time(); c, lk = quiet(inv4.box, 'E', [83], 8)
        report('K3 long E hubs, S=83, <=8 pairs: next right end in H*c4', c['members'] > 180000 and not lk,
               '%d members, next in H*c4 %d, leaks %d (%.0f s)' % (c['members'], c['next in H*c4'], sum(lk.values()), time.time() - t0))
    if not QUICK:   # one two-step leak at S = 83: long E -> long P -> window E hub [1485,15,335] (OPEN, proof.md section 8 G2)
        t0 = time.time(); c, lk = quiet(inv4.box, 'P', [83], 6)
        report('K6 long P-mode right ends (CP), S=83: next in H*c4', sum(lk.values()) == 1 and lk.get('next not in H*c4: H2 window') == 1,
               '%d members, next in H*c4 %d, leaks %d %s (%.0f s) -- the leak is P=31 [1,35,36,34,52,30,56,29,110,82,164] -> window hub [1485,15,335]' % (
                   c['members'], c['next in H*c4'], sum(lk.values()), dict(lk), time.time() - t0), open_=True)
    # short right ends: the look-ahead clause Hs_4 is not inductive (OPEN, proof.md section 8 G1)
    t0 = time.time(); leaks = collections.Counter(); mem = 0; ex = []
    for ak in range(1, 41):
        for b1 in range(1, 21):
            for a in range(1, 81):
                R = (True, [], 0, [a, b1, ak])
                if inv4.Hc4(R): continue
                mem += 1
                o, err = inv4.succ(R)
                if err: leaks[err] += 1; ex.append(R); continue
                h = inv4.Hc4(o[1][0])
                if h: leaks[h.split(':')[0]] += 1; ex.append(R)
    report('K4 short E hubs [a0<=80,b1<=20,ak<=40] in H*c4: next in H*c4', bool(leaks) and all(tuple(R[3]) in ((79, 12, 32), (77, 12, 34), (75, 12, 36)) for R in ex),
           '%d members, %d leak %s: %s -- Hs_4 is a look-ahead and not inductive (%.0f s)' % (mem, len(ex), dict(leaks), [R[3] for R in ex], time.time() - t0), open_=True)
    o = inv4.orbit((True, [], 0, [79, 12, 32]), 9)
    seq = [('E' if x[0] else 'P%d' % x[2]) + ('W' if x[1] else '') for x, ev in o]
    walls = [i for i, (x, ev) in enumerate(o) if x[1]]
    report('K5 [79,12,32]: short chain reaches a P-mode right end with walls', bool(walls),
           'right ends %s; walls at index %s; outside H*c4 at %s' % (' '.join(seq), walls, [i for i, (x, ev) in enumerate(o) if inv4.Hc4(x)]), open_=True)


# ---------------------------------------------------------------- L
def sec_L():
    """skeptic round 2: the window family, wider short boxes, multi-step chains (scripts/round2.py)"""
    import inv4, round2 as R2, io, contextlib
    def quiet(f, *a):
        buf = io.StringIO()
        with contextlib.redirect_stdout(buf): r = f(*a)
        return r
    # L1: the Clean start formula also holds for window right ends (exact)
    rng = random.Random(21); n = 0; bad = []; t0 = time.time(); dl = collections.Counter()
    for S in ([8, 19, 40] if QUICK else [8, 19, 40, 83]):
        Sn = 2 * S + (3 if S % 2 == 0 else 2)
        for ak in range(2 * S - 1, Sn - 1):
            for _ in range(3 if QUICK else 6):
                kind = rng.choice(['E1', 'E2', 'P1', 'P2'])
                b1 = rng.randint(1, 30); a1 = 2 * rng.randint(1, 30); b2 = rng.randint(1, 30)
                if kind[0] == 'E':
                    Y = [2 * rng.randint(0, 60) + 1, b1] + ([a1, b2] if kind == 'E2' else []) + [ak]
                    m0 = MS.M(True, [], 0, Y, 0, []); V = MS.hub_walls(Y, (Y[0] - 1, 2 * Y[1]))
                else:
                    P = 2 * rng.randint(1, 60) + 1; Y = [1, b1] + ([a1, b2] if kind == 'P2' else []) + [ak]
                    m0 = MS.M(False, [], P, Y, 0, []); V = MS.hub_walls(Y, (P - 2, 2 * Y[1] + 1))
                tgt = MS.M(False, MS.normX(V), ak - S, [1, 1, 0], S - 1, [])
                r = visit_seq(mtostr(m0), [mtostr(tgt)], 3 * 10 ** 6)
                n += 1; dl[ak - 2 * S + 1] += 1
                if r[0] != 'ok': bad.append((kind, Y, r))
    report('L1 window right end: Clean start F_P(V, ak-S, [1,1,0], S-1)', not bad,
           '%d window right ends (S<=%d, delta counts %s), %d misses %s (%.0f s)' % (n, 40 if QUICK else 83, dict(dl), len(bad), bad[:2], time.time() - t0))
    # L2: with the WindowStart rule, delta = 0 window right ends are ruled by the existing rules (exact, 3 events);
    #     delta in {1, 2} stop at RightEndP P in {2,3} with walls or a V1 right end with walls
    rng = random.Random(22); cnt = collections.Counter(); bad = []; t0 = time.time(); why = collections.Counter()
    with R2.window_patch():
        for S in ([8, 19, 40] if QUICK else [8, 19, 40, 83]):
            Sn = 2 * S + (3 if S % 2 == 0 else 2)
            for ak in range(2 * S - 1, Sn - 1):
                dlt = ak - 2 * S + 1
                for _ in range(6 if QUICK else 15):
                    Y = [2 * rng.randint(1, 60) + 1, rng.randint(1, 30)] + ([2 * rng.randint(1, 30), rng.randint(1, 30)] if rng.random() < 0.5 else []) + [ak]
                    m0 = MS.M(True, [], 0, Y, 0, [])
                    ch = R2.chain((True, [], 0, Y), 1)
                    if ch[0][0] == 'UNRULED':
                        cnt['delta %d unruled' % dlt] += 1; why['delta %d: %s' % (dlt, ch[0][1][:28])] += 1; continue
                    cnt['delta %d ruled' % dlt] += 1
                    r = check_macro(m0, 3, 3 * 10 ** 6)
                    if r[0] not in ('ok', 'skip', 'cap'): bad.append((Y, r[0], r[1]))
                    cnt['exact ' + r[0]] += 1
    report('L2 WindowStart + existing rules: exact (3 events) wherever ruled', not bad and cnt['exact ok'] > 0,
           '%s, %d exact misses %s (%.0f s)' % (dict(cnt), len(bad), bad[:2], time.time() - t0))
    report('L2b WindowStart: the unruled cases (RightEndP P<=3 at a wall, V1 right end with walls)', len(why) > 0,
           '%s -- delta in {1,2} always, delta = 0 when a Push1End is followed by a V1 right end at the next wall, '
           'e.g. [25,6,28,13,79] (proof.md 4.4, 8 G2)' % dict(why), open_=True)
    # L3: the V1 right end with walls writes (101)^q 1 (101)^r: a left word outside the grammar ('111' never occurs in
    #     a wall stack (10)^p (101)^q); exact run from the delta = 1 window hub [21,3,38] (S = 19)
    cells, head, st = parse('0^inf <A (10)^21 (011010)^3 (10)^38 0^inf')
    pad = 20000; t = bytearray(pad) + bytearray(cells) + bytearray(pad); p = pad + head; nst = 0; found = None; lastL = True
    while nst < 2 * 10 ** 6 and found is None:
        tr = T[st][t[p]]
        if tr is None: found = ('halt', nst); break
        t[p] = tr[0]; p += tr[1]; st = tr[2]; nst += 1
        if st == 0 and tr[1] < 0 and t[p] == 0:
            left = bytes(t[max(0, p - 4000):p + 1])
            if b'\x01\x01\x01' in left: found = ('glued wall', nst)
    report('L3 delta=1 window hub [21,3,38]: left word (101)^q 1 (101)^r appears', bool(found) and found[0] == 'glued wall',
           '%s -- a tape form outside the grammar of proof.md section 2' % (found,), open_=True)
    if QUICK: return
    # L4/L5: long boxes at S = 168 (one step)
    t0 = time.time(); c, lk = quiet(inv4.box, 'P', [168], 6)
    report('L4 long P box S=168 (<=6 pairs, CP): next in H*c4', True,
           '%d members, next in H*c4 %d, leaks %d %s (%.0f s) -- the window family (lower bound)' % (
               c['members'], c['next in H*c4'], sum(lk.values()), dict(lk), time.time() - t0), open_=True)
    t0 = time.time(); c, lk = quiet(inv4.box, 'E', [168], 8)
    report('L5 long E box S=168 (<=8 pairs): next right end in H*c4 (one step)', c['members'] > 10 ** 6 and not lk,
           '%d members, next in H*c4 %d, leaks %d (%.0f s)' % (c['members'], c['next in H*c4'], sum(lk.values()), time.time() - t0))
    ch = R2.chain((True, [], 0, [201, 36, 136, 52, 120, 56, 116, 57, 226, 138, 275]), 2)
    report('L5b two-step window leak from a long E member at S=168', inv4.Hc4((True, [], 0, [201, 36, 136, 52, 120, 56, 116, 57, 226, 138, 275])) is None
           and ch[0][2] is None and ch[1][2] == 'H2 window',
           '[201,36,136,52,120,56,116,57,226,138,275] -> P%d %s -> %s' % (ch[0][0][2], ch[0][0][3], ch[1][0][3]), open_=True)
    # L6: short kinds on wider boxes (the skeptic's round-2 boxes)
    for mode, expect_clean in (('Et1', True), ('Eseg', True), ('P1w', False), ('E1w', False), ('Pt1', False)):
        t0 = time.time(); c, lk, ex = quiet(R2.short_box, mode)
        det = '%d members of %d, next in H*c4 %d, leaks %d %s (%.0f s)' % (c['members'], c['candidates'], c['next in H*c4'], sum(lk.values()), dict(lk), time.time() - t0)
        if expect_clean: report('L6 short box %s: next in H*c4' % mode, c['members'] > 0 and not lk, det)
        else: report('L6 short box %s: next in H*c4' % mode, True, det + ' e.g. %s' % (str(list(ex.values())[:1])[:160]), open_=True)
    # L7: an H*c4 member reaches an unruled 'reflect not clean' (U24) within 4 traversals
    ch = R2.chain((True, [], 0, [255, 35, 3]), 6)
    report('L7 [255,35,3] (in H*c4) reaches an unruled event', inv4.Hc4((True, [], 0, [255, 35, 3])) is None and ch[-1][0] == 'UNRULED',
           ' -> '.join(('P%d ' % x[0][2] if not x[0][0] else 'E ') + str(x[0][3]) if x[0] != 'UNRULED' else 'UNRULED ' + x[1] for x in ch), open_=True)


# ---------------------------------------------------------------- M
def sec_M():
    """skeptic round 2: one corner of the window family ruled -- RightEndP with P = 2 at a wall (row U4) is RightEndP to
    P = 0 followed by Absorb0 (scripts/round2.py corner_patch); exact for 2 events, plus a negative control"""
    import round2 as R2
    def frames(n, seed):
        rng = random.Random(seed)
        for i in range(n):
            nw = rng.choice([1, 1, 2, 3])
            X = [(2 * rng.randint(1, 15), 2 * rng.randint(1, 10)) for _ in range(nw)]
            Y = [1, rng.randint(1, 12)] + ([2 * rng.randint(1, 10), rng.randint(1, 10)] if rng.random() < 0.4 else []) + [rng.randint(1, 40)]
            yield MS.M(False, X, 2, Y, 1, [])
    c = collections.Counter(); bad = []; t0 = time.time()
    with R2.corner_patch():
        for m0 in frames(100 if QUICK else 300, 5):
            r = check_macro(m0, 2, 4 * 10 ** 6); c[r[0]] += 1
            if r[0] not in ('ok', 'unruled', 'skip', 'cap'): bad.append((m0.X, m0.Y, r[0]))
    report('M1 RightEndP P=2 at a wall = RightEndP to P=0 + Absorb0 (exact, 2 events)', not bad and c['ok'] > 0.7 * sum(c.values()),
           '%s, %d misses %s (%.0f s)' % (dict(c), len(bad), bad[:2], time.time() - t0))
    orig = MS.step; hit = 0; n = 0
    def wrong(s, ev):
        if not s.edge and s.d == 1 and not s.Z and s.P == 2 and s.X:
            s = s.copy(); s.Y[1] += 1; s.Y[-1] += 2; s.d = 0; s.P = 0; ev.append('Wrong'); MS.absorb(s, 0, ev, 'Absorb0')
            if not s.edge and s.P < 2: return MS.virtual(s, ev)
            return s
        return orig(s, ev)
    MS.step = wrong
    try:
        for m0 in frames(20 if QUICK else 40, 6):
            r = check_macro(m0, 2, 4 * 10 ** 6)
            if r[0] == 'unruled': continue
            n += 1; hit += r[0] == 'ok'
    finally: MS.step = orig
    report('M2 negative control (ak + 2 instead of ak + 1) never reached', hit == 0 and n > 0, '%d/%d reached' % (hit, n))
    # how much of the window family this corner rule absorbs (macro level only)
    rng = random.Random(22); why = collections.Counter()
    with R2.window_patch(), R2.corner_patch():
        for S in [8, 19, 40, 83]:
            Sn = 2 * S + (3 if S % 2 == 0 else 2)
            for ak in range(2 * S - 1, Sn - 1):
                for _ in range(15):
                    Y = [2 * rng.randint(1, 60) + 1, rng.randint(1, 30)] + ([2 * rng.randint(1, 30), rng.randint(1, 30)] if rng.random() < 0.5 else []) + [ak]
                    ch = R2.chain((True, [], 0, Y), 1)
                    why['delta %d %s' % (ak - 2 * S + 1, 'ruled' if ch[0][0] != 'UNRULED' else ch[0][1][:28])] += 1
    report('M3 window hubs with WindowStart + RightEndP2W: what is still unruled', True,
           '%s -- the V1 right end with walls remains (proof.md 8 G2)' % dict(sorted(why.items())), open_=True)

# ---------------------------------------------------------------- H
def Bs(z):
    out = [0] * (len(z) + 2); acc = 0
    for l in range(len(z), 0, -1):
        acc += z[l - 1] if l % 2 == 0 else -z[l - 1]; out[l] = acc
    return out
def zip_ok(b, k, tau):
    e = b[k + 1] % 2
    return b[k] == (2 * b[k + 1] + 4 + e if k % 2 == 0 else 2 * b[k + 1] - 2 * tau - 4 - e)

def sec_H():
    """if B'(k) = 2 tau - B(k-1) for all k in a range, then the even-k zipper at k for B' is equivalent to the odd-k
    zipper at k-1 for B, and the odd-k zipper at k for B' to the even-k zipper at k-1 for B (exact identities)"""
    ok = True; n = 0
    rng = range(-12, 13)
    for tau in range(0, 9):
        for x, y in itertools.product(rng, rng):          # x = B(k-1), y = B(k);  B'(k) = 2tau - x, B'(k+1) = 2tau - y
            for kpar in (0, 1):
                bp = {1: 2 * tau - x, 2: 2 * tau - y}       # B' at positions k, k+1 (k has parity kpar)
                lhs = (bp[1] == (2 * bp[2] + 4 + bp[2] % 2 if kpar == 0 else 2 * bp[2] - 2 * tau - 4 - bp[2] % 2))
                rhs = (x == (2 * y - 2 * tau - 4 - y % 2 if kpar == 0 else 2 * y + 4 + y % 2))
                ok &= lhs == rhs; n += 1
    for _ in range(20000):
        tau = random.randint(0, 10 ** 30); x = random.randint(-10 ** 31, 10 ** 31); y = random.randint(-10 ** 31, 10 ** 31)
        if random.random() < 0.5: y = random.randint(-10 ** 31, 10 ** 31); x = 2 * y - 2 * tau - 4 - y % 2
        for kpar in (0, 1):
            bp1, bp2 = 2 * tau - x, 2 * tau - y
            lhs = (bp1 == (2 * bp2 + 4 + bp2 % 2 if kpar == 0 else 2 * bp2 - 2 * tau - 4 - bp2 % 2))
            rhs = (x == (2 * y - 2 * tau - 4 - y % 2 if kpar == 0 else 2 * y + 4 + y % 2))
            ok &= lhs == rhs; n += 1
    report('H1 shift-reflection swaps the two zipper families', ok, '%d cases' % n)
    # on orbits: every G transition satisfies B'(k) = 2 tau - B(k-1) (2 <= k <= 2m-1) and h = 5 + B(1) - e
    import seed_clause as SCL, hubinv_H
    from hubinv_Hc3 import zseq_c
    random.seed(21); g = 0; bad = 0; N = 100 if QUICK else 400
    n = 0
    while n < N:
        R = hubinv_H.rnd_R(random.choice(['Rc', 'Rt']), 0, random.choice([5459, 1e30]))
        if R is None or hubinv_H.H(R) is not None: continue
        n += 1
        try: oo = SCL.orbit(R, 8)
        except MS.Unruled: continue
        for (x0, _), (x1, ev) in zip(oo, oo[1:]):
            if len(x0[3]) < 3 or len(x1[3]) < 3: continue      # segment-less hubs have no z sequence
            k0, t0_, z0 = zseq_c(*x0); k1, t1_, z1 = zseq_c(*x1)
            if z0 is None or z1 is None or t0_ != t1_ or len(z1) != len(z0) + 2 or not x1[0]: continue
            b0 = Bs(z0); b1 = Bs(z1); tau = t0_
            # growth: z' = [h] + z with the tail re-paired; check the band of identities on the shared range
            m = len(z0) // 2
            okk = all(b1[k] == 2 * tau - b0[k - 1] for k in range(2, 2 * m))
            if not okk: continue        # not a growth transition (collapse or short); classified by hubinv_classify
            g += 1
            e = 5 + b0[1] - z1[0]          # new head entry h = z'_1 = 5 + B(1) - e
            bad += e not in (0, 1)
    report('H2 growth transitions on random orbits: B\'(k) = 2tau - B(k-1), head h = 5 + B(1) - e', bad == 0 and g > 0,
           '%d growth transitions, %d with e not in {0,1}' % (g, bad))

# ---------------------------------------------------------------- I
def sec_I():
    # eat of a chunk whose (10)-run is odd: halts (the one halting precursor; G1 excludes it)
    random.seed(5); h = 0; n = 0
    for _ in range(10 if QUICK else 30):
        B = random.randint(1, 6); A = 2 * random.randint(0, 5) + 1; c = random.randint(1, 6)
        st = '0^inf <A (10)^%d (011010)^%d (10)^%d (010)^1 (011010)^%d (10)^%d (010)^%d (011010)^1 (10)^2 0^inf' % (
            2 * random.randint(1, 20) + 1, random.randint(1, 9), 2 * random.randint(0, 9), B, A, c)
        n += 1; r = visit_seq(st, ['0^inf A> 1 0^inf'], 2 * 10 ** 6); h += r[0] == 'halt'
    report('I1 eat of an odd (10)-run in a chunk halts (precursor)', h >= n - 1, '%d/%d halt' % (h, n))

if __name__ == '__main__':
    random.seed(16); t0 = time.time()
    only = sys.argv[2].split(',') if len(sys.argv) > 2 else None
    for name, f in (('A', sec_A), ('B', sec_B), ('C', sec_C), ('D', sec_D), ('E', sec_E), ('F', sec_F), ('G', sec_G),
                    ('H', sec_H), ('I', sec_I), ('J', sec_J), ('K', sec_K), ('L', sec_L), ('M', sec_M)):
        if only and name not in only: continue
        f()
    fails = [k for k, (ok, d, op) in RES.items() if not ok]
    opens = [k for k, (ok, d, op) in RES.items() if op and ok]
    print('SUMMARY %s (%d checks, %d fail; %d OPEN items = known gaps, proof.md section 8) %.0f s' % (
        'PASS' if not fails else 'FAIL', len(RES) - len(opens), len(fails), len(opens), time.time() - t0))
    if opens: print('open:', opens)
    if fails: print('failed:', fails)