[TomZahavy]

Summary

This PR introduces three structural reduction predicates in BusyBeaver/Defs.lean (HasStackReduction, HasOdometerReduction, and HasTransducerReduction), formalizes 9 community-documented bbchallenge Wiki machines under these three predicates, and adds 20 open BB(6) acceleration problems across stacked, odometer, and transducer dynamics in BusyBeaver/BB6/Accelerations/ — including 13 higher-level Poincaré / epoch accelerations (HighLevelState) that contract multi-step drains, carry sweeps, and transient modes onto minimal single-stack or single-mode sections (335 -> 424 theorems across 59 -> 88 machines in BusyBeaverChallenge.lean and comparator/busy_beaver.json).

1. Structural Reduction Predicates (BusyBeaver/Defs.lean, BusyBeaver/BB6/Accelerations/Stack.lean)

• HasStackReduction: Closed two-sided variable-length digit-stack system (StackTuple, IsValidStackModes with bounded HalfTapeView prefixes ≤ 8) with non-blank/blank block recurrences (stackDigit, stackSepLen), non-surjective head-symbol boundaries, certified ReachesPlus closure from init [], blank-tape reachability of a multi-digit stack (3 ≤ L_g.length + R_g.length), and an arbitrary-depth stack-frame transfer transition (with 1-digit helper HasStackReduction.of_oneDigit in Stack.lean).
• HasOdometerReduction: Closed mixed-radix odometer stack + active bit-stream system (evalOdomR / evalOdomL) with certified decrement (cap (dec stk) = cap stk - 1), zero-capacity drain (drain), 0-bit reflection, unconditional ReachesPlus step partition and closure over all (stk, w), and blank-tape reachability of a non-trivial odometer stack (2 ≤ stk₀.length ∧ 1 ≤ cap stk₀).
• HasTransducerReduction: Closed bidirectional macro-word transducer (IsValidTransducerModes, iterTransducerMacro) over strict-sub-Kraft block alphabets (kraftSum) with certified orbit expansion, a non-bypassable multi-token halting exit gate (exitNext), and unbounded sweeps in both directions.

2. Formalized bbchallenge Wiki Machines (9 Machines)

• Stacked (HasStackReduction, 6 machines):
  • M_1RB1LA_1RC0RF_1RDHHH_0LE1RB_HHH0LA_1LD1RF (Wiki)
  • M_1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_HHH0LB (Wiki)
  • M_1RBHHH_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA (Wiki)
  • M_1RB1RA_1LC0RC_HHH0LD_0LE0RF_1RE0RA_0LF1LB (Wiki)
  • M_1RB0RE_0RCHHH_1LD1LE_1LE1LD_1RF0LC_1RA1RF (Wiki)
  • M_1RBHHH_0RC1RD_1LA0LA_1LE0RB_1LF1LE_1LC0LD (Wiki)
• Odometer (HasOdometerReduction, 2 machines):
  • M_1RB0LB_0RC0LD_1LD1RE_0LA0RF_0RD1RF_0RCHHH (Wiki, Beaver Math Olympiad Problem 10)
  • M_1RB0LD_0RCHHH_1LD0RF_0LE0RA_0RA1LF_0LA1LB (Wiki, Beaver Math Olympiad Problem 11, macro-equivalent reflected holdout)
• Transducer (HasTransducerReduction, 1 machine):
  • M_1RB0LD_0RCHHH_0LD0RF_1LE1LD_0LA0RD_0RB1RA (Wiki (Bell_eats_counter), macro-equivalent holdout)

3. Open BB(6) Acceleration Problems (20 Machines, 13 with Higher-Level Poincaré Accelerations)

Every open machine certifies is_valid_acceleration and isHalt_iff_acceleration; the 13 machines marked [+HL] additionally define HighLevelState and prove is_valid_highLevel_acceleration, isHalt_iff_highLevel_acceleration, and acceleration_iff_highLevel_acceleration via IsValidAcceleration.of_collatz:

