計算しない計算

Verlinde entropic gravity の Lean 形式化プロジェクト (com-junkawasaki/projects/2604-linde) における ADR-0001 の翻案。原文 docs/adr/0001-computation-as-thermal-mass-blocker.md より。

1. 出発点 — 数論問題は「計算順序」「経路」「グラフ位相」に還元できるか

カタラン予想や素数分布のような数論的問題を、もっと組合せ論的・幾何的な対象に翻訳できないか。具体的には次の三つを試した。

計算順序の問題: (ℤ, ×) の中で因数分解の順序を識別子として使えないか
経路依存の問題: 数論命題を経路依存性として捉えられないか
グラフ位相の問題: 素数の分布を有限グラフの位相不変量で特徴付けられないか

結論は、いずれも構造的・論理的に閉ざされている、というものだった。

Reduction	Why it fails
Computation order	The Fundamental Theorem of Arithmetic kills order information inside `(ℤ, ×)`
Path dependence	`Π¹₀` statements are universal closures of decidable predicates — path-independent by definition
Graph topology	Finite graph invariants are decidable; Gödel-class separation prevents encoding `Th(ℕ, +, ×)`

2. 物理化する — Verlinde + Bekenstein + Landauer

次に、情報を厳密に物理量として取ったらどうなるかを試した。

Shannon: 情報のエントロピー
Landauer: 1 bit の消去には少なくとも k_B T ln 2 の熱
Verlinde: 重力 = エントロピー gradient による力 F = T ∇S
Bekenstein: 領域内情報量に上限 S ≤ 2π R E / ℏ c

このもとで「情報=質量=熱」を辞書として取り、メタ数学的 blocker を物理量として評価する。観測可能宇宙の総情報量はおよそ 10^122 bit。

Blocker	Required information	Physically possible?	Effect
Gödel / Tarski	`ℵ₀`	×	strengthened
MRDP (Hilbert 10)	`ℵ₀`	×	strengthened
`Π¹₀` exhaustive numerical check	`ℵ₀`	×	strengthened
P vs NP (execution)	`2ⁿ`	capped at `n ≤ 327`	physical blocker added
Catalan’s proof	`~10⁶` bits	trivial	already decidable
Faltings, FTA, quadratic reciprocity	compact	trivial	positive result

Physical Church-Turing thesis: 任意の effective な物理表現 ρ について、deg_T(ρ(φ)) = deg_T(φ)。すなわち Turing degree は物理化で保存される。

⇒ 情報の物理化は blocker を dissolve しない。むしろ Bekenstein 上限により blocker は強化される。

3. 反転 — 計算自体が熱質量を持つ

ここまでは標準的な見方の延長線上にある。しかし dual な視点に立てば、別の地形が見えてくる。

計算自体が熱質量を持ち、その熱質量が物質的 blocker になっている。

すなわち、blocker とは「証明可能性の上限」ではなく、「計算という熱力学的操作が累積する物質的質量そのもの」である。

すると、問いは反転する。

旧: 何が計算可能か = 何処までエントロピーを支払えるか
新: 何を計算しなくて済ませられるか = 何処で熱質量を払わずに答えに到達できるか

そして次が核心になる。

定理はエントロピー圧縮器であり、熱シンクである。

Faltings の有限性定理を持ち出すことで、本来必要だった有理点の総列挙という大規模熱質量をゼロにする。FTA を invoke することで、因数分解の場合分け探索をゼロにする。Mihailescu を invoke することで、Catalan 型方程式の総当たりをゼロにする。

定理は、それを発見した人類が支払った認識的コストを、後続の利用者が支払わずに済むようにする装置である。これは Verlinde の entropic gravity と同じ熱力学的世界観を、メタ数学側に映したものだ。

4. Decision: 「計算しない計算」

各計算課題について、対応する blocker 定理を invoke して計算をスキップする。これは諦めではなく、熱質量予算の最適化である。

カタログの一部を抜粋する。

A. Arithmetic & Number Theory

#	Skip	Invoke	Structural alternative
A1	Reordering checks for individual factorizations	FTA	Axiomatize uniqueness (`Nat.factorization`)
A2	Diophantine brute force	MRDP (Hilbert 10)	Algebraic proof per problem, or accept undecidability
A3	Enumerate rational points on high-genus curves	Faltings	Abstract as a finite set; bound only
A4	Inspect primes individually to guess distribution	Chebotarev / PNT	Density functions
A7	Generic `xᵖ - yᵍ = 1` search	Mihailescu	Accept the unique solution `(3,2,2,3)`

