Wolfram Physics Formalization

_{Our tech stack is ontological:

Hardware — Physics

Software — Mathematics

Our engineering workflow is simple: discover, build, grow, learn & teach}

_{Notice of Proprietary Information

This document outlines foundational concepts and methodologies developed during internal research and development at Apoth3osis. To protect our intellectual property and adhere to client confidentiality agreements, the code, architectural details, and performance metrics presented herein may be simplified, redacted, or presented for illustrative purposes only. This paper is intended to share our conceptual approach and does not represent the full complexity, scope, or performance of our production-level systems. The complete implementation and its derivatives remain proprietary.}

Wolfram Physics Formalization

Machine-checked proof that confluence and causal invariance are independent properties
Lean 4 formalization of Piskunov's 2020 counterexamples for Wolfram Physics / SetReplace systems + a Wolfram Physics Project WM148 causal-invariance case study (fresh-vertex semantics)

Credo

"The genome doesn't specify the organism; it offers a set of pointers to regions in the space of all possible forms, relying on the laws of physics and computation to do the heavy lifting." — Michael Levin

Our company operates as a lens for cognitive pointers: identifying established theoretical work and translating it into computationally parsable structures. By turning ideas into formal axioms, and axioms into verifiable code, we create the "Lego blocks" required to build complex systems with confidence.

Acknowledgment

We humbly thank the collective intelligence of humanity for providing the technology and culture we cherish. We do our best to properly reference the authors of the works utilized herein, though we may occasionally fall short. Our formalization acts as a reciprocal validation—confirming the structural integrity of their original insights while securing the foundation upon which we build. In truth, all creative work is derivative; we stand on the shoulders of those who came before, and our contributions are simply the next link in an unbroken chain of human ingenuity.

Part of the broader HeytingLean formal verification project: https://apoth3osis.io

Results (One Story)

This repo mechanizes two complementary facts about Wolfram/SetReplace-style rewriting:

Independence (CE1/CE2): confluence and causal invariance are independent properties.
WM148 (Wolfram Physics Project): under an explicit fresh-vertex semantics and equivalence up to vertex renaming, WM148 is causally invariant (in the sense of SystemFresh.CausalInvariant).
Observable-event (“GC”) causal graphs (bridge abstraction): a coarse-grained causal graph notion that discards events whose created expressions do not survive to the endpoint; this makes CE1’s “detour step” disappear (see HeytingLean.WPP.Wolfram.Counterexamples.CE1.causalGraphGC_iso_short_long).

The point is that the counterexamples rule out “confluence ⇒ causal invariance” under naive matching, while WM148 demonstrates a principled semantics (fresh allocation + α-equivalence) where a concrete WPP model satisfies causal invariance.

Three notions of “causal invariance” used in this repository (be precise when citing):

SetReplace-style (terminating) causal-graph invariance: HeytingLean.WPP.Wolfram.Properties.CausalInvariant compares System.causalGraphOf across normal-form evolutions.
Observable-event (“GC”) causal-graph invariance: HeytingLean.WPP.Wolfram.Properties.GCausalInvariant compares System.causalGraphGCOf across normal-form evolutions (coarse-graining; not SetReplace’s definition).
Wolfram Physics branch-pair resolution (fresh vertices): HeytingLean.WPP.Wolfram.SystemFresh.CausalInvariant is joinability-up-to-iso for one-step forks in the fresh-vertex semantics.

A) Independence Theorem (CE1/CE2)

CE1 Multiway + Branchial Graph: Confluent but NOT causally invariant

In the Wolfram Physics Project, causal invariance was proposed as the keystone property ensuring observer-independent physics. Many assumed it was equivalent to confluence (unique normal forms).

This formalization proves they are independent:

Systems can be confluent without being causally invariant
Systems can be causally invariant without being confluent

Note (why CE1 is subtle): CE1’s two maximal evolutions reach the same normal form but have different lengths. This breaks SetReplace-style causal-graph invariance, but under the observable-event (“GC”) causal graph abstraction the two evolutions have isomorphic causal graphs (HeytingLean.WPP.Wolfram.Counterexamples.CE1.causalGraphGC_iso_short_long).

Counterexamples Visualized

CE1: Confluent ∧ ¬Causal-Invariant All paths converge to same normal form, but causal graphs differ	CE2: Causal-Invariant ∧ ¬Confluent Multiple normal forms exist, but causal graphs are isomorphic
CE1 Branchial structure	CE2 Branchial structure

B) WM148 Case Study (Fresh-Vertex Semantics)

