W6-1 planning stage: independent check (2026-10-14)

This is a check of the formal-planning stage (W61Exit.v, W61Plan.v, plan.md). It was made from a fresh compile in a separate directory. None of the author's files were edited.

Verdict

• The exit is real. W61Exit.v recompiles with no Admitted, admit or Axiom. Every lemma rests on nothing, or on functional_extensionality_dep only. The statements say what proof.md says for T2, O, C and E′/E″.
• The reduction in W61Plan.v is not valid yet. The Admitted tail_round is false as stated: two counterexamples are proved in Coq below. From the four open statements you can therefore prove False, so "nonhalt follows from exactly 4 open statements" proves nothing yet. The repair of the statement is small. The repair of the invariant behind it is real work, and part of it is not in the plan.
• The estimate is optimistic. The plan says about 10 stages (range 9-12), about 20 h. My estimate is about 14 stages (range 12-18), about 28 h. The decision card should be corrected (section 6).

1. Recompilation

Setup:

• a fresh directory with copies of the three files;
• Coq 8.20.1, switch bb6, ulimit -s unlimited, ulimit -v 8000000, nice -n 10;
• one coqc at a time, with pgrep -xc coqc = 0 before each one.

SOBCv10.v was compiled from scratch rather than reusing the author's .vo.

The vendor SOBCv10.v, upstream cdaf693:verify/SOBCv10.v and rocq/build/SOBCv10.v have the same sha256. The rocq files and their build/ copies are identical. git status in vendor shows only the untracked .coq-native/ from 2026-10-09. Nothing in vendor/ is newer than proof.md.

2. Assumptions, lemma by lemma

Print Assumptions on every lemma in the report's "proved" list:

A grep of W61Exit.v finds no Admitted, admit, Axiom, Parameter, Hypothesis, Conjecture, Abort or guard switches.

