#!/usr/bin/env python3
"""check_proof.py, pool #30 = 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.
Checks every numbered claim of proof.md against the Turing machine (exhaustive small cases + random large ones)
and the Lemma D chain on the rules-only orbit and on adversarial residues.
   python3 -B check_proof.py [--quick] [--seed S]      full run (writes data/check_proof_seed<S>.json)
   python3 -B check_proof.py --adv N [--seed S]        stand-alone stress run of the adversarial Lemma D section
Prints one line per claim (PASS/FAIL, instances) and writes data/check_proof.json.
Claim ids match proof.md: W* = window (finite) rules, S* = shift rules, LP* = local pass, RP* = region pass,
B = bounce, E* = eats, R = restart, D6 = nested bounce, H = grammar closure, I = initial segment,
O = model = TM, D.* = Lemma D links, FIN = finite part."""
import sys, os, random, json, time, math, itertools
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, os.path.join(HERE, 'scripts'))
import common
import nest_model as M
from fs_val_rules import inG, inc_rule, rG, rblock, TAILS

QUICK = '--quick' in sys.argv
SEED = int(sys.argv[sys.argv.index('--seed') + 1]) if '--seed' in sys.argv else 1
random.seed(SEED)
TT = common.T
ST = 'ABCDEF'
RES = {}
T0 = time.time()

def rec(cid, ok, info=None):
    r = RES.setdefault(cid, {'n': 0, 'pass': 0, 'fail': []})
    r['n'] += 1; r['pass'] += bool(ok)
    if not ok and len(r['fail']) < 3: r['fail'].append(str(info)[:400])

def rbits(n): return ''.join(random.choice('01') for _ in range(n))
def norm(w): return w.rstrip('0')

# ---------------------------------------------------------------------------------------------------------------
# window runner: a finite rewrite on a window, run for exactly n steps; every executed transition must read a cell
# inside the window, so the rule holds in every context (the cells outside are random junk and never read).
def window(s, h, q, n):
    pad = 8
    tape = bytearray(int(c) for c in rbits(pad) + s + rbits(pad))
    pos = pad + h; q = ST.index(q)
    for _ in range(n):
        if not (pad <= pos < pad + len(s)): return ('READ_OUTSIDE', pos - pad)
        tr = TT[q][tape[pos]]
        if tr is None: return ('HALT',)
        w, d, q = tr; tape[pos] = w; pos += d
    return (''.join(map(str, tape[pad:pad + len(s)])), pos - pad, ST[q])

def wrule(cid, s, h, q, s2, h2, q2, n):
    got = window(s, h, q, n)
    rec(cid, got == (s2, h2, q2), (s, h, q, '->', got, 'expected', (s2, h2, q2)))

# ---------------------------------------------------------------------------------------------------------------
# local pass LP(X): from  junk 011 C> X 0^inf  run until the head first enters the cell left of that 011
# (x0-4). Returns (state, steps, cells x0-3..x0-1, X region normalized). By construction LP never reads x0-4.
def lp(X, maxsteps=10**7):
    junk = rbits(6)
    s = junk + '011' + X
    tape = bytearray(int(c) for c in s) + bytearray(len(X) + 600)
    x0 = len(junk) + 3; pos = x0; q = 2; st = 0
    while st < maxsteps:
        tr = TT[q][tape[pos]]
        if tr is None: return ('HALT', st)
        w, d, q = tr; tape[pos] = w; pos += d; st += 1
        if pos == x0 - 4:
            return (ST[q], st, ''.join(map(str, tape[x0-3:x0])), norm(''.join(map(str, tape[x0:]))))
        if pos >= len(tape) - 2: return ('EDGE', st)
    return ('MAX', st)

def lp_expect(X):
    """LP by the rule table of proof.md section 3.2 (recursive), returns (X', d, steps)"""
    X = norm(X)
    if X == '' or X[0] == '0': return ('1' + X[1:] if X else '1', 0, 4)               # LP0
    if X.startswith('11'):                                                                # LP11
        if len(X) > 2 and X[2] != '0': return None
        return (X[3:], 1, 8)
    if X in LPT: return LPT[X]
    if X.startswith('101'):                                                               # LPC: carry
        j = 3; e = 0
        while X[j:j+3] == '001': j += 3; e += 1
        if X[j:j+3] not in ('000', '00', '0', '') : return None
        R = X[j+3:]
        if len(X) <= j: R = ''
        sub = lp_expect(R)
        if sub is None: return None
        R2, dR, sR = sub
        return ('001' + '001' * (e + dR) + '000' + R2, 0, sR + 8 * e + 20)
    if X.startswith('10001'):                                                             # LP5 (D5)
        j = 5; e = 0
        while X[j:j+3] == '001': j += 3; e += 1
        if X[j:j+3] not in ('000', '00', '0', ''): return None
        R = X[j+3:] if len(X) > j else ''
        R2, dR = inc_rule(R) if inG(R) else (None, None)
        if R2 is None: return None
        return ('01001' + '001' * (e + dR) + '000' + R2, 0, None)
    return None

# the six constant words of LPT (proof.md 3.2): X -> (X', d, steps)
LPT = {}
def build_LPT():
    for w in ['1', '10010001', '10110001', '1000010001', '1001000010001', '10010010001']:
        r = lp(w)
        LPT[w] = (r[3] if r[2] == '100' else r[3][3:], 0 if r[2] == '100' else 1, r[1])

# ---------------------------------------------------------------------------------------------------------------
def section_A():
    """W1..W9: window rules (single es proofs) and S1..S3: shift rules (induction on the window rule)"""
    wrule('W1 Fb on 1:  1 F> 1 -> 1 1 F>', '11', 1, 'F', '11', 2, 'F', 5)
    wrule('W2 F> 001 -> 011 F>', '001', 0, 'F', '011', 3, 'F', 3)
    wrule('W3 F> 000 -> 011 C>', '000', 0, 'F', '011', 3, 'C', 3)
    wrule('W4 C> 101 -> 111 F>', '101', 0, 'C', '111', 3, 'F', 9)
    wrule('W5 011 E> 0 -> E> 0 010 (left step)', '0110', 3, 'E', '0010', 0, 'E', 5)
    wrule('W6 marker turn: 0 E> 0 -> 1 1 F>', '00', 1, 'E', '11', 2, 'F', 3)
    wrule('W7 F> 01 -> 00 F>', '01', 0, 'F', '00', 2, 'F', 2)
    wrule('W8 region entry d=0: 011 <A 100 -> E> 001 000', '011100', 2, 'A', '001000', 0, 'E', 4)
    wrule('W9 region entry d=1: 011 <A 101 -> E> 001 001', '011101', 2, 'A', '001001', 0, 'E', 4)
    wrule('W10 D6 exit: 011 E> 1 -> <A 100 0', '0111', 3, 'E', '1000', -1, 'A', 4)
    wrule('W11 C> 10 -> 11 F>', '10', 0, 'C', '11', 2, 'F', 4)
    for n in range(0, 14):
        wrule('S1 SL: (011)^n E> 0 -> E> 0 (010)^n', '011' * n + '0', 3 * n, 'E', '0' + '010' * n, 0, 'E', 5 * n)
        wrule('S2 SR: F> (001)^n -> (011)^n F>', '001' * n, 0, 'F', '011' * n, 3 * n, 'F', 3 * n)
        wrule('S3 SB: F> 1 (1)^n after a 1:  1 F> 1^n -> 1^(n+1) F>', '1' * (n + 1), 1, 'F', '1' * (n + 1), n + 1, 'F', 5 * n)

