A Lean 4 formalization of discrete causal posets and convex-cone models for AQEI constraints. Features 130+ machine-checked theorems covering chain-complex homology proxies, $Z_1$ cycle space stability, and bidirectional equivalence of 1-cycle proxies.
formal-verification convex-optimization interactive-theorem-proving discrete-geometry homology order-theory lean4 mathlib4 causal-posets quantum-energy-inequalities
-
Updated
Feb 27, 2026 - Lean