本記事はHashnodeに公開したAtlas Theorem: How Far Can You Zoom Out?の日本語訳です
TL;DR
- ベテランのレビュアーは、コードを全行読まない。確認したい性質に応じて、読む解像度を切り替える。 その粗い読みがバグを見逃さない保証はあるのか。この記事は、その保証の条件を証明した話だ
- AAT(代数的アーキテクチャ論)は、ソースコードを Source of truth とし、実装を Atom という部品に抽象化、仕様を law 方程式化して、アーキテクチャを代数幾何の武器で解析する理論。欠陥はコホモロジー類、つまり代数的な指紋として現れる
- その AAT で、Atlas 定理と呼ぶ定理を AI エージェントのループが Lean 4 で証明した。一方が他方の粗視化である2つの adequate な読みが較正条件 C を満たすなら、診断の指紋は完全に一致する。粗くしても欠陥は消えず、細かくしても捏造されない。条件を破れば両方の事故が実際に起きる(有限反例つき)
- エージェントは登頂までに自分の証明対象を4回反証した。さらに no-go の論法が「形だけの条件では原理的に不可能」を示し、係数の定義そのものの作り直しを強制した。実働5日間、31 モジュール / 13,028行、4レーンの敵対査読
- 記事はドット絵と標本化定理から始めて、4回の反証と条件 C の発見を経て、AI がコードを書く時代のレビューにとっての意味まで述べる
フォトリアルな肖像画でも、16×16 のドット絵でも、人は同じ顔を感じ取る。漫画理論家のスコット・マクラウドはこれを単純化による増幅と呼んだ。線を減らすことは情報を捨てることではなく、本質を際立たせることだ、と。
では、ソフトウェアアーキテクチャの診断で同じことが言えるだろうか。サービス粒度で見ても、モジュール粒度で見ても、同じバグが同じ場所に見える。 体感ではなく、証明された保証として。
この記事は、その保証を Lean 4 で形式証明するまでの記録だ。証明に挑んだ AI エージェントは、証明するはずだった主張を4回反証してしまった。そして、その4回が一番の収穫だった。主役は個々の証明テクニックではない。反証を「失敗」ではなく「成果」として蓄積させた規律だ。
すべて2026年8月4日〜8日、実働5日間の出来事である。
| ラウンド | 出来事 | 残ったもの |
|---|---|---|
| 反証1 | 「塗り」の持ち上げ忘れ | 条件1本と有限反例(Lean 937行) |
| 反証2 | 並行する持ち上げの見落とし | 条件もう1本と有限反例(622行) |
| 反証3 | 環状線の持ち上げ先がずれる | 条件さらに1本と有限反例(903行) |
| 転回 | no-go: 条件の継ぎ足しでは原理的に届かない | 係数の定義の作り直し |
| 反証4 | 改訂仕様のスペック穴 | 宣言規則の修理と有限反例(433行) |
| 登頂 | 24サイクルで主張 (i)–(v) 全証明 | 31 モジュール / 13,028行 |
前提: どんなプロジェクトか
対象は AlgebraicArchitectureTheoryV2。ソースコードを Source of truth とし、実装をAtomという部品に抽象化、仕様をlaw方程式化。アーキテクチャを幾何として扱い、代数幾何の武器で解析する。それが AAT(代数的アーキテクチャ論)であり、このモノレポはその理論を Lean 4 で形式検証している。
この理論には、ずっと見て見ぬふりをされてきた急所があった。粒度選択だ。
アーキテクチャを分析するとき、誰もが暗黙に解像度を選んでいる。サービス単位で見るのか、モジュール単位か、メソッド単位か。もし選んだ粒度によって診断結果が変わるなら、その診断はアーキテクチャの性質を測っているのか。それとも観測者の都合を測っているのか。
この問題の先例がひとつある。標本化定理(Nyquist–Shannon)である。信号の帯域に対してサンプリングが粗すぎると、実在しない周波数が現れ(エイリアシング)、実在する信号が消える。カメラのモアレ縞は前者の目に見える姿だ。粒度選択の問題は、アーキテクチャ診断における標本化の問題にほかならない。
用語集
| 用語 | 何であるか |
|---|---|
| 読み(reading) | ソースコードをどの解像度で部品(Atom)に区切るかの選択。ドット絵の「ドット数を決めること」に相当 |
| 診断類 | 欠陥の代数的な指紋。個々のファイルの中ではなく、部品どうしの貼り合わせのねじれとして計算される(数学的にはコホモロジー類 H¹。後述「定理の舞台」で定義)。ゼロなら整合、非ゼロなら欠陥 |
| adequate | 「語りたい法則(law)が、その解像度で語れる」こと。ドット絵師の技術(顔に効く区別だけを残す)の形式化 |
| 比較写像 | 細かい読みの診断と粗い読みの診断を突き合わせる橋。この橋が同型(1対1対応)なら「診断は解像度に依らない」 |
| witness | 主張の実例・反例を、抽象論ではなく有限の具体データとして Lean に固定したもの |
主張 — Atlas 定理
十分に情報を保った粗視化なら、細かく見ても粗く見ても、検出される欠陥の指紋は増えも減りもしない。
Atlas 定理(正式名: Diagnostic Resolution Invariance Theorem)
一方が他方の粗視化になっている2つの adequate な読みが、較正条件 C を満たすなら、比較写像は同型である。すなわち、解像度の選択は診断を一切変えない。細かく測っても診断は増えず(No-New-Diagnostics 系)、粗く測っても消えない。
対として: 条件を破る粗視化では、実在しない欠陥が現れるか、実在する欠陥が隠れることが実際に起きる(有限反例つき)。
Lean 上では、これを5つの主張の束として固定している。(i) 比較写像の構成、(ii) その全単射性、(iii) 系(細かく測っても新しい診断は生まれない)、(iv) 条件を破る反例3種、(v) 全条件成立下で非ゼロの診断が実際に流れる発火 witness。冒頭の表の「主張 (i)–(v)」はこの5つだ。
定理の舞台 — nerve・読み・係数
アーキテクチャの観測は nerve という有限の組み合わせ構造で表す。頂点にあたるのが chart。部品と、その部品が担当する範囲(台)の宣言だ。2つの chart の間の依存や重なりが edge、3つの chart の整合が確認済みであるという宣言が face(三角形)。nerve に要求する公理は最小限で、各 face の3辺(boundary triple)の端点が噛み合っていること、つまりある3つの chart A, B, C について e₀ : A → B、e₁ : A → C、e₂ : B → C の形に揃っていること。それだけだ。
解像度の選択は読み(reading)で表す。細かい読みと粗い読みの間に「一方が他方の粗視化である」という関係が成り立つとき、細かい側の値を粗い側の値へ送る因子写像 π が一意に立つ(この粗さ順序と因子写像の存在・一意性は、同じリポジトリで先に証明済みの定理をそのまま輸入している)。細かい側・粗い側それぞれの nerve を、chart / edge / face の対応が端点・boundary と可換になる nerve 射 φ で結ぶ。これが「ドット絵と原画の対応」の形式化だ。
係数は law から生成する。law family の各 law を読みに通して降ろした(descend した)評価値から、後述する生成契約 K0 / K1 に従って各 cell の上の係数空間を作り、3段の複体を組む。
C⁰(chart 上) --d₀--> C¹(edge 上) --d₁--> C²(face 上)
d₀ は「edge の両端での値の差」、d₁ は「face の3辺での値の交代和 e₀ − e₁ + e₂」。d₁ ∘ d₀ = 0 が成り立つので(これも公理ではなく、face の端点整合から定理として導く)、1次コホモロジー
H¹ = (d₁ で消える 1-cochain) / (d₀ の像)
が定義できる。これが「診断類(指紋)」の正体だ。直観としてはこうなる。どの隣接2部品も局所的には整合しているのに、一周すると帳尻が合わない。その「ねじれ」だけが商として H¹ に生き残る。だから欠陥の指紋は個々のファイルの中ではなく、貼り合わせの構造に宿る。
最後に比較写像。nerve 射 φ と係数の descend 可換性から複体の間の射(cochain map)が立ち、H¹ の間の誘導写像が得られる。Atlas 定理の核心の主張 (ii) は「条件 C の下で、この誘導写像が全単射」。全射性が「粗くしても診断は隠れない」、単射性が「粗くしても偽の診断は生まれない」に対応する。
冒頭のドット絵の比喩は、飾りではなくこの構造と部品単位で対応している。
| 定理側 | 知覚側 |
|---|---|
| 不変性定理 | ドット絵でも同じ顔が見える |
| adequacy | ドット絵師の技術(効く区別だけ残す) |
| 偽陽性の反例 | パレイドリア(雲が顔に見える) |
| 隠蔽の反例 | 解像度不足で表情が消える |
| 較正条件 C の破れ | モアレ / エイリアシング |
| law 相対性 | 顔認識には足りるドット絵が、細かい文字を読むには足りない |
美術史家エルンスト・ゴンブリッチは、絵は半分しか描かれておらず残りは観る者が補完する、と論じ、その補完を観者の分け前と呼んだ。AAT の言葉に翻訳するとこうなる。解像度を変えても不変なのは絵(コード)そのものではなく、観る者が絵から評価する内容、形式化すれば law family である。だからこそ不変性は law 相対的になる。
そして、この「観る者」には見覚えがあるはずだ。ベテランエンジニアのコードレビューである。経験を積んだレビュアーは、全行を舐めるようには読まない。API の互換性を見るときはインターフェースの粒度で、競合状態を疑うときは行の粒度で。確認したい性質に応じて、読む解像度を切り替える。 適切なレビュー粒度の選択は、今のところ経験と勘に属する技能だ。Atlas 定理は、このレビュー粒度を数学的に扱えるようにする一歩である。「この性質を見るには、どの粗さまでなら情報が落ちないか」という問いに、初めて厳密な足場を与える。
ただし、人間の目も、ベテランの勘も、これを無保証でやっている。だから雲に顔が見え、レビューでは見落としが起きる。この定理が問うたのは「どんな条件が揃えば、これが保証つきになるか」だった。そしてその条件、較正条件 C の正体は、着手時点では誰にも分かっていなかった。要求文書(証明対象を固定した研究計画書)には最初からこう書いた。「C が自明なら定理は言い換えにすぎず、C が強すぎれば定理は空である。C の正体こそが定理の中身である」。
その言葉どおりになった。4回も。
反証ラウンド 1〜3 — もぐら叩き
証明は AI エージェントの自律ループで進めた。人間(私)は要求文書を凍結し、裁定だけを行う。エージェントは証明か反証のどちらかを Lean で固定するまで止まらない。以下の3ラウンドは、その序盤にループが持ち帰った成果。すべて反証である。
反証1: 「塗り」の持ち上げ忘れ
最初の条件候補 C0–C3(当初の4条件)は、点(チャート)と線(依存関係)の対応だけを見ていた。エージェントが見つけた反例はこうだ。粗い地図ではある一周が「塗り潰された三角形」になっている。つまり問題なしと宣言する面(face)が貼られている。ところが細かい地図に持ち上げると輪郭だけで塗りがない。粗い側では消える欠陥の指紋が、細かい側では消えずに残る。 比較写像は同型になりようがない。
937行の Lean ファイルとして反例が固定され、条件に「塗りも持ち上がること」(C4)が加わった。
獲得した条項 C4(平文): 粗側の各 face は、nerve 射の face 対応で写る細側の face を少なくとも一つ持つ。
反証2: 並行する持ち上げ
C4 を足した条件 C0–C4 も破られた。粗い地図の一本道に、細かい地図では並行する2本の道が対応するケースだ。C0–C4 はすべて成立しているのに、並行する2本の間にできる細い一周が、細かい側にだけ新しい指紋を残す。「同じ粗い道に写る複数の持ち上げどうし」を制御する条項がなかったのだ。持ち上げの一意性(C5)が加わった。
獲得した条項 C5(平文): 各粗側 edge に写る細側 edge は高々一つ(既存の存在条項 C2 と合わせて、ちょうど一つ)。
反証3: 環状線のずれ
C0–C5 も破られた。今度は粗い地図の環状線(自分自身に戻る道)だ。その唯一の持ち上げが、細かい地図では別々の交差点を結んでいた。すると粗い側の非ゼロの指紋が、細かい側では消えてしまう。反証1・2が全射性(粗い側が診断を見逃す方向)を破ったのに対し、こちらは単射性(粗い側だけが幻の診断を見る方向)の破れだ。「自分に戻る道の持ち上げは、やはり自分に戻ること」(C6 候補)が必要だった。
獲得した条項 C6(平文): 両端点が同一 chart に落ちる粗側 edge(self-loop)へ写る細側 edge は、それ自身 self-loop である。
3ラウンドを終えて、嫌な予感が形になりつつあった。条項を足すたびに、別の穴が見つかる。 この継ぎ足しは収束するのか。
ひとつだけ、最初から決めていたことが効いていた。反証は毎回、使い捨ての反論ではなく有限反例の Lean ファイルとして固定される。これらは後に、定理の反例パート(「条件を破るとこう壊れる」の証明)の素材として本体に編入される。ゴミになった反証はひとつもない。
転回 — ループを止めた no-go
ここで人間の出番が来た。裁定は、条項の継ぎ足しループを止めること。代わりに、条件候補を総当たりで検査する計算探索(ハント)を別働隊として走らせる。このとき停止条件を3つ、事前に決めて渡した。
- A(成功): 既知の反例3件を除外し、探索範囲に新たな反例がない条件が見つかる
- B(構造的否定): そのような条件が原理的に存在しないことが示される
- C(停滞): どちらにも進まなくなる
結果は B だった。しかも探索の産物としてではなく、探索を設計する過程で見つかった一つの論法によって。条件が足りなかったのではない。条件を書くための言語そのものが足りなかった。 それが判明したのだ。
論法は2点分離と呼んでいる。同じ形(点と線と面の構成、incidence)の上で、係数データだけを変えた3つの世界が作れる。
| 世界 | 比較写像 |
|---|---|
| 全部の係数次元が 1 | 同型 ✅ |
| 一部の係数だけ 0(support hole) | 単射でない ❌ |
| 細かい側の係数だけ2重化 | 全射でない ❌ |
ところが、それまでに検討した条件候補は、C0–C5 も、C6 も、圏論の教科書から輸入した候補さえも、すべて形だけから計算される述語だった。形が同じなら区別できない。つまり、正しい例をひとつでも受理する「形だけの条件」は、同じ顔をした偽物も必ず受理してしまう。どんなに条項を賢く継ぎ足しても、この言語の中に答えはない。
標本化定理の比喩に戻るとこうなる。サンプリング格子の配置(形)をどれだけ工夫しても、信号の帯域(係数)を宣言しなければ、エイリアシングが起きない保証は原理的に書けない。
ここから、係数は law の評価値から一意な規則で生成するという**係数生成契約(K0/K1)**が導入され、条件 C は係数の座標ごとの部分地図(subnerve)の上で課す形に相対化された。重要なのは、この定義変更が趣味の選択ではないことだ。no-go がある以上、他にやりようがない。定義は設計されたのではなく、発見された。
発見された言語 — 係数生成契約 K0 / K1 と条件 C の全文
まず係数の側から。
K1(台の導出)。台(担当範囲)を宣言できるのは chart だけ。edge の台は両端 chart の台の交わり、face の台は3本の boundary edge の台の交わりとして機械的に導出する。cell ごとに独立な台宣言を許すと、no-go の「support hole」、つまり特定の edge の係数だけを空にする細工を手で作れてしまう。だから宣言の自由度そのものを削る。
K0(係数の生成)。係数体は ℚ に固定する。各 cell の係数座標は対 (law, 値)。「値」はその law の descend 評価が cell の台上に取る相異なる値で、多重度は常に1。値の出現回数や台の要素数を index にすることは認めない。これが no-go の「複製」を殺す。各次数の空間は
C⁰ = {(chart, law, 値)} 上の ℚ-値関数空間
C¹ = {(edge, law, 値)} 上の ℚ-値関数空間
C² = {(face, law, 値)} 上の ℚ-値関数空間
で、微分は座標ごとの生成だ。d₀ の (edge, law, 値) 成分は両端 chart の同一 (law, 値) 成分の差、d₁ の (face, law, 値) 成分は boundary triple の交代和 e₀ − e₁ + e₂。同一 label は恒等で対応し、label 不在は零。これ以外の座標対応は一切生成しない。 d₁ ∘ d₀ = 0 は公理として置かず、face の端点整合から label ごとの計算で定理として導く。比較写像の係数部分も宣言せず、(law, 値) 上の恒等対応として descend の π-可換性から生成する。座標の追加・複製・省略はすべて禁止。「契約」という言葉のとおり、宣言できることを最小限まで絞るのがこの言語の本体だ。
座標 subnerve と相対化。各係数座標 (law, 値) について、その座標を持つ cell(descend 評価が導出台の上にその値を取る cell)の成す部分 nerve を座標 subnerve と呼ぶ。K0 / K1 の下では、H¹ と比較写像は座標ごとのブロックに直和分解し、各ブロックは当該 subnerve 上の1次元定数係数の比較に還元される。この分解が相対化の数学的根拠だ。幾何的な条件 C1–C4 は座標 subnerve ごとに課せば足り、大域的な C0・C5・C6 は nerve 全体で課す。
そのうえで、条件 C の全文はこうなる。
-
C0(被覆像の合致): 各粗側 chart の台は、その fiber に属する細側 chart 台の
π-像の合併に等しい - C1(fiber の連結性): 各座標 subnerve で、各粗側 chart の fiber グラフ(その chart に写る細側 chart と、fiber 内に収まる細側 edge のグラフ)は非空かつ連結
- C2(edge lift の存在): 各座標 subnerve で、各粗側 edge は subnerve 内に持ち上げを持つ
-
C3(局所 fiber acyclicity): 各座標 subnerve で、fiber グラフ上の任意の有理 1-cycle は、boundary edge がすべて fiber 内にある細側 face の boundary の
ℚ-線形結合で張られる。fiber の1次ホモロジー消滅と同値な局所条件 - C4(coarse-face lift): 各座標 subnerve で、各粗側 face は face 対応で写る細側 face を少なくとも一つ持つ — 反証1の獲得物
-
C5(unique coarse-edge lift): 各粗側 edge の
φ-fiber は高々一元。C2 と合わせて「ちょうど一つ」— 反証2の獲得物 - C6(self-loop endpoint reflection): 両端点が同一の粗側 chart に落ちる edge(self-loop)へ写る細側 edge は、それ自身 self-loop — 反証3の獲得物
最後に、この条件リストには禁止規則が付いている。C には「比較写像が同型である」「どちらか一側の H¹ が消える」に相当する条項、またはそれに近い片方向条項を入れてはならない。それは証明すべき結論を仮定に密輸する行為だからだ。唯一の明示例外が C3 で、これは個々の fiber の内部データしか見ない局所条件であり、古典 Čech 理論で被覆に課す Leray 型の局所非輪状仮定に相当する。「どこまでが正当な仮定で、どこからが密輸か」の線引き自体を条件リストの一部として固定してあるのは、証明者が AI エージェントだからだ。抜け道は仕様で塞ぐ。
反証4、そして登頂
改訂した仕様でループを再起動すると、数サイクルの基盤整備のあと、エージェントは改訂仕様そのもののスペック穴を突いてきた(反証4)。nerve 射では、粗側に対応物を持たない細側の辺や面を「対応なし(退化成分)」と宣言できる。その宣言規則に穴があった。面を対応なしにする条件が、その面を囲む辺3本の側の宣言まで要求していなかったのだ。この穴の反例では、比較写像の構成(主張 (i))自体が成立しない。433行の反例で確定し、宣言のhereditary 化(面を対応なしにするなら、囲む辺3本も対応なし宣言済みであること)で修理された。
そこからは一気だった。修理後に再々起動したループは、24回の反復(サイクル)で登り切る。
登頂ルート — 証明の構造
第一段: ブロック分解。K0 / K1 の生成規則の下で、複体・H¹・比較写像が係数座標 (law, 値) ごとのブロックに直和分解することを定理化する。各ブロックは座標 subnerve 上の1次元定数係数の比較に還元される。大域の問題が、「部分地図の上の一番単純な係数」の問題の直和に割れるのだ。以降はブロックごとに攻めればよい。
第二段: 単射性。ブロック比較写像の kernel を解析し、粗側で非ゼロの診断類が細側で消えないことを示す。C6 が効くのはここだ。反証3が見つけた「粗側の非ゼロ類が細側で蒸発する」事故経路を塞ぐ(反証4の hereditary 性は、それより手前の「比較写像がそもそも構成できる」段階を支えている)。
第三段: 全射性(山場)。細側の任意の診断類が粗側から来ることを示す。ルートは4手。
- C3 を「fiber を一周する周回量(period)の消滅」に翻訳する離散版 Stokes の定理。局所の面充填が、一周積分の消滅という解析風の言明に化ける
- 消滅した period から、fiber ごとの**原始関数(primitive)**を構成する。「回転がないベクトル場にはポテンシャルがある」の有限グラフ版だ
- primitive で正規化した残差を、C2 / C5 の「持ち上げがちょうど一つ」という通信路を使って粗側の 1-cochain として表す(descent)
- C4 の face lift で、その 1-cochain が粗側でも cocycle であることを確認して昇格する。これで全射性が閉じる
第四段: 主定理と系。ブロックの全単射を直和分解に沿って束ね、global の全単射 = 主張 (ii)。その帰結として、細かく測っても新しい診断類は生まれないという No-New-Diagnostics 系 = 主張 (iii)。
第五段: 反例と発火。不適切な粗視化の反例3種、すなわち偽の診断の発生・実在する診断の隠蔽・条件 C 破れ(主張 (iv)。反証ラウンドの遺産がここの素材になる)と、全条件が同時に成立し、かつ非ゼロの診断類が実際に比較写像を流れる単一の発火 witness(主張 (v))。(v) がないと、定理は「条件 C を満たす例が実は存在しない」形で空文化しうる。それを Lean の具体データで封じる。
条件が証明の中で果たす役割は、きれいに分業している。C3 が局所の一周を殺し、C2 / C5 が持ち上げの一意な通信路を作り、C4 が面の整合を運び、C6 と hereditary 性が self-loop と退化宣言の事故を防ぎ、C0 / C1 が土台を張る。 4回の反証で獲得した条項の一つひとつが、単射性・全射性の証明の特定のステップで実際に使われる。飾りの条項はひとつもない。
最終成果物は Lean 31 モジュール、13,028行。新規宣言は標準公理のみに依存し、sorry や追加公理はひとつもない。仕上げの検収は、数学2レーン+Lean 2レーンの独立した敵対レビューが全レーン「major finding なし」、さらに別建ての完了監査(証明のズル経路の検査を含む)を通過している。
AI エージェント運用の規律
このプロジェクトの AI 運用の原則は一貫している。「AI を安易な解に逃がさない」。数学研究では、それは次の役割分担になった。人間は裁定だけ(仕様の凍結・改訂の承認・停止条件の設計)。実装エージェントは証明ループ。レビューエージェントは敵対査読。
5日間を支えた規律は6つ。
- 反証の一級市民化 — 「反証も正規の成果」と要求文書に事前に書いてあった。だから4回の反証は士気の低下ではなく蓄積になり、反例は定理本体の素材に編入された
- 急所の事前宣言 — 「条件 C の正体こそが定理の中身」と最初に書いてあったから、反証のたびに「失敗した」ではなく「中身が一つ掘れた」と読めた
- 仕様の凍結 — ループ中は要求文書を変えない。改訂は人間の裁定と独立レビューを通す。ゴールポストが動かないから、反証が本物の反証として意味を持つ
- 条項と発火の対称則 — 条件を1つ足すたび、「その条件が空文でなく実際に働く」witness の要求も対で足す。定理が条項の重ね着で空洞化する経路を塞ぐ
- 語彙レベルの診断への切替 — 継ぎ足しが3周した時点で、「もっと条項を」ではなく「この言語で書けるのか」を問うた。no-go はこの切替の産物
- 多レーン敵対査読 — 実装したエージェントとは別のエージェントが、数学とLeanの独立レーンで査読する。「証明したことにする」誘因を構造的に潰す
何度も何度も罠を踏んだ結果、この規律が出来上がった。
現状の限界
- この結果は Lean による機械検証+内部の多レーン査読まで。外部の査読(論文投稿)はこれからで、現在準備中だ
- 定理は有限モデル・固定した係数体の上の主張である。条件 C は十分条件であり、必要性の一般的な特徴づけは未解決として明示的に残している
- 「診断が不変」であって「観測がすべて不変」ではない。粗い読みで生の観測が同じに見えるわけではなく、law が評価する内容の指紋が一致するという主張だ
なぜ「Atlas」か
atlas(地図帳)は、同じ世界を異なる縮尺で描いた地図の集まりだ。どのページを開いても同じ国が写っている。それがこの定理の主張である。
命名はマーケティングではなく、理論の内部から来ている。AAT の正本には以前から chart atlas(チャートの集まりとしての被覆)という語彙があり、「chart atlas が変われば」という一節さえある。Atlas 定理は文字通り、chart atlas の取り替えに対する診断の不変性だ。数学側の偶然もひとつ。多様体の同一性が atlas の選択に依らないことは、微分幾何で最初に習う不変性原理である。
次の一歩は決まっている。実在のマイクロサービスシステムを、サービス/モジュール/メソッドの3粒度で測り直し、adequate な範囲で診断が安定すること、adequacy を破る粗視化で偽陽性と隠蔽が実測されること。定理と反例対を実データで再演する解像度スイープだ。ドット絵の顔が本物と同じである保証を、今度は本番のコードベースで。
最後に、なぜ今この定理なのか。AI がコードを書く時代、開発のボトルネックは生成からレビューへ移った。AI エージェントがコードを書く速度は人間が行の解像度でレビューできる速度をとうに超え、「どこまで粗く読んでも安全か」が開発パイプラインのスループットを決める問いになった。 レビューをスケールさせる道は読む解像度を粗くすることしかなく、その粗さが診断を歪めないという保証は、これまで存在しなかった。Atlas 定理はその保証を初めて定理の形で問うた一歩だ。そして偶然ではなく、この定理自体が「AI の爆速の出力を人間がどう検収するか」という同じ問題のただ中で、多レーン査読と監査という運用側の答えに支えられて証明された。運用と数学が、同じボトルネックを両側から掘り進んでいる。