`IndisputableMonolith.Relativity.Compact`

IndisputableMonolith/Relativity/Compact.lean · 12 lines · 0 declarations

Explainer status: ready · generated 2026-05-13 18:50:26.804285+00:00

   1-- Compact Objects Module Aggregator
   2import IndisputableMonolith.Relativity.Compact.StaticSpherical
   3import IndisputableMonolith.Relativity.Compact.BlackHoleEntropy
   4
   5/-!
   6# Compact Objects Module
   7
   8Static spherically symmetric solutions and entropy:
   9- `StaticSpherical` - Static spherical solutions ds² = -f(r)dt² + g(r)dr² + r²dΩ²
  10- `BlackHoleEntropy` - Bekenstein-Hawking entropy derived from ledger capacity
  11-/
  12

source mirrored from github.com/jonwashburn/shape-of-logic