A Lean 4 library for geometric analysis.
lake exe cache get
lake build
Requires Mathlib at the SHA pinned in lake-manifest.json.
Pre-v0.1.0, experimental. PRE-PAPER sorry'd statements and narrow structural axioms are tracked with explicit repair plans in module docstrings (search for **Sorry status**: / axiom).
The library is designed for downstream research consumption, teaching use, and Mathlib upstream candidacy. Issues and PRs welcome.