1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA

Deepen pass (overnight 2026-10-10)

Result: confidence stays med (better understood, not closed). Not a cryptid. Status CHECKPOINT_A, stage deepen.

The three phases are one bouncer. Look at the tape when the head turns at the left, i.e. A reads 0 after a left move with cell p-2 = 0 (the "left-turn frame"): - P-mode: 0^inf X (10)^P <A Y (010)^d Z 0^inf - edge mode: 0^inf <A Y (010)^d Z 0^inf - Y = (10)^a0 (011010)^b1 (10)^a1 ... (011010)^bk (10)^ak, with a0 = 1 in P-mode - X = walls, alternating (10)^p (101)^q; Z = pending chunks (more Y-type stuff followed by its own (010)-run)

Each round trip takes (10)^2 off P, or in edge mode extends the left edge (a0 += 2). It also eats one (010) at the right end, and adds (10)^2 to ak plus (011010) to b1 (P-mode only). - Right phase: every Transfer is this bouncer, with P = the (01)-run and d = the (011)^T run, restarted at the right end when d runs out. That restart is the nested Conv. - Middle phase (the old open gap): the same P-mode bouncer after P runs out at a wall (101)^q. At P=3 the wall becomes the new d-run and the old (Y, d) is pushed into Z ("Push"). At P=2 the wall is absorbed into Y ("Absorb"). The bouncer then continues on the next (10)^p. With q odd and P=2, the wall and the (10)^p behind it are absorbed together. - Left phase: once P reaches 0^inf ("ToEdge"), edge mode eats the remaining d-runs and Z chunks until d = 0 and Z is empty (the hub), then Sweep.

New rules, validated by exact simulation (scripts/vrules.py reach: target tape and head offset at a left-turn frame, plus step count):

• Contexts in the sims: X = 0-2 random wall pairs; Z empty, one or two L-chunks, or an R-parsed chunk; Y with 1-3 segments; values 1..6 and up to 300.
• Step formulas: bounce formulas exact on 60 fitted + 280 checked instances; eat formulas exact on 40 fitted each.
• Negative controls die: BounceP with ak+1 0/6, EatE6 with ak+2 0/6, BounceE steps+2 0/6 (scripts/val_neg_deepen.py).
• Eat-through is a new regime, first seen at 5.6e5 steps. When the d-run ends on the odd alignment (d = 1 next to a chunk), the bouncer does not merge the chunk into Y. It eats through it: one (011010) or two (10) per 2 trips, then the chunk's own (010)-run with one extra unit. When the d-run ends on the even alignment (d = 0 next to a chunk), the chunk simply becomes part of Y. That is not an event: the next parse just sees a longer Y.

Coverage check (accelerated simulator, scripts/accel_sim.py). Direct simulation, except that BounceP/E, Eat* and Transfer are applied in bulk with their exact step counts. Everything else (Push, Absorb, ToEdge, chunk-boundary steps, right-end restarts, Sweep, the init phase) is simulated directly. - It equals the C engine exactly (tape, head offset, state, step) at 1.0e5, 1.0e6, 1.45e7, 5.3e7, 2.1e8 and 1.05e9 (scripts/cmp_accel_vs_c.py). The 1e10/3e10 check is in deepen.json evidence if it finished. - It ran to 1.02e12 steps (span 1.4M cells) with no halt (scripts/far_accel.py). Only about 200 bulk bounce/eat applications and 2.4e5 Transfers were needed. So every phase up to that horizon is bounces + eats + Transfers + events that each take at most about 2 round trips. - Event census from steps 46,734 to 1.1e9 (scripts/events_log.py + events_classify.py), with examples: - Push P=3 at an even wall: 206,227 [10^68 101^52] P=3 Y=[1,23,44] d=52 -> P=65 Y=[1,2,2] d=50 Z=(011010)^24 (10)^48 (010)^48. - Push P=3 at an odd wall: 536,736 [10^29 101^71] P=3 Y=[1,17,32] d=36 -> P=26 d=69 Z=(011010)^18 (10)^36 (010)^31 + old Z. - Absorb P=2: 51,601 [10^84 101^14] P=2 Y=[1,3,4] d=35 -> P=84 Y=[1,11,6] d=33. - ToEdge P=1: 75,609 P=1 Y=[1,24,46] d=50 -> E Y=[5,24,48] d=48. - ToEdge P=2: 542,125 -> E Y=[1,15,28] d=43. - Also: eat-through entry/exit at chunk boundaries, right-end restarts (nested Conv), and the hub Sweep. - The first 46,734 steps (up to hub 0^inf <A (10)^85 (011010)^7 (10)^46 0^inf) are irregular, which is fine for a direct-computation init.

Still open (why not high): closed-form rules for the event types listed above, each with its parity cases: - Push: P=3, wall q even or odd, and which alignment the pushed chunk ends up in. - Absorb: P=2, wall q even or odd (q odd also absorbs the next (10)^p). - ToEdge: P=1 or 2. - Eat-through entry and exit at chunk boundaries. - The P-mode right-end restart. - Sweep for k segments.

Also still open: a closure proof that the grammar (X walls, Y, d, Z chunks at even/odd alignment) maps into itself for all values, including tiny ones (q<=3, b=1, a=1, chunk sizes 1). Today these events are only simulated, not ruled.

Non-halting argument (sketch, not yet checked): every update is additive, with each segment changing by O(1) per trip. Every branch is a local parity or alignment case (P mod 2, d mod 2, q mod 2, chunk alignment). So if the finite local event set is closed on the grammar, the machine cannot halt whatever the segment sizes do. Halting would need a local configuration outside the grammar, not arithmetic luck. That makes it a "chaotic but closed" fractal, not a cryptid (ground rule 6 does not apply). - Suggested proof architecture: the FractalType7v4 style. Prove BounceP/BounceE/Eat* by ind over the trip count, the events by es and chains, Transfer/Conv as already planned, and use an inductive Good predicate on the segment grammar. - The next observation step is the event catalogue: enumerate the small local cases by brute force from random grammar instances (scripts/events_log.py on random hubs) and fit each one.

Deepen pass 2

Result: confidence stays med. Recommend more observation, aimed at a parity invariant. Not flagged as a cryptid yet, but see the last bullet. Status CHECKPOINT_A, stage deepen2.

Main finding: the grammar with free exponents is not closed. I ran a random-instance stress test (scripts/stress_grammar.py). It builds left-turn frames X (10)^P <A Y (010)^d Z with tiny or random exponents, 0-4 walls, 1-4 Y segments and 0-3 Z chunks, and runs each on the accelerated simulator for 3e7 steps. - Results: 40/150 instances halt with L-aligned chunks only (seed 31), 55/150 with mixed chunk alignments (seed 32). Outputs are in scripts/stress_grammar_*.txt. - Minimal witness: 0^inf (10)^3 (101)^1 (10)^3 <A (10) (011010)^1 (10)^1 (010)^12 0^inf halts at step 1,277. - Factor test on (10)^p (101)^q (10)^P <A (10)(011010)^b (10)^a (010)^d: across 12 probes, it halts exactly when P is odd (a Push), q is odd and a is odd. With q even, a even or P even it runs on. - From blank, every Push at an odd wall has an even ak (for example 536,736: q=71, ak=32).

So round 1's sketch ("only local parity cases, so cannot halt") is wrong as stated. Non-halting needs parity invariants carried through every event. The open question is now whether those parities are forced locally (then a regular invariant exists) or depend on accumulated sums (then this is cryptid-like).

New closed-form rules (scripts/val_events2.py; exact target frame by simulation, vrules.reach):

• Negative controls die: AbsorbChain stopping at the first wall 0/16, Push with ak+2 0/16.
• AbsorbChain is a binary-carry propagation across the walls. Even walls pass the carry on and an odd wall stops it, except for the first wall, which enters with carry 2.

Event census to 1.2e10 steps (accel sim, 25,136 frames): only about 200 non-bulk transitions in total. They split into two groups: - Left-exhaustion: Push (q even or odd), Absorb, ToEdge P=1 and P=2. - Right-exhaustion: d=0 or d=1 at chunk boundaries, right-end restarts, and the hub/Sweep.

