"""Simulation evidence for the DELTA proof.md of the twin 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.

The parent (kill #12) is 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF, whose run model, epoch rules and
Theorem are proved in its passing .v file and checked by its own check_proof.py.  This script checks every
claim of the delta (proof.md labels R, A, C, B, T, H, F, G) and, with --model, re-runs the parent's
model-level sections D, E1, E2 (TM-independent, imported from the parent's check_proof.py).  Run:
    ulimit -v 6000000; python3 -B check_proof.py [--quick] [--seed S] [--model]
Exit code 0 iff every check passed.  Stdlib + a C compiler (scripts/edge_scan.c).

Sections
  R  relation: not a renaming or mirror image of the parent (all 720 relabelings x 2 mirrors);
     the best relabeling sigma (twin A..F = parent B,C,D,E,F,A) differs in exactly one transition
     (twin F0 = 1RF, i.e. parent-named A0 = 1RA instead of 1RB); sigma(parent) = Eqv.v TM113.tm
  A  TM-level rules on the twin TM itself: R1, R2, R2e, HALT exactly as the parent's (same steps, and the
     same transition sequence under sigma); R3' = the parent's R3 with A0 B0 replaced by F0 F0 F1 B1 A1 A0
     (twin names), same tape effect, +4 steps; F0 occurs in no other rule
  C  initial segment: blank, state A -> step 8 conf([],[1]) -> 23 -> 38 -> step 48 conf([],[2,2,1])
  B  run model == twin TM: B1 macro step by macro step from step 48; B2 every left-edge configuration of
     the raw twin to step 4*10^8 == the model's (twin step counts); B3 tools/sim.py C-core spot checks
  T  trajectory twin: twin, Eqv.v TM113.tm (= parent started in B) and parent pass the same words O_n([]);
     twin = TM113 + 4(n+1) steps at edge return n; twin conf([],[2,2]+O_n) vs parent conf([],[3,2]+O_n)
  H  budget-2 edge lemma (model): Ep(W) = (c,W'), c <= 2  =>  conf([],[2,2]+W) -> conf([],[4-c,2]+W')
  F  top level: every epoch of O_n([]) costs exactly 2 (parent section F, imported)
  G  the twin's undefined transition D0 is read only in the HALT pattern (D always reads 1 from blank)
"""
import importlib.util
import itertools
import os
import random
import subprocess
import sys
import tempfile
import time

TWIN = "1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB"
PARENT = "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF"
TM113 = "1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RA1LB"      # vendor/busycoq/verify/Eqv.v:2601 (TM113.tm)
ROOT = "[local working file]"
HERE = os.path.dirname(os.path.abspath(__file__))
PDIR = os.path.join(ROOT, "machines", PARENT)
QUICK = "--quick" in sys.argv
MODEL = "--model" in sys.argv
SEED = int(sys.argv[sys.argv.index("--seed") + 1]) if "--seed" in sys.argv else 2026
FAIL = []
ST = "ABCDEF"
SIGMA = dict(zip("ABCDEF", "BCDEF" + "A"))     # twin state -> parent state
SIGINV = {v: k for k, v in SIGMA.items()}       # parent state -> twin state
HEAD = ST.index(SIGINV["A"])                     # the run model's head state: parent A = twin F

# the parent's check_proof.py: its run model (mstep, Ep, orbits, to_model) is TM-independent
_spec = importlib.util.spec_from_file_location("parent_check", os.path.join(PDIR, "check_proof.py"))
P = importlib.util.module_from_spec(_spec)
_spec.loader.exec_module(P)


def ok(label, cond, info=""):
    if not cond:
        FAIL.append((label, info))
        if sum(1 for f in FAIL if f[0] == label) <= 3:
            print("  FAIL", label, info)
    return 1 if cond else 0


# ----------------------------------------------------------------------------------------------
# machines
def parse(s):
    """{(state letter, sym): (w, 'L'|'R', next letter) or None}"""
    tab = {}
    for q, blk in zip(ST, s.split("_")):
        for sym in (0, 1):
            t = blk[3 * sym:3 * sym + 3]
            tab[(q, sym)] = None if t[2] == "-" else (int(t[0]), t[1], t[2])
    return tab


def unparse(tab):
    out = []
    for q in ST:
        blk = ""
        for sym in (0, 1):
            t = tab[(q, sym)]
            blk += "---" if t is None else f"{t[0]}{t[1]}{t[2]}"
        out.append(blk)
    return "_".join(out)


def relabel(tab, pi, mirror=False):
    """pi: new state -> old state.  The machine with old state pi(X) called X (and L/R swapped if mirror)."""
    inv = {v: k for k, v in pi.items()}
    out = {}
    for X in ST:
        for sym in (0, 1):
            t = tab[(pi[X], sym)]
            if t is None:
                out[(X, sym)] = None
            else:
                d = t[1] if not mirror else ("L" if t[1] == "R" else "R")
                out[(X, sym)] = (t[0], d, inv[t[2]])
    return out


class Tape:
    """exact simulator; ones = set of positions holding 1; state = letter."""

    def __init__(self, tab, ones, head, state):
        self.tab, self.ones, self.head, self.state = tab, set(ones), head, state
        self.steps, self.halted, self.halt_read, self.seq = 0, False, None, []

    def run(self, n, trace=False):
        tab, ones, h, q = self.tab, self.ones, self.head, self.state
        for _ in range(n):
            s = 1 if h in ones else 0
            t = tab[(q, s)]
            if trace:
                self.seq.append(q + str(s))
            if t is None:
                self.halted, self.halt_read = True, q + str(s)
                break
            w, d, q2 = t
            (ones.add(h) if w else ones.discard(h))
            h += 1 if d == "R" else -1
            q = q2
            self.steps += 1
        self.head, self.state = h, q
        return self


TW, PA = parse(TWIN), parse(PARENT)


def sig(seq):
    """twin transition names -> parent names"""
    return [SIGMA[x[0]] + x[1] for x in seq]


# ----------------------------------------------------------------------------------------------
def section_R():
    print("R  relation to the parent: renaming / mirror search")
    best = []
    exact = []
    start_kept = {False: 99, True: 99}
    for perm in itertools.permutations(ST):
        pi = dict(zip(ST, perm))
        for mirror in (False, True):
            cand = relabel(PA, pi, mirror)
            diff = [(X, s) for X in ST for s in (0, 1) if cand[(X, s)] != TW[(X, s)]]
            if not diff:
                exact.append((perm, mirror))
            best.append((len(diff), "".join(perm), mirror, diff))
            if pi["A"] == "A":
                start_kept[mirror] = min(start_kept[mirror], len(diff))
    best.sort()
    ok("R1 no exact renaming/mirror", not exact, exact)
    top = [b for b in best if b[0] == best[0][0]]
    ok("R2 unique best = sigma, 1 transition", len(top) == 1 and top[0][1] == "BCDEFA" and not top[0][2]
       and top[0][0] == 1 and top[0][3] == [("F", 0)], top)
    sp = relabel(PA, SIGMA)
    ok("R2 the differing cell", sp[("F", 0)] == (1, "R", "A") and PA[("A", 0)] == (1, "R", "B")
       and TW[("F", 0)] == (1, "R", "F"), (sp[("F", 0)], TW[("F", 0)]))
    ok("R3 sigma(parent) == Eqv.v TM113.tm", unparse(sp) == TM113, unparse(sp))
    d113 = [i for i, (a, b) in enumerate(zip(TWIN, TM113)) if a != b]
    ok("R4 twin = TM113 with F0 1RA -> 1RF", d113 == [37] and TM113[35:38] == "1RA" and TWIN[35:38] == "1RF", d113)
    nxt = best[1]
    print(f"   1440 candidates (720 relabelings x mirror): exact matches {len(exact)}; best: sigma = "
          f"twin ABCDEF -> parent {top[0][1]}, {top[0][0]} differing transition {top[0][3]} (twin F0 = 1RF,"
          f" sigma(parent) F0 = 1RA, the parent's A0 = 1RB renamed); runner-up {nxt[0]} differences; with the start state kept (pi(A) = A):"
          f" min {start_kept[False]} differences, mirrored min {start_kept[True]}")
    print(f"   sigma(parent) = {unparse(sp)} = Eqv.v TM113.tm; twin differs from it only at F0 (string index 37)")
    print("   => not a renaming/mirror. In parent names the twin is the parent with A0 := 1RA, started in state B")


