<sub>Our tech stack is ontological:
Hardware — Physics
Software — Mathematics

Our engineering workflow is simple: discover, build, grow, learn & teach</sub>

---

_{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.}

---

Multiway Rewriting Systems as ∞-Groupoids

A Machine-Checked Foundation for Computational Universes
From term rewriting to homotopy types: mechanized proofs that multiway systems form ∞-groupoids, with applications to the Wolfram Physics Project.

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

---

The Vision: Computation as Geometry

What if every computation carried geometric structure? What if the branching paths through a program's execution space formed not just a graph, but a homotopy type—an object where paths between states, paths between paths, and higher paths all carry mathematical meaning?

This repository provides machine-checked proofs that this vision is mathematically sound. We show that:

1. Any rewriting system (term rewriting, graph rewriting, hypergraph rewriting) naturally generates a multiway system—a space of all possible execution paths.

2. Multiway systems form ∞-groupoids. The paths are morphisms; path compositions are higher cells; the whole structure satisfies the horn-filling conditions that define an ∞-groupoid (Kan complex).

3. This structure is computable. We provide executable demos that explore bounded slices of multiway/branchial graphs for concrete systems, with deterministic JSON output verified against Wolfram Language.

4. The framework extends to physics. We instantiate the pipeline for Wolfram Physics Project systems (CE1, CE2, WM148), proving their multiway graphs also form ∞-groupoids and computing geometry observables (distance, ball growth, dimension estimates).

---

Why This Matters

For Computer Science

The multiway perspective reveals that non-determinism has structure. When a computation can branch (different evaluation orders, non-deterministic choices, concurrent interleavings), the space of all branches isn't just a set—it's a higher category. Paths that reach the same result via different routes may be "the same" at one level but "different" at another.

This has immediate applications:

• Confluence analysis: When do all paths lead to the same place? (Church-Rosser property)
• Concurrency semantics: Interleaving as categorical structure
• Program equivalence: Two programs are equivalent if their multiway spaces are homotopy-equivalent

For Mathematics

We mechanize a concrete instance of the homotopy hypothesis: the correspondence between ∞-groupoids and homotopy types. Our construction:

Rewriting System → Multiway Quiver → Free Groupoid → Nerve → Kan Complex

proves that the nerve of a free groupoid is always a Kan complex (∞-groupoid), and applies this to multiple concrete systems.

For Physics

The Wolfram Physics Project proposes that physical spacetime emerges from the multiway evolution of abstract rewriting systems. Our formalization provides:

• Rigorous foundations: Machine-checked proofs of causal invariance, confluence, and ∞-groupoid structure for concrete Wolfram Model rules
• Geometry observables: Computable distance, ball growth, and dimension estimates on branchial graphs
• Rulial structure: Morphisms between rule systems and their induced higher homotopies

For AGI Research

Ben Goertzel's OpenCog Hyperon framework uses MeTTa (Meta Type Talk) as a "language of thought" for AGI. In his Reflective Metagraph Rewriting paper, Goertzel establishes that:

• MeTTa execution traces form ∞-groupoids. Non-deterministic program execution generates multiple traces; homomorphisms between traces are homotopies.
• The space of all MeTTa codebases is an (∞,1)-topos—which Goertzel notes is "basically the same as the Ruliad."

Our formalization provides machine-checked proofs of exactly these structures:

Goertzel/Hyperon Claim	HeytingLean Theorem
Execution traces form ∞-groupoids	SSet.KanComplex SKYInfty
Ruliad as (∞,1)-topos	Sieve frame + nucleus on closed sieves
Self-modification preserves structure	Rulial inclusion → induced functors

This matters for beneficial AGI: if goal structures are encoded categorically, then homotopy invariants become alignment constraints preserved under self-modification.

---

What We Prove

Core Theorems

Theorem	Statement	Module
SKY Confluence	churchRosser_steps	LoF/Comb/Confluence.lean
Kan Complex (SKY)	SSet.KanComplex SKYInfty	LoF/Combinators/InfinityGroupoid/SSet.lean
Kan Complex (WPP)	SSet.KanComplex (WppRel.Infty R)	WPP/InfinityGroupoid/SSet.lean
Sieve Frame	Sieve X is a complete Heyting algebra	LoF/Combinators/Topos/SieveFrame.lean
Nucleus Fixed Points	Ω_J inherits frame structure	LoF/Combinators/Topos/SieveNucleus.lean
Truncation Bridge	Bicategory = 2-truncation of 3-cells	LoF/Combinators/Category/Completion3CellTruncationBridge.lean
Rulial Monotonicity	Branch resolution lifts through rule inclusion	WPP/Rulial/HigherCells.lean
Geometry Invariance	Observables stable under relabeling	WPP/Wolfram/Geometry/Observables.lean

