Open Research Index

BrandonMYates/schwarzschild-comparator

Brandon Yates

Palomar Registrypalomar/PALOMAR-2026-08-27-000020Aug 27, 2026gr-qcscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-27-000020
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000020/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000020/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'