Apoth3osis
<_MODELS/CAUSAL_CONFLUENCE

Multiway Causality Visual Model

Two graphs side by side. One is deterministic but breaks relativity. The other preserves relativity but isn't deterministic. Both are verified in Lean 4—what you see is the proof, rendered in 3D.

Lean Counterexamples

Wolfram Spatial Hypergraph

What You're Seeing

This visualization shows two counterexample systems from Piskunov's 2020 paper, formalized in Lean. They prove that confluence (determinism) and causal invariance (relativity) are logically independent properties.

CE1
Left graph (blue). This system always reaches the same final state—it's deterministic. But different observers see different causal structures. It's confluent but not causally invariant.
CE2
Right graph (purple). All observers agree on what caused what—the causal structure is invariant. But the system can end at different states. It's causally invariant but not confluent.
NODES
Each glowing sphere is a state in the multiway system. Edges show how states transform under rule application. The node positions are computed using force-directed layout.
CONES
The wireframe cones at root nodes represent causal cones—like light cones in relativity, they show what events can causally influence what. When cones align, observers agree.
HYPERGRAPH
The right panel applies the same Lean-certified rules to a larger Wolfram Physics hypergraph. Space is modeled as a hypergraph of relations evolving via substitutions like {{x,y,z},{u,y,v}} → {{w,z,x},{z,w,u},{x,y,w}}, the same idea Stephen Wolfram describes for the atoms of space.
DIVERGENT
Red-highlighted links show branchial differences—places where the two systems diverge. This is where the counterexample property becomes visible.

The Core Insight

Physics assumes determinism and relativistic agreement go together. These counterexamples show they don't. The Lean proofs make this machine-verifiable.

>PROPERTIES

Understanding the Two Properties

Confluence

Think: Computing 2+3 vs 3+2. Different order, same answer.

Formally: All paths through the multiway graph reach the same final state. The system is deterministic regardless of evaluation order.

theorem CE1.confluentNF

Causal Invariance

Think: Einstein's relativity. Different observers, same causal structure.

Formally: The causal graph (what caused what) is isomorphic across all evaluation orders. Observers agree on causation.

theorem CE2.causalInvariant
>VISUAL_GUIDE

Reading the Visualization

The Animation Cycle

The visualization alternates focus between CE1 and CE2. When a graph is active, it pulses slightly and becomes fully opaque. The inactive graph fades to 25% opacity.

The Stats Panel

Bottom right shows the active graph's metrics: node count, edge count, branchial links, and depth. "Divergent links" counts branchial pairs that differ between CE1 and CE2.

The Legend

Bottom left explains the visual elements: causal edges (evolution paths), divergent branchials (highlighted in red), and causal cones (showing the "light cone" structure).

>SIGNIFICANCE

Why This Matters

For the Wolfram Physics Program

Wolfram conjectured that a "theory of everything" must have causal invariance. This research shows that achieving causal invariance is a separate challenge from achieving determinism—both must be addressed independently in any fundamental theory.

For Scientific Visualization

This model demonstrates a new paradigm: visualizations driven by formally verified proofs. The node positions, edge connections, and graph structures all come from data exported by Lean. What you see is mathematically certified.

>GALLERY
CE1 and CE2 from Lean

CE1 and CE2 from Lean

Both counterexample graphs rendered side-by-side from verified proof data.

Multiway topology

Multiway topology

Reference diagram showing how branching paths create the multiway structure.

>STATUS

This model runs in your browser using WebGL. The graph data is loaded from JSON files exported by the Lean proof build. For enhanced versions with larger graphs and audio, contact rgoodman@apoth3osis.io.