pith. sign in
module module high

IndisputableMonolith.Relativity.Compact.BlackHoleEntropy

show as:
view Lean formalization →

The BlackHoleEntropy module defines the event horizon area for Schwarzschild black holes and links it to ledger capacity for entropy calculations in Recognition Science. It supplies the geometric objects required for compact object analysis. Researchers modeling black hole thermodynamics within the RS framework would cite these definitions. The module consists of definitions together with short positivity lemmas.

claimHorizon area $A_h = 4π r_s^2$ for Schwarzschild radius $r_s$, with black hole entropy $S_{BH}$ obtained via ledger capacity limit.

background

This module belongs to the Relativity.Compact section, which treats static spherically symmetric solutions of the form ds² = -f(r)dt² + g(r)dr² + r²dΩ² and derives Bekenstein-Hawking entropy from ledger capacity. It imports the RS time quantum τ₀ = 1 tick from Constants and metric constructions from Geometry.Metric. The central object is HorizonArea, defined as the area of the event horizon for a Schwarzschild black hole.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The declarations feed the BlackHoleEntropy component of the parent Relativity.Compact module. They realize the derivation of Bekenstein-Hawking entropy from ledger capacity as stated in the Compact module documentation. The module advances the compact objects development inside the RS framework.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)