Unique-Continuation-Planar
A Lean 4 formalization of every theorem, lemma and proposition of "Unique continuation on planar graphs" (Bou-Rabee, Cooperman and Ganguly): a harmonic function on a periodic plane graph with periodic conductances that is bounded by one on a set of density at least 1 - epsilon is constant (Theorem 1.1), together with the exponential upper bound (Theorem 1.2), the zero case (Theorem 1.3), the topological lemma, the exponential lower bound of the appendix with its polynomial approximation lemma and three-ball proposition, and non-planar periodic conductances on Z^2 with a harmonic function…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-27-000010
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-27-000010/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-27-000010/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'