#!/usr/bin/env python3
"""check_proof.py: checks every claim of proof.md for W4-3 (1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---) and its
siblings 512 / 588. Each check prints PASS or FAIL with its counts; the exit code is the number of failures.

Sections (proof.md section in brackets):
  S1  machine table, sweep cycles, the only way into F                                   [1, 2.1]
  S2  the defect model (8 rules + halting rule) against direct simulation:
      exhaustive small tapes, random large tapes                                        [2.2, 2.3]
  S3  Lemma B (single-block event lists, footprints), Lemma C / C' on the exact defect model:
      exhaustive K <= 2 with tight gaps, random K <= 10                                  [4.1, App. D]
  S4  Lemma T (counting), word level K = 2..9 and defect model K = 2..8                  [4.1]
  S5  Lemma L (the left word): 81-word ternary counter, closed form, record, in context;
      Lemma L81 (episode 81 event by event)                                            [4.2, App. E]
  S6  Lemma R (the 81-entry right table): every entry at the minimal long gaps,
      all {min, min+4} combinations, random huge gaps; free stretches (transfer 2.4)     [4.3, App. A]
  S7  the interval program and the record step, symbolically in u (independent jump
      verification, cycle composites), record-visit formulas, the window vectors V_r(u),
      concrete steps 16-39 without acceleration                                        [5, 6, App. B, F]
  S8  the regrouping arithmetic and the exchange / K schedule                           [6.2, 6.3]
  S9  X/Y synchronization: per-visit rates and the closed forms X_k, F_j                 [5.4]
  S10 base case: record exit 16 regenerated from the blank tape and compared with direct
      simulation (341, and 512 / 588 through their renaming); membership and (H) at cell
      level at 16-39; record numbering and the operational record exit (review1/lo_moves.c) [3, 7, App. C]
  S11 random deep-chain perturbations, run to the next record exit                       [7]
  S12 proof.md's appendices, 6.4 formulas and V_r(u) table are exactly the data checked  [3.4, 6.4, App. A-F]
Usage: nice -n 10 python3 -B check_proof.py [--full] [--only S1,S7,...] [--appendix]
  Default run: about 2-3 minutes. --full adds: chain lemma K = 3 exhaustive on the compressed TM (1.4M runs), Lemma T
  K = 9, the siblings' record exit 16 regenerated by the model, and 10 perturbations per record exit 16-27 (3 per exit
  28-32). --appendix prints proof.md's Appendices A-F and the 6.4 formulas from the checked data.
AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic)."""
import sys, os, random, itertools, bisect, pickle, copy, time, subprocess, re
from fractions import Fraction as Fr

HERE = os.path.dirname(os.path.abspath(__file__))
SC = os.path.join(HERE, 'scripts')
for d in ('rules_stage', 'induction_stage', 'sync_stage', 'closeout3'):
    sys.path.insert(0, os.path.join(SC, d))
sys.path.insert(0, os.path.join(HERE, '..', '..', 'tools'))
_argv = sys.argv[:]
sys.argv = sys.argv[:1]
from dmodel import TMT, Model, model_from_tape, LCYC, RCYC, parse_tm, TM
from blocktm import run_block
from mixed_chain import offsets, words, predict, read
from run_model import model_from_blank
from read_blocks8 import setup
import check_model_random as CMR
from check_model_random import tm_events, model_events, rand_tape
import window as W
from symcore import Aff, gshape, apply, run_interval, tab, T, K0
sys.argv = _argv

FULL = '--full' in sys.argv
ONLY = None
if '--only' in sys.argv:
    ONLY = set(sys.argv[sys.argv.index('--only') + 1].split(','))
RESULTS = []
ORDER = [5, 0, 1, 2, 3, 4]
NXT = {r: ORDER[(ORDER.index(r) + 1) % 6] for r in ORDER}


def claim(sec, text, ok, detail=''):
    RESULTS.append((sec, text, bool(ok)))
    print(f"  [{'PASS' if ok else 'FAIL'}] {text}" + (f"  ({detail})" if detail else ''), flush=True)


def section(name, title):
    if ONLY and name not in ONLY:
        return False
    print(f"\n{name}  {title}", flush=True)
    return True


# ------------------------------------------------------------------------------------------------- S1
def s1():
    t = parse_tm(TM)
    undefined = [k for k, v in t.items() if v is None]
    claim('S1', 'the only undefined transition is F reading 1', undefined == [('F', 1)], f'{undefined}')
    into_f = sorted(k for k, v in t.items() if v and v[2] == 'F')
    claim('S1', 'F is entered only from A reading 1', into_f == [('A', 1)], f'{into_f}')
    ok = True
    for cyc, dirn in ((['B0', 'C1', 'A0', 'B1'], 1), (['D1', 'D0', 'E1', 'C0'], -1)):
        for i, sr in enumerate(cyc):
            s, r = sr[0], int(sr[1]); w, mv, nx = t[(s, r)]
            nxt = cyc[(i + 1) % 4]
            ok &= w == 1 - r and mv == dirn and nx == nxt[0] and int(nxt[1]) == 1 - r
    claim('S1', 'sweep cycles: right B0 C1 A0 B1, left D1 D0 E1 C0; every sweep step complements its cell', ok)
    # proof.md 2.2, second table: the transitions at a defect e (cells e, e+1 equal), for each direction and d
    want = {(-1, 0): ['C0', 'D0'], (-1, 1): ['E1', 'C1'], (-1, 2): ['D0', 'E0'], (-1, 3): ['D1', 'D1'],
            (1, 0): ['B0', 'C0'], (1, 1): ['C1', 'A1', 'F0', 'A0', 'B1'], (1, 2): ['A0', 'B0'], (1, 3): ['B1', 'B1']}
    after = {(-1, 0): 'L', (-1, 1): 'R', (-1, 2): 'R', (-1, 3): 'L', (1, 0): 'L', (1, 1): 'R', (1, 2): 'R', (1, 3): 'R'}
    ok = True; halt_ok = True
    for (dirn, d), seq in want.items():
        for e in range(100, 104):
            phi = (e - d) % 4
            if dirn > 0:
                st, s0 = {0: ('B', 0), 1: ('C', 1), 2: ('A', 0), 3: ('B', 1)}[(e - phi) % 4]; pos = e
            else:
                st, s0 = {0: ('D', 1), 3: ('D', 0), 2: ('E', 1), 1: ('C', 0)}[(e + 1 - phi) % 4]; pos = e + 1
            for extra in (False, True):
                tape = {}
                for x in range(e - 12, e + 1): tape[x] = s0 if (e - x) % 2 == 0 else 1 - s0
                for x in range(e + 1, e + 14): tape[x] = s0 if (x - e - 1) % 2 == 0 else 1 - s0
                if extra:                               # a second defect at e+1 (only the wiggle case cares)
                    for x in range(e + 2, e + 14): tape[x] = 1 - tape[x]
                q, x, used = st, pos, []
                for _ in range(len(seq) + 1):
                    r = tape[x]; used.append(f'{q}{r}'); tr = t[(q, r)]
                    if tr is None: break
                    w, mv, nx = tr; tape[x] = w; x += mv; q = nx
                if extra:
                    if (dirn, d) == (1, 1): halt_ok &= used == ['C1', 'A1', 'F1']
                    continue
                ok &= used[:len(seq)] == seq
                # after the listed transitions the head is back in a sweep cycle, moving as the rule says
                nxt = used[len(seq)] if len(used) > len(seq) else None
                cyc = {'R': {'B0', 'C1', 'A0', 'B1'}, 'L': {'D1', 'D0', 'E1', 'C0'}}[after[(dirn, d)]]
                ok &= nxt in cyc
    claim('S1', 'the transitions of the eight defect rules (proof.md 2.2), after which the head is back in the stated '
          'sweep cycle', ok)
    claim('S1', 'the wiggle with a second defect at e+1 runs C1, A1 and then F reads 1 (the halt)', halt_ok)


# ------------------------------------------------------------------------------------------------- S2
def compare_instance(cells, lo, p, state, direction, max_ev, max_steps):
    PAD = CMR.PAD = max(400, 2 * len(cells) + 400)       # the comparison window (both engines stop at its edge)
    full = [0] * PAD + cells + [0] * PAD
    tev, n = tm_events(cells, lo, p, state, direction, max_ev, max_steps)
    m = model_from_tape(full, lo - PAD, p, state, direction)
    mev = model_events(m, max_ev, max_steps, p)
    # a wiggle is two reversals (F, then A one step later); one cut by the step limit would read as a turn
    tev = [x for x in tev if x[2] < max_steps - 8]; mev = [x for x in mev if x[2] < max_steps - 8]
    k = min(len(tev), len(mev))
    same = k > 0 and tev[:k] == mev[:k]
    return same, bool(tev and tev[-1][0] == 'halt' and k == len(tev))


def s2():
    tot = ok = halts = 0; t0 = time.time()
    for n in range(1, 13):
        for mid in itertools.product((0, 1), repeat=max(0, n - 2)):
            cells = [1] + list(mid) + ([1] if n >= 2 else [])
            for p in range(-2, len(cells) + 2):
                v = cells[p] if 0 <= p < len(cells) else 0
                for direction in (-1, 1):
                    cyc = LCYC if direction < 0 else RCYC
                    for (s, r) in cyc:
                        if r != v: continue
                        same, h = compare_instance(cells, 0, p, s, direction, 25, 400)
                        tot += 1; ok += same; halts += h
    claim('S2', 'defect model = direct simulation, EXHAUSTIVE: every tape word of length 1-12 between blank ends, '
          'every head cell within 2 of the word, every sweep state (25 events or 400 steps each)', ok == tot,
          f'{ok}/{tot} agree, {halts} reach the halt, {time.time() - t0:.0f} s')
    rng = random.Random(20261012); tot = ok = halts = 0
    for it in range(10000):
        if it % 2:
            cells = rand_tape(rng)
        else:                                   # long alternating stretches between defects
            cells = [1]
            for _ in range(rng.randint(2, 12)):
                g = rng.choice([1, 2, 3, 4, 5, rng.randint(6, 40), rng.randint(40, 200)])
                for _ in range(g - 1): cells.append(1 - cells[-1])
                cells.append(cells[-1])         # a defect
            if cells[-1] == 0: cells.append(1)
        lo = rng.randint(-5, 5); direction = rng.choice([-1, 1])
        p = lo + rng.randrange(len(cells)); v = cells[p - lo]
        cyc = LCYC if direction < 0 else RCYC
        s = rng.choice([s for (s, r) in cyc if r == v])
        same, h = compare_instance(cells, lo, p, s, direction, 60, 20000)
        tot += 1; ok += same; halts += h
    claim('S2', 'defect model = direct simulation, RANDOM: 10,000 tapes up to ~2,400 cells, 60 events each', ok == tot,
          f'{ok}/{tot} agree, {halts} reach the halt')


# ------------------------------------------------------------------------------------------------- S3
BIG = 4001
STAT = {'minA': 10 ** 9}