The ∞-Groupoid Pipeline

flowchart LR
  subgraph Input["Rewriting System"]
    rules["Rules: SKY, CE1, WM148"]
    step["stepRel : State → State → Prop"]
  end

  subgraph Category["Categorical Structure"]
    paths["Paths : State → State → Type"]
    cat["Path category: MWObj, LSteps"]
    gpd["FreeGroupoid"]
  end

  subgraph Homotopy["Homotopy Theory"]
    nerve["CategoryTheory.nerve"]
    kan["SSet.KanComplex"]
    infty["∞-groupoid"]
  end

  rules --> step
  step --> paths
  paths --> cat
  cat --> gpd
  gpd --> nerve
  nerve --> kan
  kan --> infty

Loading

---

Systems Formalized

SKY Combinators

The classic combinator calculus extended with Y (fixed-point combinator):

• K x y → x
• S x y z → x z (y z)
• Y f → f (Y f)

Key results: Full confluence, enumerable one-step edges, ∞-groupoid packaging.

Wolfram Physics Project Systems

System	Description	Confluence	∞-Groupoid
CE1	Counterexample 1 (edge splitting)	✗	✓
CE2	Counterexample 2 (triangle formation)	✗	✓
WM148	Rule 148 with fresh vertices	✓ (causal invariant)	✓

---

Executables

SKY Demos

cd RESEARCHER_BUNDLE

# Multiway exploration
lake exe sky_multiway_demo -- --demo sk --maxDepth 3
lake exe sky_multiway_demo -- --demo y --maxDepth 2

# Full artifact pipeline (Lean → LambdaIR → C)
lake exe sky_bundle_demo

Wolfram Physics Demos

cd RESEARCHER_BUNDLE

# ∞-groupoid counts (states/paths at each depth)
lake exe wolfram_infty_demo -- --sys ce1 --maxDepth 3
lake exe wolfram_infty_demo -- --sys ce2 --maxDepth 3
lake exe wolfram_infty_demo -- --sys wm148 --maxDepth 6

# Geometry observables (distance, ball growth, dimension)
lake exe wolfram_geometry_demo -- --sys ce1 --maxR 4
lake exe wolfram_geometry_demo -- --sys wm148 --depth 3 --maxR 5

---

Interoperability

