BB(10) > グラハム数

レベルf_(ω+1)の10状態マシン 1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_0RG1LD_1RH1LG_1LC0RG_0LJ0LI_1RZ0LC 以下では、このマシンをn1と呼びます。これは空白テープから停止し、その正確なスコアはCoqで証明されており、スコアはf_(ω+1)の2つの値の間にあります。現在のBB(10)チャンピオンは、高速増加階層のωレベルで、公開されている上限f_ω(f_ω(25))を持っています。n1はそれを上回り、BB(10)をω+1レベルに引き上げます。 執筆日 2026-10-08 0 1 A 1RB 0RA B 1LC 1LF C 1RD 0LB D 1RA 1LE E 1LI 0LC E0 はベースマシンの停止遷移でした F 0RG 1LD G 1RH 1LG H 1LC 0RG I 0LJ 0LI 新しい J --- 0LC 新しい; J0 は未定義で、停止です（文字列中の1RZ） どこから来たのか 状態A–Hは、ベースマシンと呼ばれる8状態のマシンを形成します。これは、状態A–EにおいてBB(8)記録1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_1LC0RH_1RG1LF（../BB8/）と一致します。これは、36桁を持つBB(7)チャンピオンのプログラムと同じ数字リスト計算を実行します。n1はベースマシンを維持し、その停止遷移E0を新しい状態Iに送り、状態IとJを追加します。 主な事実 ここで、T = 2↑^37 3 は、BB(8)記録が計算する値であり、F(x) = 2↑^x 4 = 2↑^(x+1) 3 です。「ones」は、Jが0を読み取ったときのテープ上の1の数です。標準スコアはσ = ones + 1です。なぜなら、停止遷移は1を書き込むからです。 停止: はい、マシンチェック済み（Coq、公理なし）。 正確なスコア: マシンチェック済み: ones = 2W + 3·2↑^(W+1)(2↑^n 5) + 12·JJ + 5、ここでJJ = (3T − 13)/7 であり、(n, W) は明示的な再帰（セクション4.4）から来ています。 下限: マシンチェック済み: ones > F^N(33)、つまり、N = (6T − 19)/7 ≈ 0.86·T 回 F を 33 に適用したものです。 レベル: マシンチェック済み、標準的な高速増加階層を使用: f_(ω+1)(JJ − 2) < ones < f_(ω+1)(6T)。 グラハム数: マシンチェック済み: ones > グラハム数。 BB(10)チャンピオン: 破られました、チャンピオン自身のCoqで証明された正確なスコアに対してマシンチェック済み。 1. 仕組み 1.1 テープの読み取り 表記は、LigockiによるBB(7)チャンピオンの分析（bbchallenge wiki page for 1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_0RG0RF）に従います。 トークン: テープはブロックD(t) = (10)^t 1 の文字列です。したがって、D0 = 1、D1 = 101、D2 = 10101、というようになります。ブロックの文字列は、1つの方法でしかトークンに分割されません。 構成: [t_1, t_2, …, t_k | A] は、テープ 0^∞ D(t_1) D(t_2) … D(t_k) D0 D(A) H> 0^∞ を意味します。トークンはテープ上のように左から右にリストされ、t_k はヘッドの隣にあります。A はアキュムレータです。そのすぐ左にあるD0は表記の一部であり、リストされていません。ヘッドは、D(A)の右にある空白セル上の状態Hにあります。リスト内では、x^j はトークンxのj個のコピーを意味します。 数字とゼロ: トークン3d + 1 は数字dです。特にトークン1（つまりD1）はゼロであり、1^n はn個のゼロを意味します。 ユニットとブロッカー: トークン3d + c（c ∈ {0, 1, 2}）はd個のユニットを保持します。クリアリングはユニットを1つずつ削除します。トークンにユニットがなくなると、cになります。c = 1 の場合、それはゼロです。c = 0 または c = 2 の場合、それはブロッカーです。クリアリングルールはD0またはD2から借りることができません。 深さ: トークンの深さは、それとアキュムレータの間のゼロの数です。[…, t, 1^j | A] では、トークンtの深さはjです。 値: アキュムレータA ≡ 1 (mod 3) の値は v = (A + 8)/3 です。リセットされたアキュムレータA = 4 の値は v = 4 です。 矢印: 2↑^0 x = 2x、2↑^1 x = 2^x、そして 2↑^(k+1) x は、1から始めて 2↑^k x を適用したものです。2つの恒等式が頻繁に使用されます: 2↑^k 2 = 4、そして 2↑^(k+1) 3 = 2↑^k 4。 Ligockiの表記では、B(a; d_1, …, d_k) = [3d_k+1, …, 3d_1+1 | 3a+1] であり、v = a + 3 です。彼のg_j(x) = 2↑^j(x+3) − 3 （BB(8)記録の定数を使用）は、以下の v ↦ 2↑^j v の写像です。 例: ステップ6447で、n1は構成 [7, 1^35 | 4] にあります。これは、1つの数字2、次に35個のゼロ、そしてアキュムレータ4（v = 4）です。テープ上では、これはD7 (D1)^35 D0 D4、つまり 101010101010101 (101)^35 1 101010101 H> です。Ligockiの表記では、これはB(1; [0]*35, 2)であり、BB(8)記録のメインフェーズの開始です。 1.2 エンジン n1は、BB(7)チャンピオンとBB(8)記録のクリアリングルールを使用します。 深さjのトークンの1ユニットをクリアすると、値vが2↑^j vに変わります。深さ0ではvを2倍します。深さ1では2^v、深さ2ではv個の2の塔になります。クリアリングは常に、ゼロではない最も近いトークンに対して機能します。そのトークンがブロッカーの場合、クリアリングルールは適用されず、リストは使い果たされます。BB(8)記録では、使い果たされたリストは停止につながります。n1では、それはセクション2の特別なイベントのいずれかを開始します。 1.3 フェーズ1: BB(8)記録の計算 空白テープから、n1は6447ステップ後に[7, 1^35 | 4]に到達します。次に、深さ35の7の2ユニットをクリアします: v = 4 → 2↑^35 4 → 2↑^35 (2↑^35 4) = 2↑^36 4 = 2↑^37 3 = T 結果は[1^36 | 3T − 8]です。36個のゼロと値v = Tです。これらは記録自身の構成です。BB(8)記録はここで停止し、その最終スイープは約12T個の1を書き込みます。シミュレーションでは、ここまでのルールはE0を読み取ることはありませんでした（セクション1.8）。したがって、ここではn1はベースマシンと全く同じように動作します。 1.4 フェーズ2: Tがカウントダウンになる リストは使い果たされました。左へのウォーク（イベントH）は、一番左に2A + 4 = 6T − 12個の新しいゼロを書き込みます。次にS0（E0の最初の読み取り）が左端を整理します。クリアリング、何も駐車されていないイベントP4、そして別のクリアリングが最初の期間開始を与えます: [2, 5, 1^(6T−19), 0, 0, 2, 1^34 | A] 左から読むと、最初の2はゴミです。D2トークンの連続で、ここでは1つ、期間ごとに4つ追加されます。5はマーカーです。1^m はカウンターで、ここではm = 6T − 19 個のゼロです。D0 D0 のペアは壁です。次のD2はブロッカーです。1^n はアクティブリストで、ここではn = 34 個のゼロです。アキュムレータは巨大な値v > Tを保持しています。クリアリングルールはアクティブリストに対してのみ機能します。アクティブリストとカウンターの間には常にブロッカー（D2、D0、またはD0 D0壁）があるため、クリアリングはカウンターのゼロを数字として使用しません。特別なイベントのみがカウンターに触れ、各イベントは固定数のゼロを削除します: 期間あたり6 + 6 + 2 = 14。 1.5 フェーズ3: 期間 期間開始時、アクティブリストは使い果たされます。ゼロのみを含み、その末端はブロッカーD2です。1期間は同じ4ステップのサイクルを2回実行します。 駐車: アキュムレータはリスト内に移動します。ゼロのすぐ外側のトークンとして（イベントP1、または2回目のP3）。その値vは現在格納されています。アキュムレータは6にリセットされます。 新しい小さな値: R2は駐車されたトークンから1ユニットを借り、隣のゼロに6をトークン9（深さn-1で3ユニット）として書き込みます。それらのユニットをクリアすると、新しい値v₁ = 2↑^n 5 が得られます。9はD0として終了するため、リストは再び使い果たされます。 展開: イベントP2（またはP4）は、約vユニットを保持する駐車されたトークンを、アクティブリストの約2v個の新しいゼロに変換します。v₁を保持するアキュムレータは、新しいゼロの反対側にあるトランジットトークンになります。アキュムレータは4にリセットされます。 ジャンプ: 新しい深さn' ≈ n + 2v のトランジットトークンをクリアすると、約2↑^(n'+1) v₁ の新しい値が得られます。トランジットトークンはD2ブロッカーとして終了するため、リストは再び使い果たされ、次のステップは駐車です。したがって、各半期間は深さをnから少なくともn + 2vに移行します。ここでvはすでに少なくとも2↑^n 4です。したがって、深さはnから少なくともF(n) = 2↑^n 4（Coq lemma growth）に移行し、1期間はnから少なくともF(F(n))に移行します。Fはf_ωの速度で増加します: 2↑^n 4 はおよそf_(n+1)(4)であり、Coqはf_ω(x) ≤ F(F(x)) を x ≥ 3 に対して証明します。展開は無料です。P2とP4は、駐車された値とトランジット値のそれぞれに対して有効であり、両者を関連付ける条件はありません。現在の小さな値は、大きな駐車された値の代金を支払う必要はありません。 1.6 フェーズ4: 終了 カウンターは6T − 19から始まり、期間ごとに14ずつ減少します。期間がカウンター7で開始すると、P1は6を取り、1を残します。これはP2には少なすぎるため、最終的な展開は異なるイベントEになります。これは一番左に固定の44セルパターンを書き込みます。そのトランジットトークンは≡ 0 (mod 3)であるため、D2ではなくD0までクリアされます。その後、マシンは左に歩いて固定パターンに入り、状態Jで0を読み取って停止します。カウンターが正確に7に達するのは、6T − 19 ≡ 7 (mod 14)、つまりT ≡ 2 (mod 7)の場合のみです。CoqはT ≡ 2 (mod 7)（T_mod7）を証明します。したがって、JJ = (3T − 13)/7 ≈ 0.43·T の完全な期間と、その後半分の期間があります。合計でN = 2