• Stacked (7 machines, 5 [+HL]):
  M_1RB0LD_1LC1RD_0LE1LA_0RB1RD_HHH0LF_1RA1LF [+HL], M_1RB0LE_1LB1RC_0RF0RD_1RE0LA_1LA1RE_HHH0RB [+HL], M_1RB0RB_1RC0LE_1LD1LA_HHH0LC_1RF1LE_1RA0RA [+HL], M_1RB1LA_1LA0RC_1RD1RC_1LE0RC_HHH0LF_1LE0LA [+HL], M_1RB1LA_1LC0RE_HHH0LD_1RE0LF_1RA1RE_1LA0LB, M_1RB1RA_1RC1LB_1LD0RA_HHH0LE_1LC0LF_1RE0LB [+HL], M_1RBHHH_0RC0LD_1LB1RC_0LE0LF_1RD1LE_1RF1RA
• Odometer (7 machines, 6 [+HL]; M_1RB1LD_0RC0LF_... also proves HasOdometerReduction):
  M_1RB0RE_1RC1RE_1LD1LC_0RB0LC_1RF0RB_HHH1RA [+HL], M_1RB1LB_1LC1LA_1RD0LB_1RA1RE_1RF0RD_HHH1RD [+HL], M_1RB1LD_0RC0LF_1LD1RE_0LA0RB_0RD1RB_0LDHHH [+HL], M_1RB1RE_1LC0RC_1RA1LD_1RB0LA_0LC1RF_HHH1RD [+HL], M_1RB1RE_1LC1LB_1LE0LD_1LE1LC_0RF1RA_HHH1RA, M_1RB1RF_1LC0RE_1RD0LC_0LB0RA_1LD1RD_1RBHHH [+HL], M_1RB1RF_1LC1LF_HHH1LD_1LE0RA_1RE1LB_1RD0LD [+HL]
• Transducer (6 machines, 2 [+HL]):
  M_1RB0LE_0RC0RA_1RD1RB_0LA0RB_1LFHHH_1LD1LF, M_1RB0RE_0RC1RE_1RD1LE_0LEHHH_1RA1LF_1RF0LC [+HL], M_1RB1LB_1RC0RD_0LA1RE_0RF1LC_1LA0RB_HHH1LC [+HL], M_1RB1LF_0RC0RB_0LD1RB_1LE0LB_0LA1LC_0LBHHH, M_1RB1RE_1LC0RA_HHH1LD_1LA0LF_0LB0LC_1RB0LB, M_1RBHHH_1LC0RF_0RA0LD_1LE1LA_1RF0LF_0LC0RA

4. Documentation (BusyBeaver/BB6/Accelerations/README.md)

• Standard free-monoid sequence notation ($\Sigma^{\ast}$, empty sequence $\varepsilon$, concatenation/push $[x] \cdot X$, repetition $[x]^k$, reversal $X^{\mathrm{rev}}$) with an explicit Sequence and Stack Notation section mapping mathematical notation to Lean List operations ([], ::, ++), plus high-level structural overview paragraphs for Stacked, Odometer, and Transducer classes and exact mathematical transition systems ($T_{\mathrm{HL}}$) for all 13 higher-level accelerations.

Verification

• python3 verify.py
• lake build BusyBeaver BusyBeaverChallenge (0 errors, 0 non-sorry warnings)
• lake comparator --config comparator/busy_beaver.json (424 theorems verified)
• Visibility & dead-code audit (lean_unused_decls.lean): 0 unused declarations, 0 leaked proof-only helpers
• Synced BusyBeaverChallenge.lean, comparator/busy_beaver.json, BusyBeaver/BB6/Accelerations/README.md, BusyBeaver/BB6/README.md, BusyBeaver/README.md, README.md, and comparator/README.md.

[mo271]

