Lean 4 formalization of distance, smoothness, and proximity gaps for expander codes. Companion to On Proximity Gaps for Expander Codes (ePrint 2026/2806).
Start with the main theorems. Paper statements include the Ligero test, sampling constraints, and an additional hybrid sampling corollary.
- Statements: definitions and verifier contracts.
- Paper lemmas and helpers: supporting proofs.
- Review entry point: declaration index.
With elan installed:
lake exe cache get
lake build LDPC LDPC.Statements.ReviewThe toolchain and dependencies are pinned in the repository.