W7-2 · 1RB1LB_1RC0LA_1RD0RE_1LA0LB_1RF---_1RB1LD (740 line 175; family: line 489)

Status: CHECKPOINT_A (observe, table level, 2026-10-14, about 1.5 h of the 2 h stage-1 budget). Confidence on the mechanism: high for 175, med for 489. Class: sheet "Skelet 1-like Class 1". Ours: an exponential counter that settles into an exact macro cycle M(X) -> M(2^36 X + 9575900996480) (175); 489 is still in a deeper "two far fields" regime at 1e1181 steps. Viewer: https://bbchallenge.org/1RB1LB_1RC0LA_1RD0RE_1LA0LB_1RF---_1RB1LD

Checks

• Byte-exact: 740 line 175 = 1RB1LB_1RC0LA_1RD0RE_1LA0LB_1RF---_1RB1LD; line 489 = 1RB0RC_1LC1RC_1LD0RB_1LA0LE_1LF---_1LC1RA.
• Same table: canon(489, A) = canon(175, D) = 1LB0LC_1RC1LC_1RD0LB_1RA0RE_1RF---_1RC1LA (489 is the same table from start D, mirrored and renamed). Starts B, C, E, F of the table are not on the 740 list. Start F = 1RB1LD_1RC0LE_1RD0RF_1LE0LB_1RB1LB_1RA--- is upstream Eqv_v2.v TM595 (tm = start F, tm' = 175, halting-equivalent; neither side is proved). eqv_1590 lines 503/504/2229/2255 are this table.
• Not K42: neither line is in reports/k42/members.tsv or members_d2.tsv.
• Ledger first (tools/attempts.py query): 8 rows, none a proof attempt; the Wave 7 planner and critic rows (qsim 1e2596, doublings 2x+c, refilled far end) are the only table-level work. No machines/ dir before today; no Astra claim; claimed as Wave 7 W7-2 in coord/claims.tsv.
• Halting condition: E is entered only by C1 (0RE) and C only by B0 (1RC), so the machine halts exactly at B> 0 1 1 (B reads 0 with 11 right of it).

Runs (every start)

Mechanism

Words: every long run is a power of a 4-cell word, either a 3-ones word (rotations of 0111) or a 1-one word (rotations of 0001). The head sweeps the whole tape; a right sweep turns 1-one words into 3-ones words and the left sweep turns them back.

1. Visit level (compress). Between events a marker crosses a run one word per left-end visit and turns each word it passes into two words on the other side: (0100)^a 11 (0001)^b goes to a+2, b-1 per visit (75 visits in a row at 1e9). That is the doubling transfer b -> 2b + c. Other phases add a small run to the big one (Z -> Z + const) or move the big run across a separator unchanged.
2. Segment level (qsim records). Each qsim rule application ends a segment whose big field changes by Z -> a Z + b with a in {1, 2, 4}. No segment ever halves a field.
3. Cycle level (175). From record 21 (step 4,111,147,719,584,449,981 = about 4.1e18) the record sequence is exactly periodic with period 42: M(X) = 0^inf 1 1011^X 10111110 1110^26 <A 01010100010000010001000100001 0^inf M(X) -->+ M(2^36 X + 9575900996480). All other fields in the period are constants (26, 28, 80, 78, 20, 18, 16, 82, 12, 10, 8, 922, 6, 1004, 2020/2024, 4072/4074). The map holds exactly for all 56 observed periods, starting from X0 = 508,932,080; X_k ≡ 0 (mod 64) for k ≥ 1 (X0 ≡ 48), and 2^36 X + c keeps X ≡ c (mod 2^36), so every parity condition inside the period sees the same residue every time.
4. Base-level validation (scripts/segval.py, work/segval175.json). Each of the 42 segments of the period was fitted as Z -> a Z + b (exact over all observed periods) and then re-run by plain TM simulation from the constructed configuration with small random Z of the same residue mod 64: 165/165 passed (every segment 2-4/4). The composite of the 42 fitted maps is X -> 68719476736 X + 9575900996480 = 2^36 X + 9575900996480, the same as the observed one. A mod-4 rerun with Z in 30..300 (work/segval175_mod4.*) was still running at write-up; the start X0 ≡ 48 (mod 64) already shows the period needs at most X ≡ 0 (mod 16).
5. The parity-flagged rules (stop-rule check). qsim's 3 collatz-flagged rules on 175 (15, 37, 58) eat a left field two words at a time (01110111^-2 per application) while a right field loses 1. Rules 37 and 58 are used once per period (119/118 uses in the planner's 90 s run, about 119 periods); rule 15 is transient only. Every field in a period is either a fixed constant or an affine function of X with X fixed mod 2^36, so the field these rules consume two at a time starts each period at the same value or the same residue, and the endpoint parity is fixed. The 42-segment base validation (point 4) covers both rules' segments.
6. 489 is in a different regime. Its far end (mirrored, on the left) holds two huge fields Y1 = 939,468,133,961,604,904 and Y2 = 10,456,559,309,013,950,600 (record 183). The record sequence is periodic with period 40 (8 rounds): D(Y1, Y2, X) -> D(Y1 - 48, Y2 - 240, 2^40 X + 377451701380050). Y1 runs out first, after 19,572,252,790,866,768 periods (Y1 mod 48 = 40; Y2 mod 240 = 200; Y2 is then 5,759,218,639,205,926,280), with X about 2^(7.8e17). Earlier, 489 already pushed one accumulator into its far end (4 90 X18 -> 64 X18 242 8392), i.e. the "big block becomes the far-end digit list" event, so its depth grows like a tower. What happens when Y1 runs out is unknown: it can only be reached symbolically (residues of Y1, Y2, X).