# ----------------------------------------------------------------------------------------------
def build(blocks):
    ones, pos, ends = [], 0, []
    for bit, cnt in blocks:
        for _ in range(cnt):
            if bit:
                ones.append(pos)
            pos += 1
        ends.append(pos - 1)
    return ones, ends


def pair_run(before, after, hb, ha, steps, label, tw_prefix=None):
    """run twin (from head state F) and parent (from A) on `before`; twin must reach `after` in `steps`;
    returns (good, twin seq, parent seq)"""
    ones_b, ends_b = build(before)
    ones_a, ends_a = build(after)
    t = Tape(TW, ones_b, ends_b[hb], "F").run(steps, trace=True)
    good = (not t.halted and t.state == "F" and t.head == ends_a[ha] and t.ones == set(ones_a))
    p = Tape(PA, ones_b, ends_b[hb], "A")
    psteps = steps - 4 if tw_prefix else steps
    p.run(psteps, trace=True)
    good_p = (not p.halted and p.state == "A" and p.head == ends_a[ha] and p.ones == set(ones_a))
    ok(label + " twin", good)
    ok(label + " parent", good_p)
    if tw_prefix is None:
        ok(label + " same transitions", sig(t.seq) == p.seq)
    else:
        ok(label + " R3 prefix", p.seq[:2] == ["A0", "B0"] and sig(t.seq[:6]) == tw_prefix
           and sig(t.seq[6:]) == p.seq[2:])
    return good and good_p, t.seq, p.seq


def rand_word(rng, maxlen=4, maxv=6):
    out = []
    for _ in range(rng.randint(0, maxlen)):
        out += [(1, rng.randint(1, maxv)), (0, rng.randint(1, 4))]
    return out


def rand_left(rng):
    out = [(0, 3)]
    for _ in range(rng.randint(0, 3)):
        out += [(1, rng.randint(1, 6)), (0, 1)]
    return out


