{"id":"palomar/PALOMAR-2026-09-11-000001","url":"https://github.com/Arthur742Ramos/lean-poincare-formalization-plan/tree/0cc7c31bf6e2dac5c0359a432f3d99803f563017/bonnet-myers","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-11-000001-v1.json","repo":"https://github.com/Arthur742Ramos/lean-poincare-formalization-plan","tags":["math.DG","math.LO","msc:53C20","msc:53C21","msc:03B35","riemannian-geometry","formal-verification","lean"],"score":0,"title":"Independent Bonnet--Myers diameter and compactness theorem","trust":"high","domain":"math.DG","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.DG","summary":"Formalizes the classical Bonnet--Myers theorem for complete connected smooth boundaryless finite-dimensional real Riemannian manifolds. From dimension n >= 2, K > 0, and the pointwise lower bound Ric(a,a) >= (n-1) K g(a,a), the selected theorem constructs the Levi--Civita connection and actual curvature, proves compactness, and gives the sharp induced extended-diameter bound pi/sqrt K. The development proves minimizing-geodesic, parallel-transport, second-variation, index-form, and metric-compactness bridges rather than assuming them.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-11","reactions":{},"formalized":true}