One argument for all starts?

No. 175 reaches the one-field cycle M after a short transient (21 qsim records, about 4.1e18 steps). 489 has two far fields of size 1e18 and 1e19 that are consumed linearly at tower depth; whether it ever reaches M (or halts) is decided by the exhaustion events of those fields, which the plan's "differ only in high digits" did not anticipate. A delta for 489 needs new rules (the D-regime and its exhaustion events), so by the plan's delta rule it stops; it is filed as a separate park-or-fund decision (decision.json).

Template

• Nearest: our kill #3 (machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/, Skelet 1-like Class 2): Individual62, one macro lemma per segment, progress_nonhalt. Here the invariant is simpler: exists m, c = M(16 m) (or the residue class mod 64), with the 42-segment chain as one M(X) -->+ M(2^36 X + c) lemma.
• Sk1Machines.v (Sk1CounterMixed / Sk1Auto): does not fit the cycle (no periodic digit words), but Sk1Auto's checked accelerated run is an option for the 4.1e18-step base segment.

Cryptid check

• 175: not cryptid. No halving, no residue split: one affine map with fixed small constants, entered after a finite transient.
• 489: no halving seen; the residue question (what the Y1 exhaustion event does) is open and lives at tower depth. Not called cryptid; filed as a decision.

Proof stage (2026-10-14, informal_proof)

• proof.md covers both starts with one invariant {N(Y): Y >= 22} u {Q(W): W >= 14} (4-cell blocks). Lemma N: N(Y) -->+ N(2^18 Y + 32859022); Lemma Q: Q(W) -->+ Q(2^18 W + 34431880). The 42-record qsim period is two N half-cycles; no residue condition is needed.
• Start A: blank --> N(508932094) (qsim M(508932080) + 14). Start D: blank --> D(X0, 10456559309013950571, 939468133961604901) (8.86M engine moves); Lemma D D(X, Y2, Y1) -->+ D(2^20 X + 349479900, Y2 - 120, Y1 - 24) (= qsim's 40-record map with X_q = X - 10) applied 39,144,505,581,733,537 times; the Y1 exhaustion absorbs Y2 and enters Q(2^33 z + 23036877419765819664) in 339,452 moves. The "tower" feared above does not happen.
• Tool: scripts/engine.py (4-cell block steps, chain steps, Diff rules proved by symbolic runs, linear forms in one parameter). check_proof.py §A-§G ALL OK (~4 min).
• The old decision card (park/fund 489) is retired to decisions/2026-10-14-superseded.json (unanswered, moot).

Attempts

• 2026-10-14 claude observe (table, lines 175/489): sims 1e10 both starts, qsim 120 s both, compress 1e9 both, qsim rule-application traces 40 s both. Result: 175 enters the exact cycle M(X) -> M(2^36 X + 9575900996480) at about 4.1e18 steps; 42/42 segments base-validated (165/165 runs). 489 is in a two-far-field regime D(Y1,Y2,X) -> D(Y1-48, Y2-240, 2^40 X + 377451701380050) with Y1 about 9.4e17; its exhaustion event is not reachable by simulation. Ledger rows appended.
• 2026-10-14 claude hand-proof (table, lines 175/489): proof.md + check_proof.py (ALL OK). Start-parametric: N cycle (start A) and Q cycle (start D), Lemma D with 3 parameters, exhaustion run into Q. Result: both starts covered at the informal level; next is formalization. Ledger rows appended.