def section_A(rng):
    print("A  TM-level rules on the twin (head state F = parent A)")
    N = 120 if QUICK else 500
    cnt = dict.fromkeys(["R1", "R3'", "R3'l", "R2", "R2e"], 0)
    f0 = dict.fromkeys(["R1", "R2", "R2e", "HALT"], 0)
    for _ in range(N):
        n, m, x, k, j = (rng.randint(0, 25) for _ in range(5))
        L, r = rand_left(rng), rand_word(rng)
        hb = len(L)
        # R1:  l 1^(n+2) <F 0 1^(m+1) 0 0 1^x 0 r  -->  l 1^(n+1) 0 1^(m+1) <F 0 1^(x+1) 0 0 r   (3m+2x+15)
        g, s, _ = pair_run(L + [(1, n + 2), (0, 1), (1, m + 1), (0, 2), (1, x), (0, 1)] + r + [(0, 3)],
                           L + [(1, n + 1), (0, 1), (1, m + 1), (0, 1), (1, x + 1), (0, 2)] + r + [(0, 3)],
                           hb, hb + 2, 3 * m + 2 * x + 15, "A1 R1")
        cnt["R1"] += g
        f0["R1"] += "F0" in s
        # R3': 0^inf <F 0 1^(k+1) 0 0 1^m 0 r  -->  0^inf 1^(k+2) <F 0 1^(m+1) 0 0 r   (3k+2m+15)
        g, _, _ = pair_run([(0, 4), (0, 1), (1, k + 1), (0, 2), (1, m), (0, 1)] + r + [(0, 3)],
                           [(0, 3), (1, k + 2), (0, 1), (1, m + 1), (0, 2)] + r + [(0, 3)],
                           0, 1, 3 * k + 2 * m + 15, "A2 R3'", tw_prefix=["A0", "A0", "A1", "C1", "B1", "B0"])
        cnt["R3'"] += g
        # R3' with an arbitrary left side l 0 (the form of the parent's tR3)
        g, _, _ = pair_run(L + [(0, 1), (0, 1), (1, k + 1), (0, 2), (1, m), (0, 1)] + r + [(0, 3)],
                           L + [(1, k + 2), (0, 1), (1, m + 1), (0, 2)] + r + [(0, 3)],
                           hb, hb, 3 * k + 2 * m + 15, "A2 R3'(l)", tw_prefix=["A0", "A0", "A1", "C1", "B1", "B0"])
        cnt["R3'l"] += g
        # R2:  l 1^(j+1) 0 1^(k+1) 0 1 <F 0 r  -->  l 1^(j+1) <F 0 1^(k+2) 0 0 r   (k+10)
        g, s, _ = pair_run(L + [(1, j + 1), (0, 1), (1, k + 1), (0, 1), (1, 1), (0, 1)] + r + [(0, 3)],
                           L + [(1, j + 1), (0, 1), (1, k + 2), (0, 2)] + r + [(0, 3)],
                           hb + 4, hb, k + 10, "A3 R2")
        cnt["R2"] += g
        f0["R2"] += "F0" in s
        # R2e: 0^inf 1^(k+1) 0 1 <F 0 r  -->  0^inf <F 0 1^(k+2) 0 0 r   (k+10)
        before = [(0, 5), (1, k + 1), (0, 1), (1, 1), (0, 1)] + r + [(0, 3)]
        after = [(0, 4), (0, 1), (1, k + 2), (0, 2)] + r + [(0, 3)]
        g, s, _ = pair_run(before, after, 3, 0, k + 10, "A4 R2e")
        cnt["R2e"] += g
        f0["R2e"] += "F0" in s
    hc = 0
    for _ in range(40):
        r = rand_word(rng)
        ones_b, ends_b = build([(0, 5), (1, 1), (0, 1)] + r + [(0, 3)])
        t = Tape(TW, ones_b, ends_b[1], "F").run(10, trace=True)
        p = Tape(PA, ones_b, ends_b[1], "A").run(10, trace=True)
        hc += ok("A5 HALT", t.halted and t.steps == 3 and t.halt_read == "D0" and sig(t.seq) == p.seq
                 and p.halt_read == "E0")
        f0["HALT"] += "F0" in t.seq
    ok("A6 F0 only in R3'", not any(f0.values()), f0)
    r3, r3l = cnt["R3'"], cnt["R3'l"]
    print(f"   R1 {cnt['R1']}/{N}  R3' {r3}/{N} (+{r3l}/{N} with a random left side l 0)"
          f"  R2 {cnt['R2']}/{N}  R2e {cnt['R2e']}/{N}  HALT {hc}/40 (reads D0 after F1 B0 C0)")
    print("   R1, R2, R2e, HALT: the parent's step counts and, under sigma, the parent's exact transition sequences;"
          " R3': parent's A0 B0 -> twin F0 F0 F1 B1 A1 A0 (sigma: A0 A0 A1 C1 B1 B0), rest identical, 3k+2m+15 steps;"
          f" F0 used by none of R1/R2/R2e/HALT ({f0})")


# ----------------------------------------------------------------------------------------------
def tmstep(L, R):
    """the run model with the twin's TM step counts (R3' = R3 + 4)"""
    rule, st = P.mstep(L, R)
    return rule, st + (4 if rule == "R3" else 0)


