Assembly TheoryThe Physics of Causation
First fully mechanized formalization of Assembly Theory's core mathematics. Proves that the Assembly Index — a universal measure of molecular complexity — equals the reuse-aware DAG join count, with tight bounds . 10 modules covering assembly spaces, pathways, bounds, quotient monotonicity, molecular semantics, hypergraph bridges, and selection predicates.
Formal Verification Certificate
Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.
Assembly Theory • Lean 4 + Mathlib • Apoth3osis Labs
Key Mathematics
ASSEMBLY SPACE
Objects Ω, primitives U, ternary join predicate J. Closure: every object is reachable from primitives via J.
ASSEMBLY INDEX
Minimum path length equals reuse-aware join count. This is the main theorem: assemblyIndex_eq_dagJoinCount.
TIGHT BOUNDS
Lower bound: doubling argument (each join doubles max leaves). Upper bound: linear chain has no reuse.
QUOTIENT MONOTONICITY
Identifying equivalent structures cannot increase complexity. Key for molecular equivalence classes.
Paper ↔ Proof Correspondence
| PAPER | PROOF | STATUS | NOTES |
|---|---|---|---|
| §2 Assembly Space (Ω, U, J) | AssemblySpace, AssemblyPath | PROVED | Paper-faithful structure with closure predicate |
| §2 Assembly Index = min path length | assemblyIndex (Nat.find) | PROVED | Well-defined via Nat.find on closed spaces |
| §2 AI = DAG join count (with reuse) | assemblyIndex_eq_dagJoinCount | PROVED | THE main result: reuse-aware join count equals AI |
| §3 Lower bound: AI ≥ log₂(size) | assemblyIndex_ge_log2 | PROVED | Tight lower bound via doubling argument |
| §3 Upper bound: AI ≤ size − 1 | assemblyIndex_le_size_sub_one | PROVED | No reuse gives linear chain |
| §4 Quotient monotonicity | assemblyIndex_quotient_le | PROVED | Equivalence can only reduce complexity |
| §5 Molecular assembly semantics | assemblyIndex_mol_le_dagJoinCount | PROVED | Bonds as primitives, vertex superposition |
| §7 Selection predicates | selected, mono_in_Theta | PROVED | High AI + high abundance = biosignature |
Proof Blueprint
Module Dependencies
Hover over a module to trace its imports. Core → Path → Index → Bounds/Quotient/Molecular.
Verified C Artifacts
Generated via CAB pipeline: Lean 4 → LambdaIR → MiniC → C. Each file carries a correctness certificate verifying semantic preservation.
assembly_space.c
Obj syntax tree: base/join + size + joinCount | from AssemblySpace + AssemblyCore
assembly_index.c
DAG join count with hash-table reuse tracking + bounds verification | from AssemblyIndex
assembly_bounds.c
Tight bounds: log₂ ≤ AI ≤ size-1 + tightness witness | from AssemblyBounds
Safe Rust Artifacts
Transpiled from verified C to idiomatic safe Rust. 16 tests passing. Download the full crate and run cargo test.
assembly_space.rs
Obj enum + Hash + size/joinCount + 5 tests | from AssemblySpace
assembly_index.rs
assembly_index via HashSet DAG tracking + 5 tests | from AssemblyIndex
assembly_bounds.rs
upper_bound_holds + lower_bound_holds + 7 tests | from AssemblyBounds
lib.rs
Crate root re-exporting all modules | from —
Cargo.toml
Package manifest (edition 2021, 0 dependencies) | from —
Provenance Chain
Research Paper
Walker, S.I., Mathis, C., Cronin, L. et al. “The Physics of Causation.” 2024. Assembly Theory proposes a universal measure of molecular complexity — the Assembly Index — that can distinguish molecules produced by selection (life, technology) from random chemistry.
Lean 4 Formalization
10 modules, 12 theorems, 2,131 lines. Machine-checked proofs of assembly index bounds, reuse-aware join count equality, quotient monotonicity, molecular semantics. Standard kernel axioms only. Zero sorry/admit.
Verified C
3 C files: assembly space, index computation with DAG tracking, bounds verification. Compiled with gcc -std=c11 -Wall -Wextra -Werror. Zero warnings.
Safe Rust
Full Rust crate with 16 tests. Idiomatic safe Rust — no unsafe blocks. cargo test: 16 passed, 0 failed.