We provide cross-platform verification against Wolfram Language and MeTTa (Hyperon's AGI language):

# One-command cross-check (Lean vs WL vs MeTTa)
python3 interop/run_crosschecks.py --all

Wolfram Language

The interop/wolfram/ directory replicates our multiway semantics in WL:

# Run WL cross-check (requires wolframscript or mathics)
bash interop/wolfram/verify_sky_wl.sh

MeTTa / Hyperon

The interop/metta/ directory provides one-step SKY rewrite rules for Hyperon:

; sky_rules.metta — K and S reduction
(= (eval1 (app (app K $x) $y)) $x)
(= (eval1 (app (app (app S $x) $y) $z))
   (app (app $x $z) (app $y $z)))

# Install Hyperon runtime (optional)
python3 -m pip install --user hyperon

# Run MeTTa cross-check
python3 interop/metta/run_demo.py --demo kdemo

The cross-check harness verifies that Lean, WL, and MeTTa produce identical one-step successors for the demo terms.

---

Visual Story

Multiway + Branchial (SK demo) Generated by Lean; load JSON in the interactive viewer More visuals	Topos / Gluing as a Nucleus Grothendieck closure on sieves packaged as Order.Nucleus Lean module
2D Proof Map Navigate declarations and clusters Open 2D	3D Proof Map Dynamic rotation preview; open for interaction Open 3D

Multiway/Branchial Graphs

SK demo (depth 3):

Y demo (depth 2):

---

Architecture

Module Structure

HeytingLean/
├── LoF/                          # Laws of Form / SKY combinators
│   ├── Comb/                     # Core syntax + reduction
│   ├── Combinators/
│   │   ├── Category/             # Path categories, groupoid completion
│   │   ├── InfinityGroupoid/     # Kan complex proofs
│   │   └── Topos/                # Sieve frame, nucleus, sheaves
│   └── MRSystems/                # M-R system bridge
│
├── WPP/                          # Wolfram Physics Project
│   ├── Wolfram/                  # Hypergraph rewriting
│   │   ├── Geometry/             # Distance, ball growth, dimension
│   │   └── *.lean                # CE1, CE2, WM148, confluence
│   ├── Rulial/                   # Rule inclusion morphisms
│   │   └── Examples/             # Concrete rulial examples
│   ├── InfinityGroupoid/         # Kan packaging for WPP
│   └── *.lean                    # Generic multiway infrastructure
│
└── CLI/                          # Executables
    ├── SkyMultiwayMain.lean
    ├── WolframInfinityGroupoidMain.lean
    └── WolframGeometryMain.lean

Key Entry Points

Layer	Purpose	Module
SKY ∞-Groupoid	Kan complex for SKY	LoF/Combinators/InfinityGroupoid/SSet.lean
WPP ∞-Groupoid	Kan complex for any WppRel	WPP/InfinityGroupoid/SSet.lean
3-Cell Calculus	Explicit higher cells	LoF/Combinators/Category/Completion3Cell.lean
Rulial Morphisms	Rule inclusion → functor	WPP/Rulial/Functor.lean
Geometry	Observable invariants	WPP/Wolfram/Geometry/Observables.lean
Topos Layer	Sieve nucleus + frame	LoF/Combinators/Topos/SieveNucleus.lean

---

Future Directions

Immediate Extensions

1. Higher-Dimensional Nerves: Use the Duskin nerve of the completion bicategory to obtain ∞-groupoids with non-trivial π₂.

2. Spectral Dimension: Extend geometry observables to compute spectral dimension from random walk statistics on branchial graphs.

3. Typed Combinators: Add a Curry-Howard layer with simply-typed SK combinators and subject reduction.

Research Horizons

1. HoTT Integration: Connect to Lean's HoTT libraries to formalize the equivalence between our Kan complexes and actual homotopy types.

2. Emergent Spacetime: Mechanize the derivation of approximate Lorentzian geometry from causal graph limits (per Gorard's relativistic Wolfram model work).

3. Quantum Branching: Extend to quantum multiway systems where branches carry amplitudes, connecting to path integral formulations.

4. Rulial Universe: Formalize the "rulial space" as a category of rule systems with morphisms as inclusions, and study its universal properties.

---

Verification

Quick Start

# Clone and enter
git clone https://github.com/Abraxas1010/sky-combinator-multiway-lean.git
cd sky-combinator-multiway-lean

# Full verification (strict build + all executables + cross-checks)
cd RESEARCHER_BUNDLE && ./scripts/verify_sky.sh

Offline Mode

First setup requires network access for lake update. After dependencies are present:

SKY_SKIP_UPDATE=1 ./scripts/verify_sky.sh

Manual Checks

cd RESEARCHER_BUNDLE

# Strict library build
lake build -- -DwarningAsError=true

# Individual demos
lake exe sky_multiway_demo -- --demo sk --maxDepth 3
lake exe wolfram_infty_demo -- --sys wm148 --maxDepth 4
lake exe wolfram_geometry_demo -- --sys ce1 --maxR 4

---

Documentation

Document	Contents
01_Lean_Map.md	Module dependency map
02_Proof_Index.md	Declaration index
03_Reproducibility.md	Build/verification instructions
06_Final_Audit.md	Full QA outputs
08_Mathematical_Audit.md	Scope and claims
TECHNICAL_REPORT_FULL.md	Extended technical report

---

Interactive Resources

• Landing Page: abraxas1010.github.io/sky-combinator-multiway-lean
• Multiway Viewer: sky_viewer.html
• Proof ↔ Artifact Bridge: proof_sky_bridge.html
• 2D Proof Map: sky_2d.html
• 3D Proof Map: sky_3d.html

---

References

Primary Sources

• Arsiwalla–Gorard–Elshatlawy, Homotopies in Multiway (Non-Deterministic) Rewriting Systems as n-Fold Categories (arXiv:2105.10822)
• Arsiwalla–Gorard, Pregeometric Spaces from Wolfram Model Rewriting Systems as Homotopy Types (arXiv:2111.03460)
• Gorard, Some Relativistic and Gravitational Properties of the Wolfram Model (arXiv:2004.14810)
• Goertzel, Reflective Metagraph Rewriting as a Foundation for an AGI "Language of Thought" (arXiv:2112.08272)

Background

• S. Wolfram, A Project to Find the Fundamental Theory of Physics — wolframphysics.org
• P. T. Johnstone, Stone Spaces (frames/locales; nuclei and sublocales)
• nLab: nucleus, Kan complex, ∞-groupoid

---

License

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