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.
Nucleus Bottleneck Autoencoder • Lean 4 + Mathlib • Apoth3osis Labs
Proof-Carrying Koopman Autoencoder
The nucleus-bottleneck autoencoder constrains the latent representation of a Koopman model to a Heyting-algebra-valued slice (0 ≤ latent ≤ 1) governed by nucleus maps. The repo ships a minimal training harness plus Lean certificates showing that the ReLU/threshold bottlenecks form legal nuclei and preserve bounded Heyting structure throughout the contraction-expansion pipeline.
- • Formal proofs live in
lean/VerifiedKoopmanand build withlake build. - • Python scripts (`train_nba.py`, `analyze_heyting.py`) demonstrate training + Heyting compliance on toy systems.
- • Reproduction docs outline the publication-grade pipeline for checkpoints + Lean artifacts.
Nucleus axioms
Files NucleusReLU.lean and NucleusThreshold.lean certify that clipped activations respect adjunction, monotonicity, and idempotence—exactly the nucleus properties required for Heyting closure.
Parametric Heyting operators
HeytingOps.lean and ParametricHeyting.lean prove the residuation laws (`himp_adjoint`) for both bounded vectors and parameterized boxes, ensuring the latent lattice behaves as expected during Koopman evolution.
Quick-start commands (CPU friendly) for the nucleus-bottleneck trainer and Heyting analysis:
python scripts/train_nba.py --system toy2d --model nba --epochs 50 --device cpu python scripts/analyze_heyting.py --system toy2d --checkpoint outputs/toy2d_nba/best.pt
Checkpoints land in outputs/<system>_<model>_*/best.pt.
- 1. Train Koopman autoencoder (NBA or end-to-end) on synthetic dynamical systems.
- 2. Use the Lean-backed Heyting analyzer to certify latent trajectories stay within the proven nucleus.
- 3. Package checkpoints + proofs for publication or reproducibility bundles.
SafEDMD Extension
The verified-koopman repository extends this foundational work with SafEDMD-inspired error bounds, SDP controller synthesis, and a Platinum verification tier, building on Strässer et al. (arXiv 2402.03145).
This is original Apoth3osis Labs research. The nucleus-bottleneck autoencoder synthesizes two classical mathematical foundations into a novel proof-carrying neural architecture.
Bernard O. Koopman
Mathematician · Operator Theory
Columbia University (1903–1981)
Introduced the Koopman operator (1931), which lifts nonlinear dynamical systems into an infinite-dimensional linear space. This operator-theoretic approach enables spectral analysis of nonlinear dynamics and is the mathematical foundation for data-driven Koopman autoencoders.
Arend Heyting
Mathematician · Intuitionistic Logic
University of Amsterdam (1898–1980)
Formalized Brouwer’s intuitionism into what are now called Heyting algebras (1930)—bounded distributive lattices with a residuated implication operator. The nucleus maps that constrain our autoencoder’s latent space are closure operators on Heyting algebras, ensuring the bottleneck preserves logical structure.
GitHub Repository
Full source (Lean + Python) plus release scripts.
Reproduction Docs
Step-by-step instructions for rebuilding the experiments.
Lean Proofs
Build locally with lake build or bash scripts/verify_lean.sh.