Still not in closed form: - Push with p=2 (a double Push). - Absorb with p_J=1 (P=1 next to a wall is not a left-turn frame). - Push with d<4. - The right-exhaustion events, the P-mode restart, and Sweep for k segments.

Regular-CTL search (native, busycoq CTL.v MITM semantics, lazy DFA): negative. - n-gram (+ seen-1 flag): n<=13 reaches an abstract HALT; n>=14 exceeds 2e7 abstract configs. - busycoq-style RWL_mod over blocks (bsz 1/2/3/6, mnc 1-6, mod 2-6, len1 3-10, len2 1-3; 20 settings): all reach HALT. - An alignment-free run-compressing DFA (4-12 runs): reaches HALT. - The stress-test result explains this: any value-free over-approximation contains halting configurations, so a CTL must track token parities. Scripts: scripts/ctl_*.py. - Following the rocq-notes lesson, nothing was run inside Coq.

Next step: 1. Log the parities of (P, q, ak, d, a_i, b_i, chunk exponents) at every event from blank to 1e10, to find the invariant, for example "ak is even at every P-exhaustion". 2. Check that each closed-form event preserves it. Push adds 4 to ak and AbsorbChain adds 2, so those two keep the parity of ak. The parity also has to survive chunk merges and eat-through. 3. If the invariant is a finite set of local parities, build a grammar-aware DFA pair that tracks them and run the MITM check (then a MITMDFA certificate is possible). 4. If it needs the parity of a sum over all segments, flag it as cryptid-like.

Decision (2026-10-10)

Question: Fund one targeted deepen stage on #16's parity invariant (a parity census at every event, then a parity-aware DFA search) before any proof work? Answer: parity_round (One targeted stage: find the parity invariant). Dennis: go with all recommendations (2026-10-10).

Funded stage (2026-10-10, parity_round)

Result: confidence stays med. Not flagged cryptid (reason below). The parity question now has a sharp answer, but the invariant that keeps the machine safe is not purely local: it also carries magnitude facts. That rules out the generic DFA route and points to an inductive Good predicate. Status CHECKPOINT_A, stage parity_round.

1. One halting mechanism, and it is local. - Eat-through (d = 1 next to a chunk) of a chunk that has an odd (10)-run halts. All (10)-runs even never halts. Random instances in both modes, 2e7 steps each: 40/40 halt vs 0/40 (scripts/eat_odd_test.py seed 61). Exact direct simulation: 19/20 halt; the one survivor has its odd run as the last run before 0^inf (scripts/val_eatchunk.py seed 71). - All 95 halts of round 2's random grammar instances are of this kind: 40/40 (seed 31) and 55/55 (seed 32). In each one, the last 12 left-turn frames include a d = 1 frame next to a chunk with an odd (10)-run (scripts/halt_classify.py). Round 2's factor test (Push at an odd wall with odd ak) is one case of this: the Push turns ak+4 into a chunk run, and the odd wall makes it get eaten.

2. New closed forms, each from random instances by exact simulation (vrules.reach):

• Here C = (011010)^B1 (10)^A1 ... (011010)^Bm (10)^Am (010)^c with every A_i even, B = ΣB_i and A = ΣA_i. S = max{S_j <= ak-1} on the staircase S_0 = 0, S_(j+1) = 2S_j + 3 (S_j even) or 2S_j + 2 (S_j odd): 0, 3, 8, 19, 40, 83, 168, ... This is round 1's Jacobsthal sequence.
• The right-phase rules are checked at the first P-exhaustion frame predicted from the start frame. The start frame alone is not a valid target: every staircase level passes through a frame of the same shape, and a wrong-level control matched the start frame 10/10 (val_hubsweep_91_startframe_criterion_INVALID.json).
• Negative controls die: EatChunk with ak+B+1 0/10, EatChunk with d = c 0/10, HubClean one level too low 0/10 twice, HubTop read as HubClean 0/10.
• Validation used ak - S >= 2 (P0 >= 2). When the start has P0 >= d0, the bouncer reaches the right end again and the rules apply a second time.
• Check against blank: 34 of the 35 right ends to 1.02e12 match the predicted clean/top start frame exactly. The 35th (P430 at step 1,477,184) starts at P0 = 427 >= d0 = 368, comes back to the right end at P = 59 with Y = (1,185,368), and that second right end is clean. It matches: wall (57,371), P0 = 29, d0 = 338.
• Still not in closed form: the window values ak in [2S-1, S_next-2] (where P and d run out together), Push with d < 4 or p = 2, and AbsorbChain with p_J = 1. None of these occurs from blank (item 3).

3. Parity census from blank to 1.02e12 steps (scripts/parity_census.py, parity_census_report.py, output parity_census_1e12.txt). 804 left-turn frames; 488 regular frames after the 46,734-step init; 0 exceptions to each of the following: - G1: every (10)-run of Z, and every inner (10)-run of Y, is even. - G2: a0 is odd in edge mode (147 frames). - G3: every wall has p = q mod 2 (207 walls). There is at most one odd wall, and when there is one, P is odd. Seen orders, nearest first: e, ee, eo, eeo, o. - G4, the eat cascade: start with (e, s) = (ak, d) mod 2 and go through the chunks. A merge (s = 0) needs e = 0. An eat sets e += B and s = c+1. - G5: ak is even in every P-mode frame with walls. That includes all 43 Pushes and all 4 Absorbs (none at an odd wall). - 454 frames satisfy G1-G5. The other 34 are mid-chunk eat frames that the predicate does not parse; they are inside EatChunk. - Facts that hold from blank but are not parity facts: - every Push has d >= 4 (43/43); - no P-mode right end has walls present (11/11); - every right end is clean or top (E-mode 16 + 8, P-mode 3 + 8, 0 other). All 16 top cases have ak = S_next - 1 exactly.

4. Do magnitudes matter? No. Parities decide. Reachable frames are rebuilt exactly (identity check: the next 5 frames match exactly, 40/40) and then perturbed (scripts/perturb_test.py, flip_fields.py): - m2, i.e. about half the exponents shifted by an even amount in [-6, 6]: 0/80 halt (2e9 steps each). - r2, i.e. half the exponents redrawn at random size with the same parity (this crosses staircase levels and event orders): 0/80 halt. - r2all (every exponent redrawn): 0/80 halt. - r2 from later frames (3e8-1e10, 2e10 steps): 0/24 halt. - In total: 0 halts in 264 same-parity runs. - odd1, one random exponent +1: 2/40 halt (both were Z (10)-runs). - Single flips by field (16 frames, 165 flips, 1e9 steps): 7 halt. Five were Z (10)-runs on the eat path. The other two were the q and ak of one Push frame (517,706). Flips of P, d, b_i, inner a_i, walls p, Z (011010)/(010), and P/d splits (20) halt 0 times.

5. Is G1-G5 closed? No (scripts/good_closure.py, good_diag.py). - 120 random G1-G5 frames, 3e7 steps each: 2 halt. Compare 40/150 and 55/150 for unconstrained grammar instances. - 73 of the 120 leave G1-G5 later: G5 44 times, G3 26, G2 2, G1 1. - The leaks come from the non-parity facts of item 3: - a P-mode bouncer with walls that reaches the right end before the wall (RightEndP makes ak odd; the restart then adds walls, giving a second odd wall or p != q); - a P-mode right end with P even that is not the top k=1 case (gives a wall with p != q); - a Push with d < 4. - Negative controls: one odd Z (10)-run, 15/30 halt. Breaking G2 or G3 alone, 0/30 halt in 3e7 steps. So these two are what the dynamics keep, not what safety needs. - What would close it: linear inequalities, i.e. the P-mode bouncer reaches its wall first, which is round 1's underflow condition P < d after a staircase. Also exact staircase relations: ak + d stays constant through BounceP (+2/-2), AbsorbChain (+2/-2) and RightEnd (+1/-1). A Push moves the pair (ak+4, d-4) into a chunk, and a later merge brings it back. So a P-mode bouncer started at (P0, S-1) that has no eat-through on the way arrives at the right end with ak = S-1 = S'_next - 1, which is exactly the top case (example: start (6, 39) at 51,527 -> AbsorbChain -> right end P50 Y=(1,28,39)). These are identities, not pseudo-random arithmetic.

