{"id":"palomar/PALOMAR-2026-09-06-000004","url":"https://github.com/Arthur742Ramos/lean-poincare-formalization-plan/tree/90d215d81d30a5f67922dce00dfa160b4878e1c5/contracted-bianchi","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-06-000004-v1.json","repo":"https://github.com/Arthur742Ramos/lean-poincare-formalization-plan","tags":["math.DG","gr-qc","math.LO","msc:53B20","msc:53C21","msc:03B35","differential-geometry","riemannian-curvature","formal-proof"],"score":0,"title":"Double-contracted second Bianchi identity for metric-compatible torsion-free connections","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":"Proves the orthonormal double contraction of the actual corrected curvature derivative of a tangent connection on a smooth finite-dimensional real manifold. The Challenge exposes the corrected commutator and the smooth tangent-vector extensions explicitly; the Solution proves the identity for every supplied extension satisfying the stated hypotheses. The derivative symmetries and cyclic Bianchi equations are derived from torsion-freeness and metric compatibility, not assumed as abstract tensor data. No separate Einstein-divergence theorem is selected.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-06","reactions":{},"formalized":true,"formalizes":[{"title":"Lecture Notes on General Relativity","identifier":"https://ned.ipac.caltech.edu/level5/March01/Carroll3/Carroll3.html","relationship":"adapts"}]}