Skip to content

Classify BB(6) hardness, port 6 missing stack cryptids, and prove halting evidence #22

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 6 commits into from
Nov 2, 2026
Merged

Classify BB(6) hardness, port 6 missing stack cryptids, and prove halting evidence #22

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
7cd6306
Add BB(6) hardness classification: BusyBeaver.BB6.Hardness and per-ma…
Oct 29, 2026
645f48f
Add HasStackReduction proofs for the three other start states of 1RB-…
Oct 29, 2026
75490e4
Prove IsHalt equivalence of the busycoq-merged pair 1RB0LE_0RC1RC_0RD…
Oct 29, 2026
e042400
Port Halving Tower #659/#209/#480, add HardnessEvidence, and update docs
Oct 29, 2026
fb51286
Address review comments on PR #22: stack transport, HardnessEvidence,…
Nov 2, 2026
365ec98
Fix namespace reference in BusyBeaver/BB6/Accelerations/README.md
Nov 2, 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
9 changes: 9 additions & 0 deletions BusyBeaver.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,9 @@ public import BusyBeaver.Cert
public import BusyBeaver.WordRLE
public import BusyBeaver.AffRLE
public import BusyBeaver.ElabRLE
public import BusyBeaver.BB6.Equivalences
public import BusyBeaver.BB6.Hardness
public import BusyBeaver.BB6.HardnessEvidence
public import BusyBeaver.BB6.M_1RB0LB_1LC0RE_1LA1LD_0LCHHH_0RB0RF_1RE1RB
public import BusyBeaver.BB6.M_1RB0LC_0LC0RF_1RD1LC_0RA1LE_HHH0LD_1LF1LA
public import BusyBeaver.BB6.M_1RB0LC_0LC1RF_1LE1RD_0RC1RC_0LA1LA_HHH1RA
Expand Down Expand Up @@ -67,6 +70,8 @@ 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_1RB0LC_1LC0RE_1LD1LC_1LA1RD_HHH0RF_0LB0RD
public import BusyBeaver.BB6.Accelerations.M_1RB0LC_1RC1RE_1LA0LD_0RB0RA_1RB1RF_1RDHHH
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
Expand All @@ -75,6 +80,7 @@ public import BusyBeaver.BB6.Accelerations.M_1RB0LE_1LB1RC_0RF0RD_1RE0LA_1LA1RE_
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_1LC0RA_1LA1LD_1LC1LF_0LC0LB_1LEHHH
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
Expand All @@ -84,8 +90,11 @@ public import BusyBeaver.BB6.Accelerations.M_1RB1LB_1RC0RD_0LA1RE_0RF1LC_1LA0RB_
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_1RE0LD_0RE0LF_1RAHHH_1RB1LF
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_1RB1RC_1LC0LE_1RD1RC_1LB0RA_HHH0LF_1RD1LF
public import BusyBeaver.BB6.Accelerations.M_1RB1RD_1LC0LE_1RA0LB_1RA1RF_0RA0RC_1REHHH
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
Expand Down
Loading
Loading