ISO · A
POLE A · PHYSICS
Surfaceology
amplitudes as surface combinatorics
時空・ループ・ゲージを捨て、punctured disk 上の非交叉曲線と辺長 uij だけを残す。振幅は u ≥ 0 が張る組合せ多面体上の積分として立ち上がる。
- discard: spacetime, loops
- keep: curves on Σg,n
- read: u ≥ 0 (positivity)
ISO · B
POLE B · LANGUAGE
Sign
semantics as tree combinatorics
実行時状態・評価順・GC を捨て、式木の節点に貼られた符号 + / − / 0 と余積 ⊙・直積 , の組合せ関係だけを残す。意味は実行前に確定する。
- discard: runtime, order
- keep: signs on AST
- read: well-signedness
SYSTEM · C
Rust
memory safety as region combinatorics
実行時所有権追跡を捨て、MIR 上の生存グラフと 借用規則 だけを残す。データ競合の不在は、NLL による領域計算が「借用矛盾なし」を返すことで コンパイル時に 読み取られる。
- discard: runtime tracking
- keep: MIR + lifetimes
- read: borrow soundness
SYSTEM · D
Lean 4
theorems as term combinatorics
実行 (基本は) を捨て、依存型の項と カーネル型チェック だけを残す。命題の正しさは、証明項が Γ ⊢ e : A の形で 型に合う という組合せ判定へと還元される。
- discard: runtime
- keep: dependent terms
- read: kernel type-check
SYSTEM · E
Coq / Rocq
theorems as CIC term combinatorics
実行 (完全に) を捨て、Calculus of Inductive Constructions 上の帰納構成と 小さなカーネル だけを残す。Prop は opaque で、証明の正しさは還元と型判定に還元される。
- discard: runtime
- keep: CIC terms
- read: kernel + Inductive
§ 01
The Cross-System Correspondence — 5 系 × 10 次元
Surfaceology ↔ Sign は 同型対応、他 3 系は 類縁
DIMENSION
Surfaceology
Sign
Rust
Lean 4
Coq / Rocq
検証対象what it checks
散乱振幅Tr φ³ 系の観測量
プログラム意味式の静的な指示対象
所有・借用メモリ安全性
命題の証明数学・依存型プログラム
命題の証明数学・依存型プログラム
組合せ台discrete support
punctured diskΣg,n + 非交叉曲線
式木 (AST)節点に符号 +/−/0
MIR + 生存グラフlifetime lattice
依存型文脈Γ ⊢ e : A
依存型文脈Γ ⊢ e : A
許容条件admissibility
uij ≥ 0正値性 (positivity)
符号整合well-signedness
借用規則no aliased mutation
型チェックカーネル承認
型チェックカーネル承認
捨てる動力学discarded
時空・ゲージループ和も含む
評価順・状態GC も含む
実行時追跡コンパイル時のみ
実行 (基本)Prop は irrelevant
実行 (完全)Prop は opaque
読み出す観測量read-out
An = ∫Ω一意な多面体積分
⟦e⟧静的意味 (実行前確定)
安全な IR+ 最適化情報
証明項type-directed
証明項type-directed
合成の原始子composition
coproduct / product曲線の余積・直積
⊙ / ,中黒・カンマ
enum / structsum / product
Σ / Π依存和・依存積
Sum / ProdInductive で導入
自動化度automation
完全自動図式クラス所与
完全自動コンパイル時
完全自動borrowck
戦術+自動化mathlib, aesop
戦術+自動化Ltac2, hammer
計算量cost model
poly(n)組合せ多面体
O(|AST|)線形 (実測 <5ms)
poly(|prog|)NLL 判定
undecidable実務では終わる
undecidable実務では終わる
正値性の姿positivity as
u ≥ 0 領域幾何的正値領域
符号伝播+ · + = +
alias-freeness領域素論理
strict positivity帰納型の要件
strict positivity+ guard 条件
盲点blind spot
全 QFTTr φ³ を超えると未拡張
動的性質停止性・資源量
関数的正しさ仕様との一致
実行性能コード生成は外部
実行性能抽出後は保証外
§ 02
The Trade-off Map — 決定可能性 × 対象領域
何を捨てるかで、何を得るかが決まる
FIG. 3 · POSITIONING
横軸に「対象領域の広さ」、縦軸に「決定可能性」を取ると、Surfaceology と Sign は左上の 狭くて決定可能 の帯に隣接して並ぶ (ISO PAIR)。Rust は右へ広がり、Lean / Coq はさらに右下へ「決定不能だが最大限に広い」領域へ抜ける。
The trade-off: 広さと自動性は交換される。
5 系すべてが 「動力学を消し、組合せ構造から意味を読む」 という同一の身振りを共有するが、その代償として 何を検証対象に選ぶか で異なる位置に落ちる。
身振りの共有は方法論の話であり、位置の違いは 設計判断 の話である。両者は独立に評価される。
-
AXIS 1 · SCOPE
Surfaceology / Sign / Rust は 特定領域 を切り取る。Lean / Coq は数学 全体 を取る。前者は自動化と引き換えに広さを、後者は広さと引き換えに自動化を捨てた。
-
AXIS 2 · POSITIVITY
u ≥ 0 (物理)、符号整合 (Sign)、alias-freeness (Rust)、strict positivity (Lean/Coq)。「許すか許さないか」 の判定こそが正値性の姿。
-
AXIS 3 · READ-OUT
振幅、静的意味、安全 IR、証明項 — 読み出される観測量 は異なるが、いずれも「実行を経由しない」という一点で同じ性質を持つ。
-
AXIS 4 · GESTURE
discard the dynamics, keep only the combinatorial positivity —— この 1 文が、5 系すべての設計動機を一意に説明する。
The shared invariant, seen through five vocabularies: positivity, read without dynamics.
物理・言語・システム・数学 — 4 つの領域を横断して、5 つの検証系は同じ 1 つの認識論を反復している。実行前に、組合せ的な整合条件だけから、観測すべき量を読み出す。この身振りは、Curry–Howard 対応が「型と証明」を結んだのと同じ意味で、「幾何と意味」を結ぶ。
本モノグラフ §§ 12–14 で示すのは、この 4 者関係が偶然の類比ではなく、正値幾何学の圏論的枠組 によって単一の対象として再構成される、という主張である。
Surfaceology ↔ Sign の同型対応 (PLATE I) は、その最も鮮明な 2 極である。Rust · Lean · Coq は、同じ枠組の別の切り口 — 異なる観測量、異なる自動化度、異なる scope を選んだ設計判断 — として位置づく。
REFS · Arkani-Hamed et al. (PRL 2025, JHEP 2025-26) · Astrauskas et al. (Prusti, 2019) · Lean 4 mathlib (2024-26) · Sozeau et al. (Rocq, 2026) · Sign α spec (2024-26)
Surfaceology · reach
all-loop Tr φ³
Feynman 展開なし・多面体積分 1 本
Sign · latency
2 min → < 5 ms
実行前検査で 16% 命令削減 (実測)
Rust · guarantee
memory-safety at compile
NLL 借用検査 (Pearce 2021)
Lean 4 · scope
Mathlib ≈ 全数学
依存型 · カーネル小 (Tang 2025)
Coq / Rocq · foundation
CIC: 40 年の実績
Rocq へ改称 · Sozeau 2026