WM148 bounded multiway graph (depth 3; deterministic fresh allocator)

rule: {{x,y}} → {{x,y},{y,z}} (one fresh vertex z)
semantics: explicit fresh allocation + equivalence up to vertex renaming (HGraph.Iso)
mechanized theorem: WM148.causalInvariant : SystemFresh.CausalInvariant (sys := WM148.sys)
executable demo: lake exe wolfram_wm148_demo (emits bounded multiway JSON; default --maxDepth 6)
import graph (WM148 slice): RESEARCHER_BUNDLE/artifacts/visuals/wm148_import_graph.svg / RESEARCHER_BUNDLE/artifacts/visuals/wm148_import_graph.html

Proof Visualizations

Explore the proof structure in 2D and 3D:

Proof ↔ Hypergraph Bridge

Click a theorem node in the proof map and use the Artifacts panel to jump directly to the corresponding multiway/hypergraph visualizations and interactive viewer.

GitHub Pages: https://abraxas1010.github.io/causal-confluence-wolfram-lean/RESEARCHER_BUNDLE/artifacts/visuals/proof_hypergraph_bridge.html

Proof Map (3D preview)	Hypergraph/Multiway Artifact (CE1 preview)
Proof Map (3D static fallback)	Hypergraph/Multiway Artifact (CE2 preview)

Direct deep-links to the interactive multiway viewer:

2D Proof Map
Pan, zoom, search declarations

wolfram_2d.html (GitHub Pages)

3D Proof Map
Rotate, zoom, explore clusters

wolfram_3d.html (GitHub Pages)

WM148-only proof/declaration map:

WM148 2D Proof Map
Pan, zoom, search declarations

wm148_2d.html (GitHub Pages)

WM148 3D Proof Map
Rotate, zoom, explore clusters

wm148_3d.html (GitHub Pages)

Declarations visualized with UMAP embeddings:

Color-coded by module family (Hypergraph, Rewrite, CausalGraph, Multiway, etc.)
Click nodes to see theorem details, file location, and code snippets.
kNN edges show proof similarity neighborhoods.

Interactive multiway viewer (CE1/CE2/WM148-depth3 built-in; or load generated_ce1.json / generated_ce2.json / generated_wm148.json):

GitHub Pages: https://abraxas1010.github.io/causal-confluence-wolfram-lean/RESEARCHER_BUNDLE/artifacts/wolfram_viewer.html (supports ?demo=ce1|ce2|wm148)
Offline: RESEARCHER_BUNDLE/wolfram_viewer.html (wrapper; supports ?demo=...) or RESEARCHER_BUNDLE/artifacts/wolfram_viewer.html (direct)

UMAP note (interpretation + limitations):

UMAP is a non-linear projection of high-dimensional feature vectors into 2D/3D; here the features are derived from Lean source text statistics and structural signals.
Only local neighborhoods are intended to be meaningful; global distances/cluster geometry are not proof-theoretic invariants.
The layout depends on hyperparameters and a random seed; reruns can rotate/warp the embedding while preserving similar local structure.
Treat these maps as navigational aids; the formal guarantee is always the Lean kernel check, not the embedding.
GitHub README pages block embedded iframes/WebGL; the README shows a lightweight preview, while the full interactive 3D viewer is on GitHub Pages.

What's Formalized

Component	Description
Hypergraph Model	SetReplace-faithful: `Expr V := List V`, `HGraph V := Multiset (Expr V)`
Rewrite Semantics	Rules, events, SetReplace-style substitutions (not assumed injective), applicability
Fresh-Vertex Semantics	Explicit fresh-name supply + α-equivalence up to vertex renaming
Injective-WLOG Lemmas	Under a “simple hypergraph” invariant, applicable matches are forced injective (standard `Fin n`/`finRange` LHS shape)
Causal Graphs	"Created then destroyed" edges, graph isomorphism
GC Causal Graphs	Observable-event (“garbage-collected”) causal graph abstraction + `GCausalInvariant`
Properties	`ConfluentNF` (unique normal forms), `CausalInvariant` (isomorphic causal graphs)
Counterexamples	CE1: confluent ∧ ¬causal-invariant, CE2: causal-invariant ∧ ¬confluent
Main Theorem	`confluence_causal_invariance_independent`
Multiway Infrastructure	Finite enumerators, branchial graphs, WPP bridges
WM148 (Wolfram Physics)	`{{x,y}} → {{x,y},{y,z}}` with explicit fresh vertices + causal invariance proof (branch-pair resolution up to `HGraph.Iso`)

