Registry · Proposition V.P102 tau-effective formalized

V.P102 — Defect entropy converges to zero

Defect entropy converges as n -> infinity: lim S_def(n) = S_def^BH >= 0, the irreducible defect entropy from black hole excisions. If all BHs have merged into a single excision (by the Merger Normal Form), S_def^BH is the entropy of that final excision.

Book V Part 6 Ch. 55

Dependency Graph

Depends on (3)

Depended on by (1)

Lean Formalization

Module: TauLib.BookV.Cosmology.CosmologicalEndstate

Symbol: Tau.BookV.Cosmology.DefectEntropyConvergesToZero