技術要約：Leanにおけるフラグ代数の形式化

問題提起

極値グラフ理論は、禁止されたパターンの集合 $H$ を回避するグラフにおける、特定の有限パターン $F$ の最大頻度に関する問題を頻繁に扱います。漸近的なTurán密度 $\pi(F; H)$ を決定することは非常に困難です。なぜなら、それは十分に大きなすべての $H$-freeグラフの挙動を制御する必要があるからです。Razborovのフラグ代数手法は、この設定に対して強力な手法を提供し、有限個の代数的条件を半正定値計画法（SDP）を通じてチェックすることによって、漸近的境界の証明を削減します。

しかし、この手法の実用的な適用は、外部のSDPソルバー（Flagmaticなど）によって生成された「候補証明書（candidate certificates）」に依存しています。これらの証明書は、数千もの正確な密度値と有理正定値（PSD）行列で構成されています。これらは数学的には正当ですが、これらの証明書を手作業で検証することは実用的ではなく、外部ソフトウェアを信頼せずに形式的な検証を行わないことは、証明の論理的な連鎖にギャップを生じさせます。課題は、外部の証明書を取り込み、基礎となる有限の組合せデータ（同型、密度、積）を検証し、外部ソルバーの信頼性に依存せず、かつデータの転記ミスも発生しない形で、証明助手（Lean）内で形式的な証明を生成できる機械チェック可能なフレームワークを作成することです。

手法

著者らは、Razborovのフラグ代数手法の包括的な形式化を、3つの層とメタ理論的な調査として構造化し、Lean 4で提示しています。

1. 仕様層（数学的基礎）

この層では、標準的な文献に密接に従い、有限単純グラフに対するフラグ代数の抽象的な数学的定義を形式化します。

• 定義: フラグ型（ラベル付きグラフの同型類）、フラグ、および自由ベクトル空間を拡大恒等式（連鎖律から導出される）による商とするフラグ代数 $A_\sigma$ を定義します。
• 意味論: 正の準同型を、構造と非負性を保存する $\mathbb{R}$ への写像として定義します。意味論的な非負性錐 $C_\sigma$ は、すべてのそのような準同型の下で非負となる要素の集合として定義されます。
• 制約付き意味論: 禁止グラフの制約 $H$ を代数の構成に組み込む伝統的な提示とは異なり、本形式化では「すべての有限単純グラフ」の周囲代数を構築します。$H$-freenessの条件は、後に「アンサンブル意味論（ensemble semantic order）」を通じて課されます。この順序は、ラベル付きフラグ上の不等式を解釈するために、ランダム拡張測量を用いて、グラフが $H$ を含む場合にゼロを割り当てる正の準同型を制限します。
• 下方演算子（Downward Operator）: ラベル付き代数要素をラベルなしの要素へと写す演算子を形式化し、それが意味論的な非負性を保存することを証明します（定理2.9）。

2. 反射層（実行可能な計算）

仕様層は非計算的な商型や抽象的な定義に依存しているため、必要な有限計算を実行するために別の「反射層」が開発されました。

• 具体的な表現: グラフを頂点として Fin n、エッジとして有限集合を用いる具体的なデータ構造（例：Sym2Graph）を使用して、グラフとフラグを表現し、列挙と決定可能な等価性を可能にします。
• 妥当性定理: この層の核となるのは、実行可能な計算（密度計算、同型チェック、下方正規化係数）が、仕様層の抽象的な定義と一致することを証明する定理です。
• メタプログラミング: カスタムのエラボレーション時コマンドにより、特定の証明書に必要なサイズに合わせて、特定のフラグ、密度テーブル、および乗法テーブルを生成します。これらのコマンドは、関連するすべての同型類がカバーされていることを保証する完全性補題を証明します。

3. 証明書・コンパイラ

このコンポーネントは、外部のSDP証明書を検証されたLeanの証明へと自動的に翻訳します。

