Formal Verification | 36 Theorems, 0 Axioms

What This Is

A machine-checked proof that two quadratic functionals on d×d real matrices — one modelling the GR exchange amplitude, the other the trace-free bath amplitude — cannot agree when d ≥ 3 and the trace is nonzero. Written in Lean 4, a language where every step is verified by the kernel. The algebra is settled. The physics interpretation remains open.

36 Theorems

0 Axioms

588 Lines of Lean

8.8s Build Time

What "0 Axioms" Means

The file contains no axiom declarations and no sorry (proof omissions). Every theorem is fully proved and checked by the Lean kernel.

Like all Lean 4 + Mathlib code, the proofs rest on Lean's type-theoretic foundations: propext, Quot.sound, and Classical.choice. You can verify this yourself with #print axioms gap_formula.

The Definitions

Five constructions. Everything else follows.

variable {d : N} [NeZero d] -- The trace-free projection: T^TF = T - (Tr T / d) * I noncomputable def traceFree (T : Matrix (Fin d) (Fin d) R) : Matrix (Fin d) (Fin d) R := T - (Matrix.trace T / (d : R)) * (1 : Matrix (Fin d) (Fin d) R) -- Frobenius norm squared: ||T||^2 = Sum_ij (T_ij)^2 noncomputable def frobeniusNormSq (T : Matrix (Fin d) (Fin d) R) : R := Sum i, Sum j, (T i j) ^ 2 -- Frobenius inner product: <A,B> = Sum_ij A_ij * B_ij noncomputable def frobeniusInner (A B : Matrix (Fin d) (Fin d) R) : R := Sum i, Sum j, A i j * B i j -- GR exchange amplitude: A_GR = ||T||^2 - 1/2 * (Tr T)^2 noncomputable def A_GR (T : Matrix (Fin d) (Fin d) R) : R := frobeniusNormSq T - (1/2) * (Matrix.trace T) ^ 2 -- Bath-TT amplitude: A_Bath = ||T^TF||^2 noncomputable def A_Bath (T : Matrix (Fin d) (Fin d) R) : R := frobeniusNormSq (traceFree T)

All 36 Theorems

Each card is a machine-verified statement. Hover for the Lean signature.

I. Trace-Free Projection

Theorem 01

Tr(T^TF) = 0

trace_traceFree

Theorem 02

traceFree² = traceFree

traceFree_idempotent

Theorem 03

traceFree(A+B) = traceFree A + traceFree B

traceFree_add

Theorem 04

traceFree(cT) = c traceFree T

traceFree_smul

Theorem 05

T = T^TF + (Tr T / d) I

decomposition

Theorem 06

Tr T = 0 implies traceFree T = T

traceFree_of_trace_zero

Theorem 07

traceFree(cI) = 0

traceFree_scalar

II. Frobenius Norm

Theorem 08

||T||² ≥ 0

frobeniusNormSq_nonneg

Theorem 09

||T||² = 0 iff T = 0

frobeniusNormSq_eq_zero_iff

Theorem 10

Γ(vacuum) = 0

decoherence_vacuum_zero

Theorem 11 // Key
||T||2 = ||TTF||2 + (Tr T)2/d
pythagorean_decomposition

Theorem 12

||cI||² = c²d

frobeniusNormSq_smul_one

III. Frobenius Inner Product

Theorem 13

<T,T> = ||T||²

frobeniusInner_self

Theorem 14

<A,I> = Tr A

frobeniusInner_one

Theorem 15 // Key
<TTF, cI> = 0
traceFree_orthogonal

Theorem 16

<A,B> = <B,A>

frobeniusInner_comm

Theorem 17

<cA,B> = c<A,B>

frobeniusInner_smul_left

Theorem 18

<A+B,C> = <A,C>+<B,C>

frobeniusInner_add_left

Theorem 19 // Key
<TTF, S> = <T, STF>
traceFree_self_adjoint

Theorem 20

4<A,B> = ||A+B||² - ||A-B||²

polarization_identity

Theorem 21

<A,B> = Tr(A^TB)

frobeniusInner_eq_trace

IV. The No-Go Chain

Theorem 22

A_GR(I₃) ≠ A_Bath(I₃)

no_go_concrete

Theorem 23

d≥3, c≠0: A_GR(cI) ≠ A_Bath(cI)

no_go_scalar

Theorem 24 // Key
d≥3, Tr T≠0: A_GR(T) ≠ A_Bath(T)
no_go_universal

Theorem 25 // Key
A_GR - A_Bath = (1/d - 1/2)(Tr T)2
gap_formula

Theorem 26

d = 2: A_GR = A_Bath (sharp)

no_go_sharp_d2

Theorem 27

d≥3, Tr≠0: A_GR - A_Bath < 0

gap_negative

V. Hilbert Space & Lie Algebra

Theorem 28

||T^TF||² ≤ ||T||²

bessel_inequality

Theorem 29

Tr([A,B]) = 0

trace_commutator

Theorem 30

traceFree([A,B]) = [A,B]

commutator_is_traceFree

Theorem 31 // Key
<A,B>2 ≤ ||A||2 ||B||2
cauchy_schwarz

Theorem 32

||A+B||²+||A-B||² = 2(||A||²+||B||²)

frobenius_parallelogram

Theorem 33

||A-tB||² = ||A||²-2t<A,B>+t²||B||²

frobenius_quadratic_form

Theorem 34

||T^TF||² = ||T||² - (Tr T)²/d

traceFree_norm_eq

VI. Geometric Structure

Theorem 35

traceFree(A^T) = (traceFree A)^T

traceFree_transpose

Theorem 36 // Key
Tr S=0: ||T-TTF|| ≤ ||T-S||
traceFree_best_approx

The Dependency Chain

How the No-Go Theorem is built from first principles.

traceFree def → trace = 0 → idempotent → orthogonality

orthogonality → Pythagorean → A_Bath = ||T||² - Tr²/d

A_GR = ||T||² - ½Tr² − A_Bath = gap: (1/d - 1/2) Tr²

gap formula → d=2: gap=0 (sharp) → d≥3: gap<0 (NO-GO)

The Gap Formula

A_GR(T) − A_Bath(T) = (1/d − 1/2) · (Tr T)²

For d ≥ 3 and Tr T ≠ 0, this is strictly negative. The Bath sees more than GR.
For d = 2, this is exactly zero. The no-go is tight.

What This Proves — and What It Does Not

What the Lean kernel certifies

Given these definitions of A_GR and A_Bath, the gap formula holds exactly.
For d ≥ 3 and Tr T ≠ 0, the two functionals disagree. No sign error, no missing case.
For d = 2, they agree exactly. The obstruction is sharp and dimension-theoretic.
traceFree is the optimal orthogonal projection — the nearest trace-free matrix in the Frobenius norm.

What it does not certify

Whether A_GR is the correct effective action for gravity.
Whether the bath amplitude should be quadratic in the Frobenius norm.
Whether spacetime behaves like a finite-dimensional Hilbert space.
Whether the physical theory is true.

These are modelling choices. The formalization settles the algebra so the debate can focus on the physics. Anyone who disagrees with the no-go must specify which definition they reject — not the computation.

Full Source Code

The complete Lean 4 file, loaded directly from RealGravity.lean. No abbreviation. No sorry.

Loading...

How to Verify

Install Lean 4 and Mathlib. Save the file as RealGravity.lean. Run:

lake build

If it compiles, it is correct. That is the contract.