def model_edges(L, R, step, limit, stepper):
    L, R = list(L), list(R)
    out = [(step, list(R))] if not L else []
    while True:
        rule, st = stepper(L, R)
        if rule == "HALT" or step + st > limit:
            return out
        step += st
        if not L:
            out.append((step, list(R)))


def to_model(t):
    return P.to_model(t.ones, t.head) if (t.state == "F" and not t.halted) else None


def section_C():
    print("C  initial segment (twin from blank, start state A = parent B)")
    t = Tape(TW, [], 0, "A")
    t.run(8, trace=True)
    ok("C1 first 8 transitions", sig(t.seq) == "B0 C0 D1 D1 D0 E1 F1 F0".split(), t.seq)
    ok("C1 step 8", to_model(t) == ([], [1]), to_model(t))
    marks = [(23, ([2], [1])), (38, ([1, 1], [1])), (48, ([], [2, 2, 1]))]
    for s, want in marks:
        t.run(s - t.steps)
        ok(f"C1 step {s}", to_model(t) == want, (s, to_model(t)))
    seen = []
    t2 = Tape(TW, [], 0, "A")
    for s in range(1, 49):
        t2.run(1)
        if t2.state == "F":
            seen.append(s)
    ok("C1 F entered at", seen == [8, 9, 10, 23, 38, 48], seen)
    print(f"   blank, state A: 8 steps (A0 B0 C1 C1 C0 D1 E1 E0 = parent B0 C0 D1 D1 D0 E1 F1 F0) -> conf([],[1]);"
          f" R3' (15) -> step 23 conf([2],[1]); R1 (15) -> step 38 conf([1,1],[1]); R2e (10) -> step 48"
          f" conf([],[2,2,1]) = conf([],[2,2]+O_0([]))")
    return t


def edge_scan(tm, start, edge, limit):
    with tempfile.TemporaryDirectory() as td:
        exe = os.path.join(td, "edge_scan")
        subprocess.run(["cc", "-O2", "-o", exe, os.path.join(HERE, "scripts", "edge_scan.c")], check=True)
        out = subprocess.run([exe, tm, start, edge, str(limit)], check=True, capture_output=True,
                             text=True).stdout
    hits = []
    for line in out.splitlines():
        f = line.split()
        if f[0] == "HALT":
            hits.append(("HALT", int(f[1])))
            continue
        s, c1, c2, runs = int(f[0]), int(f[1]), int(f[2]), [int(v) for v in f[3:]]
        if c1 == 0 and c2 == 0 and not runs:
            hits.append((s, "blank"))
        elif c1 == 0 and c2 == 1:
            hits.append((s, runs))
        else:
            hits.append((s, ("odd", c1, c2, runs)))
    return hits


SCANS = {}


