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
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.
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.