tm61 prints the 12 transitions of 1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF, the string at line 10 of the 740 list. perm and nonhalt are a correct mirror-and-rename bridge (A..F to D,E,F,A,B,C, our start = SOBCv10's state D).

3. Do the statements say what plan.md and proof.md claim?

C (cycler). Busycoq's notation l {{q}}> r puts the head on the first cell of r, in state q. So (rev Yw *> L) {{B}}> 0inf is "L, then Y, then the head in state B on the first blank cell". Yw is proof.md's 70-cell Y, cell for cell.

• cycler_step gives L Y B> to L 100 Y B>, for every L.
• cycler_nonhalt gives ~ halts from that configuration for every L, through busycoq's progress_nonhalt_simple.

So C really is nonhalting from the cycler entry. Lemma O ends exactly in that form: overflow_base ends in (rev Yw *> [0;1;0;1] *> l) {{B}}> 0inf.

O (overflow). overflow_base is proof.md's Lemma O with w = 1: B U^13 B t becomes 1010 Y B>, with l never read. overflow_column and overflow_columns extend it to any all-B layout through SOBCv10's raw_B_forward and raw_Us_to_Xs. This matches proof.md section 5.4.

T2 (raw pass). It matches proof.md section 3 and opening family (c):

• tail_word k is U^(2k+1) B t.
• y_after k is the level k − 1 word of proof.md's table (A, B, E t, D t, A t, B t).
• raw_tail_columns: every column B^(e+1) becomes E^e A, the last one becomes E^e, the U run grows by one pair, 101 is written on the left, and the head comes back in state F.

"Any column layout" means any widths with every digit B. That is the only case that occurs, because the raw pass starts at a trigger, when the counter is all B.

E′ and E″.

• nested_pre_left is proof.md 5.2's list identity.
• nested_launch gives E′ its S f calls, with the far end never read.
• nested_required es e is proof.md's h″ − 1. I checked this by hand for one column, 3(2^b − 1), and for two columns, 3·2^(a+b) − 2^a − 3, against h″ = 3·2^(W−1) − S − 2.
• With f = h_t − 1 = 4·2^W − S − 3, the hypothesis nested_required es e <= f of nested_exit holds with margin (5/2)·2^W, as proof.md 5.3 says.

What remains open is that exception 9 actually reaches nested_exit's configuration (exception_call_left c f, then B>, then an all-B layout, then U^11 B t). That is tail_round_trigger's job, as plan.md says.

Two small slips in plan.md, neither of which matters:

• The report counts 98/200/344/502/696/910 steps, which is run_c 97 etc. plus one.
• columns_step_exists is at SOBCv10 line 2589, not inside the quoted range 3159-3310.

4. Problems in the open statements (W61Plan.v)

4.1 tail_round is false as stated (proved)

Both lemmas below compile, and Print Assumptions lists only tail_round.

(a) k = 4 without a trigger. Take current = 100, previous = 10, zs = [], last = [SB;SA;SA] (value 1, length 3), k = 4, lv = 5.

• The precondition holds and tail_triggers is false, since eff_level = 4.
• The conclusion asks for tail_round_pre … (S 4) …, whose field tp_k says 5 ≤ 4.

This is tail_round_false_k4 : False.

(b) A last column of length 2. Take last = [SD;SD] (value −3), k = 1, lv = 4.

• The precondition holds.
• The conclusion asks for length last' = 1 together with tp_last_len : 2 <= length last'.

This is tail_round_false_len2 : False.

The chain in sobc_D_nonhalt uses only k = 1, 2, 3 and lengths 29 to 26, so the statement fix is two hypotheses: k <= 3 (or tp_k : k <= 5 in the conclusion) and 3 <= length last. Until then, the four Admitted are inconsistent.

Proof skeleton of (a), from W61Check.v:

Definition cx_last4 : list SDigit := [SB; SA; SA].
Lemma cx_pre4 : tail_round_pre 100 10 [] cx_last4 4 5.  (* constructor; lia / vm_compute *)
Lemma cx_not_trig4 : ~ tail_triggers 4 cx_last4 5.      (* vm_compute *)
Lemma tail_round_false_k4 : False.
Proof.
  destruct (tail_round _ _ _ _ _ _ cx_pre4 cx_not_trig4)
    as [zs' [last' [lv' [_ [P _]]]]].
  destruct P as [_ _ _ _ _ Hk _]. lia.
Qed.

4.2 The draft precondition is not inductive

Forall column_safe zs does not survive a step. SOBCv10's own column step breaks it. A width-4 column of value 3 whose right neighbour is even steps to 2^4 − 1 = 15 > 2^4 − 6. This is safe_not_preserved, which is closed.

SOBCv10 carries columns_schedule, the abstract schedule theory at lines 3345-3790, for exactly this reason. With a tail, the rightmost z-column steps with the last column's parity, not with the constant true of SOBCv10's abstract_columns_next. So that theory is not reusable unchanged, although plan.md lists it as reused unchanged.

Only 4 rounds are needed, so SOBCv10's lineage_inputs_safe (line 942, which takes arbitrary input parities) looks like the right tool. That is new glue, and the plan does not include it.

tp_last_window does not survive a step either. The last column's law v → 2^(w−1) − ⌊v/2⌋ keeps the upper bound only when v ≥ 12. The window also admits small and negative v.

It does hold on the real trajectory. I recomputed proof.md section 4, deficits included:

• 391,468,375 → 72,701,269 → 97,867,094 → 18,175,317;
• the signed values are 72,701,269 − 2^28 and 18,175,317 − 2^27;
• eff_level is 3, −1, 4, 0.

Suggestion. The last column is concrete in all four rounds (29 to 26 digits, known values). Pin it in the precondition, or state four round lemmas with the concrete last column. That avoids a general signed-digit invariant, and it is also the plan's own fallback for the T3 risk.

5. Is the estimate honest?

It is optimistic by about 40%. The plan's top value (12) is at the bottom of my range.

Why the opening costs more than 2 stages:

• Families (a), (b) and (d) are new dynamics on words with C/t markers and D/E digits (B^m C t C A^2 t^2, A^p C A^m D^2 A U E A). They are not SOBCv10's words.
• The closed forms of (b) and (d), with (1292·2^m + 4)/3 and (140·2^m + 4)/3, were checked on only 11 and 9 small pairs. Their induction proofs start from scratch.
• n4 = 3·2^29 − 2 is a nat, and the entry has 2^n4 terms. One stray cbn or vm_compute on n4 builds 1.6·10^9 constructors.

Plan.md's own line counts point the same way: 800-1,200 generalized lines plus 600-900 new opening lines is about 1,400-2,100 hard lines. That is more than any kill in this repo so far, and those took 500-1,800 lines, mostly adapted from a close template.

The re-ask after R4 is a good control, but by then about 8-10 h are spent and the opening, the other big unknown, has not started. A cheaper order would be:

1. the statement repair (4.1) and the invariant design (4.2), half a stage;
2. a spike proving family (b)'s closed form, the least checked claim;
3. then R2 onward.

6. What the decision card should say

• Effort: "about 14 × 2 h (range 12-18)" instead of "about 10 × 2 h (range 9-12)".
• The rationale line "W61Plan.v reduces nonhalt to exactly 4 stated lemmas" should become: "…to 4 stated lemmas; one of them (tail_round) is false as stated and is restated in R1 (independent check)".
• "Low risk of a wrong claim" is fair about the machine, since the exit is proved and the mechanism is robust. It is not yet true of the formal round statements.

Reviewer's files (scratch, not part of the machine folder)

• /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/w61check/W61Check.v: Print Assumptions for every lemma, the two counterexamples, safe_not_preserved.
• /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/w61check/cc.sh and build1.out: the build script and its log.