Wolfram Physics — Proof/Declaration Map

Proof ↔ Hypergraph Bridge

Click a theorem/definition in the proof maps to jump directly to the corresponding Wolfram multiway/hypergraph visualizations and the interactive viewer.

Open proof_hypergraph_bridge.html

WM148 (Fresh-Vertex Semantics) — Proof/Declaration Map

Focused UMAP visualization of the WM148 causal-invariance development (including the demo executable module).

Data source: wm148_proofs.json.

Multiway Graph Visualizations

Static DOT/SVG graphs (counterexamples + WM148):

• CE1 (Confluent but NOT causally invariant):
  • Multiway graph (depth 3)
  • Branchial graph
  • Combined view
• CE2 (Causally invariant but NOT confluent):
  • Multiway graph (depth 2)
  • Branchial graph
  • Combined view
• WM148 (fresh-vertex semantics; bounded multiway demo):
  • Multiway graph (depth 3)
  • Import graph (SVG) / import graph (HTML)

Interactive Multiway Viewer

Interactive viewer for bounded multiway graphs (CE1/CE2/WM148-depth3 built-in). You can also load generated_ce1.json, generated_ce2.json, or generated_wm148.json.

• Open viewer (CE1) / CE2 / WM148
• Wrapper (CE1) / CE2 / WM148

Wolfram Language Cross-Check (Mathics / Wolfram Engine)

The bundle includes a Wolfram Language implementation of the CE1/CE2 bounded multiway JSON (and a small WM148 bounded multiway JSON), and an automated WL↔Lean equivalence check that runs on either wolframscript or the open-source mathics runtime.

• Pipeline diagram (SVG) / GraphViz source (DOT)
• tools/wolfram_ce1_ce2.wl (WL reference implementation)
• scripts/verify_wolfram_wl.sh (automated equality check)

Key Theorems (Proof DAGs)

• Counterexamples.confluence_causal_invariance_independent — Main independence theorem
• Counterexamples.CE1.confluentNF — CE1 is confluent
• Counterexamples.CE1.not_causalInvariant — CE1 is NOT causally invariant
• Counterexamples.CE2.causalInvariant — CE2 is causally invariant
• Counterexamples.CE2.not_confluentNF — CE2 is NOT confluent
• stepStates_iff_step — Bridge: Finset ↔ Step relation
• WM148.causalInvariant — WM148 is causally invariant (fresh-vertex semantics)

UMAP Interpretation (Limitations)

• UMAP is a non-linear projection of high-dimensional feature vectors (here: Lean source text features) into 2D/3D.
• Only local neighborhoods are intended to be meaningful; global distances and cluster geometry are not proof-theoretic invariants.
• Treat these maps as navigational aids; the formal guarantee is the Lean kernel check.