Pith. sign in
module module high

IndisputableMonolith.Gravity.BlackHoleEntropyFromLedger

show as:
view Lean formalization →

The module establishes the leading-order black-hole entropy in Recognition Science as S_lead(A) = A/4. Researchers deriving black-hole thermodynamics from discrete ledger models would cite it as the base relation before combinatorial counts. The module structures its content as a sequence of definitions and direct equalities that import the RS time quantum and cost functions to reach the area-law form.

claimThe leading-order RS black-hole entropy satisfies $S_{\rm lead}(A) = A/4$ in RS-native units.

background

The module resides in the Gravity domain and imports the fundamental RS time quantum τ₀ = 1 tick from Constants together with cost definitions. It applies these to express entropy via the J-cost and phi-ladder structures already present in the Recognition Science framework. The local setting is the leading term of the black-hole entropy expansion before any orbit counting or information arguments are introduced.

proof idea

This is a definition module whose argument consists of direct equalities and positivity statements. It defines S_lead via the imported constants, proves S_lead_pos, then establishes S_lead_eq_BH by algebraic reduction to the standard area law.

why it matters in Recognition Science

The module supplies the entropy formula that feeds BlackHoleHorizonStates, which replaces the asserted relation with a combinatorial Q₃-orbit count, and BlackHoleInformationPreservation, which uses it for the page-curve and unitarity analysis. It fills the leading-order term required by Plan v5 Track E3.

scope and limits

used by (2)

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 (12)