def chain_run(p, side, phi, A=None, count=None):
    """Exact defect model on a tape holding only the chain p (blank far away). Head enters from `side` with phase phi.
    Returns (exit side, exit phase, new defects) or ('COLLIDE'|'HALT'|'LOOP', ...)."""
    Lb, Rb = p[0] - 4, p[-1] + 4
    m = Model(list(p), p[0] - 300, p[-1] + 300, Rb + 1 if side == 'R' else Lb - 1, -1 if side == 'R' else 1, phi)
    for _ in range(20000):
        if m.dir < 0 and m.next_left() < Lb:
            xs = 'L'; break
        if m.dir > 0 and m.next_right() > Rb:
            xs = 'R'; break
        kind, cell, k = m.event()
        if count is not None: count[0] += 1
        if kind == 'halt': return ('HALT', None, None)
        if A is not None and m.D: STAT['minA'] = min(STAT['minA'], m.D[0] - A)
    else:
        return ('LOOP', None, None)
    if len(m.D) != len(p): return ('COLLIDE', None, None)
    return (xs, m.phi % 4, tuple(m.D))


def gap_choices(m, rng=None):
    if rng is None:
        if m == 1: return [(g1,) for g1 in (1, 5, 9, BIG)]
        out = []
        for g1 in (1, 5, BIG):
            for s1 in (4, 8, BIG - 1):
                for s2 in (4, 8, BIG - 1):
                    out.append((g1, g1 + s1, g1 + s1 + s2))
        return out
    if m == 1: return (rng.choice([1, 5, 9, 1 + 4 * rng.randint(3, 300)]),)
    g1 = rng.choice([1, 1, 5, 1 + 4 * rng.randint(2, 3000)])
    s1 = rng.choice([4, 4, 8, 4 * rng.randint(3, 3000)]); s2 = rng.choice([4, 4, 8, 4 * rng.randint(3, 3000)])
    return (g1, g1 + s1, g1 + s1 + s2)


def build(lab, ms, gs, inters, b=10000):
    p, bases = [], []
    for i, (x, m, g) in enumerate(zip(lab, ms, gs)):
        if i: b = bases[-1] + gs[i - 1][-1] + inters[i - 1]
        bases.append(b); p += [b + o for o in offsets(x, m, g)]
    return p, bases


def predict_carryback(lab, nm1):
    out = []; first_u = True
    for i, x in enumerate(lab):
        if i < nm1 or x == 'D0': out.append('D2')
        elif x == 'U2': out.append('W0' if first_u else 'U0'); first_u = False
        else: return None
    return tuple(out)


def check_chain_word(lab, nm1, ms, gs, inters, runner):
    p, bases = build(lab, ms, gs, inters)
    if any(q2 <= q1 for q1, q2 in zip(p, p[1:])): return None
    A = bases[0] - 2 if nm1 else None
    cK = (bases[-1] + 1) % 4; c1 = (bases[0] + 1) % 4; K = len(lab)
    res = []
    xs, xphi, q = runner(p, 'R', cK, A)
    exp_side, exp_lab = predict(lab, nm1)
    ok = xs == exp_side and read(q, ms, gs, bases) == exp_lab
    if ok and xs == 'R':
        j = max(i for i in range(K) if lab[i] not in ('U2', 'D0'))
        ok = (xphi - cK) % 4 == (0 if (lab[j][0] == 'D' and exp_lab[-1][0] == 'D') else 2)
    if ok and xs == 'L':
        ok = (xphi - c1) % 4 == 2
    res.append(ok)
    if exp_side == 'L':
        xs2, xphi2, q2 = runner(p, 'L', c1 + 2, A)
        exp2 = predict_carryback(lab, nm1)
        ok2 = xs2 == 'R' and exp2 is not None and read(q2, ms, gs, bases) == exp2
        ok2 = ok2 and (xphi2 - cK) % 4 == (0 if all(x[0] == 'D' for x in exp2) else 2)
        res.append(ok2)
    return res


BLOCK_TABLE = {   # proof.md 4.1, the single-block runs: (state, entry side, entry phase - c) -> (exit side, phase change, state)
    3: {('U0', 'R', 0): ('R', 2, 'U1'), ('U1', 'R', 0): ('R', 2, 'U2'), ('U2', 'R', 0): ('L', 2, 'U2'),
        ('W0', 'R', 0): ('R', 2, 'W1'), ('W1', 'R', 0): ('R', 2, 'D0'), ('D0', 'R', 0): ('L', 2, 'D0'),
        ('D1', 'R', 0): ('R', 0, 'D0'), ('D2', 'R', 0): ('R', 0, 'D1'), ('U2', 'L', 0): ('R', 2, 'U0'),
        ('U2', 'L', 2): ('R', 0, 'W0'), ('D0', 'L', 2): ('R', 2, 'D2')},
    1: {('U0', 'R', 0): ('R', 2, 'U1'), ('U1', 'R', 0): ('R', 2, 'D0'), ('D0', 'R', 0): ('L', 2, 'D0'),
        ('D1', 'R', 0): ('R', 0, 'D0'), ('D2', 'R', 0): ('R', 0, 'D1'), ('D0', 'L', 0): ('R', 2, 'U0'),
        ('D0', 'L', 2): ('R', 2, 'D2')}}


ROLE = {3: ('dg', 's1', 's2', 's3'), 1: ('dg', 'sp')}
RANGE = {3: ((-2, 0), (0, 2), (0, 3), (0, 2)), 1: ((-2, 0), (0, 2))}     # proof.md 4.1, Lemma B (offsets from U0 places)


def block_trace(p, side, phi):
    """One single-block run on the exact model with event bookkeeping: returns (exit side, exit phase, final defects,
    events as (dir, role, d, kind), per-defect [min, max] positions, set of toggled or tested edges)."""
    Lb, Rb = p[0] - 4, p[-1] + 4
    m = Model(list(p), p[0] - 300, p[-1] + 300, Rb + 1 if side == 'R' else Lb - 1, -1 if side == 'R' else 1, phi)
    rng = [[x, x] for x in p]; touched = set(); evs = []; n = len(p)
    for _ in range(100):
        if m.dir < 0 and m.next_left() < Lb: xs = 'L'; break
        if m.dir > 0 and m.next_right() > Rb: xs = 'R'; break
        e = m.next_left() if m.dir < 0 else m.next_right()
        d = (e - m.phi) % 4; dirn = 'L' if m.dir < 0 else 'R'; idx = m.D.index(e) if e in m.D else None
        kind, cell, k = m.event()
        if kind == 'halt' or len(m.D) != n or idx is None: return None
        touched |= {'turnR': {e - 1, e}, 'turnL': {e, e + 1}, 'wiggle': {e, e + 1, e + 2}}.get(kind, set())
        evs.append((dirn, idx, d, kind))
        for i, x in enumerate(m.D): rng[i][0] = min(rng[i][0], x); rng[i][1] = max(rng[i][1], x)
    else:
        return None
    return xs, m.phi % 4, tuple(m.D), tuple(evs), rng, touched


BLOCK_EVENTS = {}


def lemma_B():
    """proof.md 4.1, Lemma B: for each of the 18 runs and every gap choice (all base choices tight / tight+4 / long, and
    40 random ones): the same event list (direction, role, d, kind); every defect stays within RANGE of its U0 place;
    every toggled or tested edge lies in [b-2, b+g_last+2]."""
    rng_ = random.Random(1); ok_ev = ok_rng = ok_fp = True; n = 0
    for m, tabm in BLOCK_TABLE.items():
        gch = gap_choices(m) + [gap_choices(m, rng_) for _ in range(40)]
        for (lab, side, dph), want in tabm.items():
            seen = set()
            for g in gch:
                b = 10000; p = [b + o for o in offsets(lab, m, g)]
                res = block_trace(p, side, b + 1 + dph); n += 1
                if res is None: ok_ev = False; continue
                xs, xphi, q, evs, rr, touched = res
                seen.add(tuple((dr, ROLE[m][i], d, kd) for dr, i, d, kd in evs))
                places = [b] + [b + x for x in g]
                ok_rng &= all(RANGE[m][i][0] <= lo_ - pl and hi_ - pl <= RANGE[m][i][1]
                              for i, ((lo_, hi_), pl) in enumerate(zip(rr, places)))
                ok_fp &= all(b - 2 <= x <= b + g[-1] + 2 for x in touched)
            ok_ev &= len(seen) == 1
            BLOCK_EVENTS[(m, lab, side, dph)] = next(iter(seen)) if seen else None
    return ok_ev, ok_rng, ok_fp, n


def fmt_block_events(evs):
    nm = {'pass': 'pass', 'turnL': 'turn', 'turnR': 'turn', 'wiggle': 'wiggle'}
    return ', '.join(f'{dr} {role} d={d} {nm[kd]}' for dr, role, d, kd in evs)


