The continuous functional calculus in Lean

技術的要約：Leanにおける連続関数解析

問題提起
連続関数解析は、$C^*$環の理論における基礎的な道具であり、可換な$C^*$部分環をコンパクト・ハウスドルフ空間上の連続関数の環と同一視することを可能にする。数学的には十分に理解されているものの、これをLeanのような証明助手で形式化することには大きな困難が伴う。主な困難は、数学的な忠実度と**使いやすさ（usability）**のバランスを取る点にある。「自然な」数学的定義は、多くの場合、依存型（例：ある要素のスペクトル上でのみ定義された関数）やバンドルされた構造（例：特定の型としての連続写像）に依存する。これらは厳密ではあるが、形式的な証明において摩擦を生む。すなわち、型が特定の要素に依存しているために書き換え（rewriting）による等式の操作が困難になったり、関数の合成を行う際に複雑な部分型への強制（subtype coercion）や連続性の証明を管理しなければならなくなったりするのである。著者らは、厳密な数学的単純さを優先する設計は、Mathlibのようなライブラリに求められる実用的な使いやすさの「リトマス試験」に失敗することを特定した。

手法と設計決定
著者らは、Lean 4を用いた連続関数解析の形式化を開発し、これをMathlibライブラリに統合した。彼らの手法は、数学的に「純粋な」定義から「実用的な」インターフェースへと移行する、反復的な設計プロセスを含んでいる。主な設計決定は以下の通りである：

1. アンバンドリングと「ジャンク値（Junk Values）」:
   関数解析を、スペクトル上の連続関数の型 $C(\sigma(a), \mathbb{C})$ から代数への写像として定義する代わりに、著者らは任意の関数 $f: \mathbb{C} \to \mathbb{C}$ と任意の要素 $a$ を受け取る関数 cfc を定義した。もし $a$ が正規（normal）でなかったり、$f$ がスペクトル上で連続でなかったりする場合、この関数は「ジャンク値」（通常は0）を返す。

   • 根拠: これにより、ユーザーは $a$ が正規であることや $f$ が連続であることを最初に証明することなく、$f(a)$ のような式を書くことができるようになる。これは、数学的な直感に基づき、「まず書き、後で考える」というアプローチを模倣しており、非自明な性質が必要になるまで証明の負担を遅らせるものである。また、引数の型が $a$ の特定の性質に依存しなくなるため、シームレスな書き換え（rw）が可能になる。

2. クラスベースの抽象化:
   異なるスカラー環（$\mathbb{C}$、$\mathbb{R}$、および $\mathbb{R}_{\ge 0}$）や異なる要素の型（正規、自己随伴、非負）を扱うために、著者らはこの関数解析を型クラス ContinuousFunctionalCalculus として実装した。

   • 述語の一般化: このクラスは、代数の要素に対する述語 $p$（例：IsStarNormal、IsSelfAdjoint、0 ≤ a）によってパラメータ化されている。これにより、コードの重複を避けることなく、単一のインターフェースで様々なケースをカバーできる。
   • Prop値かデータか: 初期のバージョンには $*$-準同型写像自体がデータとして含まれていた。しかし、定義的等価性（二つの異なる構成が同じ写像であっても定義的に等しくない場合があること）の問題を避けるため、最終的な設計では、このクラスを Prop とした。これは、特定の性質を持つ一意な $*$-準同型写像の「存在」を主張するものであり、写像そのものを格納するものではない。

3. 非単単位代数の扱い:
   この形式化は非単単位 $C^*$環にも拡張される。すべての定義において最小単位化のような外的な構成に依存する代わりに、著者らは**準スペクトル（quasispectrum）**の固有の定義を導入した。非単単位の関数解析は、0で消える（または0を0に写す）関数に対して定義されており、単単位と非単単位の文脈を絶えず切り替える必要を回避している。

4. autoParam による自動化:
   連続性と正規性の証明を手動で渡す際の冗長性を軽減するため、著者らはLeanの autoParam 機能を利用した。「$f$ はスペクトル上で連続である」といった仮定にはデフォルトのタクティクが備わっている。ユーザーが証明を提供しない場合、Leanは既存の補題（aesop や fun_prop など）を用いて、それを自動的に合成しようと試みる。

5. 独立したクラスとしての一意性:
   合成の性質（$g(f(a)) = (g \circ f)(a)$）は理論の中心である。著者らは、ストーン＝ウィアシュトラスの定理（$\mathbb{R}_{\ge 0}$ に対しては失敗する）を用いるのではなく、一意性の議論を用いてこれを証明した。彼らは $*$-準同型の一意性を別のクラス ContinuousMap.UniqueHom にカプセル化することで、異なるスカラー環にわたって合成の性質を汎用的に導出できるようにした。

主要な貢献と成果

• 初の形式化: 本研究は、連続関数解析を任意の証明助手において初めて形式化したものである。
• Mathlibへの統合: 実装はMathlibにマージされており、複素数、実数、および非負の実数に関する関数解析の統一されたインターフェースを提供している。
• 使いやすさの検証: 設計は、以下の「リトマス試験」を含む具体的なテストによって検証された：
  • 連続でない関数（例：$x \mapsto x^{-1}$）を用いた逆元（$f(a^{-1})$）の定義。
  • 自己随伴要素および非負要素に対する正の部分・負の部分および平方根の構成。
  • $\mathbb{R}$ 上の行列（Mathlibにおいて大域的な計量構造を持たないもの）への関数解析の適用。
• 自動化: インターフェースは高レベルの自動化をサポートしており、ユーザーは最小限の手動介入で $f(-a) = (x \mapsto f(-x))(a)$ のような性質を証明できる。
• 応用: このインターフェースは、すでに以下のような高度な結果の形式化に使用されている：
  • 非単単位 $C^*$環における近似単位の存在。
  • 両方の変数に関する関数解析の連続性。
  • 写像 $a \mapsto |a|$、$a \mapsto a^p$、および $a \mapsto \log(a)$ に関する性質。
  • ユニタリ要素および射影に関する結果。

意義と限界
本論文は、その意義を主に設計哲学に求めている。すなわち、大規模な形式ライブラリにおいてツールが効果的であるためには、定義における厳密な数学的純粋さよりも、エンドユーザーのエルゴノミクス（使いやすさ）を優先しなければならないということを示している。ジャンク値を受け入れ、型をアンバンドリングすることで、著者らは数学者にとって直感的に振る舞うインターフェースを作り上げ、厳密な依存型アプローチでは極めて困難になるであろう複雑な操作（合成や書き換えなど）を可能にした。

著者らは現在の状態について謙虚であり、以下のいくつかの限界を認めている：

• 簡約補題（Simp Lemmas）: autoParam をトリガーするために明示的な引数が必要なため、多くの補題は手動の介入なしには simp ルールとして使用できず、一部の証明が意図したよりも冗長になっている。
• $\mathbb{R}_{\ge 0}$ の複雑さ: スカラー環として非負の実数を使用することは、特定の技術的な障害（例：切断された減算、環構造の欠如）を導入し、それらには個別の定理の記述を必要とする。
• 実 $C^*$環: このフレームワークは実 $C^*$環をサポートするように設計されているが、実代数上の複素数に関する関数解析（これは異なる関数のドメインを必要とする）の具体的なケースはまだ完全には統合されておらず、今後の課題とされている。

結論として、本論文は、深い作用素環理論を使いやすい形式システムへと翻訳するプロセスを記録しており、交互定理証明の文脈における数学的な優雅さと実用的な有用性の間のトレードオフを浮き彫りにしている。