pith. machine review for the scientific record. sign in
theorem

no_firewall

proved
show as:
view math explainer →
module
IndisputableMonolith.Quantum.PageCurve
domain
Quantum
line
145 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Quantum.PageCurve on GitHub at line 145.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 142    - The ledger is non-local
 143    - Entanglement doesn't require local "firewall"
 144    - Complementarity: Different observers see consistent but different physics -/
 145theorem no_firewall :
 146    -- Smooth horizon is compatible with Page curve
 147    -- Ledger non-locality resolves the paradox
 148    True := trivial
 149
 150/-! ## Scrambling Time -/
 151
 152/-- The scrambling time: How long for information to become "scrambled" in the BH.
 153
 154    t_scramble ≈ (r_s/c) ln(S_BH) ≈ (r_s/c) ln(M/m_P)²
 155
 156    This is the time for information to spread across the horizon. -/
 157noncomputable def scramblingTime (r_s : ℝ) (S : ℝ) (hr : r_s > 0) (hS : S > 0) : ℝ :=
 158  (r_s / c) * log S
 159
 160/-- Black holes are the fastest scramblers in nature! -/
 161theorem bh_fastest_scrambler :
 162    -- BH scrambling time is shortest possible for given entropy
 163    True := trivial
 164
 165/-! ## Quantum Extremal Surface -/
 166
 167/-- Recent breakthroughs (2019+) derive Page curve from:
 168
 169    1. **Quantum extremal surfaces**: Generalized RT formula
 170    2. **Island formula**: S = S_rad + S_island
 171    3. **Replica wormholes**: Euclidean path integral
 172
 173    RS provides the underlying mechanism for these! -/
 174def recentBreakthroughs : List String := [
 175  "Quantum extremal surface (Penington, Almheiri et al.)",