#!/usr/bin/env python3
"""check_proof.py -- simulation evidence for proof.md of 1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---

Run from this directory:  python3 -B check_proof.py  [--quick]
Sections (match proof.md section 7):
  A  token window lemmas W1..W6 (exact finite runs; the head never leaves the window)
  B  right-sweep rules R1..R5 on random parameters (exact runs, step formulas)
  C  left turnaround L (inc_L) exhaustively over the word domain, length <= 9 (8 with --quick)
  D  departure rules GEN / ABS1 / ABS0 / ABSO1 on random instances (direct simulation to the next departure)
  E  right-part lemmas H1..H4 on random right parts (pure arithmetic on the model)
  F  trajectory: C dumper to 1e8 steps, lockstep model check + every invariant clause, open lemmas O1/O2 probed
  G  initial segment: blank tape -> first departure at step >= 2000 (exact config and step)
Nothing here is a proof. Every check prints PASS/FAIL; the last line is SUMMARY.
Review 2026-10-10 added: L with right context O and the empty word; spacing-3 and edge-case departures;
P_k (replaces O1) exhaustively; Safe(w, tau) and H4-with-strips on the trajectory.
"""
import sys, os, random, itertools, subprocess
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, os.path.join(HERE, 'scripts', 'deepen'))
from linc import inc_L                       # noqa: E402
from model3 import step as model_step, inc, abs0   # noqa: E402
from nextdep import next_departure           # noqa: E402
from tok import parses, compact              # noqa: E402

QUICK = '--quick' in sys.argv
TM = '1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---'
S = 'ABCDEF'
TR = {}
for qi, part in enumerate(TM.split('_')):
    for s in (0, 1):
        t = part[3*s:3*s+3]
        TR[(S[qi], s)] = None if t == '---' else (int(t[0]), 1 if t[1] == 'R' else -1, t[2])
TOK = {'0': '00', '1': '10', 'O': '100', 'I': '110'}
def w2s(w): return ''.join(TOK[c] for c in w)
B = '10110'
RESULTS = []
def report(name, ok, detail=''):
    RESULTS.append((name, ok))
    print(('PASS ' if ok else 'FAIL ') + name + ('  ' + detail if detail else ''))

def runwin(cells, pos, q, maxn=10**6):
    c = list(cells); n = 0
    while 0 <= pos < len(c) and n < maxn:
        tr = TR[(q, c[pos])]
        if tr is None: return c, pos, q, n, True
        c[pos] = tr[0]; pos += tr[1]; q = tr[2]; n += 1
    return c, pos, q, n, False
def bits(s): return [int(x) for x in s]

# ---------------------------------------------------------------- A: token window lemmas
print('== A: token window lemmas')
# (name, before-cells, head index, state, after-cells, exit side 'L'/'R', exit state, steps)
WL = [
    ('W1  E> 1 -> 1 E>',            '10',          0, 'E', '10',          'R', 'E', 4),
    ('W2  1 E> I -> I 1 E>',        '10110',       2, 'E', '11010',       'R', 'E', 13),
    ('W3  E> O -> <F I',            '100',         0, 'E', '110',         'L', 'F', 7),
    ('W4  1 E> T -> <F O T',        '10'+'11'+'0'*7, 2, 'E', '100'+'11'+'0'*6, 'L', 'F', 19),
    ('W5  I 1 <F -> <F 1 I',        '11010',       4, 'F', '10110',       'L', 'F', 9),
    ('W6  I <F -> <F O',            '110',         2, 'F', '100',         'L', 'F', 3),
]
for name, bef, p, q, aft, side, q2, n in WL:
    c, pos, qq, k, h = runwin(bits(bef), p, q)
    ok = (not h and ''.join(map(str, c)) == aft and qq == q2 and k == n and
          ((side == 'L' and pos == -1) or (side == 'R' and pos == len(bef))))
    report(name, ok, f'{k} steps')

# ---------------------------------------------------------------- B: right-sweep rules
print('== B: right-sweep rules (exact runs, sentinel left part "10" so F stops on entering it)')
def run_right(R, maxn=10**7):
    """tape = '10' + R + 0^pad, E at the first cell of R; stop when F first reads a cell left of R.
    returns (new R string trimmed to len, steps) or None"""
    L = '10'; pad = 40
    c = bits(L + R + '0'*pad); pos = len(L); q = 'E'; n = 0
    while n < maxn:
        tr = TR[(q, c[pos])]
        if tr is None: return ('HALT', n)
        c[pos] = tr[0]; pos += tr[1]; q = tr[2]; n += 1
        if pos < len(L):
            return (q, pos - len(L), ''.join(map(str, c[len(L):])).rstrip('0'), n)
    return ('MAX', n)
def Rstr(g, D, G): return B*g + ''.join(('110' if d else '100') + B*G[i] for i, d in enumerate(D)) + '11'
rng = random.Random(7)
okR1 = all(runwin(bits(B*n), 0, 'E')[1:4] == (5*n, 'E', 17*n) and ''.join(map(str, runwin(bits(B*n), 0, 'E')[0])) == '11010'*n for n in range(0, 31))
report('R1  E> B^n -> C^n E>, 17n, n=0..30', okR1)
okR2 = all(runwin(bits('11010'*n), 5*n-1, 'F')[1:4] == (-1, 'F', 9*n) and ''.join(map(str, runwin(bits('11010'*n), 5*n-1, 'F')[0])) == B*n for n in range(1, 31))
report('R2  C^n <F -> <F B^n, 9n, n=1..30', okR2)
cnt = {'R3': 0, 'R4': 0, 'R5': 0}; bad = []
for trial in range(600 if QUICK else 2000):
    a = rng.randint(1, 25); j = rng.randint(0, 6); bs = [rng.randint(0, 12) for _ in range(j)]
    kind = rng.choice(['zero', 'end'])
    if j == 0 and kind == 'zero':
        R = B*a + '100' + B*rng.randint(0, 3) + '11'; tail = R[5*a+3:]
        exp = B*a + '110' + tail; n_exp = 26*a + 7; key = 'R3'
    elif kind == 'zero':
        rest = B*rng.randint(0, 3) + '11'
        R = B*a + ''.join('110' + B*b for b in bs) + '100' + rest
        exp = B*(a-1) + ''.join('100' + B*b for b in bs[:-1]) + '100' + B*(bs[-1]+1) + '110' + rest
        n_exp = 26*(a+sum(bs)) + 16*j + 7; key = 'R4'
    else:
        R = B*a + ''.join('110' + B*b for b in bs) + '11'
        exp = B*(a-1) + ''.join('100' + B*b for b in bs) + '100100' + '11'
        n_exp = 26*(a+sum(bs)) + 16*j + 13; key = 'R5'
    r = run_right(R)
    ok = r[0] == 'F' and r[1] == -1 and r[2] == exp.rstrip('0') and r[3] == n_exp
    cnt[key] += 1
    if not ok and len(bad) < 5: bad.append((key, a, bs, r[:2], r[3] if len(r) > 3 else None, n_exp))
report(f'R3/R4/R5 exact output and step formula on random parameters {cnt}', not bad, str(bad[:3]))

# ---------------------------------------------------------------- C: left turnaround
print('== C: left turnaround L:  0^inf w <F B  ->  0^inf inc_L(w) E> B')
def in_domain(w):
    """WS-domain for the left turnaround (proof.md 3.2): first token not 0; last token 0/1; w not ending I1;
    markers (O/I) pairwise >= 3 tokens apart."""
    if not w or w[0] == '0' or w[-1] in 'OI' or w.endswith('I1'): return False
    m = [i for i, ch in enumerate(w) if ch in 'OI']
    return all(b - a >= 3 for a, b in zip(m, m[1:]))