B. Computability & Complexity

#	Skip	Invoke	Structural alternative
B1	Exhaustive numerical check of `Π¹₀` statements	Bekenstein + Gödel	Finite-step formal proof only
B2	A universal halting algorithm	Church-Turing	Accept undecidability
B4	SAT brute force for `n > 327`	Bremermann	Heuristic, or accept NP-hardness
B7	Decide CH inside ZFC	Cohen forcing	Accept independence

C. Complexity-Theoretic Meta-Blockers

#	Skip	Invoke	Structural alternative
C1	Natural-proof attacks on P ≠ NP	Razborov-Rudich	Search non-natural methods
C2	Relativizing approaches	Baker-Gill-Solovay	Non-relativizing methods
C3	Algebrizing approaches	Aaronson-Wigderson	Non-algebrizing methods

D. Physical-Representation Bypass Attempts

#	Skip	Invoke	Structural alternative
D1	Solving undecidable problems with quantum computation	`BQP ⊆ EXPTIME`	Don’t try
D2	Lowering Turing degree by changing physical representation	Degree invariance under physicalization	Representation is for structural discovery only
D3	CTC / hypercomputation implementations	Quantization + Bekenstein forbid them	Don’t try
D4	Hilbert-Pólya / AdS-CFT to decide the undecidable	Degree preservation	Tools for finding structure, not solutions

5. 熱質量予算の運用ルール

新しい研究方向や形式化タスクを評価するときの関門：

Information cost: 必要 bit 数を見積もる
Bekenstein check: I_required ≤ 10^122 か
Turing degree check: deg_T ≤ 0 か
Bremermann / Margolus-Levitin check: 物理時間内に終わるか (n ≤ 327 ルール)
Blocker invocation: スキップしてよい計算は対応する定理を明示的に invoke する

6. Lean 形式化 — Verlinde の重力公式

この方針の最初の応用として、Verlinde (2010) の entropic gravity を Lean 4 で形式化した。ホログラフィック・スクリーン、ホログラフィック束縛、Unruh 温度、等分配定理、E = M c² という五つの物理仮定から、ニュートン万有引力の法則 F = G M m / R² が field_simp と linear_combination のみで導かれる。

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

namespace Verlinde

/-- Verlinde's gravitational acceleration formula. From the five
    physical postulates compressed into a single identity, `a = G M / R²`
    follows by pure commutative-ring manipulation. -/
theorem gravitational_acceleration
    {G hbar c kB R M a : ℝ}
    (hG    : G    ≠ 0)
    (hhbar : hbar ≠ 0)
    (hc    : c    ≠ 0)
    (hkB   : kB   ≠ 0)
    (hR    : R    ≠ 0)
    (entropic :
      (1 / 2) *
        (4 * Real.pi * R ^ 2 * c ^ 3 / (G * hbar)) *
        kB *
        (hbar * a / (2 * Real.pi * kB * c)) = M * c ^ 2) :
    a = G * M / R ^ 2 := by
  have hπ  : Real.pi ≠ 0 := Real.pi_ne_zero
  have hR2 : R ^ 2  ≠ 0 := pow_ne_zero _ hR
  have hc2 : c ^ 2  ≠ 0 := pow_ne_zero _ hc
  have simp_lhs :
      (1 / 2) *
        (4 * Real.pi * R ^ 2 * c ^ 3 / (G * hbar)) *
        kB *
        (hbar * a / (2 * Real.pi * kB * c))
      = R ^ 2 * c ^ 2 * a / G := by
    field_simp
    ring
  rw [simp_lhs] at entropic
  rw [div_eq_iff hG] at entropic
  have cancel_c2 : R ^ 2 * a * c ^ 2 = G * M * c ^ 2 := by
    linear_combination entropic
  have key : R ^ 2 * a = G * M := mul_right_cancel₀ hc2 cancel_c2
  rw [eq_div_iff hR2]
  linear_combination key

/-- Newton's law of gravitation. Combine with `F = m a` and the
    above to recover `F = G M m / R²`. -/