Nice addition (including the 13 new HighLevelState Poincaré accelerations)! CI, comparator sync (424 theorems), TNF normalization, duplicate/isomorphism checks across all 82 BB(6) holdouts, and the pinned State/HighLevelState definitions on the 20 open problems all look great. (Heads-up on Palomar limits: BusyBeaverChallenge.lean is now at 9,168 lines, still within Palomar's 10,000-line per-file cap with ~830 lines of headroom. We could split them at some point)

A few specification tightening items on the three new Challenge predicates, plus documentation/formula fixes on 1c15434:

1. Challenge Predicate Tightening (BusyBeaver/Defs.lean & BusyBeaverChallenge.lean)

1. HasStackReduction degeneracy loophole (BusyBeaver/Defs.lean:366-417, BusyBeaverChallenge.lean:410-461)

   • For the 6 Wiki stack machines, BusyBeaverChallenge.lean exposes only the existential has_stack_reduction : HasStackReduction target.
   • Although BusyBeaver/README.md:28 and BusyBeaver/BB6/Accelerations/README.md:12 describe HasStackReduction as requiring "non-trivial multi-digit stack reachability", HasStackReduction currently omits both:
     1. Any blank-tape stack-growth / multi-digit reachability witness (compare HasTransducerReduction), and
     2. Any length bound on HalfTapeView prefixes in IsValidStackModes (compare p.length ≤ 8 in IsValidTransducerModes) or any unbounded stack-sweep requirement.
   • As written, any 2-cell cycler (L = R = [] untouched behind HalfTapeView.id), any machine halting in ≥ 2 steps (absorbing the penultimate finite tape into vL/vR around encLeft []/encRight []), and any 1-counter machine (L = [a], R = []) satisfies HasStackReduction. Since all 6 proofs in Accelerations/ are genuine multi-digit stack systems, bounding HalfTapeView prefixes and adding a blank-tape multi-digit stack reachability / unbounded-sweep witness (or pinning State/encode/next in BusyBeaverChallenge.lean) will close this loophole.

2. Dead prefix guard in HasOdometerReduction (BusyBeaver/Defs.lean:500-520, BusyBeaverChallenge.lean:544-564)

   • Both the step partition and IsInOdomSystem closure quantify only over w satisfying w.head = 0 ∨ (w.tail.head = 0 ∧ (w.tail.tail.head = 0 ∨ w.tail.tail.tail.head = 0)) (omitting w = 11... and w = 1011...), whereas IsInOdomSystem allows arbitrary w, so IsInOdomSystem is not actually asserted to be closed.
   • All 3 odometer proofs (M_1RB0LB_..., M_1RB0LD_0RCHHH_1LD0RF_..., M_1RB1LD_0RC0LF_...) already prove step_R_partition and step_R_closed unconditionally for all (stk, w) and ignore that hypothesis (fun stk w _ => ...). Dropping the prefix guard (and requiring blank-tape reachability of a non-trivial odometer stack, e.g. cap stk ≥ 1 or stk.length ≥ 2) makes closure unconditional with minimal proof changes.

3. Bypassed exit gate in HasTransducerReduction & M_1RB0LD_0RCHHH_0LD0RF_1LE1LD_0LA0RD_0RB1RA.lean (BusyBeaver/Defs.lean:618-629, BusyBeaverChallenge.lean:662-673)

   • Because the exit-gate entry condition allows ∨ (L = tL_exit :: tL_exit :: L' ∧ R' = R) and m_exit = .hR11 is only entered from .hR1 on .T1 :: .T1 :: L', the pfxL_halt disjunct is bypassed (exact Or.inr ⟨rfl, rfl⟩ at M_1RB0LD_0RCHHH_0LD0RF_1LE1LD_0LA0RD_0RB1RA.lean:206).
   • As a consequence:
     1. stepMacro .hR11 [.T1] R = none even though the TM does not halt on [.T1] (it transitions in 3 steps to (.hR, [], .U10011 :: R), already proved as step_hR11_T1_singleton).
     2. pfxL_halt = [.T100, .T000, .T000] never occurs after (.T1, .T1) on the blank-tape orbit (where (.T1, .T1) is followed by .T100, and both .T1 :: .T1 :: L'' and .T1 :: .T100 :: L'' halt in 23 steps for all L'').
   • Defining stepMacro .hR11 [.T1] R = some (.hR, [], .U10011 :: R) and tightening the exit gate so stepMacro = none implies halting on the reachable orbit makes stepMacro halting-faithful.

---

2. BusyBeaver/BB6/Accelerations/README.md & Minor Fixes

4. Blank-tape step counts ("(after N TM steps)") in 13 of 20 subsections of BusyBeaver/BB6/Accelerations/README.md

   • The .lean module docstrings match exact blank-tape simulation from init [] to encode start, whereas 13 subsections in BusyBeaver/BB6/Accelerations/README.md have stale/swapped step counts:

   Section	Machine	README.md	Actual (.lean)
   §1.1 (L87)	1RB0LD_1LC1RD_0LE1LA_0RB1RD_---0LF_1RA1LF	11	19
   §1.2 (L121)	1RB0LE_1LB1RC_0RF0RD_1RE0LA_1LA1RE_---0RB	19	12
   §1.3 (L145)	1RB0RB_1RC0LE_1LD1LA_---0LC_1RF1LE_1RA0RA	9	16
   §1.4 (L189)	1RB1LA_1LA0RC_1RD1RC_1LE0RC_---0LF_1LE0LA	9	7
   §1.5 (L243)	1RB1LA_1LC0RE_---0LD_1RE0LF_1RA1RE_1LA0LB	3	1
   §1.6 (L282)	1RB1RA_1RC1LB_1LD0RA_---0LE_1LC0LF_1RE0LB	11	19
   §2.1 (L355)	1RB0RE_1RC1RE_1LD1LC_0RB0LC_1RF0RB_---1RA	11	16
   §2.2 (L401)	1RB1LB_1LC1LA_1RD0LB_1RA1RE_1RF0RD_---1RD	3	6
   §2.4 (L477)	1RB1RE_1LC0RC_1RA1LD_1RB0LA_0LC1RF_---1RD	3	4
   §2.5 (L525)	1RB1RE_1LC1LB_1LE0LD_1LE1LC_0RF1RA_---1RA	11	4
   §2.6 (L564)	1RB1RF_1LC0RE_1RD0LC_0LB0RA_1LD1RD_1RB---	3	6
   §2.7 (L596)	1RB1RF_1LC1LF_---1LD_1LE0RA_1RE1LB_1RD0LD	9	5
   §3.3 (L726)	1RB1LB_1RC0RD_0LA1RE_0RF1LC_1LA0RB_---1LC	4	8

5. Two formula typos in BusyBeaver/BB6/Accelerations/README.md (all other base T and high-level T_HL recurrences match Lean next / highLevelNext):

   • §1.3 (L175, 1RB0RB_1RC0LE_1LD1LA_---0LC_1RF1LE_1RA0RA): In the high-level contraction \Xi(u, v, L, r, R), the "if u = 0 and v ≥ 1 is odd" branch writes F_{\mathrm{HL}}(v + 1, c^+, L', r, R); in Lean's exitC (let b' := b - 1; if b' % 2 = 0 then some (.F (b' + 3) ...)), (v - 1) + 3 = v + 2 (matching T(C(0, v, ...)) = F(v + 2, ...)), so this should be F_{\mathrm{HL}}(v + 2, c^+, L', r, R).
   • §2.2 (L410-411, 1RB1LB_1LC1LA_1RD0LB_1RA1RE_1RF0RD_---1RD): In both "if d ≥ 2 is even" branches, [0]^{(d-1)/2} has a half-integer exponent; Lean's d_lean / 2 (for d = d_lean + 1 even) is [0]^{(d-2)/2}.

6. Terminology, attribution & stray @[simp]

   • "prefix-free" → "strict-sub-Kraft" in BusyBeaver/README.md:30 and BusyBeaver/BB6/Accelerations/README.md:14: kraftSum < (k + 2)^maxLen enforces strict sub-Kraft rather than prefix-freeness (e.g. TokL = {[1], [0,0,0], [1,0,0]} has [1] as a prefix of [1,0,0]; BusyBeaver/Defs.lean already says strict-sub-Kraft).
   • "state-relabeled" attribution in BusyBeaver/BB6/Accelerations/README.md:27-28, M_1RB0LD_0RCHHH_1LD0RF_0LE0RA_0RA1LF_0LA1LB.lean:14, and M_1RB0LD_0RCHHH_0LD0RF_1LE1LD_0LA0RD_0RB1RA.lean:14: neither machine is a state/mirror relabeling of the cited Wiki RLE (1RB0LD_0RC---_1LD0RF_... differs in 6 transitions from BMO Problem 11 while realizing the reflected macro-odometer; 1RB0LD_0RC---_0LD0RF_... differs in 2 transitions from 1RB0LE_0RC---_1LC0RD_0RB1RA_1LF1LE_0LA1LF and shifts raw blank-tape step counts by -2). Suggest "macro-equivalent holdout" / "behaviorally equivalent holdout".
   • Stray @[simp] followed by a blank line at BusyBeaverChallenge.lean:7728 (above M_1RB1LA_1RC0RF_1RDHHH_0LE1RB_HHH0LA_1LD1RF.has_stack_reduction).

[TomZahavy]

Thanks for the thorough review, @mo271! All 6 items have been addressed in d36c45f:

1. HasStackReduction degeneracy loophole (BusyBeaver/Defs.lean, BusyBeaverChallenge.lean, BusyBeaver/BB6/Accelerations/Stack.lean, and all 6 Wiki stack files)

   • Bounded HalfTapeView prefixes (IsValidStackModes): Added (HalfTapeView.casesOn vL List.length List.length) ≤ 8 and (HalfTapeView.casesOn vR List.length List.length) ≤ 8 so finite-tape prefixes cannot absorb arbitrary halting trajectories.
   • Blank-tape multi-digit stack reachability: Strengthened init [] ⊢⁺ evalStackCfg m_g L_g R_g to require 3 ≤ L_g.length + R_g.length ∧ ∃ x ∈ L_g ++ R_g, 1 ≤ x.1, ruling out 0-digit cyclers and 1-counter encodings.
   • Arbitrary-depth stack-frame transfer: Added an explicit unbounded stack-frame transfer transition (evalStackCfg m (x :: z :: L) R ⊢⁺ evalStackCfg m' (g z :: L) (f R) or its right-pop mirror, with ∀ s, s.length ≤ (f s).length) so stack frames beyond depth 1 actively participate in transitions across arbitrary stack tails.
   • Updated OneDigitStackReduction / HasStackReduction.of_oneDigit in BusyBeaver/BB6/Accelerations/Stack.lean and proved the strengthened witnesses in all 6 Wiki stack files (M_1RB1LA_1RC0RF_1RDHHH_0LE1RB_HHH0LA_1LD1RF, M_1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_HHH0LB, M_1RBHHH_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA, M_1RB1RA_1LC0RC_HHH0LD_0LE0RF_1RE0RA_0LF1LB, M_1RB0RE_0RCHHH_1LD1LE_1LE1LD_1RF0LC_1RA1RF, M_1RBHHH_0RC1RD_1LA0LA_1LE0RB_1LF1LE_1LC0LD).

2. Unconditional HasOdometerReduction closure & non-trivial blank-tape stack (BusyBeaver/Defs.lean, BusyBeaverChallenge.lean, and all 3 odometer files)

   • Removed the dead w.head = 0 ∨ ... prefix guard from both the evalOdomR step partition and IsInOdomSystem closure so closure holds unconditionally for all (stk, w).
   • Strengthened blank-tape reachability (init [] ⊢⁺ evalOdomR stk₀ w₀) to require 2 ≤ stk₀.length ∧ 1 ≤ cap stk₀, and updated M_1RB0LB_0RC0LD_1LD1RE_0LA0RF_0RD1RF_0RCHHH (stk₀ = [.L0, .L0], cap = 3), M_1RB0LD_0RCHHH_1LD0RF_0LE0RA_0RA1LF_0LA1LB (stk₀ = [.L0, .L2, .L0], cap = 1), and M_1RB1LD_0RC0LF_1LD1RE_0LA0RB_0RD1RB_0LDHHH (stk₀ = [.L0, .L0], cap = 3).

3. Non-bypassable HasTransducerReduction exit gate & halting-faithful stepMacro (BusyBeaver/Defs.lean, BusyBeaverChallenge.lean, M_1RB0LD_0RCHHH_0LD0RF_1LE1LD_0LA0RD_0RB1RA.lean)

   • Removed the bypassed ∨ (L = tL_exit :: tL_exit :: L' ∧ R' = R) disjunction and replaced pfxL_halt with a non-bypassable multi-token halting exit set exitNext : List TokL (exitNext.Nodup ∧ exitNext ≠ []) such that:
     • (stepMacro m_exit [tL_exit] R).isSome for every R (so [tL_exit] cannot spuriously return none),
     • stepMacro m L R = none ↔ (m = m_exit ∧ ∃ t₂ L'', t₂ ∈ exitNext ∧ L = tL_exit :: t₂ :: L''), and
     • every t₂ ∈ exitNext is certified to halt (ReachesPlus ... { state := none, tape := ... }) both on [tL_exit, t₂] for all R and on tL_exit :: t₂ :: (sfx ++ L'') (sfx.length ≤ 2) for all L'', R.
   • In M_1RB0LD_0RCHHH_0LD0RF_1LE1LD_0LA0RD_0RB1RA.lean:
     • Defined stepMacro .hR11 [.T1] R = some (.hR, [], .U10011 :: R) (3 TM steps) and stepMacro .hR11 (.T1 :: .T000 :: L) R = some (.hR1, L, .U10001 :: R) (12 TM steps), leaving stepMacro = none iff m = .hR11 and L = .T1 :: t₂ :: L'' with t₂ ∈ [.T1, .T100].
     • (Subtlety noted while proving the general-tail lemma): on L = [.T1, .T1] ++ L'' or [.T1, .T100] ++ L'', the TM halts in 23 steps whenever L'' = [] or L'' = [.T000, .T000] ++ L''' (which covers the blank-tape invariant where .T000 blocks pad the exterior), whereas if L'' starts with .T1 or .T100 (e.g. L'' = [.T100]), step 4 enters .hR behind [1, 1, 1, 0, 0, 1] and runs the full Bell_eats_counter transducer until R empties twice rather than halting in 23 steps for arbitrary R. Certifying both the empty-tail (L'' = []) and bounded-suffix (sfx = [.T000, .T000]) halting witnesses captures the exact halting behavior without overclaiming uniform 23-step halting on unreachable non-.T000 outer tails.

4. Blank-tape step counts in BusyBeaver/BB6/Accelerations/README.md

   • Updated all 13 "after N TM steps" counts (§1.1 19, §1.2 12, §1.3 16, §1.4 7, §1.5 1, §1.6 19, §2.1 16, §2.2 6, §2.4 4, §2.5 4, §2.6 6, §2.7 5, §3.3 8) and mechanically cross-checked all 20 subsections against the .lean step_init theorems (0 mismatches).

5. Formula typos in BusyBeaver/BB6/Accelerations/README.md

   • §1.3 (1RB0RB_1RC0LE_1LD1LA_---0LC_1RF1LE_1RA0RA): Fixed F_{\mathrm{HL}}(v + 1, c^+, L', r, R) → F_{\mathrm{HL}}(v + 2, c^+, L', r, R) in the odd-v branch of $\Xi(0, v, L, r, R)$ to match exitC's b' + 3 = (v - 1) + 3 = v + 2.
   • §2.2 (1RB1LB_1LC1LA_1RD0LB_1RA1RE_1RF0RD_---1RD): Fixed both even-d exponents from [0]^{(d-1)/2} to [0]^{(d-2)/2} to match d_lean / 2 for $d = d_{\mathrm{lean}} + 1$ even.

6. Terminology, attribution & stray @[simp]

   • Updated "prefix-free" → "strict-sub-Kraft" in BusyBeaver/README.md, BusyBeaver/BB6/Accelerations/README.md, and the PR description.
   • Updated "state-relabeled" → "macro-equivalent reflected holdout" (1RB0LD_0RC---_1LD0RF_0LE0RA_0RA1LF_0LA1LB) and "macro-equivalent holdout" (1RB0LD_0RC---_0LD0RF_1LE1LD_0LA0RD_0RB1RA) in BusyBeaver/BB6/Accelerations/README.md, both .lean module docstrings, and the PR description.
   • Removed the stray @[simp] attribute and blank line above M_1RB1LA_1RC0RF_1RDHHH_0LE1RB_HHH0LA_1LD1RF.has_stack_reduction in BusyBeaverChallenge.lean.

Verification

• lake build BusyBeaver BusyBeaverChallenge (0 errors, 0 non-sorry warnings)
• lake comparator --config comparator/busy_beaver.json ("Your solution is okay!", 424 theorems)
• lean_unused_decls.lean (0 unused declarations, 0 leaked proof-only helpers)
• python3 verify.py & GitHub /markdown MathJax check (589 <math-renderer> spans, 0 leaked TeX)