def section_B(t48):
    print("B  run model == twin TM")
    nmac = 3000 if QUICK else 40000
    t = Tape(TW, set(t48.ones), t48.head, t48.state)
    L, R = [], [2, 2, 1]
    kinds = {}
    good = True
    i = 0
    for i in range(nmac):
        rule, st = tmstep(L, R)
        ok("B1 no-halt", rule != "HALT")
        kinds[rule] = kinds.get(rule, 0) + 1
        t.run(st)
        if to_model(t) != (L, R) or not P.model_ok(L, R):
            ok("B1 model==TM", False, (i, rule, L, R[:8], to_model(t)))
            good = False
            break
    print(f"   B1 {nmac if good else i} macro steps from step 48 identical to the twin TM (TM step"
          f" {48 + t.steps:,}); rules used {kinds}")
    limit = 3 * 10 ** 7 if QUICK else 4 * 10 ** 8
    hits = edge_scan(TWIN, "A", "F", limit)
    SCANS["twin"] = hits
    pred = model_edges([], [1], 8, limit, tmstep)
    ok("B2 edge scan == model", hits == pred,
       next(((i, h, p) for i, (h, p) in enumerate(zip(hits, pred)) if h != p), (len(hits), len(pred))))
    ctrl = model_edges([], [1], 8, limit, P.mstep)      # control: the parent's R3 step count (no +4)
    ok("B2 control (parent step counts) differs", ctrl != hits and [R for _, R in ctrl[:len(hits)]]
       == [R for _, R in hits[:len(ctrl)]])
    edges = [(s, R) for s, R in pred if s >= 48]
    ok("B2 edge form", all(R[:2] == [2, 2] for s, R in edges))
    words = [R[2:] for s, R in edges]
    top = P.top_orbit(len(words) - 1)
    ok("B2 words == O_n([])", words == top)
    print(f"   B2 raw twin to step {limit:,} (scripts/edge_scan.c, edge state F): {len(hits)} left-edge"
          f" configurations = conf([],[1]) (step 8) and conf([],[2,2]+O_n([])) for n = 0..{len(edges) - 1}"
          f" (last at step {edges[-1][0]:,}), each at the model's exact step; nothing else; no halt")
    try:
        sys.path.insert(0, os.path.join(ROOT, "tools"))
        import sim
        m = sim.parse(TWIN)
    except Exception as e:  # pragma: no cover
        print("   B3 skipped (tools/sim.py unavailable):", e)
        return
    checked = 0
    for n, (step, R) in enumerate(edges):
        if n < 6 or n % 8 == 0 or n == len(edges) - 1:
            res = sim.run(m, max_steps=step)
            c = res.final
            tape = c.tape if isinstance(c.tape, (bytes, bytearray)) else bytes(c.tape)
            ones = {c.lo + i for i, b in enumerate(tape) if b}
            lr = P.to_model(ones, c.pos) if (c.state == "F" and not res.halted) else None
            checked += ok("B3 edge==sim.py", lr == ([], R), (n, step))
    print(f"   B3 {checked} of those edge returns re-checked with the tools/sim.py C core")


def section_T():
    print("T  trajectory twin: the same word sequence O_n([]) as TM113 (parent from B) and the parent")
    limit = 3 * 10 ** 7 if QUICK else 4 * 10 ** 8
    tw = SCANS.get("twin") or edge_scan(TWIN, "A", "F", limit)
    t113 = edge_scan(TM113, "A", "F", limit)          # Eqv.v TM113.tm itself (head state F, as the twin)
    pB = edge_scan(PARENT, "B", "A", limit)           # parent started in state B
    par = edge_scan(PARENT, "A", "A", limit)          # the parent (kill #12)
    ok("T1 TM113 == parent from B", t113 == pB)
    twe = [(s, R) for s, R in tw if s >= 48]
    t3e = [(s, R) for s, R in t113 if s >= 44]
    n = min(len(twe), len(t3e))
    ok("T2 same words", [R for _, R in twe[:n]] == [R for _, R in t3e[:n]])
    ok("T2 offset 4(n+1)", all(twe[i][0] - t3e[i][0] == 4 * (i + 1) for i in range(n)),
       [(twe[i][0] - t3e[i][0]) for i in range(min(n, 5))])
    pe = [(s, R) for s, R in par if isinstance(R, list) and s >= 50]
    k = min(len(twe), len(pe))
    ok("T3 parent words", [R[2:] for _, R in pe[:k]] == [R[2:] for _, R in twe[:k]]
       and all(R[:2] == [3, 2] for _, R in pe))
    print(f"   to step {limit:,}: TM113 scan == parent-from-B scan ({len(t113)} edge configurations);"
          f" twin and TM113 pass the same {n} words [2,2]+O_n([]), the twin 4(n+1) steps later at return n"
          f" (one R3' per top epoch + one in the init); the parent passes [3,2]+O_n([]) for n = 0..{len(pe) - 1}")
    if QUICK:
        return
    try:
        sys.path.insert(0, os.path.join(ROOT, "tools"))
        import sim
    except Exception as e:  # pragma: no cover
        print("   T4 skipped (tools/sim.py unavailable):", e)
        return
    span = {}
    for name, tm in (("twin", TWIN), ("parent", PARENT), ("TM113", TM113)):
        r = sim.run(sim.parse(tm), max_steps=10 ** 9, final=False)
        ok("T4 no halt at 1e9", not r.halted, name)
        span[name] = (r.hi - r.lo + 1, r.nonzeros)
    print(f"   T4 at step 10^9 (tools/sim.py C core): cells visited / nonzeros  twin {span['twin']},"
          f" parent {span['parent']}, TM113 {span['TM113']}  (the observer's 133/134)")