def turnaround(w, pad=30):
    L = '0'*pad + w2s(w); R = B*2 + '0'*8
    c = bits(L + R); pos = len(L) - 1; q = 'F'; n = 0; lo = pos; hi = pos
    while n < 10**6:
        tr = TR[(q, c[pos])]
        if tr is None: return ('HALT', n)
        c[pos] = tr[0]; pos += tr[1]; q = tr[2]; n += 1
        lo = min(lo, pos); hi = max(hi, pos)
        if pos < 2: return ('OOB', n)
        if q == 'E' and tr[1] > 0 and pos >= len(L) - 4 and c[pos:pos+5] == [1, 0, 1, 1, 0] and pos == len(L):
            left = ''.join(map(str, c[:pos])).lstrip('0')
            return ('OK', n, left, hi - len(L) + 1, len(L) - lo)
        if pos > len(L) + 1: return ('RIGHT', n)
    return ('MAX', n)
maxlen = 8 if QUICK else 9
tot = good = 0; badC = []; steps_tab = {}; reach_right = 0; out_dom_bad = 0; out_dom = 0
for n_ in range(1, maxlen+1):
    for tup in itertools.product('01OI', repeat=n_):
        w = ''.join(tup)
        if w[0] == '0': continue
        dom = in_domain(w)
        r = turnaround(w)
        if not dom:
            if w[-1] in '01' and not w.endswith('I1'):
                out_dom += 1
                ok_o = r[0] == 'OK' and r[2] == w2s(inc_L(w))
                if not ok_o: out_dom_bad += 1
            continue
        tot += 1
        ok = r[0] == 'OK' and r[2] == w2s(inc_L(w))
        if ok:
            good += 1
            cross0 = w[-1] == '0' and w[:-1].rstrip('1').endswith('I')   # I-crossing with t = 0
            if r[3] > 2 or (r[3] == 2 and not cross0): reach_right += 1
            if all(ch in '01' for ch in w):
                u = w[:-1]; k = len(u) - len(u.rstrip('1'))
                key = (w[-1], 'edge' if k == len(u) else 'stop0')
                steps_tab.setdefault(key, {}).setdefault(k, set()).add(r[1])
        elif len(badC) < 5: badC.append((w, r))
report(f'L on all {tot} domain words of length <= {maxlen}: machine == inc_L; reads right of w only on an I-crossing with t=0 (tail I 1^k 0), and then only the first token 10 of B', good == tot and reach_right == 0, str(badC))
# step formula for marker-free words: steps = 6k + 13 + 8*[t=1]... fitted and checked here
fit_ok = True; fitted = {}
for key, d in steps_tab.items():
    for k, ss in d.items():
        if len(ss) != 1: fit_ok = False
        fitted[(key, k)] = min(ss)
# report the affine law per class
law = {}
for (key, k), s in sorted(fitted.items()):
    law.setdefault(key, []).append((k, s))
law_ok = True; law_txt = []
for key, pts in law.items():
    (k0, s0), (k1, s1) = pts[0], pts[1]
    slope = (s1 - s0) // (k1 - k0); icpt = s0 - slope*k0
    law_ok &= all(s == slope*k + icpt for k, s in pts)
    law_txt.append(f'{key}: {slope}k+{icpt}')
report('L step count is affine in the carry length k for marker-free words (' + '; '.join(sorted(law_txt)) + ')', fit_ok and law_ok)
print(f'     (outside the domain, last token 0/1: {out_dom} words, {out_dom_bad} where the machine differs from inc_L)')