def section_RP():
    """RP0 / RP1 in any left context (window starts at the marker)"""
    for n in range(1, 31 if not QUICK else 12):
        for _ in range(4):
            Xp = rbits(random.randint(0, 12)) + '1'
            wrule('RP0  l 0 (011)^n <A 100 X -> l 110 0 (011)^n C> X  [8n+4]',
                  '0' + '011' * n + '100' + Xp, 3 * n, 'A', '1100' + '011' * n + Xp, 3 * n + 4, 'C', 8 * n + 4)
            wrule('RP1  l 0 (011)^n <A 101 000 X -> l 110 0 (011)^(n+1) C> X  [8n+7]',
                  '0' + '011' * n + '101000' + Xp, 3 * n, 'A', '1100' + '011' * (n + 1) + Xp, 3 * n + 7, 'C', 8 * n + 7)

def check_lp(cid, X):
    exp = lp_expect(X)
    got = lp(X)
    if exp is None: rec(cid, False, ('no rule', X, got)); return
    X2, d, st = exp
    ok = got[0] == 'A' and got[2] == ('100' if d == 0 else '101') and \
        (got[3] == norm(X2) if d == 0 else got[3] == norm('000' + X2) or (got[3] == '' and norm(X2) == '')) and \
        (st is None or got[1] == st)
    rec(cid, ok, (X, 'exp', exp, 'got', got))

def section_LP():
    build_LPT()
    # LP0: any word starting with 0 (exhaustive to length 10) and ''
    for L in range(0, 11 if not QUICK else 8):
        for bits in itertools.product('01', repeat=L):
            check_lp('LP0  011 C> 0 r -> <A 100 1 r  [4]', '0' + ''.join(bits))
    check_lp('LP0  011 C> 0 r -> <A 100 1 r  [4]', '')
    for L in range(0, 10 if not QUICK else 7):
        for bits in itertools.product('01', repeat=L):
            check_lp('LP11 011 C> 110 r -> <A 101 000 r  [8]', '110' + ''.join(bits))
    for w in LPT:
        r = lp(w)
        rec('LPT  six constant words (es)', r[0] == 'A' and r[2] in ('100', '101'), (w, r))
    # LPC carry and LP5 (D5) over G rests and over non-G H rests whose LP is itself in the table
    rests = ['', '1', '010001', '110001'] + [rG(4) for _ in range(60 if not QUICK else 20)]
    rests += ['11' + '001' * random.randint(0, 3) + '000' + (rG(3) or '1') for _ in range(20)]
    rests += ['01' + '001' * random.randint(0, 3) + '000' + (rG(3) or '1') for _ in range(20)]
    for e in range(0, 9 if not QUICK else 5):
        for R in rests:
            if lp_expect(R) is None: continue
            check_lp('LPC  011 C> 101 a^e z R -> <A 100 001 a^(e+dR) z R\'  [s(R)+8e+20]',
                     '101' + '001' * e + ('000' + R if R else ''))
            if inG(R):
                check_lp('LP5  011 C> 10 001 a^e z R -> <A 100 01 001 a^(e+d) z inc R', '10001' + '001' * e + ('000' + R if R else ''))
    for _ in range(100 if not QUICK else 30):     # large random G words: GI end to end
        W = rG(12)
        if W.startswith('101') and random.random() < 0.5: W = '101' + '001' * random.randint(10, 40) + W[3:]
        check_lp('LPC  011 C> 101 a^e z R -> <A 100 001 a^(e+dR) z R\'  [s(R)+8e+20]', W)
    # GI = recursive composition; compare with fs_val_rules.inc_rule (the G-level statement)
    for _ in range(300 if not QUICK else 80):
        W = rG(8)
        got = lp(W); exp = inc_rule(W)
        ok = got[0] == 'A' and ((exp[1] == 0 and got[2] == '100' and got[3] == norm(exp[0])) or
                                (exp[1] == 1 and got[2] == '101' and got[3] == norm('000' + exp[0])))
        rec('GI   inc on G = LP0/LP11/LPC composition', ok and inG(exp[0]), (W, exp, got))
    # D6 right pass: 011 C> 10 101 a^e z R  ->  011 1 110 0 (011)^(e+1) C> R
    for e in range(0, 12 if not QUICK else 6):
        for R in ['', '1', rG(3) or '1', rG(5) or '1']:
            s = '011' + '10101' + '001' * e + '000' + R + '0' * 4
            n = 4 + 5 + 2 + 3 * e + 3
            got = window(s, 3, 'C', n)
            exp = ('011' + '1' + '110' + '0' + '011' * (e + 1) + R + '0' * 4, 3 + 5 + 3 * (e + 1), 'C')
            rec('D6a  right pass 011 C> 10 101 a^e z R -> 011 1 110 0 (011)^(e+1) C> R  [3e+14]', got == exp, (e, R, got, exp))

def run_from(tape, pos, q, stop, maxsteps=10**8):
    st = 0
    while st < maxsteps:
        tr = TT[q][tape[pos]]
        if tr is None: return ('HALT', st, pos, q)
        w, d, q = tr; tape[pos] = w; pos += d; st += 1
        r = stop(tape, pos, q, st)
        if r: return (r, st, pos, q)
    return ('MAX', st, pos, q)

def hub_tape(a, b, X, left_junk=True):
    """junk (instead of 0^inf) then (110)^a 0 (011)^b C> X 0^inf; returns tape, pos, marker index, first index"""
    junk = rbits(20) if left_junk else '0' * 20
    s = junk + '110' * a + '0' + '011' * b
    first = len(junk); marker = first + 3 * a; pos = len(s)
    tape = bytearray(int(c) for c in s + X) + bytearray(len(X) + 2000)
    return tape, pos, marker, first

