[TomZahavy]

Summary

This PR ports all remaining 22 BB(6) Hard holdout cryptid machines into google-deepmind/cryptids, modularizes the shared BusyBeaver/Defs/ definitions, tightens the cryptid specification predicates, and registers 37 new comparator theorems (698 → 735 total theorems in comparator/busy_beaver.json, with definition_names: []).

1. Modular Core Definitions (BusyBeaver/Defs/) & Integrity Checks

• Splits BusyBeaver/Defs.lean into clean modular submodules and re-exports them through BusyBeaver/Defs.lean:
  • Defs/Core.lean: Machine execution semantics and reachability relations (ReachesPlus, ReachesStar).
  • Defs/Patterns.lean: Level A pattern-set invariants (IsClosedPatternSet, HasCollatzReduction), Level B accelerations (IsValidAcceleration), and rule-bounded cryptids (IsCryptid).
  • Defs/Stack.lean: Stack-word representations, views (HalfTapeView, viewPrefixLen), and stacked reductions (HasStackReduction).
  • Defs/Odometer.lean: Mixed-radix odometer stack and bitstream systems (HasOdometerReduction).
  • Defs/Transducer.lean: Bidirectional word-stack transducers (HasTransducerReduction).
  • Defs/WordRun.lean: Word-run stack systems (IsNowhereDenseFamily, WordStackSpec, IsWordRunCryptid), requiring IsNowhereDenseFamily strictly on both sides (removing IsBoundaryAlignedSide disjuncts) and defining viewPrefixLen with HalfTapeView.casesOn so BusyBeaver.viewPrefixLen needs no definition_names exemption.
  • Defs/Segmented.lean: Partitioned segmented schemas (SegRegionKind.WellFormed, IsClosedSegmentedSystem, IsSegmentedCryptid) enforcing non-empty finite/word-run/block regions, non-trivial single-bit encoding exclusion, and bounded gadgets (w.length ≤ 16).
• Adds CORE_MANIFEST.json, tools/check_manifest.py, and tools/render_challenge.py with CI verification in .github/workflows/busy_beaver_ci.yml (SHA-pinned actions and !BusyBeaver/**/*.md path filter).

2. 22 Ported BB(6) Hard Holdout Cryptid Machines

• 11 Segmented Cryptids (IsSegmentedCryptid + pinned is_closed_segmented_system) in BusyBeaver/BB6/Accelerations/:
  • M_1RB0LA_0RC0RB_1LD1LA_1LC1RE_1RF0RD_1LAHHH.lean
  • M_1RB0LA_0RC0RB_1LD1LA_1LC1RE_1RF0RD_1LCHHH.lean
  • M_1RB0LD_0RC1RD_1LA1RA_1LE0LE_1RF0LA_0RAHHH.lean
  • M_1RB0RA_0LC0RE_1LE1LD_0LEHHH_1LF0LC_1RA1LE.lean
  • M_1RB0RE_1LC1RA_1LD0LC_0RE0LA_1RA1RF_0RAHHH.lean
  • M_1RB0RE_1RCHHH_0RD0RC_1LE1LF_1LD1RA_1RC0LF.lean
  • M_1RB0RF_1LCHHH_1LF1LD_1RE0LD_0RC0RE_1LC1RA.lean
  • M_1RB0RF_1LCHHH_1RD0LC_0RE0RD_1LF1LC_1LE1RA.lean
  • M_1RB1RF_1RC0RA_1LD1RB_1LE0LD_0RA0LB_0RBHHH.lean
  • M_1RBHHH_0RC0RB_1LD1LE_1LC1RF_1RB0LE_1RA0RD.lean
  • M_1RBHHH_1LC0RB_0LD0LC_1RE1RB_1RD1LF_1LA0LE.lean