Quick Start

Verify Everything (One Command)

cd RESEARCHER_BUNDLE
./scripts/verify_wolfram.sh

This runs strict builds, runs the Wolfram multiway demo, and also emits + checks a small certified LambdaIR → MiniC → C compilation artifact (see RESEARCHER_BUNDLE/artifacts/compiler/).

Run the Demo

cd RESEARCHER_BUNDLE
lake exe wolfram_multiway_demo              # CE1 (default)
lake exe wolfram_multiway_demo -- --sys ce2  # CE2
lake exe wolfram_wm148_demo                 # WM148 (fresh-vertex semantics; bounded multiway JSON)

Emit Verified Compiler Artifacts (LambdaIR → C)

From the standalone bundle:

cd RESEARCHER_BUNDLE
lake exe wolfram_bundle_demo
cc artifacts/compiler/c/wpp_add1.c -O2 -std=c11 -o artifacts/compiler/bin/wpp_add1
./artifacts/compiler/bin/wpp_add1   # expected output: 42

Run in Wolfram Language (optional)

This repo ships a pure Wolfram Language script that reproduces the CE1/CE2 bounded multiway JSON output of wolfram_multiway_demo, and a small WM148 bounded multiway JSON used to cross-check the fresh-vertex semantics:

RESEARCHER_BUNDLE/tools/wolfram_ce1_ce2.wl

In Mathematica / Wolfram Engine:

Get["RESEARCHER_BUNDLE/tools/wolfram_ce1_ce2.wl"];
Export["ce1_from_wl.json", CE1JSON[3], "JSON"];
Export["ce2_from_wl.json", CE2JSON[2], "JSON"];
Export["wm148_from_wl.json", WM148JSON[3], "JSON"];

Compare against the Lean-produced files:

RESEARCHER_BUNDLE/artifacts/generated_ce1.json
RESEARCHER_BUNDLE/artifacts/generated_ce2.json
RESEARCHER_BUNDLE/artifacts/generated_wm148_wlcheck.json

If you have wolframscript installed, the bundle also provides an automated cross-check:

cd RESEARCHER_BUNDLE
./scripts/verify_wolfram_wl.sh

If you do not have Wolfram Engine installed, the same cross-check can be run with the open-source WL runtime mathics:

python3 -m pip install --user mathics3 packaging
cd RESEARCHER_BUNDLE
./scripts/verify_wolfram_wl.sh

Key Theorems

-- Main independence result
theorem Counterexamples.confluence_causal_invariance_independent :
  (∃ sys, ConfluentNF sys ∧ ¬CausalInvariant sys) ∧
  (∃ sys, CausalInvariant sys ∧ ¬ConfluentNF sys)

-- CE1: confluent but not causally invariant
theorem Counterexamples.CE1.confluentNF : ConfluentNF Counterexamples.CE1.sys
theorem Counterexamples.CE1.not_causalInvariant : ¬CausalInvariant Counterexamples.CE1.sys
theorem Counterexamples.CE1.causalGraphGC_iso_short_long :
  CausalGraph.Iso (Counterexamples.CE1.sys.causalGraphGCOf [Counterexamples.CE1.e13] Counterexamples.CE1.s2)
    (Counterexamples.CE1.sys.causalGraphGCOf [Counterexamples.CE1.e12, Counterexamples.CE1.e23] Counterexamples.CE1.s2)

-- CE2: causally invariant but not confluent
theorem Counterexamples.CE2.causalInvariant : CausalInvariant Counterexamples.CE2.sys
theorem Counterexamples.CE2.not_confluentNF : ¬ConfluentNF Counterexamples.CE2.sys
theorem Counterexamples.CE2.causalInvariantGC : GCausalInvariant Counterexamples.CE2.sys

-- WM148: causally invariant (fresh-vertex semantics; branch-pair resolution up to renaming)
theorem WM148.causalInvariant : SystemFresh.CausalInvariant (sys := WM148.sys)

-- Bridge: finite enumerator agrees with Step relation
theorem stepStates_iff_step : t ∈ stepStates s ↔ Step s t

-- Fresh-vertex semantics: different fresh allocations are isomorphic (α-equivalence)
theorem SystemFresh.Event.applyWith_iso : HGraph.Iso (e.applyWith τ₁ s) (e.applyWith τ₂ s)

-- Injective-WLOG (under simple-hypergraph invariant)
theorem System.Event.injective_of_applicable_of_finRange_mem_lhs : Function.Injective e.σ

Axiom Footprint

The formalization uses only standard Lean kernel axioms:

