{"id":"palomar/PALOMAR-2026-09-02-000007","url":"https://github.com/Arthur742Ramos/lean-poincare-formalization-plan/tree/80b71f3a239ac2b294c91c66d020476f667a1306/curvature","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-02-000007-v3.json","repo":"https://github.com/Arthur742Ramos/lean-poincare-formalization-plan","tags":["math.DG","math.LO","msc:53C21","msc:53C25","msc:03B35","riemannian-geometry","curvature","lean","levi-civita"],"score":0,"title":"Levi–Civita connections and metric-determined curvature invariants in Lean","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 a coherent static Riemannian theorem family for smooth finite-dimensional manifolds: existence of a global C^1 Levi–Civita covariant derivative, independence of the bundled curvature tensor from the chosen Levi–Civita realization, symmetry of the Ricci contraction, and independence of both Ricci and scalar curvature from that realization. These are standard classical results assembled at the current Mathlib manifold/vector-bundle API boundary. The contribution claimed here is a kernel-checked Lean formalization of the theorem family and its bundled constructions, not a new…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-03","reactions":{},"formalized":true,"formalizes":[{"title":"Foundations of Differential Geometry, Vol. I","identifier":"https://books.google.com/books/about/Foundations_of_Differential_Geometry_Vol.html?id=ss7bEAAAQBAJ","relationship":"formalizes"}]}