6. Parity-aware DFA (MITM) search: negative (scripts/ctl_parity_rl.py, output ctl_parity_rl.txt; native, CTL.v semantics, nothing run in Coq). - The family is round 2's alignment-free run-compressing parser, with no truncation (K = 48 runs) and counts exact below mnc and mod 2 above. - mnc 3, 4, 5 reach an abstract HALT after 1.1e5-2.1e5 abstract configs. With mod 4 it caps at 3e6. - The HALT witnesses are configurations with many odd walls and more than 40 runs. No real frame looks like that. - This is the item 5 picture: a finite-state abstraction cannot keep the inequality (P < d) or the exact staircase relation (ak = S_next - 1), and without them it allows unsafe walls. So a CTL certificate is unlikely for this machine. The proof should be an inductive Good predicate (FractalType7v4 style).

Exit condition. - The funded exits were: a local, preserved invariant -> proof.md; the parity of a sum over segments -> flag cryptid-like. - Neither fits cleanly. G4 does use a mod-2 running sum (ak + ΣB over eaten chunks), but that is finite-state, and item 4 shows halting does not depend on magnitudes. The cryptid protocol (pseudo-random arithmetic decides halting) therefore does not apply. - What blocks proof.md is not parity. Closure needs the inequality and the exact staircase relations of item 5. - Since this departs from the literal stop rule, it is a new decision for Dennis (decision.json).

Still open: 1. A closed macro-level Good predicate: G1-G5 plus (a) the underflow inequality for P-mode bouncers with walls, (b) d >= 4 at Push, (c) the right-end kinds via the exact ak + d relation. Check it with good_closure.py (it reports the first frame that leaves the predicate) until it is closed. 2. Closed forms for the window values other than top, Push with d < 4 or p = 2, and AbsorbChain p_J = 1. They are needed only if the predicate cannot exclude them. 3. The init (46,734 steps, direct) and the hub at 46,734 as the base case.

Decision (2026-10-10, auto-applied)

Question: Fund one stage to close #16's macro-level invariant (the parity rules plus the underflow inequality and the exact staircase relation), checked on random instances, before proof.md? Answer: macro_closure (One stage: close the macro-level invariant). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was at lunch). Override any time.

Funded stage (2026-10-10, macro_closure)

Result: not closed; confidence stays med; not a cryptid. Status CHECKPOINT_A, stage macro_closure. - The decided predicate (G1-G5 plus the three magnitude facts) is not closed. - Even a 4-cycle lookahead version leaks slightly. The leaks are rare late underflow failures and small-value corner events, and the real machine passes all of them without halting. - The missing facts are linear relations between neighbouring walls and the staircase level, plus rules for the corner events. Neither is written down yet.

What was done: 1. Built a counter-level macro simulator (scripts/macro_sim.py) that applies only validated rules, so closure can be tested over many cycles at once. 2. Found and validated four new rules. 3. Ran the macro simulator from blank far past the C horizon. 4. Ran the decided closure test: G1-G5 plus underflow, Push d >= 4 and staircase, on random instances on the accelerated simulator. 5. Ran hub-level tests to find what the closure really needs.

1. Macro simulator. The state is a left-turn frame: mode, walls X, P, Y, d and chunks Z. The simulator applies BounceP/E, merge, EatChunkP/E, RightEndP/E, Push, AbsorbChain, ToEdge1/2, HubClean, HubTop, PModeClean and PModeTop, plus the new rules below. Any situation outside a rule's validated range raises "unruled" and names the reason. Those reasons are the leaks a closure predicate has to exclude. - It matches the census from blank exactly: 278 of 278 visible frames from the hub at step 46,734 to step 1.024e12 (macro_vs_census.py). Its other 2 frames lie inside a Transfer staircase, which the accelerated simulator jumps over. - On 80 random G1-G5 frames (3e7 steps each on the accelerated simulator, seed 102), 1,358 macro frames appear in the reference run (val_macro.py trace, val_macro_trace_102.txt). The 2 others lie inside a right phase (d = 1 during a long right-phase bounce), which the reference jumps over. 0 real misses.

2. New rules (exact target frame by simulation, vrules.reach):

• Negative controls die: EatToEdge with a0+2 0/10, RightPhaseLong with ak+2 0/10, PushFresh with (10)^2 0/8, HubTopK1 read as HubClean 0/10.
• From blank:
• EatToEdge occurs, first at 2.41e9 steps with P0 = 2.
• HubTopK1 occurs about 960 times in the first 40,000 events, all after step 1e12, so the census comparison does not reach them.
• PushFresh does not occur.

3. From blank, far past the C horizon (far_macro.py). - 260,000 macro events with no unruled event. That reaches runs longer than 10^4300 cells, so step counts far beyond 10^8000. - That run then stopped on Python's limit for printing big integers, not on a machine event. A rerun without the limit (strict rules, plus the P = 1 ToEdge1 and PushFresh cases) passed the same mark at 769 s, with runs of 14,906 bits (about 10^4487), still with no unruled event. - First 60,000 events, i.e. 8,723 right ends (shapes_census.py): - up to 7 walls, 7 chunks and 17 runs in Y; - Push cascades up to 7 deep; - 122 distinct traversal signatures, with new ones still appearing at right end 8,488. - So the segment list is not bounded by 3, as the 1e12 census suggested.

4. The decided closure test fails (good_closure2.py). Good+(D) means G1-G5 plus three facts, read off the macro rules over the next D traversals: - G6: no P-mode right end while walls remain; - G7: every Push has d >= 4 and p >= 3, and every event stays in its validated range; - G8: the next right end is clean or top, with P0 >= 2.

Results (0 halts in all 160 instances; seeds 131 and 132 also had 0 halts in 120 instances, run before PushFresh was ruled):

Why it fails: the three facts describe the current traversal. Whether the next traversal underflows depends on how the walls of the new hub relate to its staircase level. A frame-level lookahead only pushes the problem one cycle further.

5. What closure really needs (hub level, macro simulator, scripts hub_perturb.py, hub_random.py, depth_g15.py, push_relations.py, absorb_parity.py).

• Reachable hubs have slack, except in t. Perturbations of the hubs at right ends 30-400 (30 right ends each):

So the staircase relation is exact, and everything else has slack.

• Random hubs mostly settle within 3 cycles, but not completely. Setup: runs log-uniform from 8 to 2S, a0 odd, inner a even, t top or clean with P0 >= 8.
• At large scale (S up to 10^30; hub_random_4_S_D40.txt), 1,719 of 2,000 stay in the ruled region for 40 right ends.

• The failures, by depth:

  depth	failures	reason
  1	1	small-value case
  2	153	P-mode right end with walls
  3	122	P-mode right end with walls
  5	4	P-mode right end with walls
  7	1	P-mode right end with walls

• So "the next 4 traversals use only validated rules" (H4) is not closed: 5 of 1,724 hubs still fail later, about 0.3%.

• At small scale (S <= 680; hub_random_5_S_D40_smax700.txt), small-value corner cases add up: 866/2000.
• On the accelerated simulator (hub_closure_accel.py, seed 161): 80 random H4 hubs with S <= 680, 2e9 steps each.
  • 0 halts; 1,174 later right ends checked.
  • 5 hubs leave H4: P-mode right end with P < 4 twice, top with P0 < 2 twice, P-mode right end with walls once.
  • The reference run passes each of these without halting.
• The underflow failure chain (derive_eat_to_wall.py): 1. The outer bouncer meets a wall whose p-1-q exceeds its d. 2. That gives a P-mode right end with walls. This is a validated rule (val_hubsweep seed 94), but it puts the odd wall (P-2, 2b1+1) inside the wall list. 3. With P-mode right ends with walls allowed, random hubs reach 979/1000. Of the other 21, 20 hit EatToWall: a nested bouncer from that odd wall eats through its parent chunk and reaches the next wall before the chunk is gone. The last one is a small-value case. 4. EatToWall is not ruled. Direct simulation of its P0 = 3 case leaves an odd (10)-run in a chunk, which is the halting precursor.

• 0 eats of an odd (10)-run occurred in any macro run (blank, perturbed or random).

• Exact relations from blank that keep underflow (40,000 events):

