#!/usr/bin/env python3
"""check_proof.py: simulation evidence for proof.md (machine #3, 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---).

Self-contained: its own direct simulator, its own canonical-form parser, its own abstract map.
Nothing here is a proof. Every claim it checks is a hypothesis until Rocq accepts it.

Sections (each prints PASS/FAIL lines and a summary):
  A  every macro rule of proof.md section 2, from random concrete instances (direct simulation)
  B  the uncovered cases (what the machine does outside the rule domain)
  C  the initial segment: blank tape -> K(2; (11,11,0); -) at step 956
  D  direct simulation from the blank tape vs the abstract map, transition by transition
  E  the parity lemma on the abstract run and defect statistics; E2 the far-end endgame table (checked, PASS/FAIL)
  F  every clause of the class invariant INV of proof.md section 3 at every cycle (segment tracking), plus the
     bookkeeping identities its proof uses (exact E-cycle touch counts, x = p_L + 2, r never drops, M >= 4)
  G  INV+(e) (proof.md 3.8, revision 3): G1 the skeptic's counterexamples to INV are excluded by (e) (and both halves
     of (e) are needed); G2 the orbit from the base E-start, every lemma of 3.8 checked step by step (L6's potential
     Phi, L5''s potentials s_i, survival of pairs 1 and 2, the far end, INV+(e) at the next start); G3 exhaustive
     boxes of INV+(e) starts at the thresholds (L* = 3, 4); G4 random chains (L* <= 40)
Section B is informational (demonstrations, no PASS/FAIL) and is not part of the SUMMARY verdict.
Usage: python3 check_proof.py [--quick] [--seed N] [--steps N] [--lmax N] [--sweep small|full] [--nrand N] [--only-g]
"""
import re, sys, random, argparse

TM = '1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---'

def parse_tm(s):
    tab = {}
    for i, blk in enumerate(s.split('_')):
        for r in (0, 1):
            t = blk[3*r:3*r+3]
            tab[(i, r)] = None if t == '---' else (int(t[0]), 1 if t[1] == 'R' else -1, ord(t[2]) - 65)
    return tab
TAB = parse_tm(TM)

# ---------------------------------------------------------------- canonical configurations
# K(h; P; T) = 0^inf <A (10)^h 11001 [ (10)^p (01)^q s(d) for (p,q,d) in P ] T 0^inf
# s(1) = 0001, s(0) = 0010;  T = None ('') | ('T1', t) = (10)^t 1 | ('T2', k) = (101)^2 (01)^k
def W(p, q, d): return '10'*p + '01'*q + ('0001' if d else '0010')

def build(h, P, T):
    s = '10'*h + '11001' + ''.join(W(*x) for x in P)
    if T is None: pass
    elif T[0] == 'T1': s += '10'*T[1] + '1'
    elif T[0] == 'T2': s += '101101' + '01'*T[1]
    return s