• 入力: 目標グラフ、禁止グラフ、提案された境界、フラグ型、および有理PSD行列を含む、FlagmaticからのJSON証明書を受け取ります。
• 検証プロセス:
  1. 再生成: 証明書のデータを信頼するのではなく、反射層を使用して必要なフラグおよび密度／乗法恒等式を再生成します。
  2. PSD検証: 有理行列を再構成し、浮動小数点演算を避け、正確な $LDL^\top$ 分解を用いて、それらが $\mathbb{Q}$ 上で正定値であることを検証します。
  3. 代数的組み立て: 検証された恒等式を使用して、証明書の代数的恒等式（ギャップ $c \cdot 1 - [F]$ を下方平方および非負の剰余へと分解すること）を展開し、最終的な不等式をチェックします。
• 信頼モデル: コンパイラスクリプトは信頼されず、証明の提案を生成します。Leanは、行列の分解や代数的正規化を含むすべてのステップを独立してチェックします。スクリプトは、証明書フラグをLeanの列挙へとマッピングするための翻訳の忠実度（監査可能な形式での生成）のみにおいて信頼されます。

4. 制約付き意味論のメタ理論

論文では、「アンサンブル意味論」（実装で使用されるもの）と「商意味論」（制約が組み込まれているもの）の関係を調査しています。

• ルート・プランタビリティ（Root-Plantability）: 著者らは、2つの意味論的アプローチが一致する条件を特徴付けるために、「ルート・プランタビリティ」と呼ばれる基準を定義します。グラフのクラスが「ブローアップ閉（blow-up-closed）」（例：$r \ge 3$ における $K_r$-free グラフ）である場合、2つの順序が一致することを証明します。
• 反例: 彼らは、$C_4$-free グラフのケースにおいて、2つの順序が異なることを示す反例を提示しており、単なる継承性だけでは一致には不十分であることを示しています。

主な結果

著者らは、7つの異なる上限証明書についてコンパイラを評価し、以下の証明を機械チェックされた証明として生成することに成功しました：

1. Mantelの定理: $\pi(K_2; K_3) = 1/2$ の証明。
2. Erdősの五角形定理: $\pi(C_5; K_3) = 24/625$ の証明。（フラグ代数を用いない証明は知られていません）。
3. $C_4$ 密度: 三角形フリーグラフにおける $C_4$ の密度の理論的な上限。
4. エッジ密度境界: $K_4$-free、$K_5$-free、および $C_5$-free グラフに対する境界。

さらに、この形式化は（コンパイラを使わずに）直接以下に使用されました：

• 明示的な構成を用いて、Mantelの定理およびErdősの五角形定理に対する一致する下限を証明すること。
• Goodmanの2つの不等式を証明すること。

これら7つの証明書はすべて、sorry や公理を含まないLeanソースファイルへとコンパイルされました。7つのうち5つは完全に decide +kernel による検証が完了しましたが、最大の2つ（$K_5$-free および $C_5$-free エッジ密度）は、計算限界のため、ネイティブの decide を必要としました。これは著者らが明示的に認めている制限事項です。

意義と主張

本論文は、有限単純グラフに対するフラグ代数手法の最初の機械チェック可能な形式化を提供し、コンピュータ支援探索と厳密な形式的証明の間の溝を埋めるものであると主張しています。その意義は以下の通りです：

• 複雑な組合せ論の検証: 大量の正確な有限データとSDPの結果に依存するフラグ代数の証明が、外部ソルバーや手作業による転記に頼ることなく、証明助手によって完全に検証可能であることを示しています。
• モジュール化されたアーキテクチャ: 仕様（数学）、反射（計算）、およびコンパイラ（自動化）の層の分離は、他の極値問題を形式化するための再利用可能なフレームワークを提供します。
• メタ理論的洞察: アンサンブル意味論とルート・プランタビリティ基準の形式化は、実装によって課される制約に対する厳密な数学的理解を提供し、「ランダム・ラベル」のアプローチが「組み込み制約」のアプローチといつ等価になるかを明確にします。
• 新しい証明: Erdősの五角形定理の最初の形式的証明、およびGoodmanの不等式とTurán密度の下限に対する新しい形式的証明を提供します。

著者らは現在の限界についても謙虚であり、このアプローチが証明書の発見のために外部のSDPソルバーに依存していること、および5頂点を超えるスケーリングがカーネルチェックによる検証において依然として大きな計算上のハードルに直面していることを指摘しています。彼らは、この研究をハイパーグラフ、有向グラフ、およびグラフォン理論への統合に向けた基礎と見ています。