Axiom	Purpose
`propext`	Propositional extensionality
`Classical.choice`	Axiom of choice
`Quot.sound`	Quotient soundness

No project-specific axioms introduced.

Documentation

File	Description
`01_Lean_Map.md`	Concept → Lean mapping
`02_Proof_Index.md`	What's proved and where (incl. WM148 causal invariance)
`03_Reproducibility.md`	Build/run commands
`04_Dependencies.md`	Lean/mathlib pins
`05_Technical_Report.md`	Technical summary
`06_Final_Audit.md`	QA status
`TECHNICAL_REPORT_FULL.md`	Full research report

Repository Structure

├── README.md                 # This file
├── .nojekyll                 # GitHub Pages helper
├── index.html                # GitHub Pages landing
├── 0[1-6]_*.md               # Documentation
├── TECHNICAL_REPORT_FULL.md  # Full report
├── artifacts/                # Static artifacts (SVG graphs, etc.)
├── tools/                    # Local tooling for this PaperPack
└── RESEARCHER_BUNDLE/
    ├── README_VERIFY.md              # One-command verification instructions
    ├── lean-toolchain               # Lean pin
    ├── lakefile.lean                # Lake package + pinned deps
    ├── lake-manifest.json           # Locked transitive dependency pins
    ├── HeytingLean/                 # Lean sources (WPP/Wolfram + compiler slice)
    ├── scripts/                     # `verify_wolfram.sh` (+ small helpers)
    ├── artifacts/
    │   ├── visuals/                 # 2D/3D viewers, previews, SVG graphs
    │   └── compiler/                # LambdaIR → MiniC → C outputs (+ `.olean` bundle)
    └── reports/                     # Build transcripts, hashes, portability checks

References

Piskunov, M. (2020). "Confluence and Causal Invariance." Wolfram Physics Bulletins
Wolfram, S. (2020). "A Project to Find the Fundamental Theory of Physics." wolframphysics.org
Gorard, J. (2020). "Some Relativistic and Gravitational Properties of the Wolfram Model." arXiv:2004.14810
SetReplace. "GitHub: maxitg/SetReplace"

Part of the HeytingLean formal verification project

License

This project is provided under the Apoth3osis License Stack v1. See LICENSE.md and the files under licenses/.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Repository files navigation

Wolfram Physics Formalization

Credo

Acknowledgment

Results (One Story)

A) Independence Theorem (CE1/CE2)

Counterexamples Visualized

B) WM148 Case Study (Fresh-Vertex Semantics)

Proof Visualizations

Proof ↔ Hypergraph Bridge

What's Formalized

Quick Start

Verify Everything (One Command)

Run the Demo

Emit Verified Compiler Artifacts (LambdaIR → C)

Run in Wolfram Language (optional)

Key Theorems

Axiom Footprint

Documentation

Repository Structure

References

License

About

Uh oh!

Releases

Packages

Uh oh!

Contributors

Uh oh!

Languages

Name		Name	Last commit message	Last commit date
Latest commit History 42 Commits
RESEARCHER_BUNDLE		RESEARCHER_BUNDLE
artifacts		artifacts
assets		assets
licenses		licenses
tools		tools
.gitignore		.gitignore
.nojekyll		.nojekyll
01_Lean_Map.md		01_Lean_Map.md
02_Proof_Index.md		02_Proof_Index.md
03_Reproducibility.md		03_Reproducibility.md
04_Dependencies.md		04_Dependencies.md
05_Technical_Report.md		05_Technical_Report.md
06_Final_Audit.md		06_Final_Audit.md
CLA.md		CLA.md
LICENSE.md		LICENSE.md
README.md		README.md
TECHNICAL_REPORT_FULL.md		TECHNICAL_REPORT_FULL.md
index.html		index.html
wolfram_audit_outstanding.md		wolfram_audit_outstanding.md

Folders and files

Latest commit

History

Repository files navigation

Wolfram Physics Formalization

Credo

Acknowledgment

Results (One Story)

A) Independence Theorem (CE1/CE2)

Counterexamples Visualized

B) WM148 Case Study (Fresh-Vertex Semantics)

Proof Visualizations

Proof ↔ Hypergraph Bridge

What's Formalized

Quick Start

Verify Everything (One Command)

Run the Demo

Emit Verified Compiler Artifacts (LambdaIR → C)

Run in Wolfram Language (optional)

Key Theorems

Axiom Footprint

Documentation

Repository Structure

References

License

About

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Uh oh!

Contributors

Uh oh!

Languages

Packages