# ----------------------------------------------------------------------------------------------
def section_H(rng):
    print("H  budget-2 edge lemma (run model)")
    n2 = 0
    pool = P.top_orbit(24 if QUICK else 30) + [P.orbit(P.rand_marker(rng, 3), rng.randint(0, 9))
                                                for _ in range(300)]
    for _ in range(300):
        W = [rng.randint(1, 6)]
        for _ in range(rng.randint(0, 4)):
            W += [rng.randint(1, 5), rng.randint(1, 6)]
        pool.append(W)
    c3 = 0
    for W in pool:
        e = P.Ep(W, count=True)
        if e is None:
            continue
        c, W2, k = e
        L, R = [], [2, 2] + W
        if c > 2:
            # cost 3: the budget-2 run must halt (its bottom frame would have to pay with value 1)
            halted = False
            for _ in range(k):
                rule, _ = P.mstep(L, R)
                if rule == "HALT":
                    halted = True
                    break
            c3 += ok("H edge2 cost3 halts", halted, W)
            continue
        inner_ok = True
        for i in range(k):
            rule, _ = P.mstep(L, R)
            if rule == "HALT" or (i < k - 1 and not L):
                inner_ok = False
                break
        n2 += ok("H edge2", inner_ok and (L, R) == ([], [4 - c, 2] + W2), (W, c))
    print(f"   {n2} cases with cost <= 2 (top orbit, marker orbits, arbitrary words): same macro steps, L != []"
          f" in between, ends at conf([],[4-c,2]+W'); {c3} cost-3 words: the budget-2 run halts (zero slack)")


def section_G():
    print("G  the twin's undefined transition D0 (= parent E0)")
    n = 2 * 10 ** 5 if QUICK else 2 * 10 ** 6
    ones, h, q = set(), 0, "A"
    d_reads = 0
    prev = None
    for _ in range(n):
        s = 1 if h in ones else 0
        if q == "D":
            d_reads += 1
            ok("G D reads 1", s == 1)
            ok("G D entered from C0", prev == "C0", prev)
        t = TW[(q, s)]
        if t is None:
            ok("G no halt", False)
            break
        prev = q + str(s)
        w, d, q2 = t
        (ones.add(h) if w else ones.discard(h))
        h += 1 if d == "R" else -1
        q = q2
    print(f"   {n:,} steps from blank: D entered {d_reads:,} times, always from C0 and reading 1 (D1 = 0LE);"
          " no halt. D reads 0 only in the HALT pattern 0^inf 1 <F 0 (A5)")


if __name__ == "__main__":
    rng = random.Random(SEED)
    t0 = time.time()
    section_R()
    section_A(rng)
    t48 = section_C()
    section_B(t48)
    section_T()
    section_H(rng)
    P.section_F()
    section_G()
    if MODEL:
        print("M  parent model-level sections (TM-independent), re-run")
        P.section_D(rng)
        P.section_E(rng)
        P.section_E2(rng)
    allfail = FAIL + P.FAIL
    print(f"\n{'ALL CHECKS PASSED' if not allfail else 'FAILURES: ' + str(len(allfail))}  (seed {SEED},"
          f" {'quick' if QUICK else 'full'}{', +model' if MODEL else ''}, {time.time() - t0:.0f}s)")
    sys.exit(1 if allfail else 0)