Verified Koopman: SafEDMD Extension
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.
Verified Koopman: SafEDMD Extension • Lean 4 + Mathlib • Apoth3osis Labs
SafEDMD-Inspired Error Bounds
This project extends the Nucleus Bottleneck Autoencoder with SafEDMD-inspired residual-covariance error bounds, SDP Lyapunov controller synthesis, and a Platinum verification tier. Building on Strässer, Berberich & Allgöwer's data-driven control framework, we provide machine-checked guarantees that the nucleus bottleneck preserves energy bounds, Heyting lattice structure, and Gram matrix constraints throughout the Koopman pipeline.
- • 10 sorry-free Lean 4 modules with 41 theorems
- • SafEDMD energy bound:
Σ R(v)² ≤ Σ v² - • Heyting adjunction for both fixed and learned bounds
- • 4 corrections/extensions vs the original paper
Nucleus Bottleneck Autoencoder
This extension builds on the original NBA, which constrains Koopman autoencoder latent space to a Heyting-algebra-valued slice governed by nucleus maps. The verified-koopman repo adds SafEDMD-style error guarantees on top of those foundational proofs.
Strässer, Berberich & Allgöwer developed the SafEDMD framework for data-driven control with guaranteed error bounds. Our formalization extends their algebraic ingredients with nucleus-aware Heyting structure and machine-checked proofs.
Robin Strässer
Research Associate · Control Systems
Institute for Systems Theory and Automatic Control (IST), University of Stuttgart
Research associate at IST Stuttgart working on data-driven control methods for nonlinear systems. Lead author of the SafEDMD framework (Automatica 2027) which provides guaranteed error bounds for Extended Dynamic Mode Decomposition with noisy measurement data.
Julian Berberich
Researcher · Data-Driven Control
Institute for Systems Theory and Automatic Control (IST), University of Stuttgart
Researcher at IST Stuttgart specializing in data-driven control theory with rigorous guarantees. Co-author of the SafEDMD framework and fundamental data-driven representations for control.
Frank Allgöwer
Professor · Director of IST
Institute for Systems Theory and Automatic Control (IST), University of Stuttgart
Full professor and director of IST Stuttgart. One of the most-cited researchers in control theory worldwide. ERC Advanced Grant recipient (2016). Research spans nonlinear control, model predictive control, and systems biology.