module module

`IndisputableMonolith.Quantum.PageCurve`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (17)

def k_B L42
structure EvolvingBlackHole L47
def remainingEntropy L57
def radiationEntropyNaive L61
def pageTime L68
def pageEntropy L79
theorem page_entropy_max_at_half L86
theorem page_entropy_final L92
theorem page_curve_from_ledger L105
structure LedgerEvolution L116
theorem information_preserved_by_page_curve L130
theorem no_firewall L145
def scramblingTime L157
theorem bh_fastest_scrambler L161
def recentBreakthroughs L174
def predictions L189
structure PageCurveFalsifier L202