• After a nested bouncer merges back, the outer bouncer reaches the next wall with d = q of that wall (264) or q-1 (303). That covers 567 of 570 merge-backs; the other 3 are inside a nested bouncer whose own d runs out first.
• A nested bouncer either cascades (p-1 < q, 1,700 times) or merges back with p-1-q >= 3 (2,428 times), never with p-1-q in {1, 2}.
• An Absorb happens only at the last wall (1,475 Absorbs + 10 AbsorbToEdge, all with no wall left). So a start with P0 even always has exactly one wall.
• Every right end is clean or top.

Exit condition. - It did not close as an explicit FractalType7v4-style predicate, so no proof.md. - No leak needs non-linear arithmetic. The missing facts are linear relations between neighbouring walls, the bouncer's d and the staircase level S, and S is a fixed sequence (0, 3, 8, 19, ...). - Most random hubs settle into this regime within 3 cycles. So this is not cryptid-like.

Superseded runs. good_closure2_121/122_*_superseded_P1bug.txt came from a macro simulator without the P = 1 ToEdge1 case, so their leaks are spurious. Seeds 131/132 ran before PushFresh was ruled.

Still open: 1. Write the attractor regime out as an explicit hub predicate: parity (a0 odd, inner a even, P0 even only with one wall), staircase (t top, or clean with P0 >= c), a minimum run size, and the underflow relations for every wall but the leftmost, as linear (in)equalities in p_j, q_j, S and P0. Read them off hubs reached from blank: exact relations such as arrival d = q or q-1. Check closure under one traversal on random H-hubs with the macro simulator, and for bounded k with an SMT solver (the macro map is piecewise linear). The macro rules become the lemmas of proof.md. 2. Rule the small-value corner events (P-mode right end with P < 4, start with P0 < 2, Push with d < 4 or p < 3, ToEdge1 with d < 4, RightEndP with P < 4) and EatToWall. Either the predicate has to exclude them, or they need rules: the reference passes them without halting. 3. #39 and R7: nothing transfers yet, because the invariant did not close. The macro simulator is written for #16's tape words ((10), (011010), (010), (101)). Check first that their Quick_Sim rules map onto the same macro events.

Decision (2026-10-10, auto-applied, round 3)

Question: Fund one stage to write #16's hub-level invariant out explicitly (parity, staircase, linear underflow relations, corner-event rules) and test its closure with the macro simulator, before proof.md? Answer: hub_invariant (One stage: write the hub invariant out). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.

Funded stage (2026-10-10, hub_invariant)

Result: the hub invariant is now written out as an explicit predicate H* (parity, staircase, a band of linear inequalities, exact "zipper" relations). Its closure test passes: 10,000/10,000 random H*-hubs over one traversal (the decided target), and 10,000/10,000 over 40 traversals at staircase levels ≥ 10^9. All 12,000 right ends from blank are in H*. It is not yet a proof invariant, for two named reasons. (1) Small-value corner events (9 families) are not ruled. They only occur when a run or a difference of tail sums is small (about 1% of 40-traversal orbits that start at small levels, none at levels ≥ 10^9), and the reference passes all 175 tested without halting. (2) The clause for short right ends (block seeds) is wider than what collapses produce: 2 of 10,000 random short seeds reach a P-mode right end with walls within 200 traversals. Confidence stays med (closer to high). Not a cryptid. Status CHECKPOINT_A, stage hub_invariant.

1. One sequence per right end, and its tail sums. A right end (hub, or P-mode right end; d = 0, Z empty) has walls (p_i, q_i), far to near, and t = ak. Add the start frame as a last, "virtual" wall whose fresh bouncer (p−1, q) is the start: (t−S+1, S−1) when t is clean, (p_m, q_m+t) when t is top (the last real wall is dropped). Flatten everything to z = (z_1, …, z_2m) and set - B(k) = Σ_{l≥k} (−1)^l z_l (tail sums with alternating signs, z_2m counted +), - τ = S−1 (clean) or t (top).

The left traversal is a stack process in Δ = d − P: - at a wall with Δ ≥ 1 the bouncer pushes Δ−1 (the chunk) and restarts with δ_i = q_i − p_i + 1; - with Δ ≤ 0 it merges the top chunk (Δ += c).

Δ plus the pending chunks is the running sum T_i = 1 + B(2i−1). So: - B(odd k ≥ 3) ≥ 0 means no P-mode right end while walls remain (this is the underflow inequality); - B(1) < 0 means the traversal ends in a P-mode right end with no walls (a collapse).

From blank, every transition between right ends is one of three kinds (2,999/2,999 over the first 3,000 right ends; scripts/hubinv_classify.py):

This is the "chaotic segment list" of round 1. A block grows by one entry per traversal. The walls of hub n are (h_n, h_(n−1)), (h_(n−2), h_(n−3)), … down to a block tail that stays fixed. In the pure case h_(n+1) = 2h_(n−1) − h_n, so deviations double with alternating sign until B(1) < 0 ends the block (example from blank: hubs 45-52, then the collapse 51 → 52 → 53).

2. Zipper relations (exact). With e = B(k+1) mod 2 (forced by the parity of the walls): - k even: B(k) = 2·B(k+1) + 4 + e - k odd: B(k) = 2·B(k+1) − 2τ − 4 − e

They hold at every interior position of every right end from blank: E-mode 1 ≤ k ≤ 2m−4, P-mode 3 ≤ k ≤ 2m−4, and also k = 2m−3 at top right ends. The tail positions are free. The shift-reflection of a G step maps the even family onto the odd one and back, so G preserves them. Consequences: - a growth hub is fixed by its block tail and its length; - in the interior the odd-index B's lie below τ and the even ones above it; - deviations from the fixed point double toward the head.

These relations are the previous stage's "arrival d = q or q−1" fact (B(2i+1) = z_2i − 4 − e).

3. H* (scripts/hubinv_H.py, function H; option MU adds a margin): - H0 shape: X empty at the right end; every b ≥ 1 and every inner a ≥ 1. - H1 parity: - E-mode: a0 odd; P-mode: a0 = 1 and P odd; inner a even. - Exceptions: a0 even or P even is allowed at a top right end with one segment (its wall is dropped), and P even at an Absorb start. - H2 staircase: - t is clean with P0 ≥ 2, or top with P0 ≥ 2; - a start with P0 even (Absorb or ToEdge2) has at most one real wall; - at a top right end with a real wall left, q_m + t is clean at level t+1. - H3 band: 0 ≤ B(k) ≤ 2τ for 2 ≤ k ≤ 2m−1. The k = 2 bound is dropped in P-mode (the odd collapse wall) and at an Absorb start. - HR: the zipper relations of item 2. - HM, margin MU (test option only, used to keep the corner events out): every z ≥ MU; MU ≤ B ≤ 2τ − MU in the band range; no wall with 1 ≤ p−q < MU; same-parity B's at least MU apart.

4. Closure tests (macro simulator unless stated; output files in scripts/):

Corner census (4,000 orbits at S ≤ 5,459, 40 right ends): 518 corner events, in macro_sim's names:

Exit condition. - The decided target is met: 0 leaks in 10^4 random H*-hubs over one traversal, confirmed on the accelerated simulator. - But H* is not yet closed without the margin. The leaks are the corner events and the seed clause, and both are finite, local and linear (no pseudo-random arithmetic). So the result is neither the "closed → proof.md" exit nor a structural "still leaking → park". A new decision (corner_rules recommended).

Still open (why not high): 1. Rule the corner families. Each has one small parameter (d ∈ {2, 3} at a Push, p ∈ {1, 2}, P < 4, P0 < 2, …) and occurs when a run or a difference of same-parity B's is small. At levels ≥ 10^9 none occurred in 400,000 transitions. Nothing excludes them from blank, though (h = 5 + B(1) − e can land on a small value). So each needs a validated rule whose output lands back in H*, as the reference shows it does (161/175 at the next right end). 2. Pin the seed clause. H* only asks parity, staircase and band of short right ends. Collapses of H* hubs produce seeds that stay in H* (0 leaks in 10^4 orbits at scale), but some random short clean hubs with a0 large against t collapse twice into a P-mode right end with P even or a band violation. The S transitions (collapse completion: cascade + edge-mode eats; Absorb starts) need closed forms, so that the seed clause becomes a set of linear relations. 3. Proof shape, once 1-2 close. Hub-to-hub induction on H*. Lemma G: stack process, shift-reflection, new head. Lemma C: the collapse wall. Lemma S: collapse completion and Absorb start. Plus the corner rules, with the validated macro rules as the lemmas below them. Base: the hub at step 46,734.