def section_B():
    """B: K(a,b+1,X) -> K(a+1,b+d,X') with X',d from LP, in any left context; never reads left of the marker"""
    pool = []
    k, T = 7, '000010001'
    def tr(a_, b_, w_): pool.append(w_)
    for ep in range(40):
        a, b, w = M.restart(k, T); k, T = M.epoch(a, b, w, tr)
    pool = random.sample(pool, min(len(pool), 400 if not QUICK else 120)) + [rG(6) for _ in range(100)]
    for X in pool:
        try: X2, d = M.inc_h(X)
        except M.Unknown: continue
        a = random.randint(0, 30); b = random.randint(1, 30)
        tape, pos, marker, first = hub_tape(a, b + 1, X)
        s_lp = lp(X)[1]
        n = b                              # region blocks left of the LP block
        steps = s_lp + (8 * n + 4 if d == 0 else 8 * n + 7)
        minpos = [pos]
        def stop(tp, p, q, st):
            minpos[0] = min(minpos[0], p)
            return 'DONE' if st == steps else None
        r = run_from(tape, pos, 2, stop, steps + 1)
        exp = norm('110' * (a + 1) + '0' + '011' * (b + d))
        got = norm(''.join(map(str, tape[first:r[2]])))
        ok = r[0] == 'DONE' and r[3] == 2 and got == exp and \
             norm(''.join(map(str, tape[r[2]:]))) == norm(X2) and minpos[0] >= marker
        rec('B    bounce = LP + RP, any left context, [s_LP + 8b+4 (d=0) | 8b+7 (d=1)]', ok, (a, b, X, X2, d, r[:2]))

def eat_run(a, X, junk=False, maxsteps=10**8):
    """from K(a,1,X) (left of (110)^a: junk or blank, but cell first-1 = 0): run until the head first enters
    first-1 or reaches a hub again; return ('L', E-state ok, k, T) or ('K', a', b', X') with min position"""
    tape, pos, marker, first = hub_tape(a, 1, X, left_junk=junk)
    tape[first - 1] = 0
    mn = [pos]
    def stop(tp, p, q, st):
        mn[0] = min(mn[0], p)
        if p == first - 1: return 'L'
        if q == 2 and tp[p-1] == 1 and tp[p-2] == 1:
            h = common.parse_K(tp, p, first)
            if h and (h[0], h[1]) != (a, 1): return 'K'
        return None
    r = run_from(tape, pos, 2, stop, maxsteps)
    if r[0] == 'L':
        s = norm(''.join(map(str, tape[first:])))
        if r[3] != 4 or not s.startswith('01'): return ('BAD', r)
        j = 2; k = 0
        while s[j:j+3] == '001': j += 3; k += 1
        return ('L', k, s[j:], mn[0] - first, r[1])
    if r[0] == 'K':
        h = common.parse_K(tape, r[2], first)
        return ('K', h[0], h[1], h[2], mn[0] - marker, r[1])
    return r

def section_E():
    for _ in range(600 if not QUICK else 100):
        a = random.choice([random.randint(1, 40), random.randint(1, 400)]); e = random.choice([0, 1, 2, random.randint(0, 25), random.randint(0, 80)]); R = rG(6 if random.random() < 0.7 else 12)
        r = eat_run(a, '001' * (e + 1) + ('000' + R if R else ''), junk=True)
        rec('E1g  K(a,1,a^(e+1) z R) -> K(a+2,e+1,R), never left of the marker', r[:4] == ('K', a + 2, e + 1, norm(R)) and r[4] >= 0, (a, e, R, r))
        Rr = R if R else ''
        R2, d2 = inc_rule(Rr)
        r = eat_run(a, '101' + '001' * e + ('000' + R if R else ''), junk=True)
        rec("E2g  K(a,1,101 a^e z R) ->* L'(a, 000 11 a^(e+d') z inc R), first-1 first visited by E",
            r[:3] == ('L', a, norm('00011' + '001' * (e + d2) + '000' + R2)) and r[3] == -1, (a, e, R, r))
    for a in range(1, 60 if not QUICK else 20):
        r = eat_run(a, '', junk=True); rec("E0   K(a,1,'') ->* L'(a+1, 0001)", r[:3] == ('L', a + 1, '0001') and r[3] == -1, (a, r))
        r = eat_run(a, '1', junk=True); rec("Et1  K(a,1,1) ->* L'(a, 000 01 a z 1)", r[:3] == ('L', a, '000010010001') and r[3] == -1, (a, r))
        r = eat_run(a, '010001', junk=True); rec("Et2  K(a,1,010001) ->* L'(a, 000 10 00 010001)", r[:3] == ('L', a, '0001000010001') and r[3] == -1, (a, r))
        r = eat_run(a, '110001', junk=True); rec('Et3  K(a,1,110001) -> K(a+1,1,001), never left of the marker', r[:4] == ('K', a + 1, 1, '001') and r[4] >= 0, (a, r))

def section_R():
    for _ in range(200 if not QUICK else 60):
        k = random.choice([0, 1, 2, random.randint(0, 60)]); Y = rbits(random.randint(0, 20))
        s = '0' + '101' + '001' * k + '000' + Y
        tape = bytearray(int(c) for c in rbits(10) + s) + bytearray(len(s) + 100)
        pos = 10; steps = 3 * k + 7
        mn = [pos]
        def stop(tp, p, q, st):
            mn[0] = min(mn[0], p); return 'DONE' if st == steps else None
        r = run_from(tape, pos, 0, stop, steps + 1)
        exp = '110' + '0' + '011' * (k + 1)
        got = ''.join(map(str, tape[10:r[2]]))
        rec('R    L(k,000 Y) -> K(1,k+1,Y) in 3k+7, never left of the A cell',
            r[0] == 'DONE' and r[3] == 2 and got == exp and mn[0] >= 10 and
            ''.join(map(str, tape[r[2]:r[2] + len(Y)])) == Y, (k, Y, got, r))

def section_D6():
    """D6 end to end: one TM bounce of '10' b-block(e) z R vs the model's epoch map (no TM inside the model)"""
    n = 0
    for _ in range(250 if not QUICK else 60):
        e = random.choice([0, 1, 1, 2, random.randint(0, 9)])
        R = random.choice(['', '1', rG(5) or '1', rG(5) or '1'])
        X = '10101' + '001' * e + ('000' + R if R else '')
        try: X2, d = M.inc_h(X)
        except M.Unknown: rec('D6   one bounce = sub-epoch to its first left record, then W10', False, X); continue
        a = random.randint(1, 30); b = random.randint(2, 30)
        r = common.bounce(a, b, X)
        rec('D6   one bounce = sub-epoch to its first left record, then W10', r[0] == 'K' and r[1] == a + 1 and r[2] == b - 1 + d and r[3] == norm(X2) and d == 0,
            (a, b, X, X2, r))