def s3():
    ok_ev, ok_rng, ok_fp, nB = lemma_B()
    claim('S3', 'Lemma B: each of the 18 single-block runs has the same event list (direction, defect role, d, rule) for '
          'every gap choice (tight, tight+4, long, 40 random)', ok_ev, f'{nB} runs')
    claim('S3', 'Lemma B: during each run every defect stays within its stated offsets of its U0 place (digit -2..0, s1 '
          '0..+2, s2 0..+3, s3 0..+2; m=1: digit -2..0, separator 0..+2)', ok_rng)
    claim('S3', 'Lemma B: every edge a run toggles or tests (the wiggle\'s e+1) lies in [b-2, b+g_last+2]', ok_fp)
    rng = random.Random(1); good = tot = 0; maxev = 0
    for m, tabm in BLOCK_TABLE.items():
        gch = gap_choices(m) + [gap_choices(m, rng) for _ in range(40)]
        labs = ['U0', 'U1', 'D0', 'D1', 'D2'] if m == 1 else ['U0', 'U1', 'U2', 'W0', 'W1', 'D0', 'D1', 'D2']
        for (lab, side, dph), want in tabm.items():
            for g in gch:
                b = 10000; c = b + 1
                p = [b + o for o in offsets(lab, m, g)]
                cnt = [0]
                xs, xphi, q = chain_run(p, side, c + dph, count=cnt); maxev = max(maxev, cnt[0])
                got = None
                if xs in 'LR':
                    seg = tuple(x - b for x in q); names = [l for l in labs if offsets(l, m, g) == seg]
                    got = (xs, (xphi - c - dph) % 4, names[0] if names else '?')
                tot += 1; good += got == want
    claim('S3', 'the 18 single-block runs of Lemma C (11 for m = 3, 7 for m = 1) on the exact defect model, every tight '
          'gap choice and 40 random ones each; each run has at most 8 events', good == tot and maxev <= 8,
          f'{good}/{tot}, at most {maxev} events')
    tot = good = 0; t0 = time.time()
    for K in (1, 2, 3):
        for nm1 in (0, 1):
            if nm1 > K: continue
            ms = [1 if i < nm1 else 3 for i in range(K)]
            gch = [gap_choices(m) for m in ms]; ich = [(5, 9, BIG)] * (K - 1)
            if K == 3:          # pairs (1,2) are exhaustive at K = 2; here block 1 is loose and feeds the pair (2,3)
                gch[0] = [gch[0][-1]]; ich[0] = (5, BIG)
            for lab in words(K, nm1):
                for gs in itertools.product(*gch):
                    for inters in itertools.product(*ich):
                        r = check_chain_word(lab, nm1, ms, gs, inters, chain_run)
                        if r is None: continue
                        tot += len(r); good += sum(r)
    claim('S3', 'Lemma C and C\' on the exact defect model, EXHAUSTIVE for K <= 2 and for the pair (2,3) at K = 3: every '
          'word of shape D^a [W] U^b, gaps {1,5,big} / {4,8,big} / inter {5,9,big}, visits from the right and carry '
          'backs from the left',
          good == tot, f'{good}/{tot} runs match, no collision or halt, {time.time() - t0:.0f} s')
    rng = random.Random(7); tot = good = 0
    for it in range(4000):
        K = rng.randint(3, 10); nm1 = rng.choice([1, 1, 0])
        ms = [1 if i < nm1 else 3 for i in range(K)]
        if rng.random() < 0.3:                       # all full: carry-out, then carry back
            a = rng.randint(0, K)
            lab = tuple(['D0'] * a + [('D0' if i < nm1 else 'U2') for i in range(a, K)])
        else:
            a = rng.randint(0, K); w = rng.choice([0, 1]) if a >= nm1 else 0
            if a + w > K: w = 0
            lab = []
            for i in range(K):
                if i < a: lab.append(rng.choice(['D2', 'D1', 'D0']))
                elif i < a + w: lab.append(rng.choice(['W0', 'W1']))
                else: lab.append(rng.choice(['U0', 'U1'] if i < nm1 else ['U0', 'U1', 'U2']))
            lab = tuple(lab)
        gs = [gap_choices(m, rng) for m in ms]
        inters = [rng.choice([5, 5, 9, 1 + 4 * rng.randint(3, 3000)]) for _ in range(K - 1)]
        r = check_chain_word(lab, nm1, ms, gs, inters, chain_run)
        if r is None: continue
        tot += len(r); good += sum(r)
    claim('S3', 'Lemma C and C\' on the exact defect model, RANDOM: 4,000 chains with K = 3..10, tight gaps with '
          'probability >= 1/2 each', good == tot, f'{good}/{tot} runs match')
    claim('S3', 'chain events never put a defect left of A - 1 (A = base of the m=1 block - 2)',
          STAT['minA'] >= -1, f"leftmost defect seen at A{STAT['minA']:+d}")
    if FULL:
        out = subprocess.run([sys.executable, '-B', 'chain_tight.py', '3'], cwd=os.path.join(SC, 'closeout3'),
                             capture_output=True, text=True).stdout
        mm = re.search(r'K <= 3: (\d+)/(\d+)', out)
        claim('S3', 'Lemma C and C\' on the compressed TM, EXHAUSTIVE for K = 3 (every adjacent pair, every arrival)',
              mm and mm.group(1) == mm.group(2) and 'ALL OK' in out, mm.group(0) if mm else out[-300:])


# ------------------------------------------------------------------------------------------------- S4
def lemma_T_words(K):
    w = ('U0',) * K; nm1 = 1; v = 0; first0 = None; late2 = 0; carries = []; okD = True; ncar = 0
    while len(carries) < 81:
        v += 1
        side, w2 = predict(w, nm1)
        if side == 'L':
            carries.append(v)
            if len(carries) >= 2: okD &= all(x == 'D0' for x in w)
            w2 = predict_carryback(w, nm1)
            if len(carries) >= 2: okD &= all(x == 'D2' for x in w2)
            ph = 0 if all(x[0] == 'D' for x in w2) else 2
        else:
            j = max(i for i in range(K) if w[i] not in ('U2', 'D0'))
            ph = 0 if (w[j][0] == 'D' and w2[-1][0] == 'D') else 2
        if ph == 0 and first0 is None: first0 = v
        if ph == 2 and first0 is not None: late2 += 1
        w = w2
    TK = (3 ** (K + 1) - 5) // 2
    spacing = all(c == (i + 1) * 3 ** K for i, c in enumerate(carries))
    return first0 - 1 == TK and late2 == 0 and spacing and okD


def lemma_T_model(K, rng):
    ms = [1] + [3] * (K - 1); lab = ('U0',) * K
    gs = [gap_choices(m, rng) for m in ms]
    inters = [rng.choice([5, 9, 1 + 4 * rng.randint(3, 500)]) for _ in range(K - 1)]
    p, bases = build(lab, ms, gs, inters)
    if any(q2 <= q1 for q1, q2 in zip(p, p[1:])): return None
    cK = (bases[-1] + 1) % 4; c1 = (bases[0] + 1) % 4; A = bases[0] - 2
    pos = tuple(p); v = 0; carries = []; phases = []; okD = True
    while len(carries) < 81:
        v += 1
        xs, xphi, q = chain_run(pos, 'R', cK, A)
        if xs == 'L':
            if (xphi - c1) % 4 != 2: return False
            carries.append(v)
            if len(carries) >= 2: okD &= all(x == 'D0' for x in read(q, ms, gs, bases))
            xs, xphi, q = chain_run(q, 'L', c1 + 2, A)
            if xs != 'R': return False
            if len(carries) >= 2: okD &= all(x == 'D2' for x in read(q, ms, gs, bases))
        elif xs != 'R':
            return False
        phases.append((xphi - cK) % 4); pos = q
    TK = (3 ** (K + 1) - 5) // 2
    return (phases == [2] * TK + [0] * (len(phases) - TK) and okD
            and all(c == (i + 1) * 3 ** K for i, c in enumerate(carries)) and v == 81 * 3 ** K)


def s4():
    res = {K: lemma_T_words(K) for K in range(2, 10)}
    claim('S4', 'Lemma T on chain words, K = 2..9: first T(K) = (3^(K+1)-5)/2 exits at c_K+2, then c_K only; a carry-out '
          'every 3^K visits; all D0 at carry-outs 2..81, all D2 after their carry backs', all(res.values()), f'{res}')
    rng = random.Random(11); Ks = range(2, 10 if FULL else 9); res = {}; t0 = time.time()
    for K in Ks:
        r = None
        while r is None: r = lemma_T_model(K, rng)
        res[K] = r
    claim('S4', f'Lemma T on the exact defect model (chain alone, re-entered from the left at c_1+2 after each carry-out), '
          f'K = {min(Ks)}..{max(Ks)}, 81 x 3^K visits each', all(res.values()), f'{res}, {time.time() - t0:.0f} s')


# ------------------------------------------------------------------------------------------------- S5
W1 = (-32, -27, -26, -21, -20, -15, -14, -9, -8, -4)
PL = (-27, -21, -15, -9)


