# check_proof.py full run, 2026-10-12 (skeptic round 2 applied): sections A-L
A1 TM5 (FractalType4.v) = #16 under A..F -> B,C,D,E,A,F    PASS  
A2 one undefined transition, D1                            PASS  [(3, 1)]
A3 halting needs B> 0 0 1 (D entered by C0/F0 only)        PASS  D entered by [('C', 0), ('F', 0)]; every 2-step history before D1 is [(('B', 0), ('C', 0))] (16 windows)
B1 shift rules (6 rules, single block + n-fold)            PASS  6 rules []
B2 right turn  x B> 010 010 -->(5) x <A 101010             PASS  
C1 P(a) holds exactly for a in S = {0,3,8,19,40,83,...}, a<=130 PASS  [0, 3, 8, 19, 40, 83]
C2 P(S) for S in levels <= 1400, 4 left contexts (l never read) PASS  
C3 TM5 Inc1 / Incs1 renamed (box 4x3x3x4 + random n)       PASS  204 instances
C4 start gadget after P(S): 9 steps to the fresh bouncer   PASS  49 instances
D1 BounceE: next frame, steps 10+20B+6A                    PASS  5860 instances []
D2 BounceP: next frame, steps 22+20B+6A'                   PASS  11620 instances []
E1 macro rules sound on the small box (K=3 events)         PASS  {'unruled': 79669, 'ok': 61931} (15 s) []
    event counts in E1: {'Push1': 35060, 'EatChunkE': 27468, 'Absorb0': 26116, 'RightEndE': 20196, 'BounceP31': 19486, 'HubLevel': 13300, 'Absorb': 12172, 'ToEdge1': 11828, 'AbsorbToEdge': 11673, 'PModeWTop': 10524, 'ToEdge2': 8206, 'HubTop': 6792, 'HubClean': 6160, 'RightEndP': 5737, 'PModeWLevel': 3357, 'EatToEdge2': 2971, 'Absorb0ToEdge': 2412, 'EatToEdge1': 2404, 'PModeWClean': 2338, 'PModeTop': 2191, 'Push1End': 2160, 'RightEndP2': 1940, 'EatToEdge4': 1847, 'Push1Edge': 1662, 'RightEndP1': 1626, 'PModeLevel': 1443, 'PModeP1Level': 1107, 'EatToEdge3': 870, 'PModeP1Top': 844, 'PModeClean': 597, 'HubTopK1': 578, 'EatLastE': 498, 'EatToEdge5Exact': 261, 'EatToEdge2Exact': 260, 'PModeP1Clean': 244, 'EatToEdge5': 120, 'Reflect': 84, 'HubSegless': 9}
E2 macro rules sound on random frames (values <= 60)       PASS  {'unruled': 185, 'ok': 715} (3 s) []
    event counts in E2: {'BounceP31': 433, 'Push1': 284, 'HubClean': 255, 'RightEndE': 195, 'EatChunkE': 193, 'Absorb': 177, 'ToEdge2': 125, 'PModeClean': 116, 'ToEdge1': 88, 'EatChunkP': 82, 'EatLastP': 79, 'RightEndP': 76, 'AbsorbToEdge': 66, 'PModeWClean': 52, 'PModeLevel': 35, 'V1RightEnd': 34, 'Absorb0': 28, 'Absorb0ToEdge': 27, 'Push1End': 27, 'HubTopK1': 26, 'PModeWTop': 21, 'PModeTop': 21, 'EatToEdge4': 18, 'EatToEdge3': 17, 'EatToEdge2': 16, 'HubLevel': 15, 'EatToEdge5': 13, 'Push1Edge': 13, 'PModeP1Clean': 10, 'HubTop': 5, 'RightEndP2': 3, 'Reflect': 3, 'PModeWLevel': 2, 'PModeP1Level': 2, 'RightEndP1': 1}
