No-Compute Computation

An adaptation of ADR-0001 from the Verlinde entropic gravity Lean formalization project (com-junkawasaki/projects/2604-linde). Source: docs/adr/0001-computation-as-thermal-mass-blocker.md.

1. The Starting Question — Can Number Theory Reduce to Order, Paths, or Graph Topology?

Can problems like Catalan’s conjecture or the distribution of primes be translated into something more combinatorial or geometric? Three reductions were considered:

Computation order: Use factorization order inside (ℤ, ×) as a discriminator
Path dependence: Recast number-theoretic propositions as path-dependent
Graph topology: Characterize prime distributions via topological invariants of finite graphs

The answer was the same in all three cases: structurally and logically closed.

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. Physicalizing — Verlinde + Bekenstein + Landauer

Next: take information seriously as a physical quantity.

Shannon: entropy of information
Landauer: erasing one bit costs at least k_B T ln 2 of heat
Verlinde: gravity is an entropic force, F = T ∇S
Bekenstein: the information in a region is bounded by S ≤ 2π R E / ℏ c

Use this as a dictionary — “information = mass = heat” — and evaluate meta-mathematical blockers as physical quantities. The total information in the observable universe is roughly 10^122 bits.

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: for any effective physical representation ρ, deg_T(ρ(φ)) = deg_T(φ). Turing degree is preserved under physicalization.

⇒ Physicalizing information does not dissolve blockers. The Bekenstein bound only strengthens them.

3. The Reversal — Computation Itself Has Thermal Mass

So far this has been a standard analysis. The dual view changes the geography:

Computation itself carries thermal mass, and that thermal mass is what makes blockers material.

A blocker is not “a ceiling on provability.” It is the accumulated thermodynamic mass of the operation called computation. The question inverts.

Old framing: what can be computed = where can we afford the entropy bill
New framing: what can we get away with not computing = where can we reach the answer without paying thermal mass

The core observation:

Theorems are entropy compressors. They are heat sinks.

Invoking Faltings collapses the astronomical thermal cost of enumerating rational points to zero. Invoking the Fundamental Theorem of Arithmetic collapses factorization case-search to zero. Invoking Mihailescu collapses Catalan-style brute force to zero.

A theorem is a device for ensuring that the epistemic cost paid by the humans who discovered it does not have to be paid again. This is the same thermodynamic worldview as Verlinde’s entropic gravity, mirrored onto meta-mathematics.

4. The Decision: Compute by Not Computing

For each candidate computational task, invoke the corresponding blocker theorem to skip the computation. This is not surrender. It is a thermal-mass budget optimization.

A partial catalog:

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. Operating the Thermal-Mass Budget

The gate any new research direction or formalization task must pass:

Information cost: estimate required bits
Bekenstein check: is I_required ≤ 10^122?
Turing degree check: is deg_T ≤ 0?
Bremermann / Margolus-Levitin check: does it finish in physical time? (the n ≤ 327 rule)
Blocker invocation: every skip is justified by an explicit theorem

6. Lean Formalization — Verlinde’s Gravity

The first application of this policy: a Lean 4 formalization of Verlinde (2010). From five physical postulates — holographic screen, holographic bound, Unruh temperature, equipartition, E = Mc² — Newton’s law of gravitation F = GMm/R² follows by field_simp and linear_combination alone.

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 numerics (M_⊕ = 5.9722 × 10²⁴ kg, R_⊕ = 6.371 × 10⁶ m) reproduce surface gravity g ≈ 9.82 m/s² and a holographic bit count of 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⁸⁴

The formalization rules from ADR-0001:

Embedding arithmetic structure into entropy is structure discovery, not dissolution. Closer in spirit to Connes-Marcolli and Manin-Marcolli’s noncommutative arithmetic geometry.
The Bekenstein bound is an explicit hypothesis (HolographicBound).
Landauer cost is an explicit budget. A LandauerCost : Proof → ℝ_≥0 type is on the table.
Blockers are recorded as axiom, not sorry, with a comment naming the thermal mass that cannot be paid.

7. The Meta-Consequence

The “computation = thermal mass” frame composes naturally with Verlinde’s worldview:

Entropic gravity: gravity = a force from an entropy gradient
This ADR: mathematical progress = an entropy (= thermal mass) gradient driven by choices not to compute

The same thermodynamic worldview applied on the physical and meta-mathematical sides. The next phase of projects/2604-linde/ is to chase this duality explicitly.

References

Physics

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.”

Number theory & computability

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). Incompleteness theorems.

Complexity barriers

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

No-Compute Computation: Blockers as Thermal Mass, Theorems as Heat Sinks