# ---------------------------------------------------------------------------------------------------------------
# grammar H (proof.md section 4)
def blocks_prefix(w, i=0):
    """parse c (z c)* from position i; yields every (j, nblocks) where a block ends"""
    out = []
    while True:
        j = M.block_end(w, i)
        if j < 0: return out
        out.append(j)
        if w[j:j+3] != '000': return out
        i = j + 3

ESTAR = set()
def build_estar():
    for w in M.TAILRULES:
        x = w
        while True:
            ESTAR.add(norm(x))
            if inG(norm(x)): break
            x, _ = M.inc_h(x)
    for w in ['010010001']:            # Et1 residue '01' a z 1 and its chain
        x = w
        while not inG(norm(x)):
            ESTAR.add(norm(x)); x, _ = M.inc_h(x)

def inO(w):
    w = norm(w)
    if w in ESTAR: return True
    p, v = w[:2], w[2:]
    if p in ('11', '01'):
        i = 0
        while v[i:i+3] == '001': i += 3
        rest = v[i:]
        if rest == '': return True
        return rest.startswith('000') and inG(norm(rest[3:]))
    if p in ('00', '10'): return inG(norm(v))
    return False

def inH(w):
    w = norm(w)
    if inG(w) or inO(w): return True
    j = M.block_end(w)
    return j > 0 and w[j:j+3] == '000' and len(w) > j + 3 and inH(w[j+3:])

def section_H():
    build_estar()
    words = set()
    smallG = [''] + TAILS
    for k in range(1, 4 if not QUICK else 3):
        for ds in itertools.product('01', repeat=k):
            for es in itertools.product(range(3), repeat=k):
                body = '000'.join(d + '01' + '001' * e for d, e in zip(ds, es))
                for t in [''] + ['000' + x for x in TAILS]:
                    smallG.append(body + t)
    smallG = sorted(set(smallG))
    for W in smallG:
        words.add(W)
        for x in range(3):
            words.add(norm('11' + '001' * x + '000' + W)); words.add(norm('01' + '001' * x + '000' + W))
        words.add(norm('00' + W)); words.add(norm('10' + W))
    words |= ESTAR
    base = sorted(words)
    for w in random.sample(base, min(len(base), 300)):
        for c in ['001', '101', '001001', '101001']:
            words.add(c + '000' + w)
    words = sorted(w for w in words if inH(w))
    tm_sample = set(random.sample(words, min(len(words), 700 if not QUICK else 200)))
    for w in words:
        try: w2, d = M.inc_h(w)
        except M.Unknown: rec('H1   every H word has exactly one LP rule and LP(H) is in H', False, w); continue
        ok = inH(norm(w2))
        if ok and w in tm_sample:
            a = random.randint(1, 20); b = random.randint(2, 20)
            r = common.bounce(a, b, w)
            ok = r[0] == 'K' and r[1] == a + 1 and r[2] == b - 1 + d and r[3] == norm(w2)
        rec('H1   every H word has exactly one LP rule and LP(H) is in H', ok, (w, w2, d))
    for W in smallG:          # every G word has an eat rule, and the eat leaves G / an H residue
        a = random.randint(1, 30)
        r = M.eat(a, W)
        ok = (r[0] == 'K' and inG(norm(r[3]))) or (r[0] == 'L' and r[2].startswith('000') and inH(norm(r[2][3:])))
        rec('H2   every G word has an eat rule; eats leave G or an H residue', ok, (W, r))
    RES['_H_words'] = len(words); RES['_ESTAR'] = sorted(ESTAR)

RHO = {'', '1', '010001', '110001', '001', '101', '001000010001'}
def section_D3():
    """proof.md D.0 / D.3: (i) an O word whose W has a block is never in G (the W-phase ends only at the bare tail);
    (ii) from every O word over a bare tail and every E* word, LP reaches G using only LP0/LP11 (D1-D4) and LPT steps,
    and the final word rho is one of RHO (at most one block, e = 0)"""
    for _ in range(3000 if not QUICK else 600):
        W = rG(6)
        if M.parse_G(W) is None: continue
        x = random.randint(0, 4)
        for w in ['11' + '001' * x + '000' + W, '01' + '001' * x + '000' + W, '00' + W, '10' + W]:
            rec('D.0  an O word whose W has >= 1 block is not in G', not inG(norm(w)), w)
    starts = []
    for t in [''] + TAILS:
        for x in range(7):
            starts += ['11' + '001' * x + '000' + t, '01' + '001' * x + '000' + t]
        starts += ['00' + t, '10' + t]
    for w0 in starts + sorted(ESTAR):
        w = norm(w0); kinds = set()
        while not inG(w):
            s0 = dict(M.STATS); w, d = M.inc_h(w); w = norm(w)
            kinds |= {k for k in M.STATS if M.STATS[k] != s0.get(k, 0)}
        pg = M.parse_G(w)
        ok = w in RHO and kinds <= {'D1', 'D2', 'D3', 'D4'} | {k for k in kinds if k.startswith('T:')} and \
             (pg is None or (len(pg[0]) <= 1 and all(e == 0 for e in pg[1])))
        rec('D.3  end of a digestion: only LP0/LP11/LPT steps, final word rho in {eps, 1, t2, t3, 001, 101, 001000010001}', ok, (w0, w, kinds))

# ---------------------------------------------------------------------------------------------------------------
def section_I():
    want = [('L', 28, 1, '0001'), ('L', 124, 2, '0001000010001'), ('L', 304, 7, '000010001')]
    got = []
    for ev in common.events(400):
        if ev[0] == 'L': got.append(ev)
        if ev[0] == 'HALT': got.append(ev)
    rec('I    blank -> L(1,0001)@28 -> L(2,0001000010001)@124 -> L(7,000010001)@304', got == want, got)

def section_O():
    """model (rules only, FAST counting) vs the TM: first left records by direct Python simulation, and the
    517 records of the stored 1e11 C log"""
    end = 3 * 10**6 if QUICK else 2 * 10**7
    tmL = [(ev[2], ev[3]) for ev in common.events(end) if ev[0] == 'L']
    M.FAST = True
    k, T = 7, '000010001'; ok = True
    for i in range(3, len(tmL)):
        a, b, w = M.restart(k, T); k, T = M.epoch(a, b, w)
        ok &= (k, T) == tmL[i]
    rec('O1   model left records = fresh TM run (Python)', ok and len(tmL) > 10, len(tmL))
    RES['_O1_records'] = len(tmL)
    path = os.path.join(HERE, 'data/fs_orbit_1e11_LE.txt')
    if os.path.exists(path):
        tm = [l.split() for l in open(path) if l.startswith('L')]
        tmL = [(int(f[2]), f[3] if len(f) > 3 else '') for f in tm]
        k, T = tmL[2]; good = 0
        for i in range(3, len(tmL)):
            a, b, w = M.restart(k, T); k, T = M.epoch(a, b, w)
            good += (k, T) == tmL[i]
        rec('O2   model left records = stored 1e11 C log', good == len(tmL) - 3, (good, len(tmL) - 3))
        RES['_O2_records'] = len(tmL) - 3