E3 negative controls (target ak+1) not reached             PASS  0/60 reached
F1 blank -> base hub [85,7,46] at step 46,734              PASS  ('ok', [46734])
F2 macro orbit from the base hub = exact run, in order     PASS  104 of 120 macro frames met in order within 60000000 steps (cap)
G1 H*c4 at every right end from blank (2001)               PASS  (6 s) []
G2 rnd_R long orbits (narrow generator), 20 trav., S<=5459 PASS  600 orbits, 12000 right ends, leaks {} (2 s)
G2 rnd_R long orbits (narrow generator), 20 trav., S<=1e+30 PASS  600 orbits, 12000 right ends, leaks {} (5 s)
G3 rnd_short seeds in H*c4 (narrow generator), S<=5459     PASS  600 seeds {'El1': 60, 'Et1': 37, 'Ec1': 127, 'Pc1': 124, 'Pt1': 94, 'Eseg': 55, 'Pet0': 18, 'Et0': 75, 'Pec1': 10}, leaks {} (2 s)
G3 rnd_short seeds in H*c4 (narrow generator), S<=1e+30    PASS  600 seeds {'El1': 58, 'Eseg': 76, 'Et0': 64, 'Pc1': 110, 'Et1': 47, 'Ec1': 110, 'Pt1': 130, 'Pet0': 3, 'Pec1': 2}, leaks {} (5 s)
H1 shift-reflection swaps the two zipper families          PASS  51250 cases
H2 growth transitions on random orbits: B'(k) = 2tau - B(k-1), head h = 5 + B(1) - e PASS  352 growth transitions, 0 with e not in {0,1}
I1 eat of an odd (10)-run in a chunk halts (precursor)     PASS  30/30 halt
J1 skeptic counterexamples: in H*c3, rejected by H*c4      PASS  H2t':ok HL:ok HL:ok CP:ok CP:ok CP:ok
J2 Hc4 is total (no exception) on a box of short right ends PASS  8448 right ends, 0 exceptions (Hc3 raised TypeError on 12 of them)
J2b Hc4 total on fuzzed tuples incl. degenerate ones       PASS  {'rejected': 38925, 'degenerate': 17039, 'member': 4036}, 0 exceptions []
CP on blank (1,500) + 300 rnd_R orbits x 40, S <= 5459: {'long P-mode right ends': 1599, 'CP holds': 1599}
J3 CP: every long P-mode right end on orbits has P = 2B(3)-2tau+3 PASS  1599/1599 (blank 1,500 right ends + rnd_R orbits x 40)
K1 long E hubs, S<=40, <=8 pairs: next right end in H*c4   PASS  22877 members of 114047 candidates, next in H*c4 22877, leaks 0 {} (2 s)
K2 long P-mode right ends (P from CP), S<=40: next in H*c4 PASS  15707 members of 66573 candidates, next in H*c4 15707 (all next short: 15707), leaks 0 {} (5 s)
K3 long E hubs, S=83, <=8 pairs: next right end in H*c4    PASS  181934 members, next in H*c4 181934, leaks 0 (18 s)
K6 long P-mode right ends (CP), S=83: next in H*c4         OPEN  128043 members, next in H*c4 128042, leaks 1 {'next not in H*c4: H2 window': 1} (41 s) -- the leak is P=31 [1,35,36,34,52,30,56,29,110,82,164] -> window hub [1485,15,335]
K4 short E hubs [a0<=80,b1<=20,ak<=40] in H*c4: next in H*c4 OPEN  21325 members, 3 leak {'LOOKK step 4': 3}: [[79, 12, 32], [77, 12, 34], [75, 12, 36]] -- Hs_4 is a look-ahead and not inductive (6 s)
K5 [79,12,32]: short chain reaches a P-mode right end with walls OPEN  right ends E P49 E P13 E P193 E E P17W E; walls at index [8]; outside H*c4 at [1, 2, 3, 4, 5, 6, 7, 8]
L1 window right end: Clean start F_P(V, ak-S, [1,1,0], S-1) PASS  60 window right ends (S<=83, delta counts {0: 24, 1: 24, 2: 12}), 0 misses [] (0 s)
L2 WindowStart + existing rules: exact (3 events) wherever ruled PASS  {'delta 0 ruled': 59, 'exact ok': 59, 'delta 1 unruled': 60, 'delta 2 unruled': 30, 'delta 0 unruled': 1}, 0 exact misses [] (0 s)
L2b WindowStart: the unruled cases (RightEndP P<=3 at a wall, V1 right end with walls) OPEN  {'delta 1: RightEndP P<4 (P=2, walls)': 30, 'delta 2: RightEndP P<4 (P=3, walls)': 30, 'delta 1: V1 right end with walls': 30, 'delta 0: V1 right end with walls': 1} -- delta in {1,2} always, delta = 0 when a Push1End is followed by a V1 right end at the next wall, e.g. [25,6,28,13,79] (proof.md 4.4, 8 G2)
L3 delta=1 window hub [21,3,38]: left word (101)^q 1 (101)^r appears OPEN  ('glued wall', 3010) -- a tape form outside the grammar of proof.md section 2
L4 long P box S=168 (<=6 pairs, CP): next in H*c4          OPEN  1079332 members, next in H*c4 1079272, leaks 60 {'next not in H*c4: H2 window': 60} (372 s) -- the window family (lower bound)
L5 long E box S=168 (<=8 pairs): next right end in H*c4 (one step) PASS  1516903 members, next in H*c4 1516903, leaks 0 (188 s)
L5b two-step window leak from a long E member at S=168     OPEN  [201,36,136,52,120,56,116,57,226,138,275] -> P59 [1, 71, 72, 68, 104, 60, 112, 58, 114, 113, 276, 54, 167] -> [2995, 29, 677]
L6 short box Et1: next in H*c4                             PASS  143766 members of 431430, next in H*c4 143766, leaks 0 {} (25 s)
L6 short box Eseg: next in H*c4                            PASS  2937 members of 2999, next in H*c4 2937, leaks 0 {} (1 s)
L6 short box P1w: next in H*c4                             OPEN  108831 members of 1071560, next in H*c4 108819, leaks 12 {'LOOKK step 4: H2 window': 4, 'LOOKK unruled: reflect not clean': 8} (38 s) e.g. [((False, [], 240, [1, 34, 8]), (True, [], 0, [249, 35, 7]))]
L6 short box E1w: next in H*c4                             OPEN  445843 members of 1427560, next in H*c4 445733, leaks 110 {'LOOKK step 4: H2 window': 10, 'LOOKK unruled: reflect not clean': 20, 'LOOKK step 4: SB short P-odd end: E outcome out of band': 80} (165 s) e.g. [((True, [], 0, [253, 35, 3]), (False, [], 250, [1, 37, 2]))]
L6 short box Pt1: next in H*c4                             OPEN  1202119 members of 1460272, next in H*c4 1201669, leaks 450 {'LOOKK step 4: H1 P even': 450} (326 s) e.g. [((False, [], 89, [1, 40, 40, 1, 39]), (True, [], 0, [157, 44, 102]))]
L7 [255,35,3] (in H*c4) reaches an unruled event           OPEN  P252 [1, 37, 2] -> P171 [1, 40, 77] -> E [67, 85, 101] -> P2 [1, 127, 82] -> UNRULED reflect not clean
SUMMARY PASS (36 checks, 0 fail; 11 OPEN items = known gaps, proof.md section 8) 1239 s
open: ['K6 long P-mode right ends (CP), S=83: next in H*c4', 'K4 short E hubs [a0<=80,b1<=20,ak<=40] in H*c4: next in H*c4', 'K5 [79,12,32]: short chain reaches a P-mode right end with walls', 'L2b WindowStart: the unruled cases (RightEndP P<=3 at a wall, V1 right end with walls)', 'L3 delta=1 window hub [21,3,38]: left word (101)^q 1 (101)^r appears', 'L4 long P box S=168 (<=6 pairs, CP): next in H*c4', 'L5b two-step window leak from a long E member at S=168', 'L6 short box P1w: next in H*c4', 'L6 short box E1w: next in H*c4', 'L6 short box Pt1: next in H*c4', 'L7 [255,35,3] (in H*c4) reaches an unruled event']
EXIT 0

# section M (added after the full run above had started), run separately: check_proof.py full M
M1 RightEndP P=2 at a wall = RightEndP to P=0 + Absorb0 (exact, 2 events) PASS  {'unruled': 49, 'ok': 251}, 0 misses [] (0 s)
M2 negative control (ak + 2 instead of ak + 1) never reached PASS  0/32 reached
M3 window hubs with WindowStart + RightEndP2W: what is still unruled OPEN  {'delta 0 V1 right end with walls': 1, 'delta 0 ruled': 59, 'delta 1 V1 right end with walls': 30, 'delta 1 ruled': 30, 'delta 2 RightEndP P<4 (P=3, walls)': 30} -- the V1 right end with walls remains (proof.md 8 G2)
SUMMARY PASS (2 checks, 0 fail; 1 OPEN items = known gaps, proof.md section 8) 14 s
open: ['M3 window hubs with WindowStart + RightEndP2W: what is still unruled']