The Koopman Lens
Watch a dynamical system flow through a proof-carrying Koopman autoencoder. The nucleus bottleneck constrains the latent representation to a Heyting-algebra-valued slice, guaranteeing that every activation respects the algebraic structure verified in Lean.
3D Dynamics View
Auto-rotating
Architecture Flow
Lean 4 Verified
A damped spiral in state space - the original dynamical system we want to model. This could be any physical process: fluid flow, neural activity, market dynamics.
The neural network encoder compresses the state into a lower-dimensional latent representation. The funnel shape shows dimensionality reduction.
The glowing cube is the nucleus-constrained region. ReLU and threshold nuclei clamp activations to stay within [0,1], preserving Heyting algebra structure.
In the latent space, dynamics become linear. The rotating grid shows the Koopman operator - a simple matrix that predicts future states.
The decoder expands the latent representation back to state space, reconstructing a prediction of the original trajectory.
The reconstructed trajectory. Ideally it overlays the input perfectly - the gap shows reconstruction error from the nucleus constraint.
Why This Matters
Standard autoencoders have no guarantees about their latent space. Values can explode, collapse, or violate mathematical invariants. The nucleus bottleneck provides a machine-checked guarantee: every activation is provably clamped to [0,1] in a way that preserves Heyting algebra structure.
This isn't just regularization - it's algebraic certification. The Lean proofs establish that ReLU and threshold are nuclei: they are idempotent (applying twice changes nothing), inflationary (never decrease), and preserve meets (respecting logical conjunction in the algebra).