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.
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.