Semantic Closure Genesis Model
Watch a mathematical proof come alive. This visualization is driven by data exported directly from verified Lean 4 theorems—the numbers you see are certified by the proof assistant, not hand-tuned by artists.
Lean-driven scene
Narrative
Semantic Closure
Proof snapshot (offline)
Fixed-point convergence visualization. Drag to rotate.
phases
3
selectors
1 -> 2 -> 0
What You're Seeing
The three glowing nodes represent the components of Rosen's (M,R)-system: metabolism (produces components), repair (rebuilds machinery), and the environment(provides resources). The system must "close" into a self-sustaining loop.
The Mathematical Core
The key theorem is closeSelector.idem: applying the closure operator twice gives the same result as applying it once. This proves self-repair doesn't lead to infinite regress.
Proof Artifacts
VerifiedKoopman Lean modulesOriginal Work
Lopez-Diaz & Gershenson: Closing the LoopDeep Dive
Full research project pageThe Nucleus Transformations
The visualization animates two key operations from the Lean proofs. These aren't arbitrary—they're the mathematical "gates" that allow self-reference to stabilize into closure.
ReLU Nucleus
Like a neural network's rectified linear unit: negative values become zero, positive values pass through. The theorem reluNucleus_idempotent proves applying ReLU twice equals applying it once.
Threshold Nucleus
Clamps values to a boundary: if below threshold, snap to threshold. The theorem thresholdNucleus_fixed_iff proves exactly when a point is stable.
output [-0.1, 0.5, 0.9]
Why This Matters
For Biology
This is a mathematical model of how life maintains itself. Every cell must continuously rebuild its own machinery while using that machinery—the closure operator shows this isn't paradoxical.
For AI
Self-improving systems face the same challenge: how do you modify the system that's doing the modifying? Closure operators provide a rigorous foundation for stable self-reference.
For Verification
This demonstrates a new paradigm: using proof assistants not just to verify code, but to generate visualizations guaranteed to be mathematically accurate.

Lean-driven visualization
Captured from the proof-parametrized WebGL scene showing closure convergence.
Concept reference
The (M,R)-system triangle: metabolism, repair, and environment in closed loop.
This model runs entirely in your browser using WebGL. The proof data is loaded from JSON files exported by the Lean build process. For the full interactive experience with sound design, contact rgoodman@apoth3osis.io.
