A Lean-Certified Proof of $K_8(4, 2) = 23$

技術要約：$K_8(4,2) = 23$ のリーン認定証明

問題提起
本論文は、$q$ 進ハミング空間における長さ $n$、半径 $r$ の被覆符号の最小サイズとして定義される正確な被覆数 $K_q(n,r)$ の決定に取り組んでいる。具体的には、8進数（octonary）の場合の長さ4、半径2における値 $K_8(4,2)$ を解決している。これまでの既存の境界（Kériの表）では、この値は $[22, 23]$ の範囲に置かれていた。下界はRodemichのルック・ドメイン（rook-domain）境界から導かれ、上界は大きなアルファベットを用いた境界によって支持されていた。本研究の目的は、下界 $K_8(4,2) \ge 23$ を証明することで、この区間を閉じることである。

手法
証明は、mathlib ライブラリを用いた Lean 4 形式の定理証明器を用いて定式化されている。これは、「証明を伴う（proof-carrying）」アプローチを採用しており、結果は明示的な上界と構造的な下界という2つの独立した証明書を通じて確立される。

1. 上界 ($K_8(4,2) \le 23$):
   著者らは、$(\text{Fin } 8)^4$ における23個の符号語からなる明示的な符号を提供する。形式的な証明では、集合の濃度が23以下であること、および周囲の空間（4096語）のすべての語が少なくとも1つの符号語からハミング距離2以内にあることを検証する。これは、有限の全探索である。

2. 下界 ($K_8(4,2) \ge 23$):
   本論文の核心は、仮説的な被覆 $C^*$（ただし $|C^*| \le 22$）に対する構造的な非存在論的議論である。証明は一連の簡約化を通じて進行する：

   • ファイバー計数 (Fiber Counting): 仮説的な被覆に対し、著者らは「ファイバー」$C^*_{i,a}$（座標 $i$ で記号 $a$ を持つ符号語）を定義する。彼らは、すべてのファイバーが少なくとも2つの符号語を含むことを証明する。これにより、各座標につき16個の符号語（8記号 $\times$ 2）という基準が確立され、$|C^*|=22$ の場合の余剰予算は最大6個（$|C^*| \le 21$ の場合は5個）となる。
   • 欠落ペアグラフ (Missing-Pair Graphs): 証明は「逆」の視点へと移行し、符号の座標ペアへの射影において、どの記号のペアが「欠落」しているかを分析する。これらの欠落したペアはグラフ $E_{ij}$ を形成する。
   • ケース $|C^*| \le 21$: 限られた余剰予算を用い、著者らは組合せ論的な計数を通じて、欠落ペアグラフが「同時4部完全グラフ（simultaneous four-partite clique）」（すべての6つの座標ペアが欠落している4つの記号 $a,b,c,d$ の集合）を含むことを示す。補題7は、このようなクリークが有効な半径2の被覆には存在し得ないことを証明しており、これによりサイズ21以下の被覆を排除する。
   • ケース $|C^*| = 22$: 残されたケースについて、証明は欠落ペアグラフの「プロファイル」の有限分類の問題へと還元される。著者らは、有効なプロファイルは必ず特定の「共通の $3+3+2$ ブロック構造」を示すことを示す。
   • SAT/LRAT の統合: これらのプロファイルの分類は、手動での列挙には大きすぎる。著者らは、制約（行/列の次数境界およびノー・クリーク条件）を、共役標準形（CNF）インスタンスへとエンコードする。彼らは、信頼できないSATソルバを使用して、充足不能性の証明である線形RAT（LRAT）証明書を生成する。
   • 形式検証: Lean はこれらの LRAT 証明書を解析し、それらの反駁（refutation）を機械的に再再生して、22語の被覆が存在しないことを証明する。
   • 最終的な矛盾: 共通のブロック構造が仮定されたとしても、著者らはその構造の「2記号コンポーネント」において矛盾を導出する。このコンポーネントは、最大4行を持つ長さ4のバイナリ強度2のアレイを必要とするが、これは数学的に不可能である。

主な貢献

• 正確な値: 本論文は、正確な値 $K_8(4,2) = 23$ を確立し、以前の既知の区間 $[22, 23]$ を閉じた。
• 形式化された下界: ファイバー計数と欠落ペアグラフから導かれる構造的な障害物を用いて、22語の被覆をすべて排除する完全な形式化された証明を Lean 4 で提供している。これは、体積引数によるものではなく、構造的な障害物によって達成される。
• 証明を伴うアーティファクト: 結果は、明示的な符号、構造的補題、CNF インスタンス、および LRAT 反駁を含む Lean アーティファクトとしてパッケージ化されている。決定的なことは、SAT ソルバは信頼された計算基盤（trusted computing base）の一部ではないことであり、Lean は内部で LRAT 証明書を検証する。
• 計算的下界のパターン: 被覆符号の下界に対して、ソルバによって生成された証拠を付加するための再利用可能なパターンを導入している。これは、「発見」（信頼できないソルバ）と「検証」（信頼できる Lean カーネル）を分離し、大規模な有限分類問題を計算的に解きながら、形式的な正当性を維持することを可能にする。

結果
主要な結果は、定理 $K_8(4,2) = 23$ である。

• 上界: 明示的な23語の符号によって証明される。
• 下界: 22語の被覆が、不可能なバイナリアレイを伴う「共通の $3+3+2$ ブロックシステム」を強制するという矛盾を導くことを示すことで証明される。
• パフォーマンス: 形式検証にはかなりの計算リソースを要する。メインの証明ファイルのカーネルモードでの再再生には約143 GiB の RAM が必要であったが、ネイティブモードではこれを約5.5 GiB に削減できた。LRAT チェックフェーズは、カーネルモードで約17分を要した。

意義と主張
本論文は、主に形式化された数学、および組合せ論的推論と計算的証明書を組み合わせる手法の領域における意義を主張している。

• 方法論的転換: 構造的組合せ論が、どのように「証明を伴う」計算的証拠と結合できるかを示している。SAT ソルバは有限の障害を発見するために使用されるが、数学的な架け橋とソルバの出力の検証は、すべて定理証明器内で行われる。
• 信頼の境界: SAT ソルバを含む形式的証明における信頼の境界を明確にしている。ソルバは信頼されておらず、Lean カーネルが LRAT 証明書と、それらの証明書を被覆符号の記述に結びつける論理的演繹をチェックする。
• スケーラビリティ: 本結果は、手動の証明には大きすぎるが、SAT ソルバによって解ける有限分類問題へと還元できる被覆符号問題に対処するためのテストケースとして機能する。
• 新しい応用なし: 本論文は、$K_8(4,2)=23$ という値自体の新しい応用を主張したり、新しい実験的プロトコルを提案したりするものではない。その貢献は、符号理論のテーブルにおける特定の未解決問題の解決と、そのような問題のための形式検証ワークフローの提示に厳密に限定される。