/machines/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---/rocq/log.md · raw

Machine #11 formalization log (1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---)

Round 1 (2026-10-10)

Compile helper: rocq/compile.sh file.v (temp dir, ulimit -v 8e6, one coqc).
Encoding: digits d0 u v / d1 u v, list LSB first; K ds a b := app_ds L0 ds <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{B}}> 0inf (left-side lists are nearest-cell first, so reading (10)^u is [0;1]^^u, (01)^v is [1;0]^^v).
DONE (rocq/machine_part.v, compiles in ~1.7 s): window lemmas S1-S6 (S1-S4, S6 via framework shift_rule_R/L, S5 by induction), T1-T14 (all es), Lb/Lf/Rb/Ro, chunkA/chunkC/chunkO, list sweeps LbS/RbS/RoS, M_spec, Mdrop_spec, O_spec, init : c0 -->* K [d1 1 2] 8 5 (unfold K, L0; cbn; solve_init).
Finisher that worked: apply evstep_refl'; simpl_tape; repeat (rewrite rot01 || rewrite rot10); try reflexivity with rot01 : [0;1]^^n *> (0 >> Y) = 0 >> ([1;0]^^n *> Y) (and rot10).
Next: abstract INV (proof.md §3, per-digit form with r = R of the digits above), closure, nonhalt.
DONE (same day): abstract part and nonhalt. Kill file 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v (692 lines) compiles in ~9 s, Print Assumptions nonhalt = Closed under the global context.
check_kill: PASS (exit 0; compile 9.3 s native, 0 assumptions, coqchk pass 1.8 s), output in rocq/check_kill.out.

Rof : list dg -> nat (LSB-first list): Rof [] = 0, Rof (d0::t) = 2*Rof t + 1, Rof (d1::t) = 2*Rof t. This is proof.md's R_j by structural recursion: R_j = 2 R_{j-1} + 1 - beta_j, R1_j = R_{j-1} + 1 - beta_j. So every per-digit condition is a predicate P d r p with r = Rof of the digits above and p = how many there are: AllD P (d::t) := AllD P t /\ P d (Rof t) (length t). No 2^j, no subtraction, no division in the per-digit data.
PA (class A) = canon, v >= Rd + 1, ub mod 2 = 1, p = 0 -> ub = 1 (the top condition is ubar_1 = 1). PB k (B: k=0, C: k=1) = canon, (v + bit) mod 2 = 1, ub >= 2^(p+k), k = 0 -> p = 0 -> d = d0 0 1. B's bound is then uniform: the top (0,0,1) has ubar 1 = 2^0.
F1 (carry, no drop) is one generic lemma over any P closed under the two touches (P (d0 u (S (S v))) r p -> P (d1 (S u) (S v)) r p, P (d1 (S u) (S v)) (S r) p -> P (d0 (S u) v) r p).
F2 (drop) needs no 2^k either: along the chain below the absorber, old/new r satisfy Rel r ro rn := rn+1 <= ro <= 2(rn+1) /\ (r = 0 -> ro = rn+1), which is preserved (ro' = 2ro, rn' = 2rn+1). That gives ubar' >= ubar/2 (index drops by one) and, for a top fall (r = 0), ubar' = ubar (B -> C).
F3 (overflow): Oz_AB, Oz_CA by induction, using Rof (Oz t u) + 1 = 2^(S (length t)).
Common (S, T, parity, LSB) closes by lia after repeat (rewrite pow2S in * ) turns every power into 2^m'.

Independent audit: check_kill PASS (17/17, compile 9.5 s, coqchk 1.8 s, same sha256 9a50aec8…). Fresh run for the submission at 12:20:40Z: PASS, compile 9.2 s, coqchk 1.8 s (submission/check_kill.txt).
status.json = KILLED_NONHALT / done. Package in submission/ (.v unchanged, proof.md copy with formal-status lines and a §6 lemma map, README.md, discord.md not posted).