Skip to content

Add BB(6) stack, odometer, and transducer reductions and 20 open accelerations #18

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
TomZahavy merged 5 commits into from
Oct 27, 2026
Merged

Add BB(6) stack, odometer, and transducer reductions and 20 open accelerations #18

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0636a6f
Add BB(6) stack, odometer, and transducer reductions and 20 open acce…
Oct 26, 2026
632b7ec
Improve sequence notation, LaTeX rendering, and family overviews in A…
Oct 26, 2026
abcdd53
Add 13 higher-level Poincare accelerations in BusyBeaver/BB6/Accelera…
Oct 26, 2026
1c15434
Fix GitHub MathJax delimiter and Kleene-star rendering in Acceleratio…
Oct 26, 2026
d36c45f
Tighten BB(6) stack, odometer, and transducer predicates and fix READ…
Oct 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 32 additions & 1 deletion BusyBeaver.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,36 @@ public import BusyBeaver.BB6.M_1RB1RF_0LC0RF_1RD1LC_HHH0LE_0RC1LF_1RA0LE
public import BusyBeaver.BB6.M_1RB1RF_1LC1LF_0RE1LD_0LB1LD_HHH1RC_1RA0RD
public import BusyBeaver.BB6.M_1RB1RF_1LCHHH_1LE1RD_1RA0RC_0LF0LA_0LD0RB
public import BusyBeaver.BB6.M_1RBHHH_1RC1LE_0RD0RF_0RE0LA_1LF0LB_1LA1LD
public import BusyBeaver.BB6.Accelerations.Stack
public import BusyBeaver.BB6.Accelerations.M_1RB0LB_0RC0LD_1LD1RE_0LA0RF_0RD1RF_0RCHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LD_0RCHHH_0LD0RF_1LE1LD_0LA0RD_0RB1RA
public import BusyBeaver.BB6.Accelerations.M_1RB0LD_0RCHHH_1LD0RF_0LE0RA_0RA1LF_0LA1LB
public import BusyBeaver.BB6.Accelerations.M_1RB0LD_1LC1RD_0LE1LA_0RB1RD_HHH0LF_1RA1LF
public import BusyBeaver.BB6.Accelerations.M_1RB0LE_0RC0RA_1RD1RB_0LA0RB_1LFHHH_1LD1LF
public import BusyBeaver.BB6.Accelerations.M_1RB0LE_1LB1RC_0RF0RD_1RE0LA_1LA1RE_HHH0RB
public import BusyBeaver.BB6.Accelerations.M_1RB0RB_1RC0LE_1LD1LA_HHH0LC_1RF1LE_1RA0RA
public import BusyBeaver.BB6.Accelerations.M_1RB0RE_0RC1RE_1RD1LE_0LEHHH_1RA1LF_1RF0LC
public import BusyBeaver.BB6.Accelerations.M_1RB0RE_0RCHHH_1LD1LE_1LE1LD_1RF0LC_1RA1RF
public import BusyBeaver.BB6.Accelerations.M_1RB0RE_1RC1RE_1LD1LC_0RB0LC_1RF0RB_HHH1RA
public import BusyBeaver.BB6.Accelerations.M_1RB1LA_1LA0RC_1RD1RC_1LE0RC_HHH0LF_1LE0LA
public import BusyBeaver.BB6.Accelerations.M_1RB1LA_1LC0RE_HHH0LD_1RE0LF_1RA1RE_1LA0LB
public import BusyBeaver.BB6.Accelerations.M_1RB1LA_1RC0RF_1RDHHH_0LE1RB_HHH0LA_1LD1RF
public import BusyBeaver.BB6.Accelerations.M_1RB1LB_1LC1LA_1RD0LB_1RA1RE_1RF0RD_HHH1RD
public import BusyBeaver.BB6.Accelerations.M_1RB1LB_1RC0RD_0LA1RE_0RF1LC_1LA0RB_HHH1LC
public import BusyBeaver.BB6.Accelerations.M_1RB1LD_0RC0LF_1LD1RE_0LA0RB_0RD1RB_0LDHHH
public import BusyBeaver.BB6.Accelerations.M_1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_HHH0LB
public import BusyBeaver.BB6.Accelerations.M_1RB1LF_0RC0RB_0LD1RB_1LE0LB_0LA1LC_0LBHHH
public import BusyBeaver.BB6.Accelerations.M_1RB1RA_1LC0RC_HHH0LD_0LE0RF_1RE0RA_0LF1LB
public import BusyBeaver.BB6.Accelerations.M_1RB1RA_1RC1LB_1LD0RA_HHH0LE_1LC0LF_1RE0LB
public import BusyBeaver.BB6.Accelerations.M_1RB1RE_1LC0RA_HHH1LD_1LA0LF_0LB0LC_1RB0LB
public import BusyBeaver.BB6.Accelerations.M_1RB1RE_1LC0RC_1RA1LD_1RB0LA_0LC1RF_HHH1RD
public import BusyBeaver.BB6.Accelerations.M_1RB1RE_1LC1LB_1LE0LD_1LE1LC_0RF1RA_HHH1RA
public import BusyBeaver.BB6.Accelerations.M_1RB1RF_1LC0RE_1RD0LC_0LB0RA_1LD1RD_1RBHHH
public import BusyBeaver.BB6.Accelerations.M_1RB1RF_1LC1LF_HHH1LD_1LE0RA_1RE1LB_1RD0LD
public import BusyBeaver.BB6.Accelerations.M_1RBHHH_0RC0LD_1LB1RC_0LE0LF_1RD1LE_1RF1RA
public import BusyBeaver.BB6.Accelerations.M_1RBHHH_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA
public import BusyBeaver.BB6.Accelerations.M_1RBHHH_0RC1RD_1LA0LA_1LE0RB_1LF1LE_1LC0LD
public import BusyBeaver.BB6.Accelerations.M_1RBHHH_1LC0RF_0RA0LD_1LE1LA_1RF0LF_0LC0RA
public import BusyBeaver.BB33.WilyCoyote
public import BusyBeaver.BB33.M_1RB0LB0RC_2LC2LA1RA_1RA1LCHHH
public import BusyBeaver.BB33.M_1RB1LB2LC_1LA2RB1RB_HHH0LA2LA
Expand All @@ -74,7 +104,8 @@ public import BusyBeaver.BB33.M_1RB2RA1LC_2LC1RB2RB_HHH2LA1LA

Formal Lean 4 specifications and kernel-verified behavioral proofs (`IsHalt`, `IsNotHalt`,
`IsClosedPatternSet`, `HasCollatzReduction`, `IsClosedStackPatternSet`,
`HasStackedCollatzReduction`, `IsValidAcceleration`, `CollatzHalts`) for Busy Beaver holdout
`HasStackedCollatzReduction`, `HasStackReduction`, `HasOdometerReduction`,
`HasTransducerReduction`, `IsValidAcceleration`, `CollatzHalts`) for Busy Beaver holdout
Turing machines (`BB(6)` and `BB(3, 3)`), connected to `ConjectureMachines.Machine` via
`BusyBeaver.Bridge`.
-/
Loading
Loading