• 8 Stack Cryptids (IsStackCryptid) in BusyBeaver/BB6/Accelerations/:
  • M_1RB0LD_0LC0RE_1LA0RD_0RB0LF_1RC1LA_0RBHHH.lean
  • M_1RB0LE_1LC0RE_0RA0LD_1LA0LF_0LC0RA_0REHHH.lean
  • M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RA_0LBHHH.lean
  • M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RA_0LEHHH.lean
  • M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RE_0LAHHH.lean
  • M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RE_0LCHHH.lean
  • M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RE_1LAHHH.lean
  • M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RE_1LEHHH.lean
• 2 Odometer Cryptids (IsOdometerCryptid) in BusyBeaver/BB6/Accelerations/:
  • M_1RB0LD_0LC0RE_1LA0RD_0RB0LD_1RC1RF_1RAHHH.lean
  • M_1RBHHH_1RC0LE_0LD0RF_1LB0RE_0RC0LE_1RD1RA.lean
• 1 Holdout (#424, Level A + Level B + IsCryptid) in BusyBeaver/BB6/:
  • M_1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_HHH1RE.lean (is_closed_pattern_set, has_collatz_reduction, is_valid_acceleration, isHalt_iff_acceleration, is_cryptid)
• Supporting infrastructure in BusyBeaver/Stack.lean and BusyBeaver/WordRunStack.lean.

3. Comparator & Challenge Registration

• Defines every new machine using load_rle_machine% and abbrev target : Machine (Fin 2) (Fin 6) := machine.toBB.
• Registers all 37 new theorems (22 cryptid goals + 11 is_closed_segmented_system + 4 #424 theorems) in BusyBeaverChallenge.lean and comparator/busy_beaver.json (735 total theorems; definition_names: []).

4. Verification

• python3 tools/check_manifest.py: PASSED (12 core files verified).
• python3 tools/render_challenge.py --check: PASSED.
• lake build BusyBeaver BusyBeaverChallenge: PASSED.
• lake comparator --config=comparator/busy_beaver.json: PASSED (Lean default kernel accepts the solution / Your solution is okay!).
• Style & hygiene check across all 36 changed .lean files: 0 disabled linters, 0 lemma declarations, 0 > 100-character lines, and 0 forbidden tokens (sorry, admit, axiom, native_decide) outside challenge stubs.

[mo271]

Splitting BusyBeaver/Defs.lean into BusyBeaver/Defs/* and adding CORE_MANIFEST.json + tools/render_challenge.py --check in CI is a very nice structural improvement! I checked out the branch, verified check_manifest.py and render_challenge.py --check, confirmed all 22 target_tm transition tables match their RLE names, and checked the witness constructions across all 22 proof files.

Found a few things we should sort out before merging:

1. CI failure (zizmor-output) + rebase onto main (and feat(busy_beaver): Port 11 single-file BB(6) proofs and SegCount #28):

   • .github/workflows/busy_beaver_ci.yml currently conflicts with main (docs(bb6): fix Pomme table link and exclude markdown from BusyBeaver CI #26) and fails the zizmor check (busy_beaver_ci.yml:52: ref-version-mismatch on # v1 -> # v1.7.0). Rebasing onto main (ideally right after merging feat(busy_beaver): Port 11 single-file BB(6) proofs and SegCount #28) will pick up # v1.7.0 and the !BusyBeaver/**/*.md path filter cleanly.

2. Anti-cheat / specification tightness in BusyBeaverChallenge.lean and BusyBeaver/Defs/:

   • All 22 proof files in this PR build genuine, non-degenerate reductions (explicit SegMode × List ... grammars with ValidSeg _ := True in the 11 segmented files, full stack/odometer reductions, and an explicit 1-pattern closed set in M_1RB1LE_...).
   • However, when BusyBeaverChallenge.lean exposes bare existential := sorry goals for external solvers:
     • IsSegmentedCryptid (BusyBeaver/Defs/Segmented.lean): SegRegionKind.gadget (w : List Γ) allows an unbounded list w, and the transition clause only requires evalCfg s ⊢⁺ cfg' (which a single TM step step M satisfies, with no macro-acceleration, drain, or unbounded-region requirement). That means for any machine with a simple 1-step local/regular invariant forbidding any finite word u on one half-tape, a solver can trivially prove IsSegmentedCryptid target_tm using Mode := Fin 6, vL = vR = .id [], and segsL s = [.gadget rawL], segsR s = [.gadget rawR] (IsNowhereDenseHalf holds by appending u past n), without discovering any macro/Collatz dynamics at all. Bounding .gadget w (e.g. w.length ≤ 16 + disallowing raw-tape wrapping, or adding macro-growth witnesses, or pinning SegState/segsL/segsR in BusyBeaverChallenge.lean) would close that loophole before Locking CORE_MANIFEST.json.
     • IsWordRunCryptid (BusyBeaver/Defs/WordRun.lean, lines 276–279): None of the 22 machines in this PR use IsWordRunCryptid yet, and lines 276–279 still use the older (∃ badL, ...) ∨ IsBoundaryAlignedSide ... disjunction rather than requiring IsNowhereDenseFamily on both encHalf specL and encHalf specR. Let's update those lines to IsNowhereDenseFamily on both sides before locking it into CORE_MANIFEST.json and BusyBeaverChallenge.lean.
     • M_1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_HHH1RE.lean (IsCryptid): Unlike the other 54 files in BusyBeaver/BB6/—which pin concrete ps plus Level B (State, start, encode, next, is_valid_acceleration, isHalt_iff_acceleration) in BusyBeaverChallenge.lean—this module only exposes existential IsCryptid target_tm (∃ ps, ps.length ≤ 16 ∧ ...). Note also that BusyBeaver/BB6/README.md lines 60–68 add it to the 55-machine BB6/ table right under "Each machine module in BusyBeaver/BB6/ below exposes both Level A (ps, is_closed_pattern_set, has_collatz_reduction) and Level B...", which doesn't hold for this file, and BusyBeaver/README.md line 121 says IsCryptid bounds "at most 16 patterns and 32 rules over alphabet size k + 2" whereas Defs/Patterns.lean only checks ps.length ≤ 16.

3. def target_tm vs load_rle_machine%:

   • All ~280 existing BB(6) modules use def machine := load_rle_machine% "..." + abbrev target := machine.toBB (so transition tables are tied directly to the RLE string via Bridge.lean without needing 22 per-machine *.target_tm entries in comparator/busy_beaver.json's definition_names). All 22 hardcoded target_tm tables match their RLE names, so this isn't a soundness bug, just worth considering switching to load_rle_machine% for consistency.

4. Category counts & linter/line-length cleanup:

   • Both the PR description and BusyBeaver/BB6/Accelerations/README.md (line 16) say IsSegmentedCryptid (10 machines) and IsStackCryptid (9 machines), whereas the actual files and table rows are 11 IsSegmentedCryptid, 8 IsStackCryptid, and 2 IsOdometerCryptid (11 + 8 + 2 = 21 + 1 IsCryptid = 22).
   • Love seeing autoImplicit = false enabled in lakefile.toml! Note though that the PR description says all lines are $\le 100$ chars, while BusyBeaver/Stack.lean and the 22 new M_*.lean files still have lines up to 128 chars with set_option linter.style.longLine false and linter.unused* false (plus quotPrecheck false in M_1RB1LE_...) at the top.

[TomZahavy]

Thanks for the thorough review @mo271! I merged #28 first, rebased onto origin/main, and addressed all four review points:

1. CI, zizmor, and rebase with #28

• Merged feat(busy_beaver): Port 11 single-file BB(6) proofs and SegCount #28 (7a0f20a) and rebased shared-core-defs-split cleanly onto origin/main.
• Verified .github/workflows/busy_beaver_ci.yml keeps the # v1.7.0 comment on SHA-pinned leanprover/lean-action, the !BusyBeaver/**/*.md path ignore filter, python3 tools/render_challenge.py --check, and python3 tools/check_manifest.py.

2. Anti-cheat tightening (IsWordRunCryptid, IsSegmentedCryptid, and #424)

• BusyBeaver/Defs/WordRun.lean: Moved IsNowhereDenseFamily here and dropped the IsBoundaryAlignedSide fallback disjuncts from IsWordRunCryptid, so IsNowhereDenseFamily is now required strictly on both encHalf specL and encHalf specR. Also switched viewPrefixLen to HalfTapeView.casesOn (motive := fun _ => ℕ) v List.length List.length, allowing us to remove BusyBeaver.viewPrefixLen from definition_names in comparator/busy_beaver.json.
• BusyBeaver/Defs/Segmented.lean: Added SegRegionKind.WellFormed (requiring blk ≠ [], non-empty .wordRun/.finWord words, exclusion of trivial [b] single-bit alphabet encodings, and .gadget w bounded to w.length ≤ 16), factored out public IsClosedSegmentedSystem over explicit (modes, ValidSeg, modeOf, segsL, segsR, evalCfg), and defined IsSegmentedCryptid via IsClosedSegmentedSystem.
• Exposed closed segmented systems: All 11 IsSegmentedCryptid files in BusyBeaver/BB6/Accelerations/ now expose their concrete (modes, ValidSeg, modeOf, segsL, segsR, evalCfg) interface and is_closed_segmented_system theorem, mirrored into BusyBeaverChallenge.lean and verified by comparator (using kernel-recursor word helpers to prevent cross-namespace match_1 deduplication collisions inside BusyBeaverChallenge.lean).
• #424 (BusyBeaver/BB6/M_1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_HHH1RE.lean): Replaced the generated proof with a clean 705-line Level A + Level B formalization pinning the 2-pattern invariant ps (pat_A, pat_Run) and State/start/encode/next, and registered all 5 theorems (is_closed_pattern_set, has_collatz_reduction, is_valid_acceleration, isHalt_iff_acceleration, is_cryptid) in BusyBeaverChallenge.lean and comparator/busy_beaver.json.

3. load_rle_machine% and definition_names cleanup

• Switched all 22 machine files (and BusyBeaverChallenge.lean) to define machine with load_rle_machine% and abbrev target : Machine (Fin 2) (Fin 6) := machine.toBB (marking helper target_tm + target_eq_target_tm private).
• Removed all 22 *.target_tm entries and BusyBeaver.viewPrefixLen from comparator/busy_beaver.json ("definition_names": []).

4. Category counts, documentation, and linter/style cleanup

• Corrected the holdout counts to 11 IsSegmentedCryptid, 8 IsStackCryptid, 2 IsOdometerCryptid (plus #424), and updated README.md, BusyBeaver/README.md (also removing the inaccurate "and 32 rules" claim in the IsCryptid row), BusyBeaver/BB6/README.md (including feat(busy_beaver): Port 11 single-file BB(6) proofs and SegCount #28's 191 / 159 + 1 IsNotHalt count reconciliation and #424 row), BusyBeaver/BB6/Accelerations/README.md, and comparator/README.md (735 theorems).
• Stripped all set_option linter.* false, quotPrecheck, maxHeartbeats, maxRecDepth, and autoImplicit overrides, converted remaining lemma declarations to theorem, marked internal helper declarations private, pruned all unused simp arguments, and wrapped all new/modified Lean files (Stack.lean, WordRunStack.lean, and all 22 M_*.lean files) to ≤ 100 characters per line.

Verification (after final edit)

• python3 tools/check_manifest.py: PASSED (12 core files verified)
• python3 tools/render_challenge.py --check: PASSED
• lake build BusyBeaver BusyBeaverChallenge: PASSED
• lake comparator --config=comparator/busy_beaver.json: PASSED (Lean default kernel accepts the solution / Your solution is okay! across all 735 theorems with definition_names: [])
• Style/hygiene check across all 36 changed .lean files: 0 lines > 100 chars, 0 disabled linters, 0 lemma, 0 forbidden tokens outside challenge stubs.

[mo271]

Thanks, LGTM