W7-1: table of line 75 (1RB1RC_1LC1LE_1RD0RA_1LB0RA_0LD1LF_1LD---), observation

Wave 7 pick W7-1 (reports/wave7/plan.md). Claimed 2026-10-14 (coord/claims.tsv). Observe stage, about 2 h.

The four listed starts

• Byte-exact: line 75 of data/holdouts/BB6_holdouts_740.txt is the string, byte for byte. The start map comes from canon(tm, s) (scratchpad starts.py).
• Direct runs of every listed string to 1e10 (C core): no halt. Spans (in table order 75 / 597 / 265 / 179) 266,777 / 266,785 / 266,829 / 266,825 cells. At 1e10 the four tapes are identical except the far-left field (20 / 24 / 46 / 44) and the head phase. Logs: data/direct_<line>_1e10.jsonl.
• qsim and compress for 75 were already run by the planner and the critic (reports/wave7/plan-data/critic/). They are not repeated here, because the exact simulator below replaces them. qsim at block 2 gives 951/951 parity-flagged rules. The reason is below: the parity of each field is a counter bit.

Notation (tokens)

At every D:R event (transition C0 -> 1RD at the right end), the tape is

0^inf  [f_1] s_1 [f_2] s_2 ... s_{k-1} [f_k]  00 11 D> 0^inf        [f] := (10)^f 1

• A field f is a run of 1s with single 0s between them: 1 (01)^f.
• A separator s is the gap between two fields:
• | is 00 (gap 2), the normal one;
• + is no extra 0 (gap 0, 11); these appear after a bounce;
• # is 000 (gap 3); this is a dead field.
• The last field L = f_k is the growing end; P = f_{k-1}.
• Tools: work/tokens.py (build/parse) and work/fields.py.

Mechanism: a binary counter whose digits are field parities

