# Apoth3osis

> Formal verification research platform bridging mathematical proofs in Lean 4 to executable computational models. We develop machine-verified theorems with complete proof chains.

## Overview

Apoth3osis explores the intersection of formal mathematics and computational modeling. Our research focuses on:

- **Formal Verification**: Machine-checked proofs using Lean 4 and Mathlib
- **Biological Systems Modeling**: Mathematical frameworks for self-reproducing systems
- **Causal Structures**: Formal analysis of determinism in discrete physics models
- **Proof-Driven Development**: Converting verified theorems to executable code

## Verified Research Projects

### Semantic Closure in Lean 4
Formalizes Robert Rosen's (M,R)-systems theory - the mathematical framework explaining what distinguishes living systems from machines. Proves closure to efficient causation using category-theoretic constructs.
- Status: VERIFIED
- Stack: Lean 4, Mathlib
- GitHub: https://github.com/Abraxas1010/semantic-closure-lean

### Causal Confluence in Wolfram Physics
Proves that causal invariance (determinism regardless of evaluation order) is equivalent to confluence in abstract rewriting systems. Connects Wolfram Physics to established computer science theory.
- Status: VERIFIED
- Stack: Lean 4, Wolfram Language
- GitHub: https://github.com/Abraxas1010/causal-confluence-wolfram-lean

## Visual Models (Proof-of-Concept)

Interactive 3D visualizations demonstrating how Lean proofs translate to computational models:

- **Nucleus Koopman**: Spectral decomposition of dynamical systems
- **SKY Multiway**: Causal invariant graph structures

## Links

- [Full Documentation](/llms-full.txt): Extended technical details
- [Research Page](/research): Complete project listings
- [Academic Papers](/research#papers): Published research

## Contact

For research inquiries or collaboration: https://www.apoth3osis.io