# --- review 2026-10-10: L for any right context whose first two cells are 1,0 (a 1 token or an O token)
def turnaround2(w, R0, pad=30):
    """0^inf w <F R0 ... ; stop when E first moves right onto the first cell after w with R0 intact.
    returns ('OK', steps, left cells, max cells read right of w) or a failure tag"""
    L = '0'*pad + w2s(w); R = R0 + '0'*8
    c = bits(L + R); pos = len(L) - 1; q = 'F'; n = 0; hi = pos
    while n < 10**6:
        tr = TR[(q, c[pos])]
        if tr is None: return ('HALT', n)
        c[pos] = tr[0]; pos += tr[1]; q = tr[2]; n += 1
        hi = max(hi, pos)
        if pos < 2: return ('OOB', n)
        if q == 'E' and tr[1] > 0 and pos == len(L) and ''.join(map(str, c[pos:pos+len(R0)])) == R0:
            return ('OK', n, ''.join(map(str, c[:pos])).lstrip('0'), hi - len(L) + 1)
        if pos > len(L) + 1: return ('RIGHT', n)
    return ('MAX', n)
ctxs = {'1 I (B)': B + B, 'O B': '100' + B, '1 O': '10' + '100' + B}
dom_words = [''] + [''.join(t) for n_ in range(1, (8 if QUICK else 9) + 1) for t in itertools.product('01OI', repeat=n_)]
dom_words = [w for w in dom_words if w == '' or in_domain(w)]
for cname, R0 in ctxs.items():
    okc = 0; badc = []; rr = 0
    for w in dom_words:
        r = turnaround2(w, R0)
        if r[0] == 'OK' and r[2] == w2s(inc_L(w)):
            okc += 1
            if r[3] > 2: rr += 1
        elif len(badc) < 3: badc.append((w, r[:3]))
    report(f'L with right context [{cname}] on {len(dom_words)} words (incl. the empty word): machine == inc_L, reads <= 2 cells right of w: {okc}/{len(dom_words)}',
           okc == len(dom_words) and rr == 0, str(badc))
# precondition is needed: with an I token (cells 110) right of w, the t=0 I-crossing words go wrong
neg = [w for w in dom_words if w and w[-1] == '0' and w[:-1].rstrip('1').endswith('I')]
negbad = sum(1 for w in neg if not (lambda r: r[0] == 'OK' and r[2] == w2s(inc_L(w)))(turnaround2(w, '110' + B)))
report(f'L precondition is sharp: with I (110) right of w, {negbad}/{len(neg)} t=0 I-crossing words differ from inc_L (all other words unaffected)', negbad == len(neg) and len(neg) > 0)

# ---------------------------------------------------------------- D: departure rules
print('== D: departure rules on random instances (direct simulation to the next departure)')
rng = random.Random(11)
def rword(n):
    w = '1' + ''.join(rng.choice('01') for _ in range(n-1))
    for _ in range(rng.choice([0, 0, 1, 1, 2]) if len(w) >= 5 else 0):
        i = rng.randint(0, len(w) - 4)
        w = w[:i] + rng.choice('OI') + w[i+1:]
    if w[-1] in 'OI': w = w[:-1] + rng.choice('01')
    return w
def ws_ok(w):
    m = [i for i, ch in enumerate(w) if ch in 'OI']
    return w[0] != '0' and w[-1] in '01' and all(b - a >= 4 for a, b in zip(m, m[1:]))
def rright(k):
    """random right part satisfying INV-R: H_i = G_i - d_(i+1) >= 0, non-increasing, H_k = G_k = 0"""
    D = [rng.randint(0, 1) for _ in range(k)]
    H = [0]*k
    for i in range(k-2, -1, -1):
        H[i] = H[i+1] + rng.choice([0, 0, 1, 1, 2, 3, rng.randint(0, 20)])
    G = [H[i] + (D[i+1] if i+1 < k else 0) for i in range(k)]
    return D, G
from collections import Counter
CD = Counter(); badD = []
N = 800 if QUICK else 3000
for t_ in range(N):
    w = rword(rng.randint(4, 24))
    if not ws_ok(w): continue
    k = rng.randint(2, 12); D, G = rright(k)
    mode = t_ % 4
    if mode == 0: g = rng.randint(2, 60)
    elif mode == 1: g = 1; D[0] = 0
    else: g = 1; D[0] = 1
    rule, pred = model_step((w, g, D, G))
    if pred is None: CD[(rule, 'no-rule')] += 1; continue
    r = next_departure(w, g, D, G)
    ok = r[0] == 'OK' and r[2] == pred
    CD[(rule, ok)] += 1
    if not ok and len(badD) < 5: badD.append((rule, w, g, D, G, r[:3], pred))
