{"id":"palomar/PALOMAR-2026-10-09-000016","url":"https://github.com/JD-Jones-ASES/PlanarMidpoint/tree/148b39618710caf576189cbdb75551cec1735201","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-09-000016-v1.json","repo":"https://github.com/JD-Jones-ASES/PlanarMidpoint","tags":["math.DG","math.CA","msc:53B12","msc:39B22","differential-geometry","connections","midpoints","lean"],"score":0,"title":"Planar Euclidean midpoint rigidity","trust":"high","domain":"math.DG","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.DG","summary":"A complete Lean proof of the dimension-two case of Nielsen–Okamura Conjecture 9.1. On any connected open planar Euclidean domain, complementarity of the actual canonical local affine-parameter midpoints of a smooth pair of dual torsion-free connections forces the symmetric cubic tensor to be constant. The proof constructs and identifies the short geodesic germs and derives the fourth-order obstruction, including the exceptional rank-deficient tensors. A second theorem needs only everywhere Frechet differentiability and vanishing of that obstruction; five fixed direction tests at every point…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-09","reactions":{},"formalized":true,"formalizes":[{"title":"Planar Euclidean midpoint rigidity","identifier":"","relationship":"formalizes"},{"title":"Nielsen–Okamura, arXiv:2609.07551v2, Section 9","identifier":"","relationship":"adapts"}]}