>_PAPER.PROOF.CODE

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 $\log_2(\text{size}) \le \text{AI} \le \text{size} - 1$ . 10 modules covering assembly spaces, pathways, bounds, quotient monotonicity, molecular semantics, hypergraph bridges, and selection predicates.

GitHub|Walker, Cronin et al. (2024)

Lean 4 Modules

Full pipeline: Space → Path → Index → Bounds → Quotient → Molecular

Key Theorems

assemblyIndex_eq_dagJoinCount, bounds, quotient, molecular

Sorry Count

All proofs complete — standard kernel axioms only

2,131

Lines of Lean

Across 10 modules

C Files

assembly_space.c, assembly_index.c, assembly_bounds.c

Rust Tests

All passing (0 failures)

Axioms

propext, Classical.choice, Quot.sound (kernel standard)

2024

Paper Year

Walker, Cronin et al. — Nature

>_VERIFICATION.SEAL

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.

12 THEOREMS VERIFIED10 MODULES2,131 LINES0 SORRY

Assembly Theory • Lean 4 + Mathlib • Apoth3osis Labs

Key Mathematics

ASSEMBLY SPACE

\mathcal{S} = (\Omega, U, J) \quad\text{where}\quad U \subseteq \Omega,\; J : \Omega \times \Omega \times \Omega \to \text{Prop}

Objects Ω, primitives U, ternary join predicate J. Closure: every object is reachable from primitives via J.

ASSEMBLY INDEX

\text{AI}(z) = \min\{|p| \mid p : \text{AssemblyPath}(z)\} = \text{dagJoinCount}(z)

Minimum path length equals reuse-aware join count. This is the main theorem: assemblyIndex_eq_dagJoinCount.

TIGHT BOUNDS

\log_2(\text{size}(o)) \le \text{AI}(o) \le \text{size}(o) - 1

Lower bound: doubling argument (each join doubles max leaves). Upper bound: linear chain has no reuse.

QUOTIENT MONOTONICITY

\text{AI}([z]_r) \le \text{AI}(z)

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

Proof Blueprint

⊢⊣⊢⊣

>_MENTAT.JOIN

“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune

A janitor who proves a theorem outranks a tenured professor who publishes noise.

Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.

ONTOLOGICAL ENGINEER8 designations

IDEA

A valid, original framing or conjecture

THEORY

Formal argument with paper-level rigor

APPLICATION

Connecting theory to observable outcomes

CODE

Working software the project depends on

EXPERIMENT

Reproducible research with methodology and data

PROOF

Machine-verified claim checked by a proof assistant

KERNEL

Foundational, load-bearing implementation

BRIDGE

Connecting subsystems or knowledge domains end-to-end

NOETIC ENGINEER8 designations

VISIONARY

Strategic direction & roadmaps

NARRATOR

Writing, documentation & papers

DESIGNER

Visual, UX & information design

EDUCATOR

Teaching, tutorials & workshops

CULTIVATOR

Community, outreach & events

DIPLOMAT

Partnerships, governance & policy

INTERPRETER

Translation, media & accessibility

SENTINEL

Ethics, review & quality assurance

Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.

APPLY TO MENTAT EXPLORE PROJECTSMESH-ENCRYPTED NETWORK FOR TRUSTED AUTONOMOUS TRANSACTIONS

>_DEPENDENCY.GRAPH

Module Dependencies

Hover over a module to trace its imports. Core → Path → Index → Bounds/Quotient/Molecular.

Foundation Core Theorems Extensions

>_VERIFIED.C

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

DOWNLOAD

assembly_index.c

DAG join count with hash-table reuse tracking + bounds verification | from AssemblyIndex

DOWNLOAD

assembly_bounds.c

Tight bounds: log₂ ≤ AI ≤ size-1 + tightness witness | from AssemblyBounds

DOWNLOAD

>_SAFE.RUST

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

DOWNLOAD

assembly_index.rs

assembly_index via HashSet DAG tracking + 5 tests | from AssemblyIndex

DOWNLOAD

assembly_bounds.rs

upper_bound_holds + lower_bound_holds + 7 tests | from AssemblyBounds

DOWNLOAD

lib.rs

Crate root re-exporting all modules | from —

DOWNLOAD

Cargo.toml

Package manifest (edition 2021, 0 dependencies) | from —

DOWNLOAD

>_PROVENANCE

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.

>_DOWNLOAD

Download Archives

Lean 4 Proofs

10 modules, 2,131 lines, 0 sorry

Verified C

3 files, gcc -Wall -Werror clean

Safe Rust

Full crate, 16 tests, 0 failures