Rocq plan for #2 (formalization prep) #

Machine #2 = 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---. Template: vendor/busycoq/verify/SOMDCv6.v, Module TM7, whose machine differs from #2 only in A1 (TM7 0RC, #2 0RF). Written 2026-10-10. This is preparation only. No proof of #2 has been written; the only Rocq for #2 is the segment probe in §3.2.

0. Summary #

1. The template route works. A top-level copy of TM7 compiles in 3.8 s with Closed under the global context, and tools/check_kill.sh gives RESULT: PASS on it in 5 s (coqchk passes in 0.8 s).
2. Most of the file carries over. With only the machine string swapped to #2, everything in TM7 compiles except two cases of RIncs_spec: an eater entering an L, and a drain pass entering an L. BigStep, the start-up from blank, and all non-L cases go through unchanged.
3. The new low-level facts are proved by the existing automation. The +1 pass is an ordinary h visit (enter as B, leave as C), and both L-entry segments emit h ++ h' ++ h^^(1+k) to the right. All 8 probe lemmas compile in 6.5 s (rocq-scratch/probe_segments_2.v).
4. The domain lemma does NOT carry over, and it is the real work. TM7 proves nonhalting with the invariant P r := exists r', RIncs hx 0 r r' ("r is in the domain"). For #2 that set is not closed: LLLL10LL1L1 is in the domain, but its image LLLLL1LLLLLLL111 is not.
   • The set image(eat) ∩ dom(eat) is closed in every test so far: exhaustive over inputs of length ≤ 12, plus about 62k random inputs of length ≤ 40.
   • Proving that closure needs a new lemma about three consecutive sweeps. Its invariant has not been found yet (§3.5).
   • A simpler fix, "the same domain with a fixed safety margin", is not closed either. Margin 2 looked closed up to length 10 but failed at length 11.
5. Size estimate. The finished file should run about 450–700 lines (TM7 has 245). Roughly 150 of those are routine. A 3-sweep domain lemma of 150–400 lines carries almost all of the risk.
6. What this means for Checkpoint A, Q2 ("extend TM7"). Extending TM7 is still the right route for the machine-facing part. The nonhalting argument needs a genuinely new idea, so proof.md must settle the invariant before any .v work.

1. Template anatomy #

1.1 Shared header (SOMDCv6.v lines 1–17) #

Framework pieces TM7 relies on (from Individual.v / Individual62.v / Longitudinal.v):

• sideRLs tm ls r1 r2. The right half of the tape, initially r1, receives the visits in ls from the left and ends as r2. Each visit (h1,h2) enters moving right in state/prefix h1 and leaves moving left as h2.
• segRLs tm ls1 ls2 w1 w2. A finite word w1 (becoming w2) turns incoming visits ls1 into outgoing visits ls2 to its right.
• segRLs_sideRLs_concat glues a segment onto a side.
• segRLs_trans, sideRLs_trans concatenate visit lists.
• segRLs_wall''. segRLs h1 h2 w w -> segRLs (h1^^n) (h2^^n) w w.
• sideRLs_1 turns a one-visit sideRLs into -->+.
• esx dispatches to solve_segRLs, solve_sideRLs, solve_init or es by goal shape.
• follow10.

1.2 Module TM7 (lines 1627–1870), item by item #

TM8 (line 1874, A1 = 0LC) reuses the same proof text.

2. Standalone TM7 copy (template validation) #

• File: rocq-scratch/TM7_toplevel.v, 261 lines, sha256 642086b1…20e59b5.
• Regenerate: { sed -n '1,17p' SOMDCv6.v; sed -n '1627,1870p' SOMDCv6.v; } > TM7_toplevel.v, i.e. the header plus the module body without its Module TM7./End TM7. lines. The body is byte-identical to upstream (checked by diff).
• Compile from a temp dir outside vendor/: coqc -Q vendor/busycoq/verify BusyCoq -Q vendor/busycoq/verify/BigInt BigInt -native-compiler yes, run under ulimit -s unlimited.
  • Wall time 3.8 s (2.7 s user, 445 MB max RSS).
  • Print Assumptions nonhalt. gives Closed under the global context.
