Verified Data-Driven Controller Synthesis
Machine-checked Lean 4 formalization extending Strässer, Berberich & Allgöwer (arXiv 2402.03145) with nucleus-bottleneck Koopman autoencoder error bounds, Heyting algebra structure, and SDP Lyapunov controller synthesis.
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.
SafEDMD Koopman • Lean 4 + Mathlib • Apoth3osis Labs
| Paper Section | Status | Lean Module |
|---|---|---|
| 2.1 Koopman Operator Theory | PROVED | KoopmanAlgebra |
| 2.2 EDMD Dictionary | PROVED | NucleusReLU, NucleusThreshold |
| 3.1 SafEDMD Error Bounds (Thm 3.1) | EXTENDED | SafEDMD |
| 3.2 Active Dictionary Restriction | PROVED | SafEDMD (projectedGramDiag_le) |
| 4 Controller Synthesis (LMI) | SIMPLIFIED | StableGenerator |
| — Heyting Lattice Structure | ORIGINAL | HeytingOps, ParametricHeyting |
| — Semantic Closure | ORIGINAL | SemanticClosure/MR/* |
SafEDMD Energy Bound
The ReLU nucleus cannot increase the finite-dimensional energy. This is the key algebraic ingredient for SafEDMD error envelopes.
Heyting Adjunction
The defining law of Heyting algebras. Proved for both fixed bounds [0, top]ⁿ and learned parametric bounds [lo, hi]ⁿ.
Gram Diagonal Bound
Projected Gram diagonal entries are bounded by unprojected ones. Critical for SafEDMD active dictionary restriction.
Non-Boolean Witness
Double negation does not recover the original for interior points. This witnesses that the latent lattice is genuinely Heyting, not Boolean.
Our formalization is SafEDMD-inspired, not a direct transcription. Key differences:
Bound formula
Scalar proportional bound (Theorem 3.1): ‖error‖ ≤ c̃ₓ ‖Φ(x) − Φ(0)‖ + c̃ᵤ ‖u‖
Residual-covariance PSD envelope E = (G + λI)⁻¹ R (G + λI)⁻¹ — SafEDMD-inspired but not direct transcription
LMI controller synthesis
6×6 block LMI for bilinear control-affine systems (equation 17)
Simplified 2×2 Schur complement for autonomous systems
Active dictionary restriction
Not discussed in the paper
Original contribution — masking out latent dimensions killed by the ReLU nucleus for honest NBA-vs-baseline comparisons
Heyting algebra structure
No lattice-theoretic content in the paper
Entirely original Apoth3osis work — bounded Heyting operations with adjunction proofs
Layer 1 (Mathlib): Mathlib.Order.Nucleus Mathlib.Data.Real.Basic
│ │
Layer 2 (Nucleus): NucleusReLU NucleusThreshold
│ │
Layer 3 (Lattice): HeytingOps ParametricHeyting
│
Layer 4 (Closure): SC.Basic → SC.ClosureOp → SC.InverseEval
│
Layer 5 (SafEDMD): SafEDMD (imports NucleusReLU)
│
Layer 6 (Dynamics): StableGenerator KoopmanAlgebra10 modules · 21 theorems · 12 definitions · 1092 lines · 0 sorry
10 C files transpiled from Lean 4 via LambdaIR → MiniC → C. Each file carries provenance headers and theorem-preservation comments. Compile-verified with gcc -std=c11 -Wall -Wextra -Werror.
Rust crate verified-koopman-proofs with 8 modules and 17 tests. All tests pass, zero warnings. Memory-safe by construction.