The Wolfram Physics Project
This formalization builds upon and contributes to the foundations established by:
"A Project to Find the Fundamental Theory of Physics"
Stephen Wolfram
The Wolfram Physics Project (2020) - A computational approach to fundamental physics through hypergraph rewriting
"Confluence and Causal Invariance"
Max Piskunov
Wolfram Physics Bulletins (2020) - The counterexamples formalized in this project
"Some Relativistic and Gravitational Properties of the Wolfram Model"
Jonathan Gorard
arXiv:2004.14810 (2020) - Physical implications and mathematical foundations
Click to expand
Hypergraph Rewriting & Causal Structure
The Wolfram Physics Project proposes that the universe can be modeled as a hypergraph that evolves through the application of simple rewriting rules. At the lowest level, everything consists of a network of "atoms of space" continually being updated—the entangled limit of everything computationally possible.
Two key properties are central to the physics: confluence (different evaluation orders reach the same result) and causal invariance(different orders produce isomorphic causal graphs). It was widely assumed these properties were equivalent.
Max Piskunov's 2020 work demonstrated through explicit counterexamples that these properties are in fact logically independent—a system can have one without the other. This formalization provides machine-checked verification of these groundbreaking results.
Multiway graph visualization of Counterexample CE1. Shows branching evaluation paths demonstrating how different rewrite orders can lead to distinct causal structures.
Machine-Verified Independence Proof
This Lean 4 formalization provides rigorous, machine-checked proofs that confluence and causal invariance are independent properties. We mechanize Piskunov's counterexamples with fresh-vertex semantics and full alpha-equivalence handling.
Confluence and causal invariance are independent
Piskunov counterexamples mechanized
Fresh-vertex semantics with alpha-equivalence
Confluent, Not Causal Invariant
System with unique normal forms but non-isomorphic causal graphs
CE1.not_causalInvariant
Causal Invariant, Not Confluent
System with isomorphic causal graphs but multiple normal forms
CE2.not_confluentNF
Fresh-Vertex Semantics
Causal invariance under explicit fresh-vertex allocation
SystemFresh.Event.applyWith_iso
| THEOREM | DESCRIPTION |
|---|---|
| confluence_causal_invariance_independent | Main independence result with existential counterexamples |
| CE1.confluentNF | CE1 has unique normal forms |
| CE1.not_causalInvariant | CE1 lacks causal invariance |
| CE2.causalInvariant | CE2 satisfies causal invariance |
| CE2.not_confluentNF | CE2 has multiple normal forms |
| WM148.causalInvariant | Fresh-vertex WM148 satisfies causal invariance |
Uses only standard Lean kernel axioms: