[TomZahavy]

Summary

This PR formalizes the hardness classification of the 33 open hard-core BB(6) holdout machines, introduces reusable stack transport infrastructure (ClosedStackSystem, ClosedStackSystem.relabel, ClosedStackSystem.mirror in BusyBeaver/BB6/Accelerations/Stack.lean) deduplicating ~3,350 lines across #285, #500, and #490, ports the 6 remaining hard-core machines into BusyBeaver/BB6/Accelerations/ with complete HasStackReduction proofs, proves the formal halting equivalence of the synchronized pair 1RB0LE_0RC1RC_0RD1LA_1LD0LA_1LF1LC_---1LC / ---0LA, and introduces 74 kernel-checked live-hazard and halting-residue theorems across 26 machine namespaces in BusyBeaver.BB6.HardnessEvidence.

Key Additions

1. Hardness Classification (BusyBeaver/BB6/Hardness.lean + 33 Per-Machine Sections):

   • Categorizes all 33 open hard-core holdouts into:
     • Problems 1–5 (8 machines): First-order Collatz-like cryptids (#330, #608, #424, #464, #79, #140, #614, #590 / #79).
     • Shielded Single-Base Exponential Cascades (11 machines): Proved $2^n, 3^n, 4^n$ cascades protected by inductive parity/drain shields where linear forms in logarithms (Baker–Wüstholz / Hensel-lifting) are required to decide halting (#688, #644, #586, #746, #693, #352, #530, #623, #625, #380, #568).
     • Problems S2–S5 (9 open machines + 1 resolved calibration case #72): Second-order Collatz-like stacked cryptids, including Halving Towers, multiplicative-drain towers, Chaotic6, and $R \neq []$ shielded mod-3 stacks (#391, #129, #660, #667, #680, #496, #549, #600, #665, plus calibration #72).
     • Wiki Open Stacks (5 machines): Open non-halting stack cryptids (#59, #85, #285, #490, #500).
     • Pointer to BMO Problem 11: Clarifies the relationship between the 33-class hard core and the 45-class solvability census (the 12-class base-3 odometer group anchored by 1RB0LD_0RC---_1LD0RF_0LE0RA_0RA1LF_0LA1LB).
   • Every hard-core machine file in BusyBeaver/BB6/ (21 files) and BusyBeaver/BB6/Accelerations/ (12 files) now documents its halting trigger (RW / RES / EQ / POW), growth regime, shield, and heuristic hazard in clean prose without dangling declaration names.

2. Stack Transport Infrastructure & 6 Missing Hard-Core Machines Ported (BusyBeaver/BB6/Accelerations/):

   • Reusable Stack Transport (BusyBeaver/BB6/Accelerations/Stack.lean): Adds state permutation and tape reflection equivariance for HasStackReduction via ClosedStackSystem.relabel and ClosedStackSystem.mirror. Exposes #85's closed stack system and compresses #285, #500, and #490 from ~1,177 lines each to ~108 lines each (saving ~3,350 lines).
   • Multiplicative-Drain Towers (Wiki E1 siblings of 1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA):
     • 1RB1RD_1LC0LE_1RA0LB_1RA1RF_0RA0RC_1REHHH (#285)
     • 1RB0RE_1LC0RA_1LA1LD_1LC1LF_0LC0LB_1LEHHH (#490)
     • 1RB0LC_1RC1RE_1LA0LD_0RB0RA_1RB1RF_1RDHHH (#500)
   • Halving Towers:
     • 1RB1RA_1LC0RC_1RE0LD_0RE0LF_1RAHHH_1RB1LF (#659, $3/2$ base-2 tower)
     • 1RB1RC_1LC0LE_1RD1RC_1LB0RA_HHH0LF_1RD1LF (#209, $5/2$ base-4 split tower)
     • 1RB0LC_1LC0RE_1LD1LC_1LA1RD_HHH0RF_0LB0RD (#480, $5/2$ base-4 dual tower)
   • All 6 machines feature complete HasStackReduction proofs, bringing the total holdouts in the repository to 95 (54 in BB6/ [53 closed-pattern + A6 is_not_halt], 35 in BB6/Accelerations/, 6 in BB33/).

3. Formal Equivalence Theorem (BusyBeaver/BB6/Equivalences.lean):

   • Proves BusyBeaver.BB6.isHalt_HHH1LC_iff_HHH0LA:
     $$\text{IsHalt } (\texttt{1RB0LE_0RC1RC_0RD1LA_1LD0LA_1LF1LC_---1LC}) \iff \text{IsHalt } (\texttt{1RB0LE_0RC1RC_0RD1LA_1LD0LA_1LF1LC_---0LA})$$
     by transporting CollatzHalts across the state isomorphism between the two machines' high-level counter systems and chaining both machines' isHalt_iff_highLevel_acceleration theorems.

4. Formal Hardness Evidence (BusyBeaver/BB6/HardnessEvidence.lean):

   • 74 public theorems under namespace BusyBeaver.BB6.HardnessEvidence across 26 machine namespaces (the 24 hard-core machines that have IsValidAcceleration, plus #568 and 1RB1RF_1LC1LF_---1LD_1LE0RA_1RE1LB_1RD0LD, out of 73 accelerated holdouts):
     • Live halting-state witnesses: Proves highLevelNext s = none (or next s = none) at an explicit reachable-format configuration for all 26 machines, proving the high-level transition function is genuinely partial.
     • Parametric residue preimages: Proves the exact MOD, EQ, DIV, and POW algebraic preimages of none under highLevelNext / next, including two-step halting proofs via (next ...).bind next = none / (highLevelNext ...).bind highLevelNext = none on #80 (parameterized by r :: R), #693, and #746.

Verification

• lake build: All 3,882 jobs across Cryptids, Challenge, BusyBeaver, and BusyBeaverChallenge built successfully with 0 errors.
• comparator/busy_beaver.json: All 506 declarations verified across all 95 machines, Equivalences, and HardnessEvidence (BusyBeaver.BB6.HardnessEvidence.*).
• python3 verify.py: All zero-dependency first-principles verifier checks passed (EXIT 0).
• Style & Hygiene:
  • 0 lines > 100 characters in all Lean source files.
  • 0 occurrences of lemma in all Lean source files.
  • 0 occurrences of sorry outside specification files (Challenge.lean and BusyBeaverChallenge.lean).
  • 0 occurrences of native_decide or disabled linters.
  • All HTML comment tags (<!-- hardness:begin/end -->) stripped from docstrings.
  • Dead-code & visibility audit: 0 unused declarations across all new modules.

[mo271]

Thanks @TomZahavy — nice additions! Equivalences.lean is super clean, the TCB diff in BusyBeaverChallenge.lean is strictly additive, and all 6 new Accelerations/ files keep internal helpers private with zero warnings/sorries.
A few things to address before merging:

1. Rebase onto main + update counts:
   • Both Prove a six-state A6 machine nonhalting from blank tape #21 (A6 is_not_halt) and Prove PA-internalized ZF inconsistency equivalences some zf machines #20 (PA ZF internalization) have landed on main, so there are merge conflicts in BusyBeaver.lean, README.md, BusyBeaver/README.md, BusyBeaver/BB6/README.md, comparator/README.md, and comparator/busy_beaver.json.
   • With A6 in BusyBeaver/BB6/, the counts bump by +1: 54 machines (312 theorems) in BusyBeaver/BB6/, 89 BB(6) holdouts, 95 total BusyBeaver/ holdouts, and 506 verified theorems in comparator/busy_beaver.json (plus keeping the a6.json and updated all.json / pa_semantics.json rows in comparator/README.md).
2. Deduplicating #285, #490, and #500 (~3,530 lines):
   • M_1RB1RD_1LC0LE_1RA0LB_1RA1RF_0RA0RC_1REHHH.lean (#285, 1,177 lines), M_1RB0RE_1LC0RA_1LA1LD_1LC1LF_0LC0LB_1LEHHH.lean (#490, 1,178 lines), and M_1RB0LC_1RC1RE_1LA0LD_0RB0RA_1RB1RF_1RDHHH.lean (#500, 1,176 lines) are full copies of M_1RBHHH_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA.lean (#85, 1,176 lines) under a state permutation (and L/R mirror for #490) plus a 7–12 step blank-tape entry.
   • Every conjunct of HasStackReduction in BusyBeaver/Defs.lean except ReachesPlus M (init []) (evalStackCfg m_g L_g R_g) is equivariant under a state bijection σ : Λ ≃ Λ and optional tape reflection. Adding a reusable relabel/mirror transport lemma for HasStackReduction (e.g. in BusyBeaver/BB6/Accelerations/Stack.lean) and exposing #85's closed stack witness would shrink those three ~1,177-line files to ~50–80 lines each (just the table-isomorphism decide check + the 7/11/12-step init_reaches_nontrivial proof) and give us reusable infra for future E1 siblings.
3. HardnessEvidence: two-step halting bug on #80 (M_1RBHHH_0RC0LD_1LB1RC_0LE0LF_1RD1LE_1RF1RA):
   • halting_residue_class_two_step (L688) currently proves only the first step:
     next (.CR (a + 2) b L 1 R) = some (.CR 1 (a + 1) (b :: L) (bump1 R).1 (bump1 R).2)
     for arbitrary R : List ℕ. When R = [], bump1 [] = (0, []), and .CR 1 (a + 1) (b :: L) 0 [] steps to some (.CR 0 (a + 6) (b :: L) 0 []) rather than halting (CR 1 _ _ d _ only halts for d ≥ 1).
   • Could we parameterize by (r : ℕ) (R : List ℕ) on r :: R and prove (next (.CR (a + 2) b L 1 (r :: R))).bind next = none (and similarly .bind highLevelNext = none on #693 L499 and #746 L522, matching #352 and #530 which already prove = none)?
4. Documentation & Hardness.lean accuracy:
   • 26 vs. 73 accelerated holdouts: BusyBeaver/BB6/README.md L5 says HardnessEvidence covers "all 26 BB(6) holdouts with explicit Collatz-like accelerations", whereas 73 BB(6) holdouts in the repo have IsValidAcceleration (HardnessEvidence covers the 24 Hardness.lean machines that have IsValidAcceleration, plus #568 and 1RB1RF_1LC1LF_---1LD_1LE0RA_1RE1LB_1RD0LD). Let's clarify that selection in BB6/README.md and Hardness.lean L18.
   • Dangling identifier / dossier references: Hardness.lean and the per-machine ## Hardness docstrings reference backticked names that don't exist in this repo (is_cryptid, is_stack_cryptid, ValidStack129, ValidStack391, ValidStack549, ValidStack660, ValidStack680, Valid3Counter116, inv_126_R_shape, rec_59_bottom_extension) as well as (see dossier) in #464 and #644. Unless those shield lemmas are being ported here, it would be clearer to describe the shields in prose rather than backticked declaration names (and avoid calling them proved shields in the PR summary).
   • #590 vs. #79: Hardness.lean L351 calls #590 a "candidate exact equivalence" to #79 and copies #79's > 3.46 × 10^{1204} TM steps in 12 cascades horizon, but while they share the exact highLevelNext map, their orbits from .A 5 2 (#79) and .A 4 3 (#590) stay disjoint ((5,2) → (10,3) → (4,11) → (27,3) vs. (4,3) → (19,3) → (13,11) → (28,3)).
5. Minor nits:
   • Namespace: Equivalences.lean uses namespace BusyBeaver.BB6, whereas HardnessEvidence.lean uses namespace BusyBeaver.HardnessEvidence (without .BB6, while Hardness.lean L19 cites BusyBeaver.BB6.HardnessEvidence).
   • HTML comments in docstrings: Worth checking that <!-- hardness:begin --> / <!-- hardness:end --> in the 33 /-! ... -/ docstrings don't render visibly in Verso / doc-gen4 (or stripping them if no sync script is checked in).
   • PR description: Bullet 1d has a typo RLE 1RB1RA_1LC1RF_1RE0LD_1LC1LF_0FR0LA_0LDHHH (0FR0LA, whereas BMO Problem 11 in Hardness.lean is 1RB0LD_0RC---_1LD0RF_0LE0RA_0RA1LF_0LA1LB), and the bullet counts (7 + 14 + 12) differ from Hardness.lean's sections (8 Problems 1–5 + 11 Cascades + 9 S2–S5 + 5 Wiki stacks = 33).

[TomZahavy]

Thanks @mo271 for the thorough and constructive review! All 5 items have been addressed:

1. Rebase onto origin/main + update counts:

   • Rebased onto latest origin/main (including Prove a six-state A6 machine nonhalting from blank tape #21 A6 is_not_halt and Prove PA-internalized ZF inconsistency equivalences some zf machines #20 PA ZF internalization).
   • Counts updated consistently across all documentation and configuration files:
     • BusyBeaver/BB6/: 54 holdout machines (53 closed-pattern holdouts + A6 is_not_halt), 312 theorems.
     • BusyBeaver/: 89 BB(6) holdouts (54 in BB6/ + 35 in Accelerations/), 95 holdouts total across BusyBeaver/ (89 in BB6 + 6 in BB33).
     • comparator/busy_beaver.json: 506 verified declarations (424 base + 8 novel Halving Towers + 74 HardnessEvidence).
     • comparator/README.md: preserves a6.json row and updated all.json (29 theorems) / pa_semantics.json (7 theorems) rows.

2. Deduplicating #285, #490, and #500 (~3,350 lines saved):

   • Added reusable state permutation and tape reflection infrastructure in BusyBeaver/BB6/Accelerations/Stack.lean:
     • reflectDir, reflectTape, mapCfg, mapState, mirrorCfg, with bidirectional step commutation theorems (step_isNone_mapCfg, step_isSome_mapCfg, reachesPlus_mapCfg).
     • structure ClosedStackSystem, which packages the stack encoding, transition table, closedness invariant, and reachability.
     • HasStackReduction.of_closedSystem, ClosedStackSystem.relabel, and ClosedStackSystem.mirror.
   • Exposed #85 (M_1RBHHH_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA.lean)'s witness as closedStackSystem.
   • Refactored #285, #500, and #490 to instantiate the transport lemmas (ClosedStackSystem.relabel for #285 and #500; ClosedStackSystem.mirror for #490), shrinking each file from ~1,177 lines to ~108 lines.

3. HardnessEvidence: two-step halting proofs:

   • #80 (M_1RBHHH_0RC0LD_1LB1RC_0LE0LF_1RD1LE_1RF1RA): parameterized by (r : ℕ) (R : List ℕ) on r :: R and proved (next (.CR (a + 2) b L 1 (r :: R))).bind next = none via simp [next, bump1].
   • #693 (M_1RB1RC_1LC1LC_1RE0LD_1LB1RF_HHH1RA_0RD1RD) and #746 (M_1RB0LF_1LC1RA_0RE0RD_HHH1LE_1LF1RC_1LC1LA): updated signatures and proofs to (highLevelNext ...).bind highLevelNext = none, matching #352 and #530.
   • All 3 signatures updated identically in BusyBeaverChallenge.lean.

4. Documentation & Hardness.lean accuracy:

   • 26 vs 73 accelerated holdouts: Clarified in BusyBeaver/BB6/README.md and Hardness.lean L18 that HardnessEvidence covers the 24 hard-core machines carrying IsValidAcceleration, plus #568 and 1RB1RF_1LC1LF_---1LD_1LE0RA_1RE1LB_1RD0LD, out of the 73 accelerated holdouts in the repo.
   • Dangling identifier / dossier references: Replaced backticked non-declaration names (is_cryptid, is_stack_cryptid, ValidStack129, ValidStack391, ValidStack549, ValidStack660, ValidStack680, Valid3Counter116, inv_126_R_shape, rec_59_bottom_extension) with clean prose descriptions across Hardness.lean and all per-machine docstrings. Removed (see dossier) in #464 and #644.
   • #590 vs #79: Clarified in Hardness.lean and #590's docstring that while they share the exact highLevelNext transition map, their orbits from $(5,2)$ vs $(4,3)$ remain disjoint ((4,3) → (19,3) → (13,11) → (28,3) vs (5,2) → (10,3) → (4,11) → (27,3)). Updated simulated horizon to 10 cascades (reaching $A(65490, 3)$).

5. Minor nits:

   • Namespace: Updated to BusyBeaver.BB6.HardnessEvidence across HardnessEvidence.lean, BusyBeaverChallenge.lean, and comparator/busy_beaver.json.
   • HTML comments: Stripped <!-- hardness:begin --> / <!-- hardness:end --> tags across all 33 docstrings.
   • PR description: Fixed typo RLE for BMO Problem 11 to 1RB0LD_0RC---_1LD0RF_0LE0RA_0RA1LF_0LA1LB, aligned bullet counts to 8 + 11 + 9 + 5 = 33, updated totals to 95 holdouts / 506 comparator declarations, and summarized the stack transport refactoring.

Verified locally:

• lake build (3,882 jobs, 0 errors, 0 warnings outside expected challenge sorrys).
• python3 verify.py (all checks pass, EXIT 0).
• 0 lines > 100 characters in all Lean source files.
• 0 occurrences of lemma in all Lean source files.

[mo271]

Thanks @TomZahavy — the ClosedStackSystem relabel/mirror refactor in Stack.lean came out super clean, and everything from the review is addressed. LGTM!

(Tiny non-blocking nit if you touch this again later: BusyBeaver/BB6/Accelerations/README.md L8 still has one (BusyBeaver.HardnessEvidence) missing .BB6.)