# ---------------------------------------------------------------------------------------------------------------
# Lemma D (proof.md section 5) on the rules-only orbit (FAST) and on adversarial residues inside the invariant.
# Notation as in proof.md: W = counter part of the residue '11' a^x z W, k = k(W), es = exponents, eta = excess,
# S = suffix sums of eta, c = positions created during the W-phase of the digestion (every tail overflow
# 110001 -> 001, wherever it happens: GI inside LP5/E2g/LPC, GI and fast counting inside D6 sub-epochs, and Et3).
def parse_residue(w):
    V = w[2:]; i = 0
    while V[i:i+3] == '001': i += 3
    x = i // 3; W = V[i+3:]
    p = M.parse_G(W)
    ds, es, t = (p if p else ([], [], ([''] + TAILS).index(W) if W in [''] + TAILS else -1))
    return x, W, ds, es, t

def tau():
    """largest own-level bounce count of an end word (E* and the special sub-residues) until G"""
    best = 0
    for w in list(ESTAR) + ['010010001', '1000010001']:
        x = w; J = 0
        while not inG(norm(x)):
            x, _ = M.inc_h(x); J += 1
        best = max(best, J)
    return best

def chain_absorptions(w):
    A = 0
    while not inG(norm(w)):
        w, d = M.inc_h(w); A += d
    return A

def end_extra():
    """T of proof.md D.3: the most a deepest level adds to its merged block beyond sum(e+2) - 2 and the overflow
    absorptions. After the last strip the word is '10' t2 or '10' t3 (their end chains absorb 5 and 2); a sub-epoch
    that ends in Et2 / Et1 adds 1 (no E2g) plus its chain ('1000010001': 4, '010010001': 1); E0 and the Et3 chain add 2."""
    return max(chain_absorptions('10010001'), chain_absorptions('10110001'),
               1 + chain_absorptions('1000010001'), 1 + chain_absorptions('010010001'), 2)

TEND = 5           # recomputed in main() by end_extra()
TAU_ = 13          # recomputed in main() by tau()

def clog(K, q):
    """max(1, ceil(log2((K+2)/(q+2)))) exactly: the depth of the D.4(c) unrolling"""
    n = 0
    while (q + 2) << n < K + 2: n += 1
    return max(1, n)

def gamma_k(k, K, Dl):
    """Lemma C with S(q) <= clog(K,q)*Dl: the largest c with 3*2^(k+c) <= 9*2^k + A_k - 5,
    A_k = 2 U(0) + sum_{q=1}^{k-1} 2^q U(q) >= sum_{q<k} 2^(q+1) eta_q   (A_0 = 0)"""
    A = 0 if k == 0 else 2 * clog(K, 0) * Dl + sum((1 << q) * clog(K, q) * Dl for q in range(1, k))
    c = 0
    while 3 * 2 ** (k + c + 1) <= 9 * 2 ** k + A - 5: c += 1
    return c

_GC = {}
def Gfix(K):
    """D.7: least G >= K with max_{k<=K} (k + Gamma(k,K)) <= G when Delta = 3G + T - 8; returns (G, Delta)"""
    if K not in _GC:
        G = K
        while True:
            Dl = 3 * G + TEND - 8
            G2 = max(k + gamma_k(k, K, Dl) for k in range(K + 1))
            if G2 <= G: break
            G = G2
        _GC[K] = (G, 3 * G + TEND - 8)
    return _GC[K]
def Delta(K): return Gfix(K)[1]
def U(K, q): return clog(K, q) * Delta(K)
def Gamma(k, K): return gamma_k(k, K, Delta(K))
def xmax(K): return U(K, 0) + Delta(K) + 7            # D.4(b): x <= S(0) + 3(k+c) + T - 1 = S(0) + Delta + 7