#39 and R7. Nothing transferred yet, and neither machine has a folder. H* is stated on the wall sequence z and the staircase level, not on #16's tape words, so the transfer would be: 1. map their Quick_Sim tape words onto the same macro events (bouncer, Push, Absorb, staircase restart) and write a macro simulator for each; 2. recompute z, B and τ at their right ends from blank, and check the band, the shift-reflection identity and the zipper relations; 3. rerun the hubinv_H.py closure tests.

Scripts (all new in this stage): - hubinv_dump.py, hubinv_zipper.py, hubinv_classify.py: the wall form, the unified sequence, the G/C/S classes. - hubinv_bsums.py: tail sums and the shift-reflection identity from blank. - hubinv_H.py: H*, the hub generators (band-only and exact-relation), the closure tests. - hubinv_identities.py, hubinv_seeds.py, hubinv_shortmine.py, hubinv_accel.py, hubinv_corners.py. - Outputs ending in _superseded.txt came from earlier versions of H* (before the zipper relations or the parity exceptions) and are kept only for the record.

Decision (2026-10-11)

Question: Fund one stage to rule #16's small-value corner events and pin the block-seed clause of H, so that H closes without a margin, before proof.md? Answer: corner_rules (One stage: rule the corner events). Dennis: go with recommendations (2026-10-11).

Funded stage (2026-10-10, corner_rules)

(Run 2026-10-11.) Result: all 9 corner families are now ruled in closed form at least in part. 5 are ruled fully: Push p<3, ToEdge1 d<4, clean P0<2, top P0<2 and eat_to_edge exact. 4 still have sub-cases left: the P-mode right end with P = 1, V1 with d = 1 when q is odd or Z is not empty, RightEndP from P = 3 or with walls, and walls with p = 0 that a bouncer reaches later. Every new rule is validated by exact simulation: 15 rule families, 520 random instances, 0 fails; negative controls reach their target 0/150 times. The corner rules leave the orbit from blank unchanged. At small levels (S <= 5,459), 9,977/10,000 orbits are now ruled for 40 traversals without any margin, against about 99% before (seed 903 at all levels: 9,896). The target (0 leaks in 10^4 orbits x 40 traversals) is not quite met. Two corner sub-families are still open (23 of 10^4 orbits), and one clause of H* does not fit the output of a new rule (67 orbits, which stay ruled). No halts. Confidence stays med (closer to high). Not a cryptid. Status CHECKPOINT_A, stage corner_rules.

TM5 lead (FractalType4.v). Same table, start state renamed: TM5 A,B,C,D,E,F = #16 B,C,D,E,A,F. - P a is our right phase (the staircase on an (01)-run, stated for any left tape l). P_S / P_S' are the level recursion S' = 2S+2 / 2S+3. Inc1/Incs1 is the inner bouncer of a Transfer. - So the Conv/Transfer lemmas of a formal proof can take P, P_S, P_S', Incs1 nearly verbatim, after renaming states. - TM5 has no walls, so it says nothing about the corner events below, which are all left-side wall events.

1. One mechanism behind the corners: two virtual frames. - Most corner events are the old rules taken one bounce further, down to P = 1 or P = 0. These two frames are not standard left-turn frames, because the cell two to the left of the head is a wall cell: - V1 = X (10)^p (101)^q (10)^1 <A (10)(011010)^b1 M (10)^ak (010)^d Z - V0 = X (10)^p (101)^q <A (10)(011010)^b1 ... - Three primitive moves: - BounceP31: P 3 -> 1, b1+1, ak+2, d-2. - Push1 (V1, d >= 2): X (10)^(p-1) <A (10)(011010)^1 (010)^q (011010)^b1 M (10)^(ak+2) (010)^(d-2) Z. - Absorb0 (V0): the AbsorbChain carry propagation, entered with carry 0 instead of 2 and without a bounce. - The old Push is BounceP31 + Push1. The old AbsorbChain is BounceP(2 -> 0) + Absorb0. - A Push1 at a wall with p = 2 gives V1 at the next wall (a chain). With p = 1 it gives V0, or edge mode with a0 = 1 when X is empty. - Chunks with c = 0 glue onto the next chunk, and zero inner (10)-runs merge their (011010)-runs. Both are tape identities. - Implemented in scripts/macro_sim2.py. macro_sim.py is kept unchanged for the earlier outputs.

2. Corner families -> rules (scripts/val_corner.py). - Each instance: a random standard frame with the small parameter fixed and all other values random (1..6 or up to 300, both parities). macro_sim2 predicts the frame after the corner and 1-2 further non-bounce events, so a right-phase target is never confused with another staircase level. vrules.reach then has to meet that frame exactly. - Results: val_corner_11.json (40 per family), val_corner_22.json, val_corner_23.json (30 per family).

• The Reflect formula has the same shape as the zipper relation B(k) = 2B(k+1)+4+e. When the staircase hits the left edge, its material comes back doubled.
• P-mode right ends with walls are switched on (PModeClean/Top with X; already validated, val_hubsweep seed 94, 30/30 + 30/30).

3. Closure without margin (scripts/hubinv_Hc.py, corner_hybrid.py). - The hybrid simulator is macro_sim2 plus an exact fallback (accel_sim) only where macro_sim2 is still unruled. It reports halts and the right ends inside the exact part. - H*c is H* widened by what the corner rules handle: P0 in {0, 1}, ak a level, first wall p = 0, Reflect, P0 = 0 with walls. H0, the inner parities, the band and the zipper relations are as in H*. - From blank: macro_sim2 gives the same 4,000 right ends as macro_sim, and 4,000/4,000 are in H*c (blank_macro2_4000.txt).

• For comparison, before this stage the census (4,000 orbits, S <= 5,459) counted 518 corner events. Seed 903 had 104/10,000 leaking orbits at all levels.

Still open (why not high): 1. P-mode right end with P = 1, also reached by RightEndP from P = 3. Its sweep makes a bouncer with no (011010) segment, 0^inf <A (10)^a0 (010)^d, in which a0 grows by 4 per trip. macro_sim2's frame grammar does not have that shape yet (Y = [a0]). For 9 of the 14 open-corner orbits at seed 1002, the exact fallback found no frame macro_sim2 could resume from within 3e7 steps. These are not halts; the fallback just cannot parse that shape. Extend the grammar with Y = [a0] (BounceE: a0+4, d-2) and fit the rule. 2. Walls with p = 0 reached later: Push1 or Absorb at the wall (0, q) left by an a0 = 1 hub or a P = 2 right end. This needs a rule with its own exact derivation. 3. V1 with d = 1 other than V1RightEnd: q odd (the orbit goes through an eat of a last odd (10)-run, which is safe at the tape end; the outcome is an E hub [2p+8+q, ., 12+q] in the probes) or Z nonempty. It did not occur in the 2 x 10^4 orbits above, so it is rare. 4. H*c clause for the RightEndP1 output. All 67 band failures at seed 1002 (and 7 at seed 1003) are the E hub with a0 = 5 right after RightEndP1. B(2) = 2 tau + 1 there, and further band positions fail too. Dynamically these orbits stay ruled for all 40 traversals. RightEndP1 is a P = 1 collapse, so it needs its own collapse clause, like the P-mode collapse (k = 2 dropped), not the growth band. 5. The seed clause (short right ends as linear relations) was not narrowed in this stage. The new rules cover most of the short-transition corners, but the S transitions are still not in closed form as a family. 6. Not done: an end-to-end trace of macro_sim2 orbits against accel_sim through the corner events. The rules are validated one family at a time, including chains of up to 4 events, but not along long orbits.

Scripts (new): macro_sim2.py, corner_hybrid.py, corner_collect.py, val_corner.py (-> val_corner_11/22/23.json, val_corner_11.txt, val_corner_22.txt), hubinv_Hc.py (-> hubinv_Hc_1002_smax5459.txt, hubinv_Hc_1003_smax1e30.txt), blank_macro2_4000.txt.