• Each half-cycle runs from one D:R to the next. The head walks left from the right end, over even fields joined by |, and stops at the first odd field (or at a + or #). Then:
• ODD: the field just left of the stopping point loses 1;
• PLUS: at a +, the field left of it loses 2 and the + becomes |.
• In both cases L grows by 3, so the parity of L flips every half-cycle.
• So the parities of the fields are the bits of a binary counter. L's parity is the clock, P loses 1 every second half-cycle, the next field every fourth, and so on: a ruler sequence.
• Fig counter_parity_3e8 shows this.
• The turning depths of the head at 3e8 follow the same ruler pattern (positions 13.2k / 10.9k / 10.5k / 3.5k / 2.5k).
• Fields are budgets. They decrease, except L and the +1/+2 that a bounce gives.

Rules (exact; random-instance validated; steps fitted with 0 residual)

• In the steps column, S is the sum of the fields from the stopping point to L, and n is their count.
• Evidence: work/validate_events.py, data/validate_events.json. ODD and PLUS were checked in-session; their scripts are inline in the session.
• Not yet fitted as closed rules. They occur only near the far end, and the oracle handles them exactly:
• PLUS with left field 1: 1 + x -> x at the far end, or a merge a + 1 + b -> a + (a+b+1)-style inside;
• the first field decremented (d = 0);
• a 0-field with nothing to its left (0 | x -> x).

Events, classified (orbit of 75, oracle calls to 2.37e14; work/classify.py data/far_A.jsonl)

• This answers the plan's four events:
• (a) Interior death, both parity cases. A death is | 0 | -> # when the left separator is |, and an immediate merge when it is +. A # then works as a counter digit: it acts odd once, and then the next carry into it is the uniform re-pairing bounce. These are the two zero events the critic saw at about 1.35e9 (237 # 247) and 1.75e9 (2990 # 9593).
• (b) Pair birth. A new L = 1 is born at every bounce, both the # bounce and the far-end overflow. The old L becomes an ordinary field.
• (c) Far-end death. See below.
• (d) Halt. Not reached anywhere: direct runs to 1e10, the exact simulator to 2.37e14, and 35 × 12 hand-built far-end events.

Exact accelerated simulator (work/accel.py)

• It applies the ODD and PLUS fast rules. Every other half-cycle goes to the oracle: the real TM (C core) runs from the rebuilt tape to the next parseable D:R. The simulator is exact by construction.
• Validated: for all four starts, the token list at the first D:R at or after 1e10 equals the direct simulation at that exact step, with state D moving R (data/validate_1e10.jsonl, 4/4 match).
• Far runs (A = 75 and C = 265): 2.367e14 steps, no halt, 203 oracle events each. The runs stopped on a MemoryError, because the oracle builds the full tape (39 M cells at 2.4e14). Logs: data/far_A.jsonl, data/far_C.jsonl.
• A and C go through exactly the same events at the same times. Their first fields always differ by exactly 26 (the four starts differ by even amounts at 1e10). At the 2.4e14 end they have the same 24 fields; only 2 vs 28 after the prefix 1 + 0 | differs.

History (line 75)

Far end (event c)

• The far end loses about 1 unit of the first field per factor of about 1.5 in time. Each far-end bounce adds 1 or 2.
• Line 75's first field reaches 2 at 2.4e14, so its natural far-end death is due soon after. 265 is 26 units behind, 179 is 24 and 597 is 4.
• Hand-built far-end deaths (work/farend_small.py, data/farend_small_{a,b}.txt):
• Setup: the real far-end block at 2.4e14 (122 | 292 | 34 | 2114), with prefix ∈ {none, 1 +, 0 |, 1 + 1 +, 1 + 0 |} and first field v = 0..6, followed by a short right part (3000 | 3001 | 2000) so that overflows come quickly.
• All 35 variants ran 12 far-end events each: no halt.
• The dead first field disappears and the next field (122) becomes the first field, eaten one unit at a time.
• Prefix shapes seen: 1 +, 0 |, 1 + 1 +, 1 + 1 + 1 +, 1 + 0 |, 0 # x, 0 + x, 0 | 0 |, 1 + 2 |, x + y. A small set, but not yet shown to be closed.
• The far end eats fields one at a time, and births at the right replace them. It does not glue new structure the way K42's escapes do.

Halting

• The machine halts only via B reading 1 with 11 to its left (B1 -> E, E1 -> F, F1 halts).
• Random tiny token lists (4,000 lists, fields 0..8, separators | + #) halt in 255 cases (3 | 4, 4 | 1, 0 + 0 + 4 | 6, ...). So a proof needs an invariant that excludes the bad local patterns. Tiny far-left fields alone are not bad; the hand-built deaths above survive.

Cryptid check (stop rule)

• Not a cryptid stop.
• Every event is a fixed affine map on the field list with a case split on parities.
• The parities are the digits of a binary counter. L's parity alternates deterministically, and the other fields' parities flip only when they are decremented or bounced.
• Nothing branches on a residue other than mod 2 of a counter digit. There is no x·m/k growth law; the only growth is L + 3 per half-cycle.
• The four starts share every event through 2.37e14.
• The qsim "Collatz" flags are this counter, which is the critic's point (1).
• Points (2)-(4) of the critic are answered above: far-end deaths are built by hand and survive; birth = bounce; the word set is the same as W4-6 but the mechanism is now explicit.

Template check

• Nearest kill: #3 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (Skelet 1-like Class 2). It is a binary down-counter on explicit digit blocks s(d), with merges and a re-pairing overflow. Its proof uses one macro rule per decrement and a per-step invariant J.
• Applies partly. The architecture carries over: a rule per half-cycle, merges, a re-pairing bounce, and an invariant on budgets with the parity defects held by the slow blocks.
• Differences: here the digits are the field parities (no digit blocks); there are 3 separator kinds plus far-end prefixes; and births happen at every bounce.
• Upstream Sk1Machines.v (mxdys, Sk1Counter with 6-phase digit words) and Sk1like_TC_v*.v (K42's) are not templates: different word sets and digits.
• One start-parametric argument covers all four lines. The starts merge into one orbit up to the first field (all even offsets, identical event times through 2.37e14). Each extra start is a #24-style delta: its own base segment to a common token-list family.

Attempts

• 2026-10-14 claude observe (table, lines 75/179/265/597): mechanism found; 9 token rules random-validated; exact accelerated simulator validated at 1e10 on all 4 starts; no halt to 2.367e14 (A, C); far-end deaths built by hand survive. Not a cryptid stop. Ledger rows added.
• 2026-10-14 claude hand-proof (table, all four starts): proof.md revision 1, OPEN. Proved: sweep lemmas, 15 macro rules with exact steps, outside-case list, region counter calculus (C1-C6), opening runs to K(c) = c | 66 | 18 | 64 (c = 47/51/73/71 at steps 30379/30722/32795/32668), start-parametric lemma SP, legal-event lemma (J => a rule applies). Open O1: J is not inductive (budget clauses B1-B5, nested deaths, far-end prefix table). check_proof.py PASS (data/check_proof.out); abstract map to 1e16 on all four starts with no outside case (data/abstract_runs.md). Ledger row added.
• 2026-10-14 claude hand-proof revision 2 (after the skeptic review of revision 1; table, all four starts): fixed both major gaps (C3 merged state for every merge event, two-mode climb automaton C5, reflection C6 with D-end/U-end branches; far-end rules FAR-0-PLUS-EVEN 6S+6n+30 and FAR-0-PLUS-ODD 6S+12n+8, checked exhaustively and on 400 random instances; J3 relaxed) and all minor gaps. Fatal gap O1 stays open. New: an exact fast map (C1/C2 jumps, exact step counts, equal to the plain map event for event to 1e11) runs the four starts to 1e100 (check_proof.py §I) and 1e150 (work/rev2/far.py) with no outside case; but 24 of 300 perturbations of line 75's 1e13 configuration leave the rule set (22 at the far end) between 1e14 and 1e85 steps (3 reach the halting + 0 +), the 22 far-end exits are (o4) 14, (o7) 5 and the halting (o1) 3; the other 2 are bulk (o5) from a planted small L. So the far end decides halting by a race on history-dependent parities: cryptid-protocol stop, status STUCK, decision.json (recommended: bounded halting search toward 1e1000). check_proof.py PASS A-I (data/check_proof.out). Ledger row added.