{"id":"palomar/PALOMAR-2026-09-08-000006","url":"https://github.com/Arthur742Ramos/lean-poincare-formalization-plan/tree/5db025e6d20d8aad714c3d116714545d1823fd8e/lichnerowicz-obata","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-08-000006-v1.json","repo":"https://github.com/Arthur742Ramos/lean-poincare-formalization-plan","tags":["math.DG","math.SP","math.LO","msc:53C21","msc:58J50","msc:03B35","riemannian-geometry","spectral-geometry","lean","eigenvalues"],"score":0,"title":"Lichnerowicz--Obata first eigenvalue and round-sphere rigidity","trust":"high","domain":"math.DG","source":"palomar","authors":["Arthur Freitas Ramos"],"reviews":0,"subject":"math.DG","summary":"Formalizes attainment of the first positive smooth Laplace eigenvalue on closed connected smooth Riemannian manifolds of dimension n >= 2, its sharp lower bound n*K under Ric >= (n-1)*K with K > 0, and equality if and only if the manifold is smoothly Riemannian-isometric to the round sphere of radius 1/sqrt K. The independent statement constructs the metric-compatible torsion-free connection and explicitly defines Ricci curvature, the Riesz gradient, the div-grad Laplacian, eigenvalue minimality, and the radius-scaled induced round metric.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-08","reactions":{},"formalized":true,"formalizes":[{"title":"Géométrie des groupes de transformations","identifier":"oclc:1212521","relationship":"formalizes"},{"title":"Certain conditions for a Riemannian manifold to be isometric with a sphere","identifier":"10.2969/jmsj/01430333","relationship":"formalizes"}]}