PAIR = re.compile(r'((?:10)*)((?:01)+)(0001|0010)')
def parse(s):
    s = s.rstrip('0')
    m = re.match(r'((?:10)*)11001', s)
    if not m: return None
    h = len(m.group(1))//2; i = m.end(); P = []
    s2 = s + '0000'              # a final s(0) = 0010 loses its last 0 to rstrip; allow it back
    while True:
        m2 = PAIR.match(s2, i)
        if not m2 or m2.end() > len(s) + 1: break
        P.append((len(m2.group(1))//2, len(m2.group(2))//2, 1 if m2.group(3) == '0001' else 0)); i = m2.end()
    rest = s[i:] if i <= len(s) else ''
    if rest == '': T = None
    elif re.fullmatch(r'(?:10)+1', rest): T = ('T1', (len(rest)-1)//2)
    elif re.fullmatch(r'101101(?:01)*', rest): T = ('T2', (len(rest)-6)//2)
    else: return ('?', rest)
    return (h, P, T)

def run_macro(h, P, T, cap=None):
    """Direct simulation from K(h;P;T) (head on the blank cell left of the word, state A) to the next
    configuration in which A stands on a new leftmost cell and the tape parses as some K(...).
    Returns ((h',P',T'), steps) | ('HALT', steps, state) | ('CAP', steps)."""
    w = build(h, P, T); n = len(w)
    if cap is None: cap = 400*n*n + 100000
    pad = 4*n + 64
    tape = bytearray(pad) + bytearray(int(c) for c in w) + bytearray(pad)
    pos = pad - 1; st = 0; lo = pos; steps = 0
    while steps < cap:
        tr = TAB[(st, tape[pos])]
        if tr is None: return ('HALT', steps, 'FA'[0] if st == 5 else st)
        tape[pos] = tr[0]; pos += tr[1]; st = tr[2]; steps += 1
        if pos < 0 or pos >= len(tape):
            ext = bytearray(len(tape))
            if pos < 0: tape = ext + tape; pos += len(ext); lo += len(ext)
            else: tape = tape + ext
        if pos < lo: lo = pos
        # canonical moment: state A on a blank cell with only blanks to its left
        if st == 0 and pos <= lo + 1 and tape[pos] == 0 and not any(tape[lo:pos]):
            r = parse(''.join('1' if b else '0' for b in tape[pos+1:]))
            if r is not None and r[0] != '?': return (r, steps)
    return ('CAP', steps)

# ---------------------------------------------------------------- the abstract map (proof.md section 2)
class Outside(Exception):
    """The configuration is outside the rule domain (proof.md section 2 "outside cases")."""

def value(P): return sum(d << j for j, (p, q, d) in enumerate(P))

def astep(h, P, T):
    """One macro step. Returns (h', P', T', rule_name). Raises Outside on an uncovered case."""
    P = [tuple(x) for x in P]; L = len(P); V = value(P)
    if V > 0:                                            # Dec family
        k = next(j for j, x in enumerate(P) if x[2] == 1)
        for j in range(k):
            if P[j][1] < 2: raise Outside('pass-through pair %d has q=%d' % (j+1, P[j][1]))
        if P[k][1] < 1: raise Outside('q=0 pair')
        N = [(p+1, q-1, 1-d) for (p, q, d) in P[:k+1]] + P[k+1:]
        if N[k][1] > 0: return h+4, N, T, 'Dec'
        pk = N[k][0]                                     # = p_k + 1
        if k < L-1:
            p2, q2, d2 = N[k+1]
            return h+4, N[:k] + [(pk+p2+2, q2, d2)] + N[k+2:], T, 'DecMerge'
        if T is None: return h+4, N[:k], ('T1', pk+1), 'DecMergeEmpty'
        if T[0] == 'T1': return h+4, N[:k], ('T1', pk+T[1]+2), 'DecMergeTail'
        raise Outside('last pair runs out with tail T2')
    if L == 0: raise Outside('empty pair list')
    if T is None:                                        # End family
        if L >= 3 and P[-1][1] == 1 and P[-2][1] == 1:
            if any(q < 2 for (_, q, _) in P[:-2]): raise Outside('X1 with another q=1')
            if P[0][0] < 2: raise Outside('X1 with p1<2')
            N = [(h+5, P[0][0]-1, 0)] + [(P[j][1], P[j+1][0], 1) for j in range(L-3)] + [(P[L-3][1], P[L-2][0], 0)]
            return 2, N, ('T2', P[-1][0]+3), 'X1'
        if any(q < 2 for (_, q, _) in P[:-1]): raise Outside('End with a non-last q=1')
        N = [(p+1, q-1, 1) for (p, q, d) in P[:-1]] + [(P[-1][0]+1, P[-1][1]-1, 0)]
        if N[-1][1] > 0: return h+4, N, ('T1', 1), 'End'
        return h+4, N[:-1], ('T1', P[-1][0]+4), 'EndLast'
    if T[0] == 'T1':                                     # Ov
        if P[0][0] < 2: raise Outside('Ov with p1<2')
        N = [(h+5, P[0][0]-1, 0)] + [(P[j][1], P[j+1][0], 1) for j in range(L-1)] + [(P[-1][1], T[1]+1, 1)]
        if any(p < 1 or q < 1 for (p, q, _) in N): raise Outside('Ov produces an empty block')
        return 2, N, None, 'Ov'
    if T[0] == 'T2':                                     # X2
        if any(q < 2 for (_, q, _) in P): raise Outside('X2 with q=1')
        N = [(p+1, q-1, 1) for (p, q, d) in P[:-1]] + [(P[-1][0]+1, P[-1][1]-1, 0), (3, T[1], 1)]
        return h+4, N, None, 'X2'
    raise Outside('unknown tail')

def touches(V, m, j):
    """Pair j (0-based) is touched by the decrement x -> x-1 iff 2^j | x; count over x in (V-m, V]."""
    return (V >> j) - ((V - m) >> j)

def bulk(h, P, T):
    """Largest m >= 1 such that m plain Dec steps (every q stays >= 1, so no merge and no outside case)
    can be applied at once. Equal to m applications of astep 'Dec': pair j loses touches(V,m,j) from q,
    gains it on p, and the digits become the bits of V-m."""
    V = value(P)
    if V == 0: return None
    def ok(m): return all(q - touches(V, m, j) >= 1 for j, (p, q, d) in enumerate(P))
    lo, hi = 0, V
    if not ok(1): return None
    lo = 1
    while lo < hi:
        mid = (lo + hi + 1)//2
        if ok(mid): lo = mid
        else: hi = mid - 1
    m = lo; Wv = V - m
    return h+4*m, [(p+touches(V, m, j), q-touches(V, m, j), (Wv >> j) & 1) for j, (p, q, d) in enumerate(P)], T, m

# ---------------------------------------------------------------- A: rule instances
def rnd(rng, size):
    return {'small': lambda: rng.randint(2, 4), 'med': lambda: rng.randint(2, 30), 'large': lambda: rng.randint(60, 300)}[size]

def gen(rule, rng, i):
    size = ['small', 'med', 'large'][i % 3]; R = rnd(rng, size)
    h = rng.choice([2, 3, 4, 5]) + 4*rng.randint(0, 6)            # all h mod 4
    L = rng.randint(1, 5)
    tails = [None, ('T1', R()), ('T2', R())]
    if rule in ('Dec', 'DecMerge', 'DecMergeTail', 'DecMergeEmpty'):
        if rule == 'DecMerge': L = max(L, 2)
        k = rng.randint(0, L-2) if rule == 'DecMerge' else (L-1 if rule in ('DecMergeTail', 'DecMergeEmpty') else rng.randint(0, L-1))
        P = [(R(), R(), 0 if j < k else (1 if j == k else rng.randint(0, 1))) for j in range(L)]
        if rule != 'Dec': P[k] = (P[k][0], 1, 1)
        T = {'DecMergeTail': ('T1', R()), 'DecMergeEmpty': None}.get(rule, rng.choice(tails))
        return h, P, T
    P = [(R(), R(), 0) for _ in range(L)]
    if rule == 'End': return h, P, None
    if rule == 'EndLast': P[-1] = (P[-1][0], 1, 0); return h, P, None
    if rule == 'Ov': return h, P, ('T1', R())
    if rule == 'X1':
        L = max(L, 3); P = [(R(), R(), 0) for _ in range(L)]
        P[-1] = (P[-1][0], 1, 0); P[-2] = (P[-2][0], 1, 0); return h, P, None
    if rule == 'X2': return h, P, ('T2', R())
    raise ValueError(rule)

RULES = ['Dec', 'DecMerge', 'DecMergeTail', 'DecMergeEmpty', 'End', 'EndLast', 'Ov', 'X1', 'X2']

def section_A(n, rng):
    print('== A. macro rules from random instances (direct simulation vs abstract map)')
    allok = True; tot = 0
    for rule in RULES:
        ok = 0; fails = []
        for i in range(n):
            h, P, T = gen(rule, rng, i)
            exp = astep(h, P, T)
            assert exp[3] == rule, (rule, exp[3], h, P, T)
            got = run_macro(h, P, T)
            good = got[0] not in ('HALT', 'CAP') and got[0] == (exp[0], exp[1], exp[2]) and got[1] >= 1
            ok += good
            if not good: fails.append((h, P, T, str(got)[:120]))
        tot += n; allok &= (ok == n)
        print('  %-14s %3d/%d %s' % (rule, ok, n, 'PASS' if ok == n else 'FAIL ' + str(fails[:2])))
    print('  A total: %s (%d instances)' % ('PASS' if allok else 'FAIL', tot))
    return allok

# ---------------------------------------------------------------- B: outside the domain
def section_B():
    print('== B. what the machine does outside the rule domain (INFORMATIONAL: demonstrations, not checks)')
    cases = [
        ('pass-through pair with q=1 (bad merge), no tail', (6, [(5, 1, 0), (7, 4, 1)], None)),
        ('pass-through pair with q=1, tail T1', (6, [(5, 1, 0), (7, 4, 1), (3, 5, 0)], ('T1', 4))),
        ('End with a non-last q=1', (6, [(5, 1, 0), (7, 4, 0)], None)),
        ('(o3) V=0, no tail, q_1=1, not the X1 shape', (2, [(6, 1, 0), (5, 8, 0), (11, 2, 0), (12, 3, 0)], None)),
        ('last pair runs out with tail T2', (6, [(9, 6, 0), (5, 1, 1)], ('T2', 5))),
        ('Ov with p1=1', (6, [(1, 6, 0), (5, 4, 0)], ('T1', 3))),
        ('X2 with a q=1', (6, [(9, 1, 0), (5, 4, 0)], ('T2', 5))),
        ('X1 pattern with L=2', (6, [(9, 1, 0), (5, 1, 0)], None)),
    ]
    for name, (h, P, T) in cases:
        try: astep(h, P, T); inside = True
        except Outside: inside = False
        r = run_macro(h, P, T, cap=3*10**6)
        out = ('HALTS after %d steps' % r[1]) if r[0] == 'HALT' else ('-> K%s after %d steps' % (str(r[0]), r[1]) if r[0] != 'CAP' else 'no canonical config within cap')
        print('  %-50s abstract map: %-8s machine: %s' % (name, 'covered' if inside else 'Outside', out))
    return None

# ---------------------------------------------------------------- C, D: initial segment and direct cross-check
def stream_canonical(max_steps):
    """Direct simulation from the blank tape; yields (step, K) at every canonical record config."""
    size = 1 << 16
    tape = bytearray(size); pos = size//2; st = 0; lo = pos; hi = pos; steps = 0
    while steps < max_steps:
        tr = TAB[(st, tape[pos])]
        if tr is None: yield (steps, 'HALT'); return
        tape[pos] = tr[0]; pos += tr[1]; st = tr[2]; steps += 1
        if pos < 0 or pos >= len(tape):
            ext = bytearray(len(tape))
            if pos < 0: tape = ext + tape; pos += len(ext); lo += len(ext); hi += len(ext)
            else: tape = tape + ext
        if pos > hi: hi = pos
        if pos < lo:
            lo = pos
            if st == 0:
                r = parse(tape[pos+1:hi+1].translate(BITS).decode())
                if r is not None and r[0] != '?': yield (steps, r)

BITS = bytes.maketrans(bytes([0, 1]), b'01')
INIT_STEP = 956
INIT_K = (2, [(11, 11, 0)], None)

def section_CD(max_steps):
    print('== C. initial segment')
    seq = []
    for s, k in stream_canonical(max_steps):
        seq.append((s, k))
    first = [x for x in seq if x[0] == INIT_STEP]
    okC = bool(first) and first[0][1] == INIT_K
    print('  canonical configs before step %d: %s' % (INIT_STEP, [(s, k) for s, k in seq if s < INIT_STEP]))
    print('  step %d: %s  -> %s' % (INIT_STEP, first[0][1] if first else None, 'PASS' if okC else 'FAIL'))
    print('== D. direct simulation from blank (%d steps) vs abstract map' % max_steps)
    from collections import Counter
    cnt = Counter(); bad = 0
    post = [x for x in seq if x[0] >= INIT_STEP]
    for (s0, k0), (s1, k1) in zip(post, post[1:]):
        try:
            h, P, T, name = astep(*k0)
            if (h, P, T) == (k1[0], k1[1], k1[2]): cnt[name] += 1
            else: bad += 1; print('  MISMATCH at step', s0, k0, '->', k1, 'predicted', (h, P, T))
        except Outside as e:
            bad += 1; print('  OUTSIDE at step', s0, e)
    okD = bad == 0 and len(post) > 1
    print('  %d consecutive canonical transitions, %s; last canonical step %d -> %s' % (sum(cnt.values()), dict(cnt), post[-1][0], 'PASS' if okD else 'FAIL'))
    return okC and okD

# ---------------------------------------------------------------- E: abstract run, parity lemma, far end
def abstract_run(lmax, cb=None, start=INIT_K):
    h, P, T = start; P = list(P)
    while len(P) <= lmax:
        b = bulk(h, P, T)
        if b:
            h1, P1, T1, m = b
            if cb: cb('bulk', (h, P, T), (h1, P1, T1), m)
            h, P, T = h1, P1, T1
        h1, P1, T1, name = astep(h, P, T)
        if cb: cb(name, (h, P, T), (h1, P1, T1), 1)
        h, P, T = h1, P1, T1
    return h, P, T

def section_E(lmax):
    print('== E. abstract run from K(2;(11,11,0);-) until L > %d' % lmax)
    from collections import Counter
    cnt = Counter(); state = {'ov': 0, 'cycles': 0, 'parity_ok': True, 'min_def': None, 'events': []}
    def cb(name, a, b, m):
        state['cycles'] += m
        cnt[name] += m if name == 'bulk' else 1
        (h0, P0, T0), (h1, P1, T1) = a, b
        if name in ('Dec', 'bulk'):
            # parity lemma: q+d mod 2 is unchanged on every pair by plain decrements
            for (p, q, d), (p1, q1, d1) in zip(P0, P1):
                if (q + d - q1 - d1) % 2 or (p + d - p1 - d1) % 2 or (p + q) != (p1 + q1): state['parity_ok'] = False
        if name == 'Ov':
            state['ov'] += 1
            L = len(P0)
            for j, (p, q, d) in enumerate(P0[:-2]):          # interior pairs at overflow time (all d = 0)
                if q % 2 == 1:                                # q-defect that survived its cycle
                    sc = q / 2**(L-1-j)
                    if state['min_def'] is None or sc < state['min_def'][0]: state['min_def'] = (sc, state['ov'], L, j+1)
        if name not in ('Dec', 'bulk', 'End', 'Ov'):
            state['events'].append((state['ov'], name, len(P0)))
    try:
        abstract_run(lmax, cb); okE = True; msg = 'no configuration outside the rule domain'
    except Outside as e:
        okE = False; msg = 'OUTSIDE: %s' % e
    print('  %s; overflows %d; cycles ~2^%d' % (msg, state['ov'], state['cycles'].bit_length()))
    print('  rule counts (bulk = plain Dec steps applied in batches):', dict(cnt))
    print('  parity lemma (q+d, p+d mod 2 and p+q unchanged by every plain Dec):', 'PASS' if state['parity_ok'] else 'FAIL')
    md = state['min_def']
    print('  defect statistic (all defects are Eq blocks, proof.md 3.3): min over interior q-defects at overflow of q/2^(L-j) = %.4f (ov %d, L %d, pair %d)' % md if md else '  no q-defects')
    xs = [e for e in state['events'] if e[1] in ('X1', 'X2', 'DecMergeTail', 'DecMergeEmpty', 'EndLast')]
    print('  rare events (ov#, rule, L):', [e for e in xs if e[1] != 'EndLast'][:20])
    return okE and state['parity_ok']

def far_endgame(lmax_snapshot=95, ov_pick=300):
    print('== E2. far-end endgame: replace the eroding segment value x and run to the first far event')
    snap = {}
    def cb(name, a, b, m):
        if name == 'Ov':
            snap['n'] = snap.get('n', 0) + 1
            if snap['n'] == ov_pick: snap['cfg'] = a
    try: abstract_run(lmax_snapshot, cb)
    except Outside: pass
    h, P, T = snap['cfg']
    res = []
    for x in range(1, 16):
        hh, PP, TT = h, P[:-1] + [(x, P[-1][1], P[-1][2])], T
        outcome = None
        try:
            for _ in range(10000):
                b = bulk(hh, PP, TT)
                if b: hh, PP, TT, _m = b
                L0 = len(PP); V = value(PP)
                k = (V & -V).bit_length() - 1 if V else None
                hh, PP, TT, name = astep(hh, PP, TT)
                far = (name == 'DecMerge' and k is not None and k >= L0 - 2) or name in ('DecMergeTail', 'DecMergeEmpty', 'X1', 'X2')
                if far: outcome = name + ('(pair L-1)' if name == 'DecMerge' else ''); break
        except Outside as e:
            outcome = 'OUTSIDE (%s)' % e
        res.append((x, outcome))
    for x, o in res: print('  x=%2d (x mod 3 = %d): %s' % (x, x % 3, o))
    def expected(x):
        if x == 2: return 'OUTSIDE'
        if x == 1 or x % 3 == 0: return 'DecMerge(pair L-1)'
        if x % 3 == 1: return 'X1'
        return 'DecMergeTail'
    bad = [(x, o) for x, o in res if o is None or not o.startswith(expected(x))]
    ok = not bad
    print('  expected: x=1 or x = 0 mod 3 -> DecMerge at pair L-1; x = 1 mod 3, x >= 4 -> X1; x = 2 mod 3, x >= 5 -> DecMergeTail;'
          ' x=2 -> outside (o1). x=2 is unreachable: x = p_L + 2 >= 3 (proof.md 3.4, S1) ->', 'PASS' if ok else 'FAIL %s' % bad)
    return ok

# ---------------------------------------------------------------- F: the class invariant of proof.md section 3 (segment tracking)
from fractions import Fraction

class Tracked:
    """Abstract run with segment identities. ids[j] = (id of the (10)-run p_j, id of the (01)-run q_j)."""
    def __init__(self, start):
        self.h, self.P, self.T = start[0], list(start[1]), start[2]
        self.n = 0
        self.ids = [(self.new(), self.new()) for _ in self.P]
        self.tid = None if self.T is None else self.new()
        self.hid = self.new()
    def new(self):
        self.n += 1; return self.n
    def step(self):
        """One bulk batch of plain Dec steps, or one astep. Returns (name, k, L_before)."""
        b = bulk(self.h, self.P, self.T)
        if b:
            self.h, self.P, self.T, m = b
            return ('bulk', None, len(self.P))
        P = self.P; L = len(P); V = value(P)
        k = (V & -V).bit_length() - 1 if V else None
        h1, P1, T1, name = astep(self.h, P, self.T)
        ids = self.ids
        if name == 'DecMerge':
            ids = ids[:k] + [(self.new(), ids[k+1][1])] + ids[k+2:]
        elif name in ('DecMergeTail', 'DecMergeEmpty', 'EndLast'):
            ids = ids[:-1]; self.tid = self.new()
        elif name == 'End':
            self.tid = self.new()
        elif name == 'Ov':
            ids = [(self.hid, ids[0][0])] + [(ids[j][1], ids[j+1][0]) for j in range(L-1)] + [(ids[-1][1], self.tid)]
            self.hid = self.new(); self.tid = None
        elif name == 'X1':
            ids = [(self.hid, ids[0][0])] + [(ids[j][1], ids[j+1][0]) for j in range(L-2)]
            self.hid = self.new(); self.tid = self.new()
        elif name == 'X2':
            ids = ids + [(self.new(), self.tid)]; self.tid = None
        self.ids = ids; self.h, self.P, self.T = h1, P1, T1
        return (name, k, L)

def class_invariants(lmax, base_ov=5):
    """Checks every clause of the invariant INV of proof.md section 3.3 at every cycle from overflow base_ov on,
    and the bookkeeping identities that its proof uses (section 3.4). Returns True iff nothing failed."""
    print('== F. class invariant INV (proof.md section 3) on the abstract run, from overflow %d to L > %d' % (base_ov, lmax))
    r = Tracked(INIT_K)
    fails = []; ov = 0; cyc = []
    stat = {'minr_reg': None, 'minr_x2': None, 'min_head': None, 'min_fused': None, 'min_drop_reg': None,
            'min_drop_x1': None, 'minM': None, 'xs': set(), 'nE': 0, 'nL': 0, 'nX1': 0, 'merge_int': 0, 'merge_x': 0, 'xsmall': set(), 'xres': set()}
    def mn(key, v, info):
        if stat[key] is None or v < stat[key][0]: stat[key] = (v, info)
    def fail(msg):
        if len(fails) < 20: fails.append(msg)
    prev_r = {}            # Eq id -> r at the previous E-start
    prev_type = None; first_E = True
    start = None           # (h, P, T, ids) at the start of the current cycle
    while len(r.P) <= lmax:
        before = (r.h, list(r.P), r.T, list(r.ids))
        name, k, L0 = r.step()
        if name != 'bulk': cyc.append((name, k, L0, before))
        if name not in ('Ov', 'X1'): continue
        ov += 1
        if start is not None and ov - 1 >= base_ov:
            h0, P0, T0, ids0 = start
            names = [c[0] for c in cyc]
            etype = 'End' in names
            ltype = ('EndLast' in names) or ('X1' in names)
            if etype == ltype: fail('ov %d: cycle is neither or both types: %s' % (ov, names))
            if prev_type is not None and etype == (prev_type == 'E'): fail('ov %d: types do not alternate' % ov)
            prev_type = 'E' if etype else 'L'
            if etype:
                stat['nE'] += 1
                x2 = T0 is not None and T0[0] == 'T2'
                L = len(P0); Ls = L + x2
                allowed = (['X2'] if x2 else []) + ['End', 'Ov']
                if names != allowed: fail('ov %d: E-cycle events %s' % (ov, names))
                Pend = cyc[-1][3][1]                   # list just before the closing Ov
                interior = range(L) if x2 else range(L - 1)
                for j in interior:
                    p, q, d = P0[j]; e = Ls - 1 - j
                    tau = 3 * 2**e - (2 if j == 0 else 1)
                    rv = Fraction(q + (1 if j == 0 else 0), 2**e)
                    thr = 4 if x2 else 5
                    if rv < thr: fail('ov %d: Eq pair %d r=%s < %d' % (ov, j+1, rv, thr))
                    mn('minr_x2' if x2 else 'minr_reg', float(rv), (ov, L, j+1))
                    if Pend[j][1] != q - tau or Pend[j][0] != p + tau: fail('ov %d: pair %d touch count != tau' % (ov, j+1))
                    good = (p + d) % 2 == 1 if not (x2 and j == L - 1) else (d == 0 and p % 2 == 0)
                    if not good: fail('ov %d: interior Ep pair %d has the wrong parity' % (ov, j+1))
                    qid = ids0[j][1]
                    if qid in prev_r:
                        drop = float(rv - prev_r[qid][0])
                        mn('min_drop_x1' if prev_r[qid][1] else 'min_drop_reg', drop, (ov, j+1))
                        if drop < (-1 if prev_r[qid][1] else 0): fail('ov %d: Eq r dropped by %s' % (ov, -drop))
                    elif j == 0 and not first_E: mn('min_head', float(rv), (ov, L))
                    elif not first_E: mn('min_fused', float(rv), (ov, L, j+1))
                    prev_r[qid] = (rv, False)
                first_E = False
                if x2:
                    if T0[1] < 4: fail('ov %d: T2(k) with k < 4' % ov)
                    x = Pend[-1][0]
                    if x != 5: fail('ov %d: x after X2 is %d, not 5' % (ov, x))
                else:
                    p, q, d = P0[-1]
                    if p < 1 or q < 6: fail('ov %d: far pair (%d,%d) not (>=1, >=6)' % (ov, p, q))
                    x = Pend[-1][0]
                    if x != p + 2: fail('ov %d: x=%d != p_L+2=%d' % (ov, x, p + 2))
                if x < 3: fail('ov %d: x=%d < 3' % (ov, x))
                (stat['xsmall'].add(x) if x <= 5 else stat['xres'].add(x % 3))
            else:
                stat['nL'] += 1
                M = len(P0)
                mn('minM', M, ov)
                if M < 4: fail('ov %d: L-start with M=%d < 4' % (ov, M))
                if T0 != ('T1', 1) and T0 is not None: pass
                lastq = P0[-1][1]
                if lastq != 2: fail('ov %d: L-start last pair q=%d != 2' % (ov, lastq))
                isx1 = 'X1' in names
                stat['nX1'] += isx1
                # every run-out is an interior Ep (k <= M-2, 1-based) or the far segment x (k = M-1)
                for (nm, kk, Lb, bef) in cyc:
                    if nm == 'DecMerge':
                        if kk + 1 <= Lb - 2: stat['merge_int'] += 1
                        elif kk + 1 == Lb - 1: stat['merge_x'] += 1
                        else: fail('ov %d: DecMerge at pair %d of %d' % (ov, kk+1, Lb))
                for qid in list(prev_r):
                    prev_r[qid] = (prev_r[qid][0], isx1)
        cyc = []
        start = (r.h, list(r.P), r.T, list(r.ids))
    ok = not fails
    for f in fails: print('  FAIL', f)
    print('  cycles checked: %d E, %d L-slot (%d of them X1); final L %d, overflows %d' % (stat['nE'], stat['nL'], stat['nX1'], len(r.P), ov))
    print('  INV(a) cycle types alternate, E-cycles are [X2,] End, Ov with exact touch counts tau_j:', 'PASS' if ok else 'see FAIL lines')
    print('  INV(b) min r of interior Eq at E-starts: regular %s (need >= 5), after X1 %s (need >= 4)' % (stat['minr_reg'], stat['minr_x2']))
    print('         new Eq from the head: min r %s; from fusions: min r %s' % (stat['min_head'], stat['min_fused']))
    print('         change of r over one period: min %s after an EndLast slot (lemma: >= 0), %s after an X1 slot (lemma: >= -1)' % (stat['min_drop_reg'], stat['min_drop_x1']))
    print('  INV(c) interior Ep parity good at every E-start; INV(d) min M at L-starts %s (need >= 4)' % (stat['minM'],))
    print('  far end: x = p_L + 2 (or 5 after X2), so x >= 3: PASS if no FAIL above; x <= 5 seen: %s; residues of x > 5 seen: %s' % (sorted(stat['xsmall']), sorted(stat['xres'])))
    print('  L-slot run-outs: %d interior Ep (legal DecMerge), %d of the far segment x' % (stat['merge_int'], stat['merge_x']))
    print('  F total:', 'PASS' if ok else 'FAIL')
    return ok

# ---------------------------------------------------------------- G: INV+(e) (proof.md section 3.8)
# Clause (e), the touch-count lemma L6, the potential s of L5, the skeptic's counterexamples, and sweeps of
# "INV+(e) at an E-start  =>  every K of the next cycle pair is in D, and INV+(e) holds at the next E-start".

def Lstar(P, T): return len(P) + (1 if (T is not None and T[0] == 'T2') else 0)

def inv_violations(h, P, T, with_e=True):
    """INV(a)-(d) (proof.md 3.3) and clause (e) (proof.md 3.8), transcribed literally. Returns the violated clauses."""
    v = []; L = len(P)
    if L == 0: return ['L=0 (o7)']
    if any(p < 1 or q < 1 for (p, q, d) in P): v.append('empty block')
    if h != 2: v.append('a:h=2')
    if P[0][0] < 7: v.append('a:p1>=7')
    ds = [d for (_, _, d) in P]
    if T is None:
        if ds != [0] + [1]*(L-1): v.append('a:digits')
        if P[-1][0] < 1 or P[-1][1] < 6: v.append('a:far pair')
        thr = 5
    elif T[0] == 'T2':
        if T[1] < 4: v.append('a:k>=4')
        if L < 2 or ds != [0] + [1]*(L-2) + [0]: v.append('a:digits')
        thr = 4
    else:
        return v + ['a:tail T1']
    Ls = Lstar(P, T)
    if Ls < 3: v.append('d:L*>=3')
    for j in range(1, Ls):                               # interior pairs j <= L*-1 (1-based)
        p, q, d = P[j-1]; e = Ls - j
        if q + (j == 1) < thr * 2**e: v.append('b:r_%d' % j)
        if T is not None and j == L:
            if not (d == 0 and p % 2 == 0): v.append('c:top pair')
        elif (p + d) % 2 != 1: v.append('c:p_%d' % j)
    if with_e:
        if P[0][0] < 2**(Ls+2) - 1: v.append('e1')
        if L < 2 or P[1][0] < 2**Ls: v.append('e2')
    return v

def mstep(h, P, T):
    """One step of the accelerated map: a bulk batch of plain Dec (name 'bulk', m decrements) or one macro step.
    Returns (h', P', T', name, k (0-based borrow pair, or None), m)."""
    b = bulk(h, P, T)
    if b:
        h1, P1, T1, m = b; return h1, P1, T1, 'bulk', None, m
    V = value(P); k = (V & -V).bit_length() - 1 if V else None
    h1, P1, T1, name = astep(h, P, T)
    return h1, P1, T1, name, k, 1

def run_to_repair(K, cap=10**6):
    """Unchecked: apply the map until (and including) the next Ov/X1. Returns (names, K'). Raises Outside."""
    h, P, T = K; names = []
    for _ in range(cap):
        h, P, T, name, k, m = mstep(h, P, T)
        if name != 'bulk': names.append((name, None if k is None else k+1))
        if name in ('Ov', 'X1'): return names, (h, P, T)
    raise RuntimeError('no re-pairing')

def cycle_pair_checked(K, fails, st):
    """One cycle pair (E-cycle, then L-slot) from an E-start K that satisfies INV+(e). Every claim that proof.md
    3.4-3.8 uses for the preservation of INV+(e) is checked on the way, most of them as exact identities.
    A failed claim is appended to `fails`; `st` collects statistics. Returns the next E-start.
    Raises Outside if a configuration outside D is reached."""
    def chk(c, tag):
        if not c: fails.append(tag)
    h, P, T = K; P = list(P); L = len(P); Ls = Lstar(P, T); x2 = T is not None
    rE = [None] + [Fraction(P[j-1][1] + (j == 1), 2**(Ls-j)) for j in range(1, Ls)]
    # ---- S1: the E-cycle
    names = []; cur = (h, P, T)
    while True:
        h1, P1, T1, name, k, m = mstep(*cur)
        if name != 'bulk': names.append(name)
        if name in ('Ov', 'X1'): before = cur; cur = (h1, P1, T1); break
        cur = (h1, P1, T1)
    chk(names == ['X2']*x2 + ['End', 'Ov'], 'S1: E-cycle events %s' % names)
    hb, Pb, Tb = before
    for j in range(1, Ls):
        tau = 3*2**(Ls-j) - (2 if j == 1 else 1)
        chk(Pb[j-1][0] == P[j-1][0] + tau and Pb[j-1][1] == P[j-1][1] - tau, 'L3: tau_%d' % j)
    chk(hb + 5 == 3*2**(Ls+1) - 1, 'L3: head block h+5 = 3*2^(L*+1)-1')
    if x2: chk(Pb[-1][:2] == (5, T[1] - 2), 'S1: appended pair gets 2 touches')
    else: chk(Pb[-1][:2] == (P[-1][0] + 2, P[-1][1] - 2), 'S1: far pair gets 2 touches')
    x = Pb[-1][0]; chk(x >= 3, 'S1: x >= 3')
    # ---- the L-start
    h, P, T = cur; M = len(P)
    chk(M == Ls + 1 and h == 2 and T is None and [d for (_, _, d) in P] == [0] + [1]*(M-1), 'S2: L-start shape')
    chk(P[-1][1] == 2 and P[-2][1] == x, 'S2: far end (x, 2) at the L-start')
    chk(all((q + d) % 2 == 0 for (p, q, d) in P[:M-2]), 'L4: L-slot q_1..q_{M-2} good')
    q1L, q2L, p2L = P[0][1], P[1][1], P[1][0]
    chk(q1L >= 11*2**(Ls-1) - 4 and q2L >= 7*2**(Ls-2) - 1, '3.8: q_1, q_2 at the L-start (from (e))')
    typ = 'X1' if x == 4 else 'EL'
    T1max = 3*2**Ls - 2 if typ == 'EL' else 2**(Ls+1) - 2
    chk(q1L >= T1max + 1 and q2L >= 3*2**(Ls-1), '3.8: q_1, q_2 exceed their touch bounds')
    st['typ'][typ] += 1; st['x'][min(x, 6)] += 1
    # ---- S2: the L-slot, with the potential s_i = (p_i + R_i)/2^e_i of L5 and the potential Phi of L6
    def svals(P, V, phase):
        N = len(P)
        c, dl = ((1, 0) if phase == 1 else (0, 1)) if typ == 'EL' else (0, 0)
        return [(Fraction(p + (V >> i0) + c*2**(N-i0-1), 2**(N-i0-1+dl)), N-i0-1+dl, p) for i0, (p, q, d) in enumerate(P)]
    phase = 1; S = svals(P, value(P), 1)
    for i in range(2, M):
        chk(S[i-1][0] == rE[i-1] - (typ == 'X1'), 'L5: s_%d at the L-start = r (EndLast slot) or r-1 (X1 slot)' % i)
    chk(S[0][0] == (9 if typ == 'EL' else 8) - Fraction(3, 2**(M-1)), 'L5: s_1 of the head block at the L-start')
    D = 0; nm = 0; merges = 0; D1 = N1 = m1 = None; events = []; xi = M - 2; xrun = False
    while True:
        V = value(P); N = len(P); Phi = D + V - 2**N
        for (s, e, p) in S[1:]:
            chk(p >= 2**e + 1, 'A-bound p_i >= 2^e_i + 1')
        h1, P1, T1, name, k, m = mstep(h, P, T)
        if name in ('Ov', 'X1'):
            break
        if name != 'bulk': events.append((name, k, N, phase))
        chk(name in ('bulk', 'Dec', 'DecMerge', 'DecMergeTail', 'EndLast'), 'S2: unexpected rule %s' % name)
        if name == 'EndLast':
            chk(phase == 1 and typ == 'EL', 'S2: EndLast only once, in an EndLast slot')
            D1, N1, m1 = D, N, merges; D = 0; merges = 0; phase = 2
            S1 = svals(P1, value(P1), 2)
            chk([s for (s, _, _) in S1] == [s for (s, _, _) in S[:-1]], 'L5: s unchanged by EndLast')
        else:
            D += m; S1 = svals(P1, value(P1), phase); V1 = value(P1)
            if name in ('bulk', 'Dec'):
                chk([s for (s, _, _) in S1] == [s for (s, _, _) in S], 'L5: s unchanged by plain Dec')
                chk(D + V1 - 2**len(P1) == Phi, 'L6: Phi unchanged by plain Dec')
            else:                                         # a merge at pair k+1 (1-based)
                merges += 1; nm += 1
                chk(k >= 2, '3.8: merge at pair %d <= 2' % (k+1))
                chk(P[k][1] == 1 and P[k][2] == 1, 'L2: run-out on an end touch of a good block')
                if xi is not None and k == xi:            # the x-block runs out: only x = 3 (first countdown) or x = 5 (second)
                    chk((x == 3 and phase == 1 and name == 'DecMerge') or (x == 5 and phase == 2 and name == 'DecMergeTail'),
                        'S2: x-block run-out with x=%d, phase %d, %s' % (x, phase, name))
                    xi = None; xrun = True
                else:                                     # otherwise an interior Ep block below the x-pair (or, once the x-pair is gone, any pair)
                    chk(xi is None or k < xi, 'S2: run-out above the x-pair (the last pair) at pair %d of %d' % (k+1, N))
                    chk(name == 'DecMerge' or phase == 2, 'S2: DecMergeTail before EndLast')
                    if xi is not None: xi -= 1
                H = V >> (k+1); dPhi = D + V1 - 2**len(P1) - Phi
                chk(dPhi == 2**(N-1) - H*2**k and dPhi >= 2**k, 'L6: Phi rises by 2^(n-1) - H 2^(k-1) >= 2^(k-1) at a merge')
                exp = [S[i][0] + Fraction(S[i][2] + 2**(k-i), 2**S[i][1]) for i in range(k)]
                if name == 'DecMerge':
                    exp += [S[k+1][0] + Fraction(S[k][2] + 3, 2**S[k+1][1])] + [s for (s, _, _) in S[k+2:]]
                    chk(exp[k] >= S[k+1][0] + 2, 'L5: fusion bound s_F >= s_b + 2')
                chk([s for (s, _, _) in S1] == exp, 'L5: s after a merge (identity)')
        h, P, T, S = h1, P1, T1, S1
    # (h, P, T) is the configuration just before the closing re-pairing; (h1, P1, T1) the next E-start
    chk((name == 'X1') == (typ == 'X1'), 'S2: slot type predicted by x (X1 iff x = 4)')
    if (name == 'X1') != (typ == 'X1') or (typ == 'EL' and D1 is None) or len(P) < 2 or len(P1) < 2:
        chk(False, 'S2: slot collapsed or ended with the wrong rule'); return (h1, P1, T1)
    st['merges'] += nm
    T1c = (h - 2)//4
    if typ == 'X1':
        D1, N1, m1 = D, len(P), merges; D2 = 0; Nf = None; Lsn = N1
    else:
        D2, Nf = D, len(P); Lsn = Nf + 1
        chk(D2 >= 2**Nf - 1 + merges, 'L6: second countdown D2 >= 2^Nf - 1 + m2')
        chk(T1c >= 3*2**(Lsn-1) - 2, 'L6: T1 >= 3*2^(L*\'-1) - 2 (EndLast slot)')
    chk(D1 >= 2**N1 - 2 + m1, 'L6: first countdown D1 >= 2^N1 - 2 + m1')
    chk(T1c == D1 + (typ == 'EL') + D2, '3.8: pair-1 touches = macro steps of the slot')
    chk(T1c >= 2**Lsn - 2, 'L6: T1 >= 2^(L*\') - 2')
    chk(T1c <= T1max, '3.8: T1 <= merge-free count')
    chk(P[1][0] - p2L <= 3*2**(Ls-1) - 1, '3.8: pair-2 touches <= 3*2^(L*-1) - 1')
    chk(Lstar(P1, T1) == Lsn and Lsn == M - nm, '3.8: L*\' = M - (number of merges)')
    chk(Lsn <= Ls + 1 and Lsn >= (4 if typ == 'X1' else 3), '3.8: 3 <= L*\' <= L*+1 (>= 4 after X1)')
    chk(P1[0][0] == 4*T1c + 7 and P1[1][0] == P[0][1], '3.8: p_1\' = 4 T1 + 7, p_2\' = q_1 at the end of the slot')
    chk(xrun == (x in (3, 5)), 'S2: the x-block runs out iff x in {3, 5}')
    if x == 4: chk(xi == len(P) - 2 and P[-2][1] == 1 and P[-1][1] == 1, 'S2: x=4 ends with X1 on (x-pair q=1, last q=1)')
    if x >= 6: chk(xi == len(P) - 1 and P[-1][1] == x - 5, 'S2: x>=6 x-pair is the top pair at the end, q = x-5')
    # the potential at the end equals the scaled value at the next E-start (L5 (iii))
    for i in range(1, Lsn):
        chk(S[i-1][0] == Fraction(P1[i-1][1] + (i == 1), 2**(Lsn-i)), 'L5: s at the end = r\' at the next E-start')
    v = inv_violations(h1, P1, T1)
    chk(not v, 'INV+(e) at the next E-start: %s' % v)
    Kn = (h1, P1, T1)
    st['cp'] += 1
    for key, val in (('e1', Fraction(P1[0][0], 2**(Lsn+2) - 1)), ('e2', Fraction(P1[1][0], 2**Lsn)),
                     ('T1', Fraction(T1c, max(1, 2**Lsn - 2)))):
        if key not in st['min'] or val < st['min'][key]: st['min'][key] = val
    return Kn

def new_stats():
    from collections import Counter
    return {'typ': Counter(), 'x': Counter(), 'merges': 0, 'cp': 0, 'min': {}}

def fmt_stats(st):
    return 'cycle pairs %d; slot types %s; x (6 = x>=6) %s; L-slot merges %d; min p_1\'/(2^(L*\'+2)-1) %.3f, min p_2\'/2^L*\' %.3f, min T1/(2^L*\'-2) %.3f' % (
        st['cp'], dict(st['typ']), dict(sorted(st['x'].items())), st['merges'], float(st['min'].get('e1', 0)),
        float(st['min'].get('e2', 0)), float(st['min'].get('T1', 0)))

BASE_K = (2, [(95, 68, 0), (34, 33, 1), (10, 15, 1), (1, 24, 1)], None)

def skeptic_counterexamples():
    """G1: the skeptic's starts satisfy INV(a)-(d) but not (e); one cycle pair later they leave D or break INV."""
    print('-- G1. skeptic counterexamples (review-invariant.md G1): excluded by (e)?')
    L20 = [(7, 5*2**19 - 1, 0)] + [(2, 5*2**(20-j), 1) for j in range(2, 20)] + [(1, 6, 1)]
    cases = [('(o7)', (2, [(7, 19, 0), (2, 10, 1), (1, 6, 1)], None)),
             ('(o4)', (2, [(7, 39, 0), (2, 20, 1), (2, 10, 1), (2, 6, 1)], None)),
             ('INV(d) at a T2 start', (2, [(7, 15, 0), (8, 8, 0)], ('T2', 4))),
             ('at-threshold L*=20', (2, L20, None)),
             ('weak survival bounds', (2, [(15, 41, 0), (8, 17, 1), (1, 9, 1)], None)),
             ('(e1) only: e2 needed', (2, [(31, 19, 0), (2, 10, 1), (1, 6, 1)], None)),      # satisfies (e1), not (e2)
             ('(e2) only: e1 needed', (2, [(7, 19, 0), (8, 10, 1), (1, 6, 1)], None))]        # satisfies (e2), not (e1)
    ok = True
    for name, K in cases:
        lit = inv_violations(*K, with_e=False); full = inv_violations(*K)
        try:
            n1, K1 = run_to_repair(K); n2, K2 = run_to_repair(K1)
            nxt = inv_violations(*K2, with_e=False)
            what = 'next E-start %s violates INV: %s' % (str(K2)[:60], nxt) if nxt else 'stays in D and INV holds next'
            if not nxt and name == 'weak survival bounds':
                what = 'next E-start p_2 = %d (bare survival bound 3*2^(L*-2)+1 = %d)' % (K2[1][1][0], 3*2**(Lstar(K2[1], K2[2])-2)+1)
        except Outside as e:
            what = 'leaves D: %s' % e
        excluded = bool(full) and not lit
        ok &= excluded
        print('  %-24s INV(a)-(d) %s; (e) violated: %s; one cycle pair under INV alone: %s -> %s' % (
            name, 'hold' if not lit else 'FAIL %s' % lit, [c for c in full if c in ('e1', 'e2')], what, 'excluded PASS' if excluded else 'FAIL'))
    return ok

def orbit_e(lmax):
    """G2: the real orbit from the base E-start (after overflow 6), every cycle pair checked by cycle_pair_checked."""
    print('-- G2. INV+(e) and all lemma identities on the real orbit, from the base E-start to L* > %d' % lmax)
    h, P, T = INIT_K; P = list(P); rep = 0
    while rep < 6:
        h, P, T, name, k, m = mstep(h, P, T)
        rep += name in ('Ov', 'X1')
    okb = (h, P, T) == BASE_K and not inv_violations(*BASE_K)
    print('  base after overflow 6: %s; INV+(e) there: %s -> %s' % ((h, P, T), inv_violations(h, P, T) or 'all clauses hold',
                                                                    'PASS' if okb else 'FAIL'))
    st = new_stats(); fails = []; K = (h, P, T)
    try:
        while Lstar(K[1], K[2]) <= lmax and len(fails) < 20:
            K = cycle_pair_checked(K, fails, st)
    except Outside as e:
        fails.append('OUTSIDE %s' % e)
    for f in fails[:10]: print('  FAIL', f)
    print('  ' + fmt_stats(st))
    ok = okb and not fails
    print('  G2:', 'PASS' if ok else 'FAIL')
    return ok

def odds(lo, n): lo += (lo % 2 == 0); return range(lo, lo + 2*n, 2)
def evens(lo, n): lo += lo % 2; return range(lo, lo + 2*n, 2)

def boxes(w):
    """Exhaustive boxes of INV+(e) starts at and just above every threshold. w = 'small' or 'full'
    (full = the skeptic's boxes, 1,027,584 starts)."""
    import itertools
    f = w == 'full'
    out = {}
    # L* = 3, regular: pairs (p1,q1,0) (p2,q2,1) (pf,qf,1); r_1 = (q1+1)/4 >= 5, r_2 = q2/2 >= 5, p1 >= 31, p2 >= 8
    out['reg L*=3'] = (((2, [(a, b, 0), (c, d, 1), (e, g, 1)], None)) for a, b, c, d, e, g in itertools.product(
        odds(31, 8 if f else 3), range(19, 31 if f else 25), evens(8, 8 if f else 3), range(10, 22 if f else 16), range(1, 11), range(6, 12 if f else 8)))
    # L* = 3, T2 start: (p1,q1,0) (p2,q2,0) T2(k); r_1 = (q1+1)/4 >= 4, r_2 = q2/2 >= 4
    out['T2 L*=3'] = (((2, [(a, b, 0), (c, d, 0)], ('T2', k))) for a, b, c, d, k in itertools.product(
        odds(31, 8 if f else 3), range(15, 27 if f else 21), evens(8, 8 if f else 3), range(8, 20 if f else 14), range(4, 12 if f else 8)))
    # L* = 4, regular
    out['reg L*=4'] = (((2, [(a, b, 0), (c, d, 1), (e, g, 1), (i, j, 1)], None)) for a, b, c, d, e, g, i, j in itertools.product(
        odds(63, 4 if f else 2), range(39, 45 if f else 42), evens(16, 4 if f else 2), range(20, 26 if f else 23), evens(2, 4 if f else 2),
        range(10, 16 if f else 13), range(1, 9), range(6, 9 if f else 7)))
    # L* = 4, T2 start
    out['T2 L*=4'] = (((2, [(a, b, 0), (c, d, 1), (e, g, 0)], ('T2', k))) for a, b, c, d, e, g, k in itertools.product(
        odds(63, 4 if f else 2), range(31, 37 if f else 34), evens(16, 4 if f else 2), range(16, 22 if f else 19), evens(2, 4 if f else 2),
        range(8, 14 if f else 11), range(4, 9 if f else 6)))
    return out

def rand_start(rng, Ls, kind):
    """A random INV+(e) start; each value is at its threshold with probability 1/2."""
    def pick(lo, span): return lo if rng.random() < 0.5 else lo + rng.randint(0, span)
    L = Ls if kind == 'reg' else Ls - 1; thr = 5 if kind == 'reg' else 4; P = []
    for j in range(1, L + 1):
        e = Ls - j
        if kind == 'reg' and j == L: P.append((pick(1, 12), pick(6, 30), 1)); continue
        q = pick(thr*2**e - (j == 1), 3*2**e + 3)
        if j == 1: p = pick(2**(Ls+2) - 1, 2**(Ls+2)); p += (p % 2 == 0); d = 0
        else:
            p = pick(2**Ls if j == 2 else 2, 2**(e+2)); p += p % 2
            d = 0 if (kind == 'T2' and j == L) else 1
        P.append((p, q, d))
    return (2, P, None if kind == 'reg' else ('T2', pick(4, 30)))

def sweeps(width, nrand, chain, lrand, rng):
    print('-- G3. exhaustive boxes (%s): INV+(e) start -> one checked cycle pair -> INV+(e) at the next E-start' % width)
    allok = True
    for name, gen in boxes(width).items():
        st = new_stats(); fails = []; n = 0; bad = None
        for K in gen:
            n += 1
            if inv_violations(*K): fails.append('generator: %s' % (K,)); break
            f0 = len(fails)
            try: cycle_pair_checked(K, fails, st)
            except Outside as e: fails.append('OUTSIDE %s' % e)
            if len(fails) > f0 and bad is None: bad = (K, fails[f0:f0+3])
            if len(fails) > 50: break
        ok = not fails; allok &= ok
        print('  %-9s %7d starts: %s | %s' % (name, n, 'PASS' if ok else 'FAIL first %s' % (bad,), fmt_stats(st)))
    print('-- G4. random chains: %d chains of %d cycle pairs, L* = 3..%d, values at threshold w.p. 1/2' % (nrand, chain, lrand))
    st = new_stats(); fails = []; bad = None
    for it in range(nrand):
        K = rand_start(rng, rng.randint(3, lrand), rng.choice(['reg', 'T2']))
        assert not inv_violations(*K), (K, inv_violations(*K))
        for _ in range(chain):
            f0 = len(fails)
            try: K = cycle_pair_checked(K, fails, st)
            except Outside as e: fails.append('OUTSIDE %s' % e)
            if len(fails) > f0:
                if bad is None: bad = (K, fails[f0:f0+3])
                break
        if len(fails) > 50: break
    ok = not fails; allok &= ok
    print('  random    %s | %s' % ('PASS' if ok else 'FAIL first %s' % (bad,), fmt_stats(st)))
    return allok

def section_G(lmax, width, nrand, chain, lrand, rng):
    print('== G. INV+(e) (proof.md 3.8): clause (e), lemma L6, the potentials of L5/L6, counterexamples, sweeps')
    r1 = skeptic_counterexamples()
    r2 = orbit_e(lmax)
    r3 = sweeps(width, nrand, chain, lrand, rng)
    ok = r1 and r2 and r3
    print('  G total:', 'PASS' if ok else 'FAIL')
    return ok

if __name__ == '__main__':
    ap = argparse.ArgumentParser()
    ap.add_argument('--quick', action='store_true')
    ap.add_argument('--seed', type=int, default=20261010)
    ap.add_argument('--steps', type=int, default=None)
    ap.add_argument('--lmax', type=int, default=None)
    ap.add_argument('--sweep', choices=['small', 'full'], default='small', help='G3 box size (full = 1,027,584 starts)')
    ap.add_argument('--nrand', type=int, default=None, help='G4 number of random chains')
    ap.add_argument('--only-g', action='store_true', help='run section G only')
    a = ap.parse_args()
    rng = random.Random(a.seed)
    n = 12 if a.quick else 45
    steps = a.steps or (2*10**6 if a.quick else 3*10**7)
    lmax = a.lmax or (60 if a.quick else 300)
    nrand = a.nrand if a.nrand is not None else (200 if a.quick else 2000)
    if a.only_g:
        ok = section_G(lmax, a.sweep, nrand, 6, 40, rng)
        print('== SUMMARY: G INV+(e)', 'PASS' if ok else 'FAIL'); sys.exit(0 if ok else 1)
    section_B()                                   # informational only
    r = {'A rules': section_A(n, rng), 'C+D init/cross-check': section_CD(steps), 'E abstract run': section_E(lmax),
         'E2 endgame table': far_endgame(), 'F invariant INV': class_invariants(lmax),
         'G INV+(e)': section_G(lmax, a.sweep, nrand, 6, 40, rng)}
    print('== SUMMARY:', ', '.join('%s %s' % (k, 'PASS' if v else 'FAIL') for k, v in r.items()), '->', 'PASS' if all(r.values()) else 'FAIL',
          '| B is informational. Simulation checks the claims of proof.md; the proof is the argument in proof.md section 3.')