Decision (2026-10-12)

Question: Fund one more short stage to rule #16's last three corner sub-families and fix the H clause for the RightEndP1 output, before proof.md? Answer: corner_rules_2* (One more corner stage). Dennis: apply recommendations (2026-10-12).

Funded stage (2026-10-10, corner_rules_2)

(Run 2026-10-12.) Result: the three open corner sub-families are ruled where H* orbits meet them, and H* gets the two missing clauses. The closure target is met: 10,000/10,000 orbits at levels <= 5,459 and 10,000/10,000 at levels <= 1e30, every event by a validated rule (no exact fallback) and every right end in the widened invariant H*c2 for 40 traversals. Fresh seeds give the same: 20,000/20,000 at each scale, and 5,000/5,000 over 200 traversals. All new rules are validated by exact simulation: 11 families, 440/440 random instances; negative controls are met 0/110 times. 0 halts. Two things keep confidence at med (now close to high). (1) The seed clause of H* (short right ends) is still wider than what the dynamics produces. 29 of 10^4 random short H* seeds leave H*c2 at scale, which was already open item 5 of corner_rules. (2) Two sub-cases are ruled only where orbits reach them: V1 with d = 1 when Z is not empty, and EatLast with too little P. Neither occurs in any H* orbit. Not a cryptid. Status CHECKPOINT_A, stage corner_rules_2.

1. The left edge as a wall with p in {-1, 0} (scripts/macro_sim3.py, block CORNER2; macro_sim2 is unchanged). - A P-mode right end with P = 1 has the first wall (P-2, 2b1+1) = (-1, 2b1+1). A wall (0, q) comes from an E hub with a0 = 1 or a P = 2 right end. - Such a wall is always the leftmost one. An interior wall with p = 0 is glued onto its left neighbour (normX, a tape identity). - The old rules carry over with p in {-1, 0}: - Absorb0 passing the leftmost wall gives edge mode with a0 = p+3, which is the old ToEdge formula. Stopping at a p = 0 wall gives P = 0, X empty, so edge mode with a0 = 1. - Push1Edge. Push1 at the leftmost wall (p, q), p in {-1, 0}, gives the segment-less bouncer 0^inf <A (10)^(2p+5) (010)^q, with the pushed chunk in front. - Segment-less bouncer Y = [a]. The edge rules apply with a0 = ak = a: BounceE a+4 per trip, RightEndE a+3, EatChunkE a+5B+2A, and a merge appends the chunk. - HubSegless. Its right end 0^inf <A (10)^a 0^inf restarts the staircase with X empty: clean, P0 = a-S-1, d0 = S-1. - RightEndP from P = 3 (X empty) gives the P = 1 right end. - Push1End (V1 with d = 1 and Z empty, any q, p >= 1). The last (010) is only half used, so the pushed chunk is the tape-end chunk (011010)^(b1+1) M (10)^(ak+3) with c = 0 and an odd last run: X (10)^(p-1) <A (10)(011010)^1 (010)^q + that chunk. The old V1RightEnd (q even, p-q-1 >= 2) is Push1End followed by a bounce and a merge. - EatLast, the eat of that tape-end chunk (d = 1, only chunk, c = 0, odd last run, the other runs even). It is safe because it sits at the tape end: - E-mode: a0 += 4B+2A+2, ak += B, d = 0; - P-mode (P >= 4B+2A+2): P -= 4B+2A+2, b1 += 2B+A+1, ak += B, d = 0, and P = 0 goes to edge mode.

2. Validation by exact simulation (scripts/val_corner2.py, as in val_corner.py). Each instance is a random frame with the small parameter fixed. macro_sim3 predicts the frame after the event and 1-5 further non-bounce events, and vrules.reach must meet it exactly.

Files: val_corner2_11.json (first 4 rows), val_corner2_12.json (next 4), val_corner2_13.json (last 3). The P = 1 right end was renamed PModeP1 after runs 11 and 12, so their chains still show PModeClean/Level/Top.

3. H*c2 (scripts/hubinv_Hc3.py, function Hc). It is H*c with two new clauses: - H0s. A segment-less E hub [a] is allowed if it is clean with P0 = a-S-1 >= 2. - H3d, the band defect. At most one band position may have B(k) = -1 or B(k) = 2τ+1. - The RightEndP1 hub (a0 = 5) has B(2) = 2τ+1. The shift-reflection of a G step, B'(k) = 2τ - B(k-1), carries this unit defect one position deeper per traversal, alternating between -1 and 2τ+1, until it leaves through the tail. - Example from seed 1002: hub [5, 85, 32, 15, 167] has B(2) = 335 = 2τ+1. The next hub [337, 2, 170, 16, 197] has B(3) = -1. Then comes the P-mode end P331 with B(4) = 335. Two traversals later the hub is back in the plain band. - So the clause replaces corner_rules' k = 2 slack, which covered only the first of these hubs. That is why 67 orbits failed there.

4. Closure without margin (macro_sim3 alone: every orbit below was fully ruled, so the exact fallback was never needed):

• Before this stage, the 25 open-corner orbits of seeds 1002/1003 split as: 11 P = 1 right ends, 4 RightEndP from P = 3, and 10 absorbs into a p = 0 wall. corner2_collect.py finds 0 Unruled events with macro_sim3.
• E2E check against the accelerated simulator: e2e3.py starts at the right end before the first CORNER2 event and requires macro_sim3's right ends in the same order (e2e3_1002.txt). Seed 1002 has 30 orbits that use CORNER2 rules (each one P = 1 right end -> Push1Edge -> HubSegless), checked for 2e8 steps each. Result: 238 macro right ends matched in order, 0 mismatches, 0 reference right ends off the macro orbit, 0 halts. In 27/30 orbits the reference gets through the CORNER2 traversal; 825 macro right ends lie past the step horizon.

Still open (why not high): 1. The seed clause. This is corner_rules' item 5, not part of this stage. Random short right ends that satisfy H* do not all stay in H*c2 (hc3_seeds.py): - seeds Ec/Et with runs >= 1,000 at levels <= 1e30 (seed 905): 9,971/10,000 stay, 27 reach a P-mode right end with P even, 2 fail the band at k = 2; - all seed kinds with runs from 1 at levels <= 5,459 (seed 906): 9,233/10,000 stay (506 P even, 61 band k = 2, 185 window right ends, 30 unruled small-value cases). - The short right ends that orbits actually produce (the S transitions: collapse completion and Absorb starts) do stay in, so H* has to state them as linear relations, not as "any short hub with parity and band". 2. V1 with d = 1 and Z not empty. The bouncer leaves (10)^(ak+2) 1 Z, a lone 1-cell separator, which is outside the grammar. The probes return to standard frames without halting (v1d1_probe.py, 8/8). It never occurs in an H* orbit (0 in 6.5 x 10^4 orbits), so either a rule or an H* argument that excludes it is needed. 3. Sub-cases seen only in generators, never on H* orbits: EatLast with P < 4B+2A+2, top with the p = -1 wall as its only wall, Absorb0 stopping at the p = -1 wall. 4. H3d was tested on the defects the dynamics produces (806 restarts), not on synthetic hubs with a defect at a random position.

Scripts (new): macro_sim3.py, val_corner2.py, corner2_collect.py, trace2.py, trace3.py, v1d1_probe.py, eatlast_probe.py, hubinv_Hc3.py, hc3_dump.py, hc3_follow.py, hc3_special.py, hc3_seeds.py, blank3.py, e2e3.py.

Decision (2026-10-12)

Question: Fund one stage to replace #16's seed clause by closed forms of the short (S) transitions, so that Hc2 becomes inductive, before proof.md? Answer: seed_clause* (One seed-clause stage). Dennis: b (fund all five), 2026-10-12.

Funded stage (2026-10-10, seed_clause)

(Run 2026-10-12.) Result: H* closes without a margin. The seed clause of H*c2 is replaced by relations read off closed forms of the short (S/C) transitions. The new predicate H*c3 passes every closure test with 0 leaks: - random short seeds of every kind drawn from the new clause: 10,000/10,000 at levels <= 1e30 and 10,000/10,000 at levels <= 5,459; - 2,000 of them over 200 traversals: 2,000/2,000; - rnd_R orbits: 10,000/10,000 at each scale, with no false rejections among about 595,000 short right ends; - from blank: 4,001/4,001 right ends.