def bnd(x, es, k, c, tau_):
    """proof.md D.7: x + 1 + sum_{q < k+c} 2^floor((q+3)/2) (e_q + 4) + 2^floor((k+c+3)/2) (tau+1), e_q = 0 for q >= k"""
    es = list(es) + [0] * c
    return x + 1 + sum(2 ** ((q + 3) // 2) * (e + 4) for q, e in enumerate(es)) + 2 ** ((k + c + 3) // 2) * (tau_ + 1)

_BW = {}
def bnd_worst(K, tau_):
    """max over k <= K of Bnd with c = Gamma(k,K), the extreme profile S(q) = U(K,q) and x = xmax(K)"""
    if K not in _BW:
        best = (-1, -1)
        for k in range(K + 1):
            S = [U(K, q) for q in range(k)] + [0]
            es = [S[q] - S[q + 1] + (1 if q < k - 1 else 0) for q in range(k)]
            best = max(best, (bnd(xmax(K), es, k, Gamma(k, K), tau_), k))
        _BW[K] = best
    return _BW[K]

def N_lo(K): return 2 ** (K + 3) - 2 ** ((Gfix(K)[0] + 1) // 2 + 4)

def analytic_threshold(tau_, KMAX):
    """D.7: kappa = running max of k. F = {kappa : Bnd_worst + 2 > N_lo}; N* = max_F Bnd_worst + 2.
    Exact rows for kappa < KMAX; for kappa >= 64 the closed-form tail bound of D.7 (checked to hold and to dominate)."""
    rows = {K: (bnd_worst(K, tau_), N_lo(K), Gfix(K)) for K in range(KMAX)}
    F = [K for K in rows if rows[K][0][0] + 2 > rows[K][1]]
    Nstar = max(rows[K][0][0] + 2 for K in F)
    rec('D.7m G(kappa) and U(kappa,q) nondecreasing in kappa', all(rows[K][2][0] <= rows[K + 1][2][0] for K in range(KMAX - 1)) and
        all(U(K, q) <= U(K + 1, q) for K in range(KMAX - 1) for q in range(K + 1)), None)
    rec('D.7f failing set F is an initial segment, every kappa in [max F + 1, KMAX) passes', F == list(range(len(F))), F)
    for K in range(16, KMAX):
        L2 = math.log2(K + 2); gam = math.log2(5 * K * L2)
        rec('D.7t G(kappa) <= kappa + gamma(kappa), gamma = log2(5 kappa log2(kappa+2)) (kappa >= 16)', Gfix(K)[0] <= K + gam, (K, Gfix(K)))
        if K >= 64:
            closed = 2 ** (K / 2) * (128 * (K * L2) ** 1.5 + 51 * (K * L2) ** 0.5)
            exact = rows[K][0][0] + 2 + 2 ** ((Gfix(K)[0] + 1) // 2 + 4)
            rec('D.7t closed-form tail bound >= Bnd_worst + 2 + 2^(floor((G+1)/2)+4), and <= 2^(kappa+3) (kappa >= 64)',
                exact <= closed <= 2 ** (K + 3), (K, exact, closed))
    around = {str(K): (rows[K][0][0], rows[K][0][1], rows[K][1], rows[K][2][0], rows[K][2][1], Gamma(K, K))
              for K in range(0, min(KMAX, 22))}
    return max(F), Nstar, around

# overflow counter for the W-phase (proof.md D.0): every 110001 -> 001, in any inc, in fast counting, and Et3
import fs_val_rules as _F
_OV = [0]; _DIG = [False]
def _inc_count(w):
    if w == '': return '1', 0
    if w in _F.TAILS:
        if w == '110001' and _DIG[0]: _OV[0] += 1
        return {'1': ('010001', 0), '010001': ('110001', 0), '110001': ('001', 1)}[w]
    c, R = _F.split(w)
    if c[0] == '0': return '1' + c[1:] + ('' if R is None else '000' + R), 0
    R2, d2 = _inc_count('' if R is None else R)
    return '0' + c[1:] + '001' * d2 + '000' + R2, 0
_add_G0 = M.add_G; _eat0 = M.eat
def _add_G_count(w, n):
    r = _add_G0(w, n)
    if _DIG[0]: _OV[0] += len(M.parse_G(r)[0]) - len(M.parse_G(w)[0])
    return r
def _eat_count(a, w):
    if w == '110001' and _DIG[0]: _OV[0] += 1
    return _eat0(a, w)
def instrument(on):
    _F.inc_rule = M.inc_rule = (_inc_count if on else inc_rule)
    M.add_G = _add_G_count if on else _add_G0
    M.eat = _eat_count if on else _eat0

def eta_of(es): return [e - 1 for e in es[:-1]] + es[-1:]
def suffix(es):
    h = eta_of(es); return [sum(h[q:]) for q in range(len(h))] + [0]

def classify(w):
    w = norm(w)
    if inG(w): return 'G'
    if w in ESTAR: return 'E*'
    if not w.startswith('11'): return '?'
    return ''

def run_epoch(N, w):
    """one model epoch from K(1,N,w) with the W-phase overflow counter; digestion = until the first hub word in G"""
    s0 = dict(M.STATS); info = {'post': None, 'b': None}
    _OV[0] = 0; _DIG[0] = True
    def tr(a_, b_, w_):
        if info['post'] is None and inG(norm(w_)):
            info['post'] = norm(w_); info['b'] = b_; _DIG[0] = False
    try:
        k2, T2 = M.epoch(1, N, w, tr)
    finally:
        _DIG[0] = False
    pp = M.parse_G(info['post']) if info['post'] else None
    return {'beta': N - info['b'], 'c': _OV[0], 'L': M.STATS.get('D6', 0) - s0.get('D6', 0),
            'S5': M.STATS.get('D5', 0) - s0.get('D5', 0), 'kpost': len(pp[0]) if pp else 0, 'k2': k2, 'T2': T2}

def lemma_checks(tag, x, es, k, r, nxt):
    """the per-epoch links of Lemma D that do not need the running maximum: C, D.2, D.3, D.4(a,b,e) for the next W"""
    eta = eta_of(es); S = suffix(es); c = r['c']; L = r['L']
    rec('D.6C Lemma C: 3*2^(k+c) <= 9*2^k + sum_q 2^(q+1) eta_q - 5' + tag,
        c == 0 or 3 * 2 ** (k + c) <= 9 * 2 ** k + sum(2 ** (q + 1) * h for q, h in enumerate(eta)) - 5, (x, es, c))
    rec('D.2  L <= floor((k+c+1)/2) and 2(L-1) + #strips <= k + c' + tag,
        L <= (k + c + 1) // 2 and (L == 0 or 2 * (L - 1) + r['S5'] <= k + c), (x, es, L, r['S5'], c))
    rec('D.3  k_post - L in {0, 1}' + tag, r['kpost'] - L in (0, 1), (x, es, r['kpost'], L))
    if nxt is None: return
    kind, x2, es2 = nxt
    if kind:                       # special next residue: profile reset
        return
    rec('D.4e every non-last block of the next W has e >= 1' + tag, all(e >= 1 for e in es2[:-1]), (x, es, es2))
    S2 = suffix(es2)
    rec("D.4a S_{t+1}(q) = 0 or S_{t+1}(q) <= S_t(2q+2) + 3(k_t+c_t) + T - 8 - 6q" + tag,
        all(S2[q] == 0 or S2[q] <= (S[2 * q + 2] if 2 * q + 2 < len(S) else 0) + 3 * (k + c) + TEND - 8 - 6 * q for q in range(len(es2))),
        (x, es, c, es2))
    rec('D.4b x_{t+1} <= S_t(0) + 3(k_t+c_t) + T - 1' + tag, x2 <= S[0] + 3 * (k + c) + TEND - 1, (x, es, c, x2))

def next_residue(T2):
    Y2 = norm(T2[3:]); kind = classify(Y2)
    if kind: return kind, 0, []
    x2, W2, ds2, es2, t2 = parse_residue(Y2)
    return '', x2, es2

def section_D(maxN, Nstar):
    """Lemma D on the rules-only orbit from epoch 3; kappa = running max of k(W) (proof.md D.7)"""
    import nest_cost
    fin = None
    M.FAST = True
    instrument(True)
    k, T = 7, '000010001'
    ep = 2; Nmax = 0; worst_ratio = 0; rows = 0; prev = None; kappa = 0; chist = {}; worstV = 0; specials = {}
    try:
        while True:
            ep += 1
            a, b, w = M.restart(k, T); N = b
            kind = classify(w)
            rec('H3   every top-level residue is ordinary (11 a^x z W, W in G) or special (in G or E*)', kind != '?', (ep, w[:40]))
            if kind: specials[kind] = specials.get(kind, 0) + 1
            x, W, ds, es, tt = parse_residue(w) if not kind else (0, '', [], [], 0)
            kW = len(es); kappa = max(kappa, kW)
            try:
                r = run_epoch(N, w)
            except (M.Unsafe, M.Unknown) as ex:
                rec('FIN  rules-only orbit: no non-G eat, no unknown word', False, (ep, N, str(ex)[:80])); return
            rec('FIN  rules-only orbit: no non-G eat, no unknown word', True)
            c = r['c']; chist[c] = chist.get(c, 0) + 1; beta = r['beta']
            rec('FIN  beta_t <= N_t - 2 on every epoch of the explicit orbit', beta <= N - 2, (ep, N, beta))
            J, A = nest_cost.JA(w)
            rec('D.1  beta = J - A (cost recursion, exact)', beta == J - A, (ep, beta, J, A))
            nxt = next_residue(r['T2'])
            if not kind:
                lemma_checks('', x, es, kW, r, nxt)
                rec('D.6G c_t <= Gamma(k_t, kappa_t) and k_t + c_t <= G(kappa_t)', c <= Gamma(kW, kappa) and kW + c <= Gfix(kappa)[0],
                    (ep, kW, c, kappa))
                S = suffix(es)
                rec('D.4c S_t(q) <= U(kappa_t, q) = max(1, ceil(log2((kappa+2)/(q+2)))) * Delta(kappa_t)',
                    all(S[q] <= U(kappa, q) for q in range(kW)), (ep, S, kappa))
                rec('D.4x x_t <= xmax(kappa_t) = U(kappa,0) + Delta(kappa) + 7', x <= xmax(kappa), (ep, x, kappa))
                B = bnd(x, es, kW, c, TAU_)
                rec('D.7a beta <= Bnd(x, es, k, c_t)', beta <= B, (ep, beta, B))
                rec('D.7b Bnd(x, es, k, c_t) <= Bnd_worst(kappa_t)', B <= bnd_worst(kappa, TAU_)[0], (ep, B, kappa))
                worst_ratio = max(worst_ratio, beta / B)
            else:
                rec('D.7s special residue: c = 0, L = 0, beta <= tau', c == 0 and r['L'] == 0 and beta <= TAU_, (ep, w, r))
                if nxt[0] == '':
                    rec('D.4r after a special residue: next W has S = 0 and x <= 1', nxt[1] <= 1 and all(h == 0 for h in eta_of(nxt[2])), (ep, nxt))
            if prev is not None:
                Lp = prev
                rec('D.5  2^(k_{t+1}+3) <= N_{t+1} + 2^(L_t+4)', 2 ** (kW + 3) <= N + 2 ** (Lp + 4), (ep, kW, N, Lp))
                worstV = max(worstV, 2 ** (kW + 3) / N)
            rec('D.7n N_t >= N_lo(kappa_t)', N >= N_lo(kappa), (ep, N, kappa))
            prev = r['L']
            if fin is None and N >= Nstar: fin = {'first_epoch_with_N>=N*': ep, 'its_N': N, 'epochs_3..below_N*': ep - 3}
            k, T = r['k2'], r['T2']
            Nmax = N; rows += 1
            if N >= maxN: break
    finally:
        instrument(False)
    RES['_D'] = {'epochs': rows, 'N_max': Nmax, 'max_beta_over_Bnd': round(worst_ratio, 4), 'kappa_end': kappa,
                 'c_histogram': {str(c): n for c, n in sorted(chist.items())}, 'special_residues': specials,
                 'max_2^(k+3)/N': round(worstV, 4), 'finite_part': fin}

# ---------------------------------------------------------------------------------------------------------------
# adversarial residues: anything the invariant allows (D.4e, D.4c profile, D.4b bound on x, k <= kappa), digested by the
# model; a sample of whole epochs is compared with the TM. Includes the Checkpoint B skeptic's examples.
def gen_inv(K):
    k = random.choice([K, K, random.randint(0, K), random.randint(1, min(K, 3))])
    S = [0] * (k + 1); mode = random.random()
    for q in range(k - 1, -1, -1):
        lo = S[q + 1]; hi = max(lo, U(K, q))
        if mode < 0.4: S[q] = hi
        elif mode < 0.7: S[q] = random.randint(lo, hi)
        else: S[q] = lo + (random.randint(0, hi - lo) if random.random() < 0.3 else 0)
    et = [S[q] - S[q + 1] for q in range(k)]
    es = [et[q] + (1 if q < k - 1 else 0) for q in range(k)]
    if random.random() < 0.5: ds = [1] * k
    elif random.random() < 0.5: ds = [random.randint(0, 1) for _ in range(k)]
    else:
        p = random.randint(0, max(0, k - 1)); ds = [random.randint(0, 1) for _ in range(p)] + [1] * (k - p)
    s = 3 if random.random() < 0.6 else random.randint(0, 3)
    x = random.choice([0, xmax(K), random.randint(0, xmax(K))])
    return x, ds, es, s

def residue_word(x, ds, es, s):
    W = M.build_G(ds, es, s) if es else ([''] + TAILS)[s]
    return norm('11' + '001' * x + ('000' + W if W else '')), W

def tm_epoch(N, Y, maxsteps=3 * 10**7):
    """the TM from K(1,N,Y) to its first left record: (k, T) or the failure event"""
    s = '0' * 64 + '110' + '0' + '011' * N
    pos = len(s)
    tape = bytearray(int(ch) for ch in s + Y) + bytearray(3 * N + len(Y) + 4000)
    ev = common.run(tape, pos, 2, lambda e: e[0] == 'L', maxsteps)
    return (ev[1], ev[2]) if ev[0] == 'L' else ev

def section_ADV(n, ntm):
    import nest_cost
    M.FAST = True
    named = [('skeptic k=2 c=2', 0, [1, 1], [17, 1], 3, None), ('skeptic x_{t+1}=17', 0, [1], [8], 1, 100),
             ('skeptic k=3 c=2 N=2917', 9, [1, 1, 1], [15, 9, 5], 3, 2917),
             ('skeptic k=16 c=4', 0, [1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1, 0, 0, 0],
              [57, 1, 57, 1, 1, 1, 1, 57, 1, 1, 1, 1, 1, 1, 1, 56], 3, None)]
    cases = [(nm, x, ds, es, s, N, True, None) for nm, x, ds, es, s, N in named]
    for i in range(n):
        if i % 3 == 2:             # unconstrained: Lemma C, D.2, D.3, D.4(a,b), D.7a need only eta >= 0
            k = random.randint(0, 6); emax = random.choice([3, 12, 40])
            es = [random.randint(1, emax) for _ in range(max(0, k - 1))] + [random.randint(0, emax) for _ in range(min(k, 1))]
            ds = [1] * k if random.random() < 0.5 else [random.randint(0, 1) for _ in range(k)]
            cases.append(('', random.randint(0, emax), ds, es, random.randint(0, 3), None, False, None))
            continue
        K = random.choice([random.randint(1, 6), random.randint(1, 12), random.randint(8, 16)])
        x, ds, es, s = gen_inv(K)
        cases.append(('', x, ds, es, s, None, False, K))
    tm_done = 0; cmax = 0; slack_a = -10**9; slack_b = -10**9
    instrument(True)
    try:
        for nm, x, ds, es, s, N, named_case, K in cases:
            Y, W = residue_word(x, ds, es, s)
            k = len(es)
            J, A = nest_cost.JA(Y); beta = J - A
            if N is None: N = beta + 2 + random.choice([0, random.randint(0, 60), random.randint(0, 3000), random.randint(0, 40000)])
            try:
                r = run_epoch(N, Y)
            except (M.Unsafe, M.Unknown) as ex:
                rec('ADV  adversarial residue: model epoch ends at a left record', False, (nm, x, es, str(ex)[:60])); continue
            rec('ADV  adversarial residue: model epoch ends at a left record', r['beta'] == beta, (nm, x, es, r['beta'], beta))
            if K is not None:
                S = suffix(es)
                rec('ADV  generator: residue satisfies the invariant (eta >= 0, S <= U(kappa), x <= xmax(kappa), k <= kappa)',
                    k <= K and all(h >= 0 for h in eta_of(es)) and all(S[q] <= U(K, q) for q in range(k)) and x <= xmax(K), (x, es, K))
                rec('D.6G c <= Gamma(k, kappa), k + c <= G(kappa) [adversarial]', r['c'] <= Gamma(k, K) and k + r['c'] <= Gfix(K)[0], (x, es, K, r['c']))
                rec('D.7b Bnd(x, es, k, c) <= Bnd_worst(kappa) [adversarial]', bnd(x, es, k, r['c'], TAU_) <= bnd_worst(K, TAU_)[0], (x, es, K))
            nxt = next_residue(r['T2'])
            lemma_checks(' [adversarial]', x, es, k, r, nxt)
            cmax = max(cmax, r['c'])
            rec('D.7a beta <= Bnd(x, es, k, c_t) [adversarial]', beta <= bnd(x, es, k, r['c'], TAU_), (nm, x, es, beta))
            if nxt[0] == '':
                S = suffix(es); S2 = suffix(nxt[2])
                for q in range(len(nxt[2])):
                    if S2[q] > 0: slack_a = max(slack_a, S2[q] - (S[2 * q + 2] if 2 * q + 2 < len(S) else 0) - 3 * (k + r['c']) + 6 * q)
                slack_b = max(slack_b, nxt[1] - S[0] - 3 * (k + r['c']))
            if (named_case or tm_done < ntm) and N <= 400:
                got = tm_epoch(N, Y)
                rec('ADV  TM epoch from K(1,N,Y) = model epoch (k, T)', got == (r['k2'], r['T2']), (nm, x, es, s, N, got, (r['k2'], r['T2'][:60])))
                tm_done += 1
            if named_case:
                RES.setdefault('_ADV_named', {})[nm] = {'k': k, 'c': r['c'], 'L': r['L'], 'beta': beta, 'N': N,
                                                        'x_next': nxt[1], 'next_es': nxt[2][:8]}
    finally:
        instrument(False)
    RES['_ADV'] = {'cases': len(cases), 'tm_epochs': tm_done, 'max_c': cmax,
                   'max over S_{t+1}(q) > 0 of (S_{t+1}(q) - S_t(2q+2) - 3(k+c) + 6q)  [bound T-8 = %d]' % (TEND - 8): slack_a,
                   'max (x_{t+1} - S_t(0) - 3(k+c))  [bound T-1 = %d]' % (TEND - 1): slack_b}

# ---------------------------------------------------------------------------------------------------------------
def main():
    global TEND, TAU_
    if '--adv' in sys.argv:          # stand-alone stress run of the adversarial section
        build_estar(); TAU_ = tau(); TEND = end_extra()
        section_ADV(int(sys.argv[sys.argv.index('--adv') + 1]), 0)
        bad = 0
        for cid in sorted(k for k in RES if not k.startswith('_')):
            r = RES[cid]; ok = r['pass'] == r['n']; bad += not ok
            print(('PASS ' if ok else 'FAIL ') + f"{r['pass']}/{r['n']}  {cid}" + ('' if ok else '  e.g. ' + str(r['fail'][:1])))
        print(RES.get('_ADV')); print('ALL PASS' if bad == 0 else f'{bad} CLAIMS FAIL', f'(seed {SEED})')
        return
    section_A(); print('A done', round(time.time() - T0, 1), flush=True)
    section_RP(); section_LP(); print('LP done', round(time.time() - T0, 1), flush=True)
    section_B(); section_E(); section_R(); print('B/E/R done', round(time.time() - T0, 1), flush=True)
    section_D6(); print('D6 done', round(time.time() - T0, 1), flush=True)
    section_H(); section_D3(); print('H done', round(time.time() - T0, 1), flush=True)
    section_I(); section_O(); print('I/O done', round(time.time() - T0, 1), flush=True)
    TAU_ = tau(); TEND = end_extra()
    RES['_tau'] = TAU_; RES['_T_end_extra'] = TEND
    k0, Nstar, around = analytic_threshold(TAU_, 48 if QUICK else 160)
    RES['_analytic'] = {'tau': TAU_, 'T': TEND, 'last_failing_kappa': k0, 'N_star': Nstar,
                        'rows kappa: (Bnd_worst, worst k, N_lo, G, Delta, Gamma(kappa,kappa))': around}
    print('threshold done', round(time.time() - T0, 1), 'N* =', Nstar, flush=True)
    section_D(max(Nstar + 1, 400000) if not QUICK else max(Nstar + 1, 20000), Nstar); print('D done', round(time.time() - T0, 1), flush=True)
    section_ADV(1500 if not QUICK else 200, 40 if not QUICK else 8); print('ADV done', round(time.time() - T0, 1), flush=True)
    bad = 0
    for cid in sorted(k for k in RES if not k.startswith('_')):
        r = RES[cid]; ok = r['pass'] == r['n']; bad += not ok
        print(('PASS ' if ok else 'FAIL ') + f"{r['pass']}/{r['n']}  {cid}" + ('' if ok else '  e.g. ' + str(r['fail'][:1])))
    for k in sorted(k for k in RES if k.startswith('_') and k != '_ESTAR'): print(k, RES[k])
    print('E* =', RES.get('_ESTAR'))
    print('ALL PASS' if bad == 0 else f'{bad} CLAIMS FAIL', f'({round(time.time() - T0, 1)} s, seed {SEED})')
    if not QUICK:
        with open(os.path.join(HERE, f'data/check_proof_seed{SEED}.json'), 'w') as f:
            json.dump({'seed': SEED, 'seconds': round(time.time() - T0, 1), 'claims': RES}, f, indent=1, default=str)

if __name__ == '__main__':
    main()