FORMAL PROOFS

The Indisputable Chain

This page is the formal backbone of Recognition Physics: a single Lean proof chain from tautology to constants and laws.

Every step is machine-checkable. There are no adjustable parameters; the structure is over-constrained and falsifiable.

If it doesn't deliver, it fails immediately—there's nothing to tune.

Open the proofs ↓

What you're looking at

Source of truth: This Lean code is the authoritative definition. If narrative pages disagree with this, the code wins.
What's proven: Starting from "nothing cannot recognize itself" we derive a unique ledger, conservation laws, J(x), φ, 3D space, 8-tick cycles, and ultimately physical constants.
How it differs: Narrative pages explain conceptually. This proves mathematically. Every line here has been verified by Lean's proof assistant.
Falsifiability: The chain is over-constrained. Change any theorem and the rest breaks. One wrong prediction invalidates everything.

The deductive spine

T1 Ledger necessity→state accounting, conservation substrate

T2 Atomicity→quantization, minimal tick/action

T3 Conservation→continuity equations ∂tρ + ∇·J = 0

T4 Unique cost→least-action, AM-GM bound

T5 k = 1, φ→scaling laws, RG fixed points

T6 d = 3→3D space, knot/topology constraints

T7 T = 2^D→minimal Hamiltonian/Gray traversal

T8 Causal cones, c→relativistic causality

See detailed theorem pages →

Assumptions & scope

Axioms: Meta-Principle (nothing cannot recognize itself), Composability, Finiteness
Working assumption: Cubic tiling (explicitly stated, to be elevated to theorem)
What would falsify: Any dimensionless prediction disagreeing with measurement at stated precision

How to read this chain

Interactive hotspots: Click any highlighted code to see what it proves and why
Hover for context: Tooltips explain the role of each theorem in the larger structure
Jump to sections: Use quick links below or the sidebar index

Meta-Principle T2 Atomicity T3 Conservation J(x) cost φ golden ratio d = 3 T = 8 α fine structure λ_rec ILG kernel

Papers & resources

Deep dive into the mathematical foundations and empirical validation:

Foundations Paper (PDF) Empirical Validation GitHub Repository

FAQ

Why Lean?

Lean is a theorem prover that guarantees correctness. Unlike hand-written proofs, Lean-verified proofs cannot contain logical errors. Every step is checked by machine.

Where are the assumptions?

All assumptions are explicit: Meta-Principle (logical necessity), Composability, Finiteness, and cubic tiling (working assumption). No hidden axioms.

What does parameter-free mean?

No adjustable numbers. Every constant (φ, α, masses) is derived from the axioms. Change nothing to fit data—the structure is rigid.

How is this different from MOND/dark matter?

MOND adds one parameter (a₀) empirically. Dark matter adds 5-6 parameters per galaxy. We derive the modification from first principles with zero free parameters.