{"id":"palomar/PALOMAR-2026-08-27-000020","url":"https://github.com/BrandonMYates/schwarzschild-comparator/tree/d8b6acf8263d4924356ac8abb62668c137ab61cd","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000020-v1.json","repo":"https://github.com/BrandonMYates/schwarzschild-comparator","tags":["gr-qc","math.DG","cs.LO","msc:83C15","msc:83C05","msc:83C22","msc:83F05","msc:53B30","msc:68V20","general-relativity"],"score":0,"title":"BrandonMYates/schwarzschild-comparator","trust":"high","domain":"gr-qc","source":"palomar","authors":["Brandon Yates"],"reviews":0,"subject":"gr-qc","summary":"Twenty-one theorems and thirty-three definitions, machine-checked in Lean 4 against Mathlib v4.32.0: the Schwarzschild, Schwarzschild-de Sitter (Kottler), Reissner-Nordstrom (with the Maxwell stress tensor defined and G = 8 pi T proved in all sixteen components), ingoing Vaidya (null dust of rank at most one, rank one wherever dm/dv ≠ 0, for a merely once-differentiable mass function), spatially flat FLRW (both Friedmann equations in Einstein-tensor form), static de Sitter, Minkowski-in-spherical and Kiselev metrics, together with Birkhoff uniqueness in the areal static gauge and the n != 2…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true}