V1 with d = 1 and Z nonempty is excluded by a parity invariant (item 5). The funded exit is met ("closed with 0 leaks -> proof.md"). Confidence high, with two caveats: - one part of the new clause is a bounded look-ahead (3 short successors) through closed-form maps, and it is not yet written out as explicit polyhedra (item 3); - inductiveness is shown by tests, not yet symbolically.

Not a cryptid. Status CHECKPOINT_A, stage seed_clause.

1. What the dynamics produces (scripts/seed_collect.py, seed_census.py -> seed_census_1_smax5459.txt). These are the short right ends (at most one real wall) on 3,000 rnd_R orbits, 78,201 distinct ones, written as rkind = E/P, P parity, clean/level/top, real walls:

• CW, the collapse-wall relation (exact). Every P-mode right end with P odd, long or short, has B(2) = 2τ + 3 + (B(3) mod 2). That is 47,668/47,668 on rnd_R orbits at both scales. A collapse puts the odd wall (P-2, 2b1+1) at the head, and the rest of z fixes its B(2). There is no Pot0: a P-odd end always has a real wall.
• P-even ends (all short) have B(2) >= 2τ + 5. The clause uses B(2) >= 2τ + 3 (PE).
• The old seed clause allowed any b1 on a short E hub, and that is the main leak. On random Ec1 with B(1) < -2τ (seed_ec1_classes.py, seed 7):
• b1 odd: 1,731/1,731 stay in H*c2;
• b1 even: 1,509/2,435 leave (H1 P even, band k = 2, or an unruled event).
• a0 mod 4 plays no role.
• Dynamically produced Ec1 with P0 odd and B(1) < -2τ always have b1 odd.

2. Closed forms of the S/C transitions (fitted on macro_sim3, which applies validated rules only; spot-checked by exact simulation): - First collapse of a short E hub (B(1) < 0). With P0 odd it is BounceP31 Push1 [RightEndP], giving Pot1. With P0 even it is Absorb [RightEndP], giving the P-even top k = 1 end. In both cases τ is unchanged and B'(1) = B(1) + 2τ + 6 + 2r, with r = 1 when the traversal ends with RightEndP: 5,842/5,842 (seed_clause.py fit, seed 21, seed_fit_21.txt). - A short P-odd end with P0 odd (all Pot1, and Poc1 with v1 even): - it collapses iff B(1) + 4·z3 <= -6 (collapses: max -6; E outcomes: min -2; seed_boundary.py, seed 52); - otherwise it ends in the E hub [a0', (P-1)/2, t' = B(2) + z3/2]: 2,521/2,521 (seed_pe_fit.py, seed 51). - Second P-mode collapse. The P-even end it produces has v1 = b1 of the E hub that started the chain, so P0 = b1 - 1 at S odd: 3,538/3,538 (seed_chain_fit.py, seed 4). That is why b1 must be odd. The same bit propagates one step back: the E outcome above has b1' = (P-1)/2, so a P-odd end whose E outcome collapses twice needs P = 3 mod 4. - Exact simulation (seed_e2e.py seed 41 -> seed_e2e_41.txt; accel_sim reference, 1e8 steps): 60 short seeds that start with a collapse, 8 right ends each, levels <= 700. - 383 macro right ends matched in order, and 35 more that the reference skipped (it sees right ends only at its accelerate calls). - The first-collapse closed form holds 39/39. - 1 reference right end is not on the macro list: the segment-less hub [1381] that the validated composite Reflect passes through (top with the p = 0 wall -> segment-less hub [n+1] -> HubSegless; same start frame, P0 = 17). - 0 halts.

3. H*c3 (scripts/seed_clause.py, function Hc3). It is H*c2 plus the following: - CW: every P-odd P-mode right end has a real wall and B(2) = 2τ + 3 + (B(3) mod 2). - PE: a P-even end (other than P = 2) has B(2) >= 2τ + 3, together with H*c2's P-even exceptions (absorb start, top k = 1). - SB: a short P-odd end with P0 odd satisfies B(1) + 4·z3 <= -6, or B(1) + z3/2 >= 1, or its E outcome t' = B(2) + z3/2 is not clean (level or top), or t' - S' is even (an absorb start, which has no band position at k = 2). - EB: along the collapse chain of a short right end (at most 3 P-mode ends in a row), no P-even end that is not an absorb start, top k = 1, level or P = 2 (on the chains seen, this is "b1 odd"), and every chain member satisfies CW/PE/SB. - Hs_K, K = 3 or 4: the next K short successors of a short right end (stopping at the first long one) are ruled and satisfy H*c2 + CW + PE + SB. - Each step is one of the closed-form S/C maps: a composite of validated rules with linear guards and parity guards. - On 4,000 seeds there are 93 distinct one-step families and 237 distinct <= 3-step paths, so Hs_K is a finite union of polyhedra intersected with congruences. - It is linear, but not yet written out. - K = 2 is not enough (5/3,000 leak); K = 3 and K = 4 both close.

4. Closure tests (output files scripts/seedcl_*.txt; the macro simulator applies validated rules only):

• The H*c2 and the H*c3-without-Hs_K columns use the same generator (rnd_short) with their own filter, so the seed sets differ.
• What H*c3 without Hs_K still leaks:
• deeper chains: the P = 3 mod 4 bit one S step back;
• small-value window right ends at levels <= 83;
• a few CW "no real wall" cases.
• Hs_K rejects these seeds. About 1% of the seeds drawn are rejected by it, most of them because the look-ahead meets an unruled small-value window.

5. V1 with d = 1 and Z nonempty is excluded (scripts/v1d1_parity.py -> v1d1_parity_7.txt, v1d1_parity_8_smax1e30.txt). Invariant, at P-mode frames with walls: - (a) every chunk in Z has an even (010)-count, except possibly the deepest one; - (b) if Z is nonempty, d + P is odd; - (c) a bouncer with P even never has Z nonempty.

Why it holds: - Walls have p = q mod 2. Even/even walls come from the hub walls, odd/odd from the collapse wall; the even/odd wall of a P-even end is absorbed, never pushed at. So a Push1 restart (p-1, q) has d + P odd. - When Z is nonempty, d is even at P = 1, so the new chunk c = d - 2 is even. An odd chunk is pushed only into an empty Z, so it is the deepest one. - Merging or eating a chunk flips d + P only when c is odd, that is only for the deepest chunk, and Z is then empty. - P-even bouncers start with Z empty and absorb at P = 2. They never push.

So at V1 with Z nonempty, d is even and never 1. Checks: 65,273 frames (levels <= 5,459) and 61,747 frames (<= 1e30) with walls and Z nonempty satisfy (a), (b) and (c) 100%.

Non-halting argument (for proof.md). - Base: the hub at step 46,734 (direct computation), in H*c3 (from blank 4,000 right ends). - Step: every right end in H*c3 goes to the next right end by a finite chain of validated macro rules (each a lemma), and the next right end is again in H*c3: - long hubs: G (shift-reflection), C (CW), the corner rules and H3d, as before; - short ones: the closed forms of item 2 and Hs_K. - No rule halts. The cases outside the rules are excluded: - V1 with d = 1 and Z nonempty, by item 5; - small-value windows, by Hs_K; - eats of odd (10)-runs, by parity G1.

Still open (for proof.md, not for Dennis): 1. Write Hs_K out explicitly: symbolic execution of macro_sim3 on parametric short right ends (93 one-step families), giving the polyhedral pieces. Then prove Hs_3(R) => Hs_3(next R) symbolically instead of by sampling. 2. The corner_rules_2 sub-cases seen only in generators (EatLast with P < 4B+2A+2, top with the p = -1 wall alone, Absorb0 stopping at the p = -1 wall): still never met on any H*c3 orbit or seed (0 unruled in the about 5 x 10^4 runs above). proof.md has to exclude them from H*c3 explicitly. 3. H3d (one unit band defect) is still tested only on dynamically produced defects.