def left_word(i):
    v = i - 1; dig = [(v // 3 ** (3 - j)) % 3 for j in range(4)]
    return tuple(sorted([-32, -4] + [PL[j] - dig[j] for j in range(4)] + [PL[j] + 1 for j in range(4)]))


LSTAT = {'ev': 0, 'steps': 0}


def left_episode(lo_rel, ds, ph, chain=(), A=1000):
    mm = Model([A + x for x in ds] + [A + x for x in chain], A + lo_rel, A + 10 ** 6, A - 1, -1, A + ph)
    near = False; hal = False; nev = 0
    for _ in range(100000):
        if mm.dir > 0 and mm.next_right() >= A: break
        e = mm.next_left() if mm.dir < 0 else mm.next_right()
        if e >= A - 3: near = True
        kind, cell, k = mm.event(); nev += 1
        LSTAT['ev'] = max(LSTAT['ev'], nev); LSTAT['steps'] = max(LSTAT['steps'], mm.steps + abs(A - mm.p))
        if kind == 'halt': hal = True; break
    i = bisect.bisect_left(mm.D, A)
    return (mm.lo - A, tuple(x - A for x in mm.D[:i])), (mm.phi - A) % 4, tuple(x - A for x in mm.D[i:]), near, hal


def rel(x):
    return 'A' if x == 0 else f'A{x:+d}'


def episode81():
    """proof.md 4.2, Lemma L81: episode 81 with the whole chain in D0 (block 1 = (A; A+3), blocks 2, 3 at the tightest
    gaps), traced event by event. Returns (lines, facts)."""
    A = 1000; chain = [0, 3] + [8 + o for o in (-2, 2, 6, 9)] + [22 + o for o in (-2, 2, 6, 9)]
    mm = Model([A + x for x in left_word(81)] + [A + x for x in chain], A - 34, A + 10 ** 6, A - 1, -1, A + 1)
    lines = []; n = 0; f = dict(max_event=-10 ** 9, tests=[], halt=False)
    while not (mm.dir > 0 and mm.next_right() >= A):
        e = mm.next_left() if mm.dir < 0 else mm.next_right()
        d = (e - mm.phi) % 4; dr = 'L' if mm.dir < 0 else 'R'; D0 = set(mm.D); lo0 = mm.lo
        if dr == 'R' and d == 1: f['tests'].append(mm.isdef(e + 1))
        kind, cell, k = mm.event(); n += 1
        f['max_event'] = max(f['max_event'], e - A)
        if kind == 'halt': f['halt'] = True; break
        D1 = set(mm.D); gone = sorted(x - A for x in D0 - D1); new = sorted(x - A for x in D1 - D0)
        if kind == 'pass': what = 'pass'
        elif kind == 'wiggle': what = f'wiggle: {rel(gone[0])} -> {rel(new[0])} (e+1 = {rel(e + 1 - A)} is no defect)'
        elif mm.lo != lo0: what = f'turn at the blank end: lo {rel(lo0 - A)} -> {rel(mm.lo - A)}, {rel(new[0])} is now a defect'
        else: what = f'turn: {rel(gone[0])} -> {rel(new[0])}'
        lines.append(f'{n:3}  {dr}  {rel(e - A):6} d={d}  {what}')
    f.update(n=n, end_p=mm.p - A, end_dir=mm.dir, end_phi=(mm.phi - A) % 4, next=mm.next_right() - A, lo=mm.lo - A,
             left=tuple(x - A for x in mm.D if x < A), chain=tuple(x - A for x in mm.D if x >= A) == tuple(chain))
    return lines, f


def s5():
    lines, f = episode81()
    claim('S5', 'Lemma L81: episode 81 with the chain all D0 (block 1 at (A; A+3)) has 31 events, none at a defect >= A; '
          'every rightward d = 1 event finds no defect at e+1 (no halt); the chain is untouched',
          f['n'] == 31 and f['max_event'] <= -1 and not f['halt'] and not any(f['tests']) and f['chain'],
          f'{f["n"]} events, {len(f["tests"])} wiggle tests, last event at A{f["max_event"]:+d}')
    claim('S5', 'Lemma L81: afterwards lo = A-37, the left defects are W_1 - 3 plus A-1, and the head is on cell A moving '
          'right at phase 1 relative to A (= c_1 + 2), its next defect being block 1\'s digit at A (d = 3)',
          f['lo'] == -37 and f['left'] == tuple(sorted([x - 3 for x in W1] + [-1])) and f['end_p'] == 0 and
          f['end_dir'] == 1 and f['end_phi'] == 1 and f['next'] == 0)
    w = (-34, W1); ph = 1; ok_form = ok_ph = True; seen = set(); hal = False
    words_ = []
    for i in range(1, 82):
        ok_form &= w == (-34, left_word(i)); seen.add(w); words_.append(w)
        w2, ph2, rest, near, h = left_episode(w[0], w[1], ph)
        hal |= h; ok_ph &= ph2 == 1
        if i < 81: w = w2
    rec = w2
    claim('S5', 'the 81 left words: W_i = {A-32, A-4} plus four m=1 blocks (A+p_j - v_j ; A+p_j+1), p = (-27,-21,-15,-9), '
          'v = base-3 digits of i-1; episode i turns W_i into W_(i+1)', ok_form and len(seen) == 81 and not hal)
    claim('S5', 'every left episode is entered and left at phase 1 relative to A (= c_1 + 2); at most 31 events and '
          'fewer than 100 steps each', ok_ph and LSTAT['ev'] <= 31 and LSTAT['steps'] < 100, f"{LSTAT}")
    exp = (-37, tuple(sorted([x - 3 for x in W1] + [-1])))
    claim('S5', 'episode 81 (the left record): lo moves 3 left and the word becomes W_1 - 3 plus a new defect at A-1',
          rec == exp, f'{rec}')
    FULLB = {'U2': (-2, 1, 5, 9), 'D0': (-2, 2, 6, 9)}
    good = tot = 0; maxw = max(max(x[1]) for x in words_)
    for i, w in enumerate(words_):
        for s2, s3 in itertools.product(FULLB, FULLB):
            chain = [0, 3]; b2 = 8; chain += [b2 + o for o in FULLB[s2]]
            b3 = b2 + 9 + 5; chain += [b3 + o for o in FULLB[s3]]; chain += [b3 + 9 + 4001]
            w2, ph2, rest, near, h = left_episode(w[0], w[1], 1, chain)
            alone = left_episode(w[0], w[1], 1)
            ok = (w2, ph2) == alone[:2] and list(rest) == chain and not h
            if i < 80: ok &= not near
            tot += 1; good += ok
    claim('S5', 'in context (first three chain blocks full, tightest gaps): same result, chain untouched, episodes 1-80 '
          'have no event at a defect >= A-3; every left word ends at A-4', good == tot and maxw == -4,
          f'{good}/{tot}, last left-word defect A{maxw:+d}')


# ------------------------------------------------------------------------------------------------- S6
def tab_entries():
    out = []
    for r in ORDER:
        for (xp, sh), sigs in tab[r].items():
            assert len(sigs) == 1
            out.append((r, xp, sh, next(iter(sigs))))
    return out


def right_run(gaps, xp, B=100002):
    """Synthetic tape: only the right region (defects B+g1, ..., hi), head about to cross B rightward at phase c_K+xp,
    c_K = B - 2 mod 4. Runs until the head is about to cross B leftward."""
    cK = (B - 2) % 4
    pts = []; x = B
    for g in gaps: x += g; pts.append(x)
    xs, hi = pts[:-1], pts[-1]
    m = Model(list(xs), B - 40, hi, B + 1, 1, cK + xp)
    te = tm = tw = 0; ev = 0; minpos = {}
    bounds = list(zip([B] + xs, xs + [hi]))
    while True:
        if m.dir < 0 and m.next_left() <= B: break
        kind, cell, k = m.event(); ev += 1
        if kind == 'halt': return None
        if ev > 200000: return None
        if kind == 'turnL':
            if cell >= m.hi - 1 or (not m.D) or cell > m.D[-1] + 1: te += 1
            else: tm += 1
        elif kind == 'wiggle': tw += 1
        if kind != 'pass':
            allp = [B] + list(m.D) + [m.hi]
            for gi, (a, b) in enumerate(bounds):
                if b - a < T: continue
                mid = (a + b) // 2; j = bisect.bisect_right(allp, mid)
                minpos[gi] = min(minpos.get(gi, 10 ** 12), allp[j] - allp[j - 1])
    i = bisect.bisect_right(m.D, B)
    return dict(ret=(m.phi - cK) % 4, ys=tuple(m.D[i:]), hi=m.hi, te=te, tm=tm, tw=tw, xs=xs, hiold=hi,
                shrink=max([gaps[gi] - v for gi, v in minpos.items()] + [0]))


def sig_predict(xs, hi, sig):
    anchors = list(xs) + [hi]
    ep, te, tm, tw, ny, nh = sig
    return tuple(anchors[a] + o for a, o in ny), anchors[nh[0]] + nh[1]


def right_free(gaps, xp, B=100002):
    """proof.md 4.3, transfer form of Lemma R: run the entry once and mark every edge that ever holds a defect (the blank
    zone above hi included) or is toggled or tested. Returns (smallest number of consecutive unmarked edges inside a long
    gap, smallest marked edge - x_1)."""
    cK = (B - 2) % 4
    pts = []; x = B
    for g in gaps: x += g; pts.append(x)
    xs, hi = pts[:-1], pts[-1]
    m = Model(list(xs), B - 40, hi, B + 1, 1, cK + xp)
    occ = set(xs); minhi = hi; ev = 0
    while not (m.dir < 0 and m.next_left() <= B):
        e = m.next_left() if m.dir < 0 else m.next_right()
        kind, cell, k = m.event(); ev += 1
        if kind == 'halt' or ev > 200000: return None
        occ |= {'turnR': {e - 1, e}, 'turnL': {e, e + 1}, 'wiggle': {e, e + 1, e + 2}}.get(kind, set())
        occ |= set(m.D); minhi = min(minhi, m.hi)
    occ |= set(range(minhi, hi + 1))
    anchors = [B] + pts; free = []
    for i, g in enumerate(gaps):
        if g < T: continue
        best = run = 0
        for y in range(anchors[i] + 1, anchors[i + 1]):
            run = 0 if y in occ else run + 1; best = max(best, run)
        free.append(best)
    return min(free), min(occ) - pts[0]


def s6():
    ents = tab_entries()
    fr = [right_free([g if not isinstance(g, tuple) else T + ((g[1] - T) % 4) for g in sh], xp) for (r, xp, sh, sig) in ents]
    claim('S6', 'transfer form of Lemma R: in every entry run at the minimal long gaps, every long gap keeps a stretch of at '
          'least 11 consecutive edges that never hold a defect and are never toggled or tested, and no edge left of x_1 is '
          'ever touched', all(x is not None for x in fr) and min(x[0] for x in fr) >= 11 and min(x[1] for x in fr) >= 0,
          f'smallest free stretch {min(x[0] for x in fr)} edges, nearest touched edge x_1{min(x[1] for x in fr):+d}')
    cnt = {r: sum(1 for e in ents if e[0] == r) for r in ORDER}
    claim('S6', 'the right table has 81 entries: r0 13, r1 9, r2 13, r3 13, r4 10, r5 23', len(ents) == 81 and
          cnt == {5: 23, 0: 13, 1: 9, 2: 13, 3: 13, 4: 10}, f'{cnt}')
    claim('S6', 'every entry returns the head at phase c_K', all(e[3][0] == 0 for e in ents))
    claim('S6', 'the first gap B -> x_1 is long in every entry', all(isinstance(e[2][0], tuple) for e in ents))
    rng = random.Random(5); tot_min = ok_min = tot_c = ok_c = tot_r = ok_r = 0; worst = 0; t0 = time.time()
    for (r, xp, sh, sig) in ents:
        Li = [i for i, g in enumerate(sh) if isinstance(g, tuple)]
        base = [g if not isinstance(g, tuple) else T + ((g[1] - T) % 4) for g in sh]

        def one(gs):
            res = right_run(gs, xp)
            if res is None: return False, 0
            ys, hi2 = sig_predict(res['xs'], res['hiold'], sig)
            return (res['ret'] == sig[0] and res['ys'] == ys and res['hi'] == hi2 and
                    (res['te'], res['tm'], res['tw']) == sig[1:4]), res['shrink']
        ok, sh0 = one(base); tot_min += 1; ok_min += ok; worst = max(worst, sh0)
        for combo in itertools.product((0, 4), repeat=len(Li)):
            gs = list(base)
            for i, a in zip(Li, combo): gs[i] += a
            ok, s_ = one(gs); tot_c += 1; ok_c += ok; worst = max(worst, s_)
        for _ in range(10):
            gs = list(base)
            for i in Li: gs[i] += 4 * rng.randint(0, 10 ** 6)
            ok, s_ = one(gs); tot_r += 1; ok_r += ok
    claim('S6', 'every entry, all long gaps at their smallest value (24..27 by residue): the table\'s result',
          ok_min == tot_min, f'{ok_min}/{tot_min}')
    claim('S6', 'EXHAUSTIVE: every entry with every long gap in {min, min+4}, all combinations', ok_c == tot_c,
          f'{ok_c}/{tot_c}, {time.time() - t0:.0f} s')
    claim('S6', 'RANDOM: every entry with every long gap + 4j, j up to 10^6 (10 per entry)', ok_r == tot_r,
          f'{ok_r}/{tot_r}')
    claim('S6', 'no long gap shrinks by more than 12 within an episode (so it stays >= 12 when it starts >= 24)',
          worst <= 12, f'largest shrink {worst}')


# ------------------------------------------------------------------------------------------------- S7
def P(s):
    """'8316u-39' or '(19683u-1)/2' -> Aff."""
    s = s.replace(' ', '')
    den = 1
    mm = re.fullmatch(r'\((.*)\)/(\d+)', s)
    if mm: s, den = mm.group(1), int(mm.group(2))
    mm = re.fullmatch(r'(\d+)u([+-]\d+)', s)
    if mm: return Aff(Fr(int(mm.group(2)), den), Fr(int(mm.group(1)), den))
    return Aff(Fr(int(s), den))


VTAB = {   # proof.md section 3.4, verbatim
    5: ('8316u-39, 24948u-36, 74844u-36', '224532u-39, 673596u-37, 7, (19683u-1)/2, 1942056u-16, 3'),
    0: ('8316u-36, 24948u-36', '74844u-39, 224532u-37, 673596u-36, 2020788u-36, 4, (1043199u+7)/2'),
    1: ('8316u-36, 24948u-35, 74844u-39, 224532u-36, 673596u-36', '2020788u-39, 7, 551124u-4, (3129597u-1)/2, 2'),
    2: ('', '8316u-39, 24948u-37, 74844u-36, 224532u-36, 673596u-37, 2020788u-37, 8, (59049u-7)/2, 5826168u-7, 3'),
    3: ('74844u-36', '224532u-39, 673596u-37, 2020788u-36, 6062364u-36, 3, (3129597u+5)/2, 2'),
    4: ('', '74844u-39, 224532u-37, 673596u-36, 2020788u-36, 6062364u-37, 7, 1653372u-4, (9388791u+3)/2, 3'),
}
V = {r: ([P(x) for x in c.split(',')] if c else [], [P(x) for x in R.split(',')]) for r, (c, R) in VTAB.items()}
PROGRAM = {}


def entry(r, xp, sh):
    ent = tab[r].get((xp, sh))
    assert ent is not None and len(ent) == 1, ('shape not in the table', r, xp, sh)
    return next(iter(ent))


def interval_checked(r, gaps, V1, E, prog=None):
    """The interval through the table, with 4-cycles jumped. Every jump is verified independently: the cycle's linear
    part fixes its increment (M d = d), and the four shapes of the cycle hold at the first and the last jumped cycle (all
    gaps are affine in the cycle index, so they hold in between), for every u."""
    trips = Aff(0); nsteps = 0
    for xp, R in ((2, V1), (0, E - V1)):
        hist = []
        while not (R.a == 0 and R.b == 0):
            assert R.b >= 0 and R.at(1) >= 1, ('negative remaining', R)
            sh = tuple(gshape(g) for g in gaps); sig = entry(r, xp, sh)
            hist.append((sh, list(gaps), sig))
            gaps, te = apply(gaps, sig); trips = trips + te; R = R - 1; nsteps += 1
            if prog is not None: prog.append(('step', xp, sh, list(gaps), R))
            if len(hist) >= 4 and R.b > 0 and len(gaps) == len(hist[-4][1]) and \
                    tuple(gshape(g) for g in gaps) == hist[-4][0]:
                cyc = hist[-4:]; d = [g - h for g, h in zip(gaps, cyc[0][1])]
                assert all(x.b == 0 and x.a % 4 == 0 for x in d)
                sigs = [c[2] for c in cyc]; shapes = [c[0] for c in cyc]
                m = 4 + int((R.at(1) - 4) % 4)
                c = Aff((R.a - m) / 4, R.b / 4)
                assert c.b > 0 and (8 * c.b).denominator == 1 and c.at(1) == int(c.at(1)) and c.at(1) >= 1

                def run4(g0):
                    g = list(g0); tr = Aff(0)
                    for s_, sg in zip(shapes, sigs):
                        assert tuple(gshape(x) for x in g) == s_, 'cycle shape broken'
                        g, te_ = apply(g, sg); tr = tr + te_
                    return g, tr
                g_first = list(gaps); R_before = R
                g1, ctr = run4(gaps)
                g2, _ = run4([g + x for g, x in zip(gaps, d)])
                assert all(a - b == x for a, b, x in zip(g2, g1, d)), 'M d != d'
                assert all(a - b == x for a, b, x in zip(g1, gaps, d))
                last = [g + x * (c - 1).a + Aff(0, x.a * (c - 1).b) for g, x in zip(gaps, d)]
                run4(last)                                  # shapes hold at the last jumped cycle, every u
                gaps = [g + Aff(x.a * c.a, x.a * c.b) for g, x in zip(gaps, d)]
                assert ctr.b == 0
                trips = trips + Aff(ctr.a * c.a, ctr.a * c.b)
                R = R - Aff(4 * c.a, 4 * c.b)
                if prog is not None: prog.append(('jump', xp, c, [x.a for x in d], ctr, shapes, R_before, g_first, last, list(gaps), R, m))
                hist = []
    return gaps, trips


def record_visit(r, Vc, End, dropoff=None):
    """Record visit + regroup + exchange (proof.md 6.1-6.3) on the window; returns (new chain window, new right gaps)."""
    pos = [Aff(0)]
    for g in reversed(Vc): pos.insert(0, pos[0] - g)
    nd = len(pos); xs = []; p = Aff(2)
    for g in End: p = p + g; xs.append(p)
    hi = xs.pop(); d = W.EXCH[r]; new = []
    for idx, q in enumerate(pos):
        i = nd - 1 - idx; dropped = d < 0 and i < -d
        new.append(q + (W.OFF0 if dropped else W.OFF2)[i % 4])
    if d < 0: chain_new = new[:nd + d]; right_new = new[nd + d:] + xs
    else: chain_new = new + xs[:d]; right_new = xs[d:]
    Bn = chain_new[-1] + 2; pts = [Bn] + right_new + [hi]
    VR2 = [y - x for x, y in zip(pts, pts[1:])]
    cg2 = [y - x for x, y in zip(chain_new, chain_new[1:])]
    Jn = W.J[NXT[r]]
    assert len(cg2) >= Jn
    deep = []
    for k in range(Jn + 1, len(cg2) + 1):
        g = cg2[-k]; ro = W.gap_role(k)
        deep.append(g.b >= 0 and int(g.at(1)) % 4 == W.RES[ro] and (8 * g.b) % 4 == 0 and g.at(1) >= W.MIN[ro])
    return (cg2[len(cg2) - Jn:] if Jn else []), VR2, all(deep), len(deep)


class LF:
    """A linear form sum(coef * var) + const over named gap variables (proof.md 5.3 / 6.4 formulas)."""
    def __init__(s, c=0, v=None): s.c = Fr(c); s.v = {k: Fr(x) for k, x in (v or {}).items() if x}
    def __add__(s, o):
        o = o if isinstance(o, LF) else LF(o); v = dict(s.v)
        for k, x in o.v.items(): v[k] = v.get(k, 0) + x
        return LF(s.c + o.c, v)
    def __sub__(s, o): o = o if isinstance(o, LF) else LF(o); return s + LF(-o.c, {k: -x for k, x in o.v.items()})
    def ev(s, env):
        out = Aff(s.c)
        for k, x in s.v.items(): out = out + env[k] * x
        return out
    def __str__(s):
        def key(k): return (k.rstrip('0123456789'), int(k[len(k.rstrip('0123456789')):]))
        t = ' + '.join((k if x == 1 else f'{x}{k}') for k, x in sorted(s.v.items(), key=lambda kv: key(kv[0])))
        if not t: return str(s.c)
        return t + (f' + {s.c}' if s.c > 0 else f' - {-s.c}' if s.c < 0 else '')


def gap_map(sig, ins):
    """An entry applied to a gap vector of linear forms (proof.md 4.3: new defects = old defect + offset)."""
    pos = []; p = LF(0)
    for g in ins: p = p + g; pos.append(p)
    ep, te, tm, tw, ny, nh = sig
    newpos = [pos[a] + o for a, o in ny] + [pos[nh[0]] + nh[1]]
    out = []; prev = LF(0)
    for q in newpos: out.append(q - prev); prev = q
    return out


def shape_vars(sh, name='g'):
    return [LF(0, {f'{name}{i + 1}': 1}) if isinstance(g, tuple) else LF(g) for i, g in enumerate(sh)]


def fmt_vec(v):
    return '(' + ', '.join(str(x) for x in v) + ')'


def cycle_composite(r, xp, shapes):
    """The composite of a 4-cycle's gap maps on variables h1..hn (long gaps) and the shape's small gaps."""
    v = shape_vars(shapes[0], 'h')
    for sh in shapes: v = gap_map(entry(r, xp, sh), v)
    return v


def record_visit_formulas(r, J, n_end):
    """proof.md 6.4: the record visit (D2/D0 offsets, exchange, regrouping) on symbolic windows: chain window c1..cJ
    (cJ ends at B-2), right region E1..En. Returns (new chain window, new right vector, gaps that go deep)."""
    pos = [LF(0)]
    for k in range(J, 0, -1): pos.insert(0, pos[0] - LF(0, {f'c{k}': 1}))
    nd = len(pos); xs = []; p = LF(2)
    for k in range(1, n_end + 1): p = p + LF(0, {f'E{k}': 1}); xs.append(p)
    hi = xs.pop(); d = W.EXCH[r]; new = []
    for idx, q in enumerate(pos):
        i = nd - 1 - idx; dropped = d < 0 and i < -d
        new.append(q + (W.OFF0 if dropped else W.OFF2)[i % 4])
    if d < 0: chain_new = new[:nd + d]; right_new = new[nd + d:] + xs
    else: chain_new = new + xs[:d]; right_new = xs[d:]
    pts = [chain_new[-1] + 2] + right_new + [hi]
    VR2 = [y - x for x, y in zip(pts, pts[1:])]
    cg2 = [y - x for x, y in zip(chain_new, chain_new[1:])]
    Jn = W.J[NXT[r]]
    return (cg2[len(cg2) - Jn:] if Jn else []), VR2, cg2[:len(cg2) - Jn]


def int_interval(r, gaps, V1, E):
    tb = {k: next(iter(v)) for k, v in tab[r].items()}
    for xp, n in ((2, V1), (0, E - V1)):
        for _ in range(n):
            sh = tuple(g if g < T else ('L', g % 4) for g in gaps)
            ep, te, tm, tw, ny, nh = tb[(xp, sh)]
            pos = []; s = 0
            for g in gaps: s += g; pos.append(s)
            newpos = [pos[a] + o for a, o in ny] + [pos[nh[0]] + nh[1]]
            prev = 0; gaps = []
            for q in newpos: gaps.append(q - prev); prev = q
    return gaps


def concrete_step(r, K, cw, R):
    """Lemma S on exact numbers, no acceleration: record-exit entry, 81 x 3^K - 1 episodes, record visit."""
    sig = entry(r, 2, tuple(g if g < T else ('L', g % 4) for g in R))
    S, _ = apply([Aff(g) for g in R], sig)
    V1 = (3 ** (K + 1) - 5) // 2; E = 81 * 3 ** K - 1
    End = int_interval(r, [int(g.a) for g in S], V1, E)
    c2, R2, dok, nd = record_visit(r, [Aff(g) for g in cw], [Aff(g) for g in End])
    return [int(x.a) for x in c2], [int(x.a) for x in R2], dok


SNAP = {}


def load_snaps():
    if SNAP: return
    for tag, files in (('341', ['snap_341.pkl', 'snap_341_e3.pkl']), ('512', ['snap_512.pkl']), ('588', ['snap_588.pkl'])):
        SNAP[tag] = {}
        for f in files:
            SNAP[tag].update(pickle.load(open(os.path.join(SC, 'closeout3', 'results', f), 'rb')))


def window_of(n, s):
    ok, cg, R = W.member(n, s); r = W.cls(n)
    return ok, (cg[len(cg) - W.J[r]:] if W.J[r] else []), R


def s7():
    load_snaps()
    okfit = True
    for i, r in enumerate(ORDER):
        _, c2, R2 = window_of(28 + i, SNAP['341'][28 + i]); _, c3, R3 = window_of(34 + i, SNAP['341'][34 + i])
        Vc = [W.fit(a, b) for a, b in zip(c2, c3)]; VR = [W.fit(a, b) for a, b in zip(R2, R3)]
        okfit &= Vc == V[r][0] and VR == V[r][1] and len(Vc) == len(V[r][0]) and len(VR) == len(V[r][1])
    claim('S7', 'the window vectors V_r(u) of proof.md 3.4 are the record-exit windows of the run at u = 1 and u = 9',
          okfit)
    allok = True; t0 = time.time()
    for r in ORDER:
        Vc, VR = V[r]; k0 = K0[r] + 4
        sig = entry(r, 2, tuple(gshape(g) for g in VR)); S, _ = apply(VR, sig)
        V1 = Aff(Fr(-5, 2), Fr(3 ** (k0 + 1), 2)); E = Aff(-1, 3 ** (k0 + 4))
        prog = []
        End, trips = interval_checked(r, S, V1, E, prog)
        PROGRAM[r] = (S, prog, End)
        End2 = run_interval(r, S, V1, E)[0]
        same = len(End) == len(End2) and all(a == b for a, b in zip(End, End2))
        c2, R2, dok, nd = record_visit(r, Vc, End)
        tc, tR = V[NXT[r]]
        if r == 4: tc = [W.scale9(x) for x in tc]; tR = [W.scale9(x) for x in tR]
        ok = same and dok and len(c2) == len(tc) and all(a == b for a, b in zip(c2, tc)) and \
            len(R2) == len(tR) and all(a == b for a, b in zip(R2, tR))
        njump = sum(1 for p in prog if p[0] == 'jump'); nst = sum(1 for p in prog if p[0] == 'step')
        claim('S7', f'Lemma S symbolically, r{r} -> r{NXT[r]}{" (u -> 9u)" if r == 4 else ""}: record-exit entry, '
              f'interval ({nst} single episodes + {njump} verified 4-cycle jumps), record visit, regroup, exchange '
              f'give V_r{NXT[r]}', ok, f'{nd} gaps go to the deep chain with U0 residues/minimums')
        allok &= ok
    # proof.md 5.3: the composite of every 4-cycle is a translation on its long gaps (linear part = identity)
    ok = True; ncyc = 0
    for r in ORDER:
        S, prog, End = PROGRAM[r]
        for p in prog:
            if p[0] != 'jump': continue
            ncyc += 1; xp, c, d, ctr, shapes = p[1:6]
            comp = cycle_composite(r, xp, shapes)
            for i, (g, x) in enumerate(zip(comp, d)):
                if isinstance(shapes[0][i], tuple):
                    ok &= g.v == {f'h{i + 1}': 1} and g.c == x
                else:
                    ok &= not g.v and g.c == shapes[0][i] and x == 0
    claim('S7', 'every 4-cycle of Appendix B, composed symbolically from its four gap maps, is f(h) = h + d: each long gap '
          'maps to itself plus its increment, each small gap to its own value (so f(h + d) = f(h) + d)', ok and ncyc == 12,
          f'{ncyc} cycles')
    # proof.md 6.4: the record-visit formulas, evaluated on V_r (chain) and the interval end, give V_(r+1)
    ok = True
    for r in ORDER:
        Vc, VR = V[r]; S, prog, End = PROGRAM[r]
        fc, fR, fdeep = record_visit_formulas(r, len(Vc), len(End))
        env = {f'c{k + 1}': g for k, g in enumerate(Vc)}; env.update({f'E{k + 1}': g for k, g in enumerate(End)})
        tc, tR = V[NXT[r]]
        if r == 4: tc = [W.scale9(x) for x in tc]; tR = [W.scale9(x) for x in tR]
        gc = [x.ev(env) for x in fc]; gR = [x.ev(env) for x in fR]
        ok &= len(gc) == len(tc) and all(a == b for a, b in zip(gc, tc)) and len(gR) == len(tR) and \
            all(a == b for a, b in zip(gR, tR))
    res = lambda g: int(g.at(1)) % 4 if (8 * g.b) % 4 == 0 and g.b >= 0 else None
    claim('S7', 'take-in classes r0, r2, r4: the interval ends with E_1 = 1 and E_2 = E_3 = 0 mod 4 for every u = 1 mod 8, '
          'all three long (so x_1, x_2, x_3 = c_K + 3 and are passed with d = 3, 2, 3: proof.md 6.3)',
          all([res(g) for g in PROGRAM[r][2][:3]] == [1, 0, 0] and all(g.at(1) >= T for g in PROGRAM[r][2][:3])
              for r in (0, 2, 4)))
    claim('S7', 'the explicit record-visit formulas of proof.md 6.4, evaluated on V_r and the interval end, '
          'give V_(r+1) for all six classes', ok)
    # concrete, no acceleration
    for tag in ('341', '512', '588'):
        good = 0; ns = range(16, 28)
        for n in ns:
            r = W.cls(n); K = K0[r] + 2 * W.epoch(n)
            ok0, cw, R = window_of(n, SNAP[tag][n]); ok1, cw1, R1 = window_of(n + 1, SNAP[tag][n + 1])
            c2, R2, dok = concrete_step(r, K, cw, R)
            good += ok0 and ok1 and dok and c2 == cw1 and R2 == R1
        claim('S7', f'line {tag}: Lemma S on exact numbers (no acceleration) maps record exit n to n+1, n = 16..27',
              good == len(ns), f'{good}/{len(ns)}')
    hi_n = 39
    good = 0; ns = range(28, hi_n + 1)
    for n in ns:
        r = W.cls(n); e = W.epoch(n); K = K0[r] + 2 * e; u = 9 ** (e - 2)
        cw = [int(x.at(u)) for x in V[r][0]]; R = [int(x.at(u)) for x in V[r][1]]
        c2, R2, dok = concrete_step(r, K, cw, R)
        r1 = NXT[r]; u1 = u * 9 if r == 4 else u
        good += dok and c2 == [int(x.at(u1)) for x in V[r1][0]] and R2 == [int(x.at(u1)) for x in V[r1][1]]
    claim('S7', f'Lemma S on exact numbers from V_r(u) (no acceleration), record exits {ns[0]}..{ns[-1]} '
          f'(u = 1, 9; up to {81 * 3 ** (K0[4] + 2 * W.epoch(hi_n)) - 1:,} episodes): gives V_(r+1)',
          good == len(ns), f'{good}/{len(ns)}, {time.time() - t0:.0f} s')


# ------------------------------------------------------------------------------------------------- S8
def u0_chain(K, rng, tight):
    """A chain in state U0 as (C) describes it: (A+2; A+3), then K-1 m=3 blocks; returns positions and A."""
    A = 1000; pos = [A + 2, A + 3]
    for j in range(K - 1):
        gi = 5 if tight else rng.choice([5, 9, 1 + 4 * rng.randint(2, 1000)])
        g1 = 1 if tight else rng.choice([1, 5, 1 + 4 * rng.randint(2, 1000)])
        s1 = 4 if tight else rng.choice([4, 8, 4 * rng.randint(3, 1000)])
        s2 = 4 if tight else rng.choice([4, 8, 4 * rng.randint(3, 1000)])
        b = pos[-1] + gi; pos += [b, b + g1, b + g1 + s1, b + g1 + s1 + s2]
    return pos, A


def is_C(pos, A):
    """(C) for a chain given as positions: m=1 block (A+2; A+3), then m=3 blocks with U0 residues and minimums."""
    if pos[:2] != [A + 2, A + 3] or (len(pos) - 2) % 4: return False
    g = [y - x for x, y in zip(pos, pos[1:])]
    for k in range(1, len(g)):
        ro = (k - 1) % 4      # gap k (1-based after the m=1 gap): 0 inter, 1 digit, 2 sep, 3 sep
        role = {0: 3, 1: 0, 2: 1, 3: 2}[ro]
        if g[k] % 4 != W.RES[role] or g[k] < W.MIN[role]: return False
    bases = [pos[0]] + [pos[2 + 4 * j] for j in range((len(pos) - 2) // 4)]
    return all((b2 - b1) % 4 == 2 for b1, b2 in zip(bases, bases[1:]))


def s8():
    # D2 images and regrouping: new block j = (s3 of old j; digit, s1, s2 of old j+1); the m=1 block takes the new digit
    rng = random.Random(3); good = tot = 0; changes = set()
    for it in range(4000):
        K = rng.randint(2, 9); tight = it < 50
        pos, A = u0_chain(K, rng, tight)
        d2 = [pos[0] - 2, pos[1] + 2] + [x + {0: -2, 1: 1, 2: 1, 3: 2}[i % 4] for i, x in enumerate(pos[2:])]
        new = [A - 1] + d2
        # drop the last defect (one-defect-later regroup leaves the old last s3 as a new digit with no separators):
        # the chain end is handled by the exchange (S7); here the regrouped prefix must be a (C) chain
        body = new[:len(new) - 1]          # A-1, A, then 4(K-1) defects regrouped; last s3 starts the next block
        A2 = A - 3
        tot += 1; good += is_C(body, A2)
        og = [y - x for x, y in zip(pos[1:], pos[2:])]; ng = [y - x for x, y in zip(body[1:], body[2:])]
        for k in range(1, len(ng)):
            changes.add(({1: 'inter', 2: 'digit', 3: 'sep1', 0: 'sep2'}[k % 4], ng[k] - og[k - 1]))
    claim('S8', 'regrouping the D2 chain one defect later, with the new digit at A-1, gives a chain satisfying (C) with '
          'A\' = A-3 (4,000 chains, 50 at the tightest gaps)', good == tot, f'{good}/{tot}')
    exp = {('digit', 3), ('sep1', 0), ('sep2', 1), ('inter', -4)}
    claim('S8', 'gap changes under the regroup: digit -> sep +3, sep1 -> sep2 0, sep2 -> inter +1, inter -> digit -4',
          {c for c in changes} == exp, f'{sorted(changes)}')
    ok = True
    for r in ORDER:
        r1 = NXT[r]; K = K0[r]; K1 = K0[r1] + (2 if r == 4 else 0)
        ndef = 4 * K - 2 + 1 + W.EXCH[r]
        ok &= ndef == 4 * K1 - 2
    claim('S8', 'exchange table: chain defects 4K-2, plus the new left digit, plus the exchange (-1,+3,-5,+3,-1,+3) '
          'give 4K\'-2 with K0 = (3,3,4,3,4,4) + 2e', ok)


# ------------------------------------------------------------------------------------------------- S9
def s9():
    if not PROGRAM:
        s7()
    rates = {}
    for r in ORDER:
        S, prog, End = PROGRAM[r]
        jumps = [p for p in prog if p[0] == 'jump']
        rates[r] = [tuple(int(x) // 4 for x in j[3] if x != 0) for j in jumps]
    exp = {5: [(-3, 24), (3,)], 0: [(9,), (9,)], 1: [(9,), (-1, 8)], 2: [(-9, 72), (9,)], 3: [(9,), (9,)],
           4: [(27,), (-3, 24)]}
    claim('S9', 'per-visit rates of the changing gaps in the two regimes (one 4-cycle jump each): r5 (-3,+24 | +3), '
          'r0 (+9 | +9), r1 (+9 | -1,+8), r2 (-9,+72 | +9), r3 (+9 | +9), r4 (+27 | -3,+24)', rates == exp, f'{rates}')
    # X exhausted / frozen and fossils in the end vectors, w = 81u
    endv = {r: PROGRAM[r][2] for r in ORDER}
    w = lambda c, a: Aff(a, 81 * c)
    has = lambda r, x: any(g == x for g in endv[r])
    ok = has(0, w(6804, -4)) and has(3, w(20412, -4)) and has(5, w(24948, -36)) and has(2, w(74844, -36))
    claim('S9', 'interval ends contain X frozen = 6804w-4 (r0), 20412w-4 (r3) and the new fossils 24948w-36 (r5), '
          '74844w-36 (r2), w = 9^e = 81u', ok)
    ok = all(3 * (6804 * 3 ** k - 4) + 8 == 6804 * 3 ** (k + 1) - 4 for k in range(10)) and \
        all(3 * (24948 * 3 ** k - 36) + 72 == 24948 * 3 ** (k + 1) - 36 for k in range(10))
    claim('S9', 'closed forms X_k = 6804 x 3^(k-4) - 4 and F_j = 24948 x 3^j - 36 satisfy X\' = 3X + 8, F\' = 3F + 72', ok)
    # r5 example of 5.4: X = 3 V1 + 2 at the start, 12 per cycle, 32 left at the switch
    S, prog, End = PROGRAM[5]
    k0 = K0[5] + 4; V1 = Aff(Fr(-5, 2), Fr(3 ** (k0 + 1), 2))
    j = [p for p in prog if p[0] == 'jump'][0]
    xi = [i for i, x in enumerate(j[3]) if x == -12][0]
    X0 = S[xi]; X_last = j[8][xi]; X_after = j[9][xi]
    nx = prog[next(i for i, p in enumerate(prog) if p is j) + 1]
    ok = X0 == V1 * 3 + 2 and X_last == Aff(32) and X_after == Aff(20) and X0 - 12 - j[2] * 12 == Aff(20) and \
        nx[0] == 'step' and nx[2][xi] == 20 and entry_ids()[(5, (nx[1], nx[2]))] == 'r5.5'
    claim('S9', 'r5: X = 3 V1 + 2 cells at the start, 12 eaten per 4-cycle, the u-terms cancel: X is 32 at the start of '
          'the last jumped cycle and 20 after it, and the next entry is r5.5 (shape L1 L3 8 20 L2)', ok,
          f'X = {fmt_aff(X0)}, at the last cycle {fmt_aff(X_last)}, after it {fmt_aff(X_after)}')
    claim('S9', 'w = 9^e = 81u: the fossil and frozen-block laws of 5.4 in u: 24948w-36 = 2020788u-36, 6804w-4 = '
          '551124u-4, 20412w-4 = 1653372u-4, 74844w-36 = 6062364u-36',
          w(24948, -36) == Aff(-36, 2020788) and w(6804, -4) == Aff(-4, 551124) and w(20412, -4) == Aff(-4, 1653372) and
          w(74844, -36) == Aff(-36, 6062364))


# ------------------------------------------------------------------------------------------------- S10
def snapshot16(start='A', shift=0):
    if start == 'A':
        m = model_from_blank()
    else:
        sys.argv = sys.argv[:1]
        from snap import model_from_blank_start
        m = model_from_blank_start(start)
    n = -shift; lo_seen = m.lo; armed = False; saved = None
    while True:
        kind, cell, k = m.event()
        assert kind != 'halt'
        if m.lo < lo_seen:
            lo_seen = m.lo
            if not armed: saved = copy.deepcopy(m)
            armed = True
        if armed and kind == 'turnL' and (not m.D or cell > m.D[-1] + 1):
            armed = False; n += 1
            if n == 16:
                blocks = setup(m); B = blocks[-1][1][-1] + 2
                mm = saved
                while not (mm.dir > 0 and mm.p <= B and mm.next_right() > B):
                    assert mm.event()[0] != 'halt'
                return mm


def lo_moves_runs():
    """Direct simulation (scripts/review1/lo_moves.c) of our table from A, B and F: the moves of lo and the record exit
    by the operational definition of proof.md 3.3."""
    import tempfile
    tmp = tempfile.mkdtemp(); exe = os.path.join(tmp, 'lo_moves')
    subprocess.run(['cc', '-O2', '-o', exe, os.path.join(SC, 'review1', 'lo_moves.c')], check=True)
    out = {}
    for tag, start, k3, n in (('341', 'A', 16, 398100000), ('512', 'B', 16, 398200000), ('588', 'F', 17, 397900000)):
        txt = subprocess.run(['nice', '-n', '10', exe, TM, start, str(n), str(k3), '20'], capture_output=True,
                             text=True).stdout.split('\n')
        moves = [tuple(map(int, l.split()[1:])) for l in txt if l.startswith('L ')]
        bursts = []
        for i, (k, old, new) in enumerate(moves):
            amt = 1 if i == 0 else old - new
            if bursts and k == bursts[-1][1] + 1: bursts[-1] = (bursts[-1][0], k, bursts[-1][2] + amt)
            else: bursts.append((k, k, amt))
        ex = [tuple(map(int, l.split()[1:3])) for l in txt if l.startswith('EXIT ')]
        out[tag] = dict(bursts=bursts, exit=ex[0] if ex else None)
    return out


def from_sim(tm, steps, rename, mirror):
    import sim
    r = sim.run(sim.parse(tm), max_steps=steps)
    c = r.final
    assert not r.halted and r.step == steps
    cells = list(c.tape); lo = c.lo; pos = c.pos; st = rename[c.state]
    if mirror:
        cells = cells[::-1]; lo, pos = -(lo + len(c.tape) - 1), -pos
    cells = [0] * 8 + cells + [0] * 8; lo -= 8
    direction = -1 if (st, cells[pos - lo]) in LCYC else 1
    return model_from_tape(cells, lo, pos, st, direction)


def same_state(m, s):
    return (tuple(m.D), m.lo, m.hi, m.p, m.dir, m.phi % 4) == (tuple(s['D']), s['lo'], s['hi'], s['p'], s['dir'], s['phi'] % 4)


def s10():
    load_snaps()
    for tag, (n0, n1) in (('341', (16, 39)), ('512', (16, 33)), ('588', (16, 33))):
        mem = [W.member(n, SNAP[tag][n])[0] for n in range(n0, n1 + 1)]
        win = []
        for n in range(28, n1 + 1):
            r = W.cls(n); u = 9 ** (W.epoch(n) - 2)
            _, cw, R = window_of(n, SNAP[tag][n])
            win.append(cw == [x.at(u) for x in V[r][0]] and R == [x.at(u) for x in V[r][1]])
        claim('S10', f'line {tag}: record exits {n0}..{n1} satisfy (L), (C), (H) with K = K0(r) + 2e; windows at 28..{n1} '
              f'equal V_r(u)', all(mem) and all(win), f'{sum(mem)}/{len(mem)}, {sum(win)}/{len(win)}')
    # (H) at cell level and the operational definition of B (proof.md 3.3)
    for tag, (n0, n1) in (('341', (16, 39)), ('512', (16, 33)), ('588', (16, 33))):
        good = 0
        for n in range(n0, n1 + 1):
            s = SNAP[tag][n]; r = W.cls(n); K = K0[r] + 2 * W.epoch(n); A = s['lo'] + 34; D = sorted(s['D'])
            cnt = sum(1 for x in D if s['lo'] < x <= s['p'] - 1)
            good += (s['dir'] > 0 and s['p'] == s['B'] - 1 and (s['p'] - s['phi']) % 4 == 3 and cnt == 10 + 4 * K - 2
                     and [x for x in D if x >= A][4 * K - 3] + 2 == s['B'])
        claim('S10', f'line {tag}: at record exits {n0}..{n1} the head is on cell B-1 in state B reading 1 (moving right), '
              f'exactly 10 + 4K - 2 pre-sweep defects lie in (lo, B-2], and B = (the (4K-2)-th defect >= A) + 2 with A = '
              f'lo + 34', good == n1 - n0 + 1, f'{good}/{n1 - n0 + 1}')
    out = lo_moves_runs()
    bursts = out['341']['bursts']
    small = [b for b in bursts if b[2] != 3]; three = [b for b in bursts if b[2] == 3]
    claim('S10', 'line 341, direct simulation: lo (the leftmost cell that has held 1, minus 1) moves left by 1 or 2 cells '
          'only at steps 1, 6-7, 838-839, 7820, 17531-17532; every other move is 3 cells in 3 consecutive steps; the 16th '
          '3-cell move is at steps 398,088,768-770',
          [(b[0], b[1]) for b in small] == [(1, 1), (6, 7), (838, 839), (7820, 7820), (17531, 17532)] and
          all(b[1] - b[0] == 2 for b in three) and len(three) == 16 and three[15][:2] == (398088768, 398088770),
          f'{len(small)} small moves, {len(three)} 3-cell moves')
    claim('S10', 'operational record exit (first moment after the record with the head in state B reading 1 and exactly '
          '10 + 4K - 2 = 20 pre-sweep defects in (lo, h-1]), direct simulation: line 341 after its 16th 3-cell move at '
          'step 398,090,000, head cell 1154; line 512 (our table from B) after its 16th at 398,095,384; line 588 (our '
          'table from F) after its 17th at 397,796,108',
          out['341']['exit'] == (398090000, 1154) and out['512']['exit'][0] == 398095384 and
          out['588']['exit'][0] == 397796108 and SNAP['512'][16]['steps'] == 398095384 and
          SNAP['588'][16]['steps'] == 397796108, f"{ {k: v['exit'] for k, v in out.items()} }")
    t0 = time.time()
    m16 = snapshot16()
    s = SNAP['341'][16]
    claim('S10', 'record exit 16 of line 341, regenerated from the blank tape with the defect model, at step 398,090,000',
          same_state(m16, s) and m16.steps == 398090000 and s['steps'] == 398090000, f'{time.time() - t0:.0f} s')
    ident = {x: x for x in 'ABCDEF'}
    ms = from_sim(TM, 398090000, ident, False)
    claim('S10', 'line 341: direct simulation to step 398,090,000 gives exactly the record-exit-16 configuration '
          '(every defect, lo, hi, head cell, direction, phase)', same_state(ms, s))
    import sim
    r = sim.run(sim.parse(TM), max_steps=398090000); c = r.final
    lo1, hi1, E = INIT16['lo1'], INIT16['hi1'], set(INIT16['E'])
    cells = {lo1: 1}
    for x in range(lo1, hi1): cells[x + 1] = cells[x] if x in E else 1 - cells[x]
    real = {x: c.read(x) for x in range(c.lo - 2, c.hi + 3)}
    ok = all(real[x] == cells.get(x, 0) for x in real) and all(c.read(x) == v for x, v in cells.items())
    ok &= (c.pos, c.state, c.symbol) == (INIT16['head'], INIT16['state'], INIT16['read']) and cells[hi1] == 1
    claim('S10', 'the explicit tape of proof.md Appendix C (cells -55..36257, equal neighbours exactly at the listed edges, '
          'head in state B on cell 1154 reading 1) is the machine\'s tape at step 398,090,000', ok)
    # 512: our table started in B; their A..F = our B, C, D, E, A, F
    r512 = dict(zip('ABCDEF', 'BCDEAF'))
    s = SNAP['512'][16]
    ms = from_sim('1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---', s['steps'], r512, False)
    claim('S10', f'line 512 (1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---), direct simulation to step {s["steps"]:,}, renamed: '
          'equals our table started in B at its record exit 16', same_state(ms, s) and s['steps'] == 398095384)
    # 588: our table started in F, mirrored; their A..F = our F, A, B, C, D, E
    r588 = dict(zip('ABCDEF', 'FABCDE'))
    s = SNAP['588'][16]
    ms = from_sim('1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD', s['steps'], r588, True)
    claim('S10', f'line 588 (1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD), direct simulation to step {s["steps"]:,}, '
          'mirrored and renamed: equals our table started in F at its record exit 16', same_state(ms, s) and
          s['steps'] == 397796108)
    if FULL:
        for tag, st, sh in (('512', 'B', 0), ('588', 'F', 1)):
            mm = snapshot16(st, sh)
            claim('S10', f'line {tag}: record exit 16 regenerated from the blank tape with the model', same_state(mm, SNAP[tag][16]))


INIT16 = dict(lo1=-55, hi1=36257, head=1154, state='B', read=1,
              E=(-54, -49, -48, -43, -42, -37, -36, -31, -30, -26, -20, -19, -10, 3, 27, 71, 108, 145, 181, 3888, 12167,
                 12174, 12295, 36255))


def fmt_aff(g):
    a, b = g.a, g.b
    if b == 0: return str(a)
    if b.denominator == 1 and a.denominator == 1:
        return f"{b}u{'+' if a >= 0 else '-'}{abs(a)}"
    den = max(a.denominator, b.denominator)
    return f"({b * den}u{'+' if a >= 0 else '-'}{abs(a * den)})/{den}"


def fmt_shape(sh):
    return ' '.join(f'L{g[1]}' if isinstance(g, tuple) else str(g) for g in sh)


def entry_ids():
    ids = {}
    for r in ORDER:
        ks = sorted(tab[r], key=lambda k: (-k[0], fmt_shape(k[1])))
        for i, k in enumerate(ks): ids[(r, k)] = f'r{r}.{i + 1}'
    return ids


def appendix():
    out = []
    ids = entry_ids()
    out.append('APPENDIX A')
    for r in ORDER:
        out.append(f'class r{r}: {len(tab[r])} entries')
        for k in sorted(tab[r], key=lambda k: ids[(r, k)].split('.')[1].zfill(3)):
            xp, sh = k; ep, te, tm, tw, ny, nh = next(iter(tab[r][k])); j = len(sh) - 1
            nm = lambda a, o: (f'x{a + 1}' if a < j else 'hi') + (f'{o:+d}' if o else '')
            out.append(f'{ids[(r, k)]:6} {xp} | {fmt_shape(sh):40} | {" ".join(nm(a, o) for a, o in ny):34} | '
                       f'hi = {nm(*nh):7} | trips {te}, mid turns {tm}, wiggles {tw}')
    out.append('APPENDIX B')
    if not PROGRAM:
        import io, contextlib
        with contextlib.redirect_stdout(io.StringIO()):
            n0 = len(RESULTS); s7(); del RESULTS[n0:]
    for r in ORDER:
        S, prog, End = PROGRAM[r]
        out.append(f'class r{r}: start  {", ".join(fmt_aff(g) for g in S)}')
        run = []
        for p in prog:
            if p[0] == 'step':
                run.append(ids[(r, (p[1], p[2]))])
            else:
                if run: out.append(f'   single: {" ".join(run)}'); run = []
                xp, c, d, ctr, shapes = p[1:6]
                inc = ', '.join(f'gap {i + 1} {int(x):+d}' for i, x in enumerate(d) if x)
                out.append(f'   cycle ({" ".join(ids[(r, (xp, sh))] for sh in shapes)}) x {fmt_aff(c)}: {inc}; '
                           f'{int(ctr.a)} trips per cycle')
        if run: out.append(f'   single: {" ".join(run)}')
        out.append(f'   end    {", ".join(fmt_aff(g) for g in End)}')
    out.append('APPENDIX C')
    load_snaps()
    for n in range(16, 28):
        r = W.cls(n); _, cw, R = window_of(n, SNAP['341'][n])
        out.append(f'{n} r{r} K={K0[r] + 2 * W.epoch(n)} | {", ".join(map(str, cw)) or "-"} | {", ".join(map(str, R))}')
    out.append('APPENDIX D')
    if not BLOCK_EVENTS: lemma_B()
    for m, tabm in BLOCK_TABLE.items():
        for (lab, side, dph), (xs, dphi, new) in tabm.items():
            evs = BLOCK_EVENTS[(m, lab, side, dph)]
            out.append(f'm={m} {lab} {"right" if side == "R" else "left "} c+{dph} -> {"right" if xs == "R" else "left "} '
                       f'{dphi:+d} {new} | {fmt_block_events(evs)}')
    out.append('APPENDIX E')
    out += episode81()[0]
    out.append('APPENDIX F')
    out += worked_run(1)
    out.append('SECTION 6.4')
    for r in ORDER:
        S, prog, End = PROGRAM[r]
        fc, fR, fdeep = record_visit_formulas(r, len(V[r][0]), len(End))
        d = W.EXCH[r]
        how = f'drop {-d}' if d < 0 else f'take in {d}'
        line = f'r{r} -> r{NXT[r]} ({how}): chain window {fmt_vec(fc) if fc else "(none)"} | right {fmt_vec(fR)}'
        if fdeep:
            nm = {0: 'digit gap', 1: 'separator gap', 2: 'separator gap', 3: 'inter gap'}; Jn = W.J[NXT[r]]
            roles = [nm[W.gap_role(Jn + len(fdeep) - i)] for i in range(len(fdeep))]
            line += f' | to the deep chain {fmt_vec(fdeep)} as ({", ".join(roles)})'
        out.append(line)
    return out


def worked_run(r):
    """proof.md Appendix F: the interval of class r step by step, with the gap map of every entry."""
    S, prog, End = PROGRAM[r]; ids = entry_ids(); out = []
    used = []
    for p in prog:
        keys = [(p[1], p[2])] if p[0] == 'step' else [(p[1], sh) for sh in p[5]]
        for k in keys:
            if k not in used: used.append(k)
    for k in sorted(used, key=lambda k: int(ids[(r, k)].split('.')[1])):
        sh = k[1]
        out.append(f'{ids[(r, k)]:6} {fmt_vec(shape_vars(sh))} -> {fmt_vec(gap_map(entry(r, *k), shape_vars(sh)))}')
    out.append(f'start        {", ".join(fmt_aff(g) for g in S)}')
    for p in prog:
        if p[0] == 'step':
            out.append(f'{ids[(r, (p[1], p[2]))]:6} ph {p[1]}  {", ".join(fmt_aff(g) for g in p[3])}   (R = {fmt_aff(p[4])})')
        else:
            xp, c, d, ctr, shapes, Rb, gf, gl, ga, Ra, mrest = p[1:12]
            comp = cycle_composite(r, xp, shapes)
            out.append(f'cycle ({" ".join(ids[(r, (xp, sh))] for sh in shapes)}): f{fmt_vec(shape_vars(shapes[0], "h"))} = '
                       f'{fmt_vec(comp)}')
            out.append(f'   R = {fmt_aff(Rb)} visits left; c = (R - m)/4 = {fmt_aff(c)} cycles, m = {mrest} visits left after')
            out.append(f'   first jumped cycle starts at {", ".join(fmt_aff(g) for g in gf)}')
            out.append(f'   last jumped cycle starts at  {", ".join(fmt_aff(g) for g in gl)}')
            out.append(f'   after the jump               {", ".join(fmt_aff(g) for g in ga)}   (R = {fmt_aff(Ra)})')
    out.append(f'end          {", ".join(fmt_aff(g) for g in End)}')
    return out


def s12():
    doc = open(os.path.join(HERE, 'proof.md')).read()
    lines = appendix()
    miss = [x for x in lines if x not in doc and not x.startswith(('APPENDIX', 'SECTION'))]
    claim('S12', 'proof.md contains every line generated from the checked data: Appendices A-F (right table, interval '
          'programs, record-exit windows 16-27, single-block event lists, episode 81, the worked r1 interval) and the '
          'record-visit formulas of 6.4', not miss, f'{len(lines) - len(miss)}/{len(lines)} lines; '
          f'first missing: {miss[:1]}')
    vt = all(f'| {", ".join(VTAB[r][0].split(", ")) if VTAB[r][0] else "(none)"} | {VTAB[r][1]} |' in doc for r in ORDER)
    claim('S12', 'proof.md section 3.4 lists exactly the vectors V_r(u) checked here', vt)


# ------------------------------------------------------------------------------------------------- S11
def s11():
    runs = [('16', '21', '2')] if not FULL else [('16', '27', '10'), ('28', '32', '3')]
    for a, b, k in runs:
        out = subprocess.run([sys.executable, '-B', 'perturb.py', 'results/snap_341.pkl', a, b, k, '99'],
                             cwd=os.path.join(SC, 'closeout3'), capture_output=True, text=True).stdout
        mm = re.search(r'(\d+)/(\d+) perturbed record exits', out)
        claim('S11', f'random deep-chain gaps (same residue, >= the role minimum) at record exits {a}..{b}, {k} each: the '
              f'exact model reaches C_(r+1) with the unperturbed window and the regrouped deep chain',
              mm and mm.group(1) == mm.group(2), mm.group(0) if mm else out[-300:])


if __name__ == '__main__':
    T0 = time.time()
    if '--appendix' in sys.argv:
        print('\n'.join(appendix())); sys.exit(0)
    for name, title, fn in (('S1', 'machine', s1), ('S2', 'defect model vs direct simulation', s2),
                            ('S3', 'chain lemma C, C\'', s3), ('S4', 'Lemma T', s4), ('S5', 'Lemma L', s5),
                            ('S6', 'Lemma R (right table)', s6), ('S7', 'interval and record step', s7),
                            ('S8', 'regrouping and exchange', s8), ('S9', 'X/Y synchronization', s9),
                            ('S10', 'membership and base case', s10), ('S11', 'perturbations', s11),
                            ('S12', 'proof.md data', s12)):
        if section(name, title):
            try:
                fn()
            except Exception as ex:
                import traceback; traceback.print_exc()
                claim(name, f'section {name} ran to the end', False, repr(ex)[:300])
    bad = [x for x in RESULTS if not x[2]]
    print(f"\n{len(RESULTS) - len(bad)}/{len(RESULTS)} claims PASS{' (--full)' if FULL else ''}, {time.time() - T0:.0f} s")
    for x in bad: print('  FAIL', x[0], x[1])
    sys.exit(len(bad))