• tools/check_kill.sh rocq-scratch/TM7_toplevel.v 1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- gives RESULT: PASS in 5.0 s total (compile 3.1 s, coqchk pass in 0.8 s, 0 assumptions). This validates the route end to end: imports allowlisted, framework fresh, top-level tm/nonhalt, and no forbidden words in upstream's text.

3. What changes for #2 #

3.1 Measured: what breaks when only tm changes #

I swapped the string in the TM7 copy and compiled it (scratchpad only, not kept):

• The first error is RIncs_spec, bullet 1 (RIncs_hx_ld). The eater's visit over ld now emits a different visit list.
• I then stubbed the two L bullets (1 and 4) in a throwaway copy that is not kept anywhere in the project. Everything else compiled: the other 8 bullets of RIncs_spec, RIncs_nxt_1, RIncs_nxt, BigStep, and the c0 -->* S' [D1] start.
• So the two L-entry segments are the only places where the machine's A1 matters.
• TM7 has no separate es/ind lemmas. Every low-level fact goes through the segment automation (esx/esc/am/wal), so no other low-level lemma touches A1.

3.2 New relation Inc and Inc_spec (segment facts verified) #

Inductive Inc: list RD -> list RD -> Prop :=
| Inc_nil: Inc [] [D1]
| Inc_d0 r: Inc (D0::r) (D1::r)
| Inc_d1 r r': Inc r r' -> Inc (D1::r) (D0::r')
| Inc_ld r r': Inc r r' -> Inc (LD::r) (LD::r').
Lemma Inc_spec r r': Inc r r' -> sideRLs tm h (toRC r) (toRC r').

Each case is cat3 plus one segment fact. The segment facts are proved in rocq-scratch/probe_segments_2.v (compiles in 6.5 s):

• segRLs tm h [] d0 d1, by esx;
• segRLs tm h h d1 d0, by esx;
• segRLs tm h h ld ld, by esx;
• sideRLs tm h 0inf (d1 *> 0inf), by esc.

Planned helper lemmas:

• Inc_total: forall r, exists r', Inc r r'.
• Inc_fun: Inc is deterministic.
• Inc_D1: the output always contains D1.

3.3 The two RIncs clauses that change #

| RIncs_hx_ld k r r1 r':  Inc r r1 -> RIncs hx (1+k) r1 r' -> RIncs hx k (LD::r) (LD::r')
| RIncs_h1_ld k r r1 r':  Inc r r1 -> RIncs hx (1+k) r1 r' -> RIncs h1 (1+k) (LD::r) (LD::r')

The other 8 clauses are TM7's, verbatim. Simulation agrees with this relation:

• rocq-scratch/py/rincs.py mirrors these exact clauses;
• out(hx,0,·) equals check_rules.eat on all 29,523 words of length ≤ 9;
• check_rules.py matches 208/208 real sweeps.

3.4 RIncs_spec: the two new bullets #

Segment facts, verified in the probe:

• Eater: segRLs tm (h' ++ h^^k) (h ++ h' ++ h^^(1+k)) ld ld. TM7's is h' ++ h^^(1+k).
• Drain pass: segRLs tm (h^^1 ++ h^^k) (h ++ h' ++ h^^(1+k)) [1;1;1;0] ld.

Both proofs are:

• rewrite lpow_add;
• then change (h ++ h' ++ h^^1 ++ h^^k) with ((h ++ h' ++ h^^1) ++ h^^k);
• then eapply segRLs_trans; [esx | wal].

Bullet shape: eapply segRLs_sideRLs_concat with the segment fact, then eapply (sideRLs_trans (ls1:=h)); [apply Inc_spec; eauto | eauto].

TM7's cat3 ends in [|eauto 1], which cannot find the sideRLs_trans split, so these bullets are written out (about 4 lines each).

3.5 The domain argument (main risk) #

TM7's invariant fails for #2. Script: rocq-scratch/py/domain_facts.py.

• Over all words of length ≤ 10, TM7's map keeps its domain (12,491 words, 0 escape).
• #2's map does not: 8 of 26,019 domain words map outside the domain.
• Over words of length ≤ 12 that end in 1, 230 domain words map outside the domain.
• Worked example: LLLL10LL1L1 → LLLLL1LLLLLLL111. On the second word, the eater reaches the tail 10001 with k = 13. The 1 becomes L, and the drain of 0001 then needs 15 passes but has 12.

So RIncs_nxt has no #2 analogue with any condition on (tp, k, tp', k'). I derived this by hand and the measurements back it: the constraints forced on a bound g(k) are contradictory (g(k+2) ≤ g(k)+1 versus g(k) ≥ k−1).

What holds instead (tested, not proved):

1. Commutation lemma RIncs_Inc: RIncs tp k r r' -> Inc r' r'' -> RIncs tp (1+k) r r''. In words, a +1 applied to a sweep's output is the same as one more pass in that sweep.
   • It holds because the count-mode digits encode the leftover passes in bijective base 2 (D0=1, D1=2, terminated by D1), and Inc is exactly bijective +1 on that code.
   • Checked on 659,938 cases (all words of length ≤ 8, k < 40).
   • Proof: induction on the RIncs derivation, inverting Inc. Every case closes with one constructor and the IH; the D0 cases need mod2 arithmetic. Estimate 40–60 lines.
2. image(eat) ∩ dom(eat) is closed under eat.
   • 0 failures exhaustive: 26,011 image words from inputs of length ≤ 10, and 197,471 from inputs of length ≤ 12.
   • 0 failures random: about 62k image words from inputs of length ≤ 40.
   • The real orbit lies in this set, since every config after S(1) is an image.

Proposed proof shape:

• Invariant: P r := (exists r0, RIncs hx 0 r0 r) /\ (exists r', RIncs hx 0 r r').
• Start: S' [LD;D1], reached at step 16 from blank (by simulation; esx should do it as for TM7). P [LD;D1] holds via r0 = [D1], with r' = [LD;LD;LD;D1;D1], which matches the step-91 config.
• Key lemma (new): RIncs tpA a s r -> RIncs tpB b r r' -> Cond(tpA,a,tpB,b,tpC,c) -> exists r'', RIncs tpC c r' r''. It describes three sweeps A, B, C side by side, digit by digit.
  • A +1 fired by B on its rest becomes a+1, by RIncs_Inc together with Inc_fun and RIncs determinism. A +1 fired by C becomes b+1.
• Induction: on a measure of the middle word r, e.g. length r + 2*(count of LD in r). This strictly drops every step even after B's Inc. TM7's structural induction on r fails here, because the sub-derivation runs on Inc r.
• Unknown: Cond. The harness rocq-scratch/py/joint.py replays the three sweeps jointly; it agrees with direct composition on 1678/1678 samples. Its data, over all inputs of length ≤ 11 where A and B succeed (71,695 inputs, C always succeeds):
  • only the mode triples xxx, 1xx, 11x, 111 occur (A's mode ≥ B's ≥ C's);
  • b >= a and 2c >= b hold at every position;
  • 111 occurs only after A has finished (a = 0).
  • Neither 2c >= b nor a TM7-style pairwise condition is inductive on its own. Hand-checking the 111 transitions breaks both, so Cond must use a and the phase (A still reading, at the right end, or finished). Finding it is the first job of proof.md.
• Shortcut tried and ruled out: a fixed safety margin. The real orbit has large slack: at count-mode entries, k exceeds the passes needed by at least 2 in the first 400 sweeps, and usually by hundreds. So I tested "the sweep still succeeds if each eater-to-count switch hands over fewer passes". Script: rocq-scratch/py/margin.py.
  • Each variant holds on the real orbit, but none is closed under the real eat.
  • Margin 1 fails on 8 words of length ≤ 10.
  • Margin 2 has 0 failures at length ≤ 10, which looked promising, but 38 at length ≤ 11 and 16 of 8,198 random words.
  • Halving the count fails on 3,240 words; taking 3/4 of it fails on 64.
  • The failures repeat the …1 L^a 111 pattern of the counterexample above, at larger sizes.
  • A TM7-style condition also fails on the margin-2 domain. The least k' that works for an hx count k is [0,9,1,10,6,11,7,12,8] for k = 0..8: not monotone, and parity-driven (margin_cond.py).
  • Any quantitative invariant would have to scale with n, the length of the L-run. That route is untested.

3.6 BigStep and nonhalt #

• BigStep is unchanged, verified by compile in §3.1.
• nonhalt changes only in P, the start (S' [LD;D1]) and the closing step. Three facts close it: the new key lemma, RIncs_Inc, and the witness r itself for the image half of P r'.

3.7 Size estimate #

4. Tactics to reuse, and pitfalls #

Reuse:

• cat3 / tr1 / wal / tr2 / am / esc unchanged.
• The rewrite lpow_add + change (… ++ h^^k) + segRLs_trans; [esx | wal] pattern for any visit list of the form "fixed prefix, then k copies".
• mod2 / sub from DivModCases for parity and predecessor case splits, as in TM7's RIncs_nxt.
• gen + inverts (LibTactics) for derivation inversion.

Pitfalls (each hit while probing):

• Open Scope nat turns list literals into list nat. [1;1;1;0] fails as a list Sym. Declare word notations (e.g. Notation w1ld := [1;1;1;0].) before Open Scope nat, as TM7 does for ld/d0/d1.
• Use 0inf, not const 0, for the blank side. const 0 is read as Stream nat.
• cat3's [|eauto 1] will not combine Inc_spec with the IH. Write the sideRLs_trans split explicitly.
• TM7's solve_v1/solve_v2 are tied to its case order. The new domain lemma needs its own automation.
• Inducting on the derivation gives no IH for the Inc premise. That is fine for RIncs_spec. For the domain lemma, use the measure induction described in §3.5.
• check_kill reads raw text, comments included. Keep the forbidden words out of the final file, even in comments (see rocq-notes, "Trust base"). The stub run in §3.1 lived only in the scratchpad.
• Stack, native and timeouts are not an issue at this size.
  • TM7 needs no ulimit change in practice; it is set anyway.
  • Native compile adds about 1 s.
  • coqchk finishes in under 1 s, far below the 600 s cap.
  • esc's vm_compute fallback (T:=10^6) is never reached by the probes; BoundedConfig with T:=10^3 suffices.

5. Files #

• rocq-scratch/TM7_toplevel.v: standalone TM7 (check_kill PASS with TM7's string).
• rocq-scratch/probe_segments_2.v: #2 segment probes (8 lemmas, all Qed).
• rocq-scratch/py/rincs.py: #2's RIncs as a function. It checks equality with check_rules.eat and the commutation lemma.
• rocq-scratch/py/domain_facts.py: the closure counterexample and the image∩dom closure test.
• rocq-scratch/py/joint.py: the 3-sweep joint harness, for testing candidate Conds.
• rocq-scratch/py/margin.py, margin_cond.py: the ruled-out fixed-margin invariants (§3.5).

Reproduce the data: cd rocq-scratch/py, then run:

• python3 -B rincs.py (about 1 min);
• python3 -B domain_facts.py 10 (about 2 min);
• python3 -B joint.py (about 5 min);
• python3 -u -B margin.py 2 11 40000 300 (about 15 min).