Scripts (new): seed_collect.py, seed_census.py, seed_clause.py (H*c3, rnd_short, closure tests, fit; default Hs_4; env BASE=1 gives H*c2, LOOKK=0 the explicit clauses only, LOOKK=K gives Hs_K, SB=0 drops SB), seed_e2e.py, seed_ec1_classes.py, seed_chain_fit.py, seed_pe_fit.py, seed_boundary.py, v1d1_parity.py. The outputs seedcl_*_noSB_superseded.txt came from the first H*c3 without SB (SB was added after an E-hub band leak, then given its level/top and absorb-start exceptions after two false rejections on rnd_R orbits).

Skeptic round 1 on proof.md (2026-10-12, stage informal_proof)

Result: OPEN. The skeptic found H*c3 not inductive (4 fatal, 3 major, 2 minor gaps; the macro rules themselves were re-confirmed: 422,018 right-end transitions, 2.6e10 exact steps). Three of the four fatal gaps are repaired in the new predicate H*c4 (scripts/inv4.py); the fourth, the short-regime clause, is open.

H*c4 = H*c3 + repairs (proof.md §5.2): - H2t': at a top right end with a real wall, the merged tail T = q_m + ak is clean at level ak + 1 (ak + 1 < T < 2ak + 1). The old H2t (Sof(T) = ak + 1) let T be a window or a level. - HL: no Level right end with ≥ 2 real walls (they break Lemma T and are never produced). - CP (new, exact): every long P-mode right end has P = 2B(3) − 2τ + 3. On orbits 2,051/2,051 (+1,599/1,599 in check J3). Sketch: P = −B_hub(1) − 1 − r (Lemma T at the first wall), B(3) = 2τ − B_hub(2) (shift-reflection), HR at k = 1 on the hub, and P odd forces r = e. - Hc4 is total (Hc3 raised TypeError on [12,2,2]).

Exhaustive back-solved boxes (every zipper tail at the given levels, every length; one traversal; inv4.py longE/longP/short):

Why the short regime is open. Hs_4 (look-ahead) is not inductive: [79,12,32] is in H*c4, its successor is not, and its chain reaches a P-mode right end with walls at depth 8 (no halt). Runs of consecutive short right ends are long: up to 44 in a row from blank and 46 on rnd_R orbits (scripts/inv4_runs.py 7 2000 5459), e.g. the alternation Ec1 ↔ Et0 with a deviation that doubles per cycle (blank right ends 363-382). So no fixed look-ahead depth can be inductive; the short regime needs its own explicit clauses (a second zipper). First data: Ec1 from Et0 / Pet0 satisfy the k = 1 zipper exactly (1,168 / 1,405, 6 with the unit defect); Et1 from Ec1 too (1,483; scripts/inv4_shortrel.py 3 300 5459); Ec1 from collapses (Pot1, Poc1, long P) lie below it.

What is left (proof.md §8): - G1 (fatal): explicit inductive clauses for the short kinds (Ec1, Et0, Et1, El1, Pet0, Pot1, Poc1, Pec1, P1/P2, Eseg), replacing EB/SB/Hs_K; include or exclude the P-mode-with-walls states on the [79,12,32] chain. - G2 (major): derive Lemma T (with the eat accounting), G, C, CP; resolve the S = 83 long-P box leak (rule ak = 2S − 1, or a band-edge clause); turn the "box" rows of proof.md §4.5 into proofs. - G5 (major): V1 parity invariant and "ak even when Push1 fires" as inductions under H1.

check_proof.py now has sections J (repairs) and K (boxes) and prints OPEN for measured gaps (K4, K5, K6).

Skeptic round 2 on proof.md (2026-10-12, stage informal_proof)

Result: STUCK. The skeptic found two fatal gaps (the window family on long right ends; the short regime), three major and one minor. None of the fatal gaps has a known repair, so the status moves from OPEN to STUCK.

Window family. Long P-mode members of H*c4 reach window E hubs: 1 at S = 83, 60 of 1,079,332 at S = 168, ≥ 96 at S = 339. Long E members reach them in two steps. The window values are 2S' − 1, 2S', 2S' + 1. This round: - Window start derived. The Clean start F_P(V, ak − S, [1,1,0], S − 1) never uses ak < 2S − 1, so it holds in the window too. Exact on 60 window right ends (check L1; scripts/round2.py window_patch). P0 − d0 = δ = ak − (2S − 1) ∈ {0, 1, 2}. - δ = 0 (S odd: P = 2, d = 2 → Absorb; S even: P = 3, d = 3 → V1 d = 1 → V1RightEnd/Push1End): ruled by existing rules (59/60 random; exact for 3 events, L2). The skeptic's δ = 0 hubs re-enter H*c4 one or two right ends later. - δ ∈ {1, 2}, and δ = 0 after Push1End with two walls (e.g. [25,6,28,13,79]): RightEndP with P ≤ 3 at a wall, or a V1 right end with walls (U4/U13). Exact runs show that the restart of a V1 right end with walls writes (10)^p (101)^q 1 (101)^r (a wall glued to a lone 1; contains 111, which no wall stack has). That is outside the grammar, so new rules and a new tape form are needed (L3, hub [21,3,38], step 3,010).

Short regime. Wider boxes (the skeptic's bounds, re-run in check_proof L6): E1w [a0 ≤ 401, b1 ≤ 40, 2 ≤ ak ≤ 90] 110 leaks; P1w (P ≤ 301) 12; Pt1 (P-mode top, one real wall) 450; Et1 and Eseg 0. The 28 "reflect not clean" hits (U24, e.g. [255,35,3] → … → P2 [1,127,82], n = 679 a top) show a further missing rule (Reflect into a top/level/window).

Derivations. - CP sketch restated: given Lemma T, CP ⟺ H1 at the successor (the round-1 choice r = e0 was circular). - V1 parity (§5.4) is now an induction over the §4 rules, conditional on H1. It uses p ≡ q only for walls that are not leftmost; the even/odd collapse wall is always leftmost. - "ak even at Push1" is not local parity: from blank, 75 of 163 EatChunk events eat a chunk with an odd six-block count (ak + B flips). It stays a census fact.

Minor. Hc4 raised ValueError on degenerate tuples (ak ≤ 0, [0]); inv4.degenerate rejects them (J2b: 60,000 fuzzed, 0 exceptions).

check_proof.py: new section L (L1-L7) and J2b. Leak counts are reported as lower bounds with their box bounds (proof.md §5.5).

Precise open lemma (why STUCK). There is a set H of right ends with K0 ∈ H such that, for every R ∈ H, the traversal from R is a finite chain of rules, and its next right end is in H. Two things are missing: - rules for P ≤ 3 right ends at a wall, the V1 right end with walls (with the glued-wall tape form it creates), and Reflect into a top/level/window; - inductive explicit clauses for the short regime.

H*c4 is not such a set. Its look-ahead clause is not inductive, and its long part leaks into window right ends at every level ≥ 83 tested.

Addendum (same round): the glued wall is transient in the one δ = 1 run followed. From [21,3,38]: V1 right end X = [(20,6)], Y = [1,10,18]; glued word at step 3,010; back in the grammar at step 4,685 as F_P(−, 17, [1,4,0], 39) (d = 2b1 + 1 + ak, the wall (20,6) absorbed: b1' = 1 + 3, P = 20 − 3); no glued word in the next 6e7 steps. So a composite rule for the V1 right end with walls (here Top-like, ak + 1 = 19 a level) probably exists; not written or validated. Free runs of 4e9 steps from the δ ∈ {1, 2} hubs [21,3,38], [25,3,17], [3003,29,678], [6101,15,1360], [6109,15,1361] do not halt.

Addendum 2 (same round): RightEndP2W, a new validated corner rule (scripts/round2.py corner_patch, not in macro_sim3): RightEndP with P = 2 at a wall (d = 1, Z empty; row U4) is RightEndP to P = 0 (b1 + 1, ak + 1, d = 0) followed by Absorb0 at V0. Exact for 2 events on the 251 of 300 random frames with 1-3 even/even walls that stay ruled that long (check M1), and the negative control (ak + 2) is never reached (M2). With WindowStart + RightEndP2W, only the V1 right end with walls stays unruled in the window family (M3: δ = 1 for S odd, δ = 2 via RightEndP P = 3 at a wall, and δ = 0 after a Push1End with two walls).