okD = not badD and all(k[1] in (True, 'no-rule') for k in CD)
report('GEN/ABS1/ABS0/ABSO1 predicted == simulated ' + str(dict(CD)), not badD, str(badD[:2]))
# ABSO1 explicitly (side case, never on the trajectory)
CO = Counter(); badO = []
for t_ in range(200 if QUICK else 600):
    x = rword(rng.randint(3, 16))
    if x[-1] not in '01': continue
    w = x + 'O1'
    if not ws_ok(w): continue
    k = rng.randint(2, 10); D, G = rright(k); D[0] = 1
    rule, pred = model_step((w, 1, D, G))
    if rule != 'ABSO1': continue
    r = next_departure(w, 1, D, G)
    ok = r[0] == 'OK' and r[2] == pred
    CO[ok] += 1
    if not ok and len(badO) < 3: badO.append((w, D, G, r[:3], pred))
report(f'ABSO1 on {sum(CO.values())} targeted instances', not badO and sum(CO.values()) > 0, str(badO))

# --- review 2026-10-10: spacing 3 (markers exactly 3 tokens apart), and the edge cases |w| = 1 and w = ''
def rword3(n):
    """random word with >= 2 markers, consecutive markers exactly 3 apart where possible"""
    w = list('1' + ''.join(rng.choice('01') for _ in range(n-1)))
    i = rng.randint(0, 2)
    while i <= len(w) - 3:
        w[i] = rng.choice('OI'); i += 3 if rng.random() < 0.7 else 4
    w = ''.join(w)
    if w[-1] in 'OI': w = w[:-1] + rng.choice('01')
    return w
def ws3(w):
    m = [i for i, ch in enumerate(w) if ch in 'OI']
    return w[0] != '0' and w[-1] in '01' and all(b - a >= 3 for a, b in zip(m, m[1:])) and any(b - a == 3 for a, b in zip(m, m[1:]))
C3 = Counter(); bad3 = []
for t_ in range(800 if QUICK else 3000):
    w = rword3(rng.randint(6, 24))
    if not ws3(w): continue
    k = rng.randint(2, 12); D, G = rright(k)
    mode = t_ % 4
    if mode == 0: g = rng.randint(2, 60)
    elif mode == 1: g = 1; D[0] = 0
    else: g = 1; D[0] = 1
    rule, pred = model_step((w, g, D, G))
    if pred is None: C3[(rule, 'no-rule')] += 1; continue
    r = next_departure(w, g, D, G)
    ok = r[0] == 'OK' and r[2] == pred
    C3[(rule, ok)] += 1
    if not ok and len(bad3) < 5: bad3.append((rule, w, g, D, G, r[:3], pred))
report('spacing 3: GEN/ABS1/ABS0/ABSO1 predicted == simulated on words with markers exactly 3 apart ' + str(dict(C3)), not bad3 and C3[('GEN', True)] > 0 and C3[('ABS1', True)] > 0, str(bad3[:2]))
CE = Counter(); badE = []
for t_ in range(100 if QUICK else 300):
    k = rng.randint(2, 10); D, G = rright(k)
    for w, g in (('1', 1), ('', rng.randint(2, 30))):
        if w == '1': D[0] = 1
        rule, pred = model_step((w, g, D, G))
        r = next_departure(w, g, D, G)
        ok = pred is not None and r[0] == 'OK' and r[2] == pred
        CE[(rule, w or "''", ok)] += 1
        if not ok and len(badE) < 3: badE.append((w, g, D, G, rule, r[:3], pred))
