CAB Certified Visual Models
These scenes are not concept art—they are programs parameterized by Lean 4 proofs. Each pipeline starts with a CAB-certified theorem, feeds the verified invariants into a GPU-friendly runtime, and produces a computational model that viewers can feel. Proof → executable → visceral experience.
- Lean 4 proofs export the nucleus/causality invariants as JSON.
- Web runtime imports those certificates and animates them deterministically.
- Every shader parameter is tagged with the theorem or Git commit that produced it.
Semantic Closure Genesis
Auto-playing visualization of the (M,R)-system proving how admissible selectors form a self-sustaining closure loop. Driven directly by the Lean nuclei proofs.
Causal Confluence Multiway
Living multiway hypergraph that shows how confluence and causal invariance separate in the Wolfram model counterexamples formalized in Lean.
The Koopman Lens
A dynamical system flows through a proof-carrying Koopman autoencoder. The nucleus bottleneck constrains latent activations to [0,1] while preserving Heyting algebra structure.
SKY Multiway Tree
Watch computation branch into a multiway tree. Every reduction path is explored, and topos-theoretic gluing identifies equivalent outcomes. The Y combinator spirals infinitely.
1. CAB Proofs
Lean 4 modules (e.g., NucleusReLU.lean) emit machine-checked invariants.
2. Runtime Translation
We serialize theorems into shader-friendly blobs and annotate every parameter with its theorem origin.
Example: β domain bounds → camera easing curve.
3. Visual Experience
Auto-playing scenes render the fixed points, multiway branches, and causal overlays precisely as certified.
Coming soon: downloadable WebAssembly builds.
Interested in embedding these models or collaborating on new proof-driven visuals? Reach out at rgoodman@apoth3osis.io with the Lean module you want visualized.