theorem
proved
no_firewall
show as:
view math explainer →
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
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.)",