theorem newton_law_of_gravitation
    {G hbar c kB R M m a : ℝ}
    (hG    : G    ≠ 0) (hhbar : hbar ≠ 0) (hc : c ≠ 0)
    (hkB   : kB   ≠ 0) (hR    : R    ≠ 0)
    (entropic :
      (1 / 2) *
        (4 * Real.pi * R ^ 2 * c ^ 3 / (G * hbar)) *
        kB *
        (hbar * a / (2 * Real.pi * kB * c)) = M * c ^ 2) :
    m * a = G * M * m / R ^ 2 := by
  have ha : a = G * M / R ^ 2 :=
    gravitational_acceleration hG hhbar hc hkB hR entropic
  rw [ha]; ring

end Verlinde

SI 単位系での数値検証 (地球の質量 M = 5.9722 × 10²⁴ kg、半径 R = 6.371 × 10⁶ m) では、地球表面の重力加速度として g ≈ 9.82 m/s²、ホログラフィック・スクリーン上のビット数として N ≈ 2 × 10⁸⁴ が再現される。

namespace Verlinde.Numerical

def G       : Float := 6.67430e-11   -- N·m²/kg²
def hbar    : Float := 1.054571817e-34
def c       : Float := 2.99792458e8
def kB      : Float := 1.380649e-23
def piF     : Float := 3.141592653589793

def M_earth : Float := 5.9722e24
def R_earth : Float := 6.371e6

def gravitational_acceleration (M R : Float) : Float :=
  G * M / (R * R)

def holographic_bits (R : Float) : Float :=
  let A := 4.0 * piF * R * R
  A * c * c * c / (G * hbar)

def bekenstein_hawking_entropy (R : Float) : Float :=
  let A := 4.0 * piF * R * R
  A * c * c * c / (4.0 * G * hbar)

end Verlinde.Numerical

#eval Verlinde.Numerical.gravitational_acceleration
        Verlinde.Numerical.M_earth Verlinde.Numerical.R_earth
-- 9.819...

#eval Verlinde.Numerical.holographic_bits Verlinde.Numerical.R_earth
-- 2.04... × 10⁸⁴

形式化の運用ルールは ADR-0001 に従う：

算術構造のエントロピー埋め込みは「構造発見」として行う。Connes-Marcolli, Manin-Marcolli の noncommutative arithmetic geometry に近い位置づけ。
Bekenstein 上限は仮定として明示する (HolographicBound)。
Landauer cost を計算予算として明示的に扱う。LandauerCost : Proof → ℝ_≥0 の導入を検討中。
sorry ではなく axiom で blocker 性を記録する。それが「物理的・論理的に支払えない熱質量」であることをコメントで明示する。

7. メタ的帰結

「計算 = 熱質量」というフレームは Verlinde の世界観と自然に整合する：

Entropic gravity: 重力 = エントロピー gradient による力
本 ADR: 数学的進展 = 「計算しない選択」によるエントロピー (= 熱質量) gradient

両者は同じ熱力学的世界観を、物理側 / メタ数学側に適用したものに他ならない。projects/2604-linde/ の今後の展開で、この双対を明示的に追究する。

References

物理

Bekenstein, J. D. (1981). “Universal upper bound on the entropy-to-energy ratio for bounded systems.” Phys. Rev. D.
Landauer, R. (1961). “Irreversibility and heat generation in the computing process.” IBM J. Res. Dev.
Margolus & Levitin (1998). “The maximum speed of dynamical evolution.” Physica D.
Verlinde, E. (2011). “On the origin of gravity and the laws of Newton.” JHEP.
Bremermann, H. J. (1962). “Optimization through evolution and recombination.”

数論・計算可能性

Mihailescu, P. (2004). “Primary cyclotomic units and a proof of Catalan’s conjecture.”
Matiyasevich, Y. (1970). Hilbert’s 10th problem.
Faltings, G. (1983). “Endlichkeitssätze für abelsche Varietäten über Zahlkörpern.”
Gödel, K. (1931). 不完全性定理.

計算量 barrier

Baker, Gill, Solovay (1975). Relativization barrier.
Razborov, Rudich (1997). “Natural proofs.”
Aaronson, Wigderson (2008). “Algebrization.”

計算しない計算 — blockerを熱質量として、定理を熱シンクとして