report('edge cases: ABS1 on w = 1 (u empty, gives 10) and GEN on the empty word (inc_L(\'\') = 10) ' + str(dict(CE)), not badE, str(badE))

# ---------------------------------------------------------------- E: right-part lemmas (arithmetic)
print('== E: right-part lemmas H1..H4 (pure model arithmetic, random right parts)')
def Hvec(g, D, G):
    k = len(D)
    return [g - D[0]] + [G[i] - (D[i+1] if i+1 < k else 0) for i in range(k)]
rng = random.Random(5)
okH1 = okH2 = okH3 = True; nH = 0
for t_ in range(4000 if QUICK else 20000):
    k = rng.randint(1, 10); D, G = rright(k); g = rng.randint(1, 40)
    if g == 1 and D[0] == 1: continue
    H = Hvec(g, D, G)
    g2, D2, G2 = inc(g, D, G); H2 = Hvec(g2, D2, G2); nH += 1
    # H1: H_i (i>=1) never decreases; H_0 drops by 1 exactly when d_1 is set
    okH1 &= all(H2[i] >= H[i] for i in range(1, len(H))) and H2[0] == H[0] - (1 - D[0])
    # H2: H_i - H_{i+1} never decreases (i>=1, over the old index range); new entries are 0
    okH2 &= all(H2[i] - H2[i+1] >= H[i] - H[i+1] for i in range(1, len(H)-1)) and all(x == 0 for x in H2[len(H):])
    # H3: last gap stays 0, g stays >= 1
    okH3 &= G2[-1] == 0 and g2 >= 1
report(f'H1  inc never lowers H_i (i>=1); H_0 drops exactly on a set of d_1  ({nH} incs)', okH1)
report('H2  inc never lowers H_i - H_(i+1); overflow appends H = 0, 0', okH2)
report('H3  inc keeps G_k = 0 and g >= 1 (from g >= 2 or d_1 = 0)', okH3)
# H4: absorption interval  Delta = 2(h_1 + c) - 1 + d_2  (c=2 ABS1, c=1 ABS0) and next h_1 formula, on the model
okH4 = True; nH4 = 0
for t_ in range(3000 if QUICK else 10000):
    k = rng.randint(2, 10); D, G = rright(k); D[0] = 1
    if G[0] - D[1] < 0: continue
    c = rng.choice([1, 2])
    g, D2, G2 = inc(G[0] + c, D[1:], G[1:]); n = 1
    while not (g == 1 and D2[0] == 1):
        g, D2, G2 = inc(g, D2, G2); n += 1
        if n > 10**5: break
    h1 = G[0] - D[1]
    okH4 &= n == 2*(h1 + c) - 1 + D[1]; nH4 += 1
report(f'H4  (no strips in between) sweeps from an absorption to the next = 2(h_1+c) - 1 + d_2  ({nH4} cases; with strips see F)', okH4)

# P_k replaces O1 (review 2026-10-10): exhaustive one-step check, INV-R + INV-W + P_k -> INV-R + P_k
for sp in (4, 3):
    pr = subprocess.run([sys.executable, '-B', os.path.join(HERE, 'scripts', 'review', 'pk_check.py'), '6' if QUICK else '7', '4', '4', str(sp)],
                        capture_output=True, text=True)
    report('P_k  ' + pr.stdout.strip().splitlines()[0], pr.returncode == 0)

# ---------------------------------------------------------------- F: trajectory
print('== F: trajectory (C departure dumper), lockstep model + invariant clauses')
SCR = os.environ.get('CP_SCRATCH', '/tmp/claude-1000/cp_bb6_m1')
os.makedirs(SCR, exist_ok=True)
exe = os.path.join(SCR, 'dep'); dump = os.path.join(SCR, 'dep.txt')
horizon = '3e7' if QUICK else '1e8'
subprocess.run(['gcc', '-O2', '-o', exe, os.path.join(HERE, 'scripts', 'deepen', 'dep.c')], check=True)
with open(dump, 'w') as f:
    subprocess.run([exe, horizon], stdout=f, stderr=subprocess.DEVNULL, check=True)
rows = []
for line in open(dump):
    p = line.split()
    if p[0] in ('HALT', 'BADLEFT') or 'RAW' in p:
        rows.append(None); continue
    st = int(p[0]); w = compact(parses(p[4])[0]); g = int(p[5])
    D = [] if p[6] == '-' else [int(ch) for ch in p[6]]
    G = [] if p[7] == '-' else [int(x) for x in p[7].split(',')]
    rows.append((st, w, g, D, G))
START = 2000
i0 = next(i for i, r in enumerate(rows) if r and r[0] >= START)
C = Counter(); badF = []
def strip(w, g):
    while w.endswith('I1'): w = w[:-2]; g += 1
    return w, g
prev_rule = []
for i in range(i0, len(rows) - 1):
    r = rows[i]; r2 = rows[i+1]
    if r is None or r2 is None: C['unparsed'] += 1; continue
    st, w, g, D, G = r
    rule, pred = model_step((w, g, D, G))
    C['lock', rule, pred == r2[1:]] += 1
    if pred != r2[1:] and len(badF) < 5: badF.append(('lock', st, rule))
    ws, gs = strip(w, g)
    k = len(D); H = Hvec(gs, D, G)
    # INV-R (proven part)
    C['R: g>=1, G_k=0, H_i>=0, H non-increasing (i>=1)', gs >= 1 and G[-1] == 0 and min(H[1:]) >= 0 and all(H[j] >= H[j+1] for j in range(1, k))] += 1
    C['R: H_i>=1 for 1<=i<=k-3 (lemma H5)', all(H[j] >= 1 for j in range(1, k-2))] += 1
    # INV-W (word shape)
    m = [j for j, ch in enumerate(ws) if ch in 'OI']
    C['W: first token not 0, last token 0/1, markers >=4 apart', ws[0] != '0' and ws[-1] in '01' and all(b - a >= 4 for a, b in zip(m, m[1:]))] += 1
    C['P_k: k>=2, or k=1, D=[1] and (g>=2 or last token 1)', k >= 2 or (k == 1 and D == [1] and (gs >= 2 or ws[-1:] == '1'))] += 1
    if rule != 'GEN':
        C[('info', 'O1 h_1>=1 at absorptions'), k >= 2 and H[1] >= 1] += 1
        if rule == 'ABS0':
            C['abs0: token before the trailing 1-run is not a marker (O2)', pred is not None] += 1
        # transient lemma T: the two sweeps after an ABS1 are GEN
        if rule == 'ABS1':
            nxt = [model_step(rows[i+j][1:])[0] if rows[i+j] else None for j in (1, 2)]
            C['T: two sweeps after ABS1 are GEN', nxt == ['GEN', 'GEN']] += 1
    C['rule', rule] += 1
# --- review 2026-10-10: Safe(w, tau) (O2 as a predicate on one configuration), H4 with strips, margins
def spaced(w, sp):
    m = [j for j, ch in enumerate(w) if ch in 'OI']
    return all(b - a >= sp for a, b in zip(m, m[1:]))
def safe(w, tau, sp):
    """word-only run to the next absorption: tau = 2g-1-d_1 sweeps, each strip adds 2; at tau = 0 an ABS0 must be defined
    and leave markers >= sp apart. Returns (ok, word at the absorption)."""
    while True:
        while w.endswith('I1'): w = w[:-2]; tau += 2
        if tau == 0:
            if w[-1] == '0':
                o = abs0(w); return (o is not None and spaced(o, sp)), w
            return True, w
        w = inc_L(w); tau -= 1
abs_idx = [i for i in range(i0, len(rows) - 1) if rows[i] and model_step(rows[i][1:])[0] != 'GEN']
starts = [i0] + [i + 1 for i in abs_idx if i + 1 < len(rows) - 1]
for i in starts:
    st, w, g, D, G = rows[i]; ws, gs = strip(w, g); tau = 2*gs - 1 - D[0]
    for sp in (4, 3):
        ok, wa = safe(ws, tau, sp)
        C['Safe(w, 2g-1-d_1), spacing >= %d, at the first departure of every interval' % sp, ok] += 1
# H4 with strips: Delta = 2(h_1 + c) - 1 + d_2 + 2s, s = number of strips in the interval
for a, b in zip(abs_idx, abs_idx[1:]):
    st, w, g, D, G = rows[a]; rule = model_step(rows[a][1:])[0]
    c = 2 if rule == 'ABS1' else 1
    if rule == 'ABSO1': continue
    h1 = G[0] - (D[1] if len(D) > 1 else 0)
    s_ = sum((len(rows[j][1]) - len(strip(rows[j][1], 0)[0])) // 2 for j in range(a + 1, b + 1))
    C['H4 with strips: Delta = 2(h_1+c) - 1 + d_2 + 2s on the trajectory', b - a == 2*(h1 + c) - 1 + D[1] + 2*s_] += 1
marg = []
for i in abs_idx:
    st, w, g, D, G = rows[i]; ws, gs = strip(w, g)
    if model_step(rows[i][1:])[0] == 'ABS0' and any(ch in 'OI' for ch in ws):
        marg.append((st, ws))
print('     ABS0 with a marker present (step, word):', marg)
lockbad = sum(v for k_, v in C.items() if k_[0] == 'lock' and k_[2] is False)
nsweeps = sum(v for k_, v in C.items() if k_[0] == 'lock')
report(f'lockstep model == machine over {nsweeps} sweeps (start step {rows[i0][0]}, horizon {horizon})', lockbad == 0 and C['unparsed'] == 0,
       str({k_[1]: v for k_, v in C.items() if k_[0] == 'rule'}))
for key in ['R: g>=1, G_k=0, H_i>=0, H non-increasing (i>=1)', 'R: H_i>=1 for 1<=i<=k-3 (lemma H5)',
            'W: first token not 0, last token 0/1, markers >=4 apart', 'P_k: k>=2, or k=1, D=[1] and (g>=2 or last token 1)',
            'Safe(w, 2g-1-d_1), spacing >= 4, at the first departure of every interval', 'Safe(w, 2g-1-d_1), spacing >= 3, at the first departure of every interval',
            'H4 with strips: Delta = 2(h_1+c) - 1 + d_2 + 2s on the trajectory',
            'abs0: token before the trailing 1-run is not a marker (O2)', 'T: two sweeps after ABS1 are GEN']:
    t_ = C[(key, True)]; f_ = C[(key, False)]
    report(f'{key}: {t_}/{t_+f_}', f_ == 0 and t_ > 0)

# ---------------------------------------------------------------- G: initial segment
print('== G: initial segment from the blank tape')
first = rows[i0]
# replay with an independent python simulator and compare the exact tape at that step
size = 4000; tape = bytearray(size); pos = size//2; q = 'A'; n = 0
while n < first[0]:
    tr = TR[(q, tape[pos])]
    tape[pos] = tr[0]; pos += tr[1]; q = tr[2]; n += 1
lo = 0
while not tape[lo]: lo += 1
hi = size - 1
while not tape[hi]: hi -= 1
left = ''.join(map(str, tape[lo:pos])); right = ''.join(map(str, tape[pos:hi+1]))
exp_left = w2s(first[1]); exp_right = Rstr(first[2], first[3], first[4])
report(f'init: c0 -->({first[0]}) 0^inf {first[1]} E> R(g={first[2]}, D={first[3]}, G={first[4]})  [left={left} right={right}]',
       q == 'E' and left == exp_left and right == exp_right)

print()
nf = sum(1 for _, ok in RESULTS if not ok)
print(f'SUMMARY {"PASS" if nf == 0 else "FAIL"}  ({len(RESULTS) - nf}/{len(RESULTS)} checks pass)')