def
definition
scramblingTime
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Quantum.PageCurve on GitHub at line 157.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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.)",
176 "Island formula",
177 "Replica wormholes (Penington, Shenker, Stanford, Yang)",
178 "Holographic entanglement entropy"
179]
180
181/-! ## RS Predictions -/
182
183/-- RS predictions for black hole evaporation:
184
185 1. **Page curve is exact**: Not just approximate
186 2. **Scrambling follows τ₀**: Discrete time steps
187 3. **φ-ladder energies**: Hawking spectrum has φ-structure