pith. machine review for the scientific record. sign in
def definition def or abbrev high

scramblingTime

show as:
view Lean formalization →

The scrambling time is the horizon light-crossing time multiplied by the natural logarithm of black-hole entropy, giving the interval over which information spreads across the event horizon. Physicists modeling black-hole evaporation and the information paradox cite this timescale when locating the turnover of the Page curve. The definition is a direct algebraic expression that multiplies r_s/c by log S under the stated positivity hypotheses.

claimFor Schwarzschild radius $r_s > 0$ and entropy $S > 0$, the scrambling time is $t_mathrm{scramble} = (r_s/c) ln S$.

background

The module QG-004 derives the Page curve for black-hole evaporation from Recognition Science ledger conservation, treating entanglement as shared ledger entries so that radiation entropy first rises then falls. The upstream result S supplies the full ILG action as the sum of the Einstein-Hilbert term and the psi-sector action, providing the gravitational setting in which the scrambling timescale appears. The definition therefore sits inside the ledger-dynamics account of information preservation during evaporation.

proof idea

The definition is a direct one-line algebraic expression (r_s / c) * log S that implements the standard logarithmic dependence of scrambling time on entropy.

why it matters in Recognition Science

This definition supplies the explicit scrambling timescale required by the Page-curve construction in the ledger-dynamics framework. It supports the module target of showing that information is redistributed rather than lost, consistent with the claim that black holes are the fastest scramblers. No downstream uses are recorded yet, leaving its insertion into pageTime or page_entropy_max_at_half as an open wiring step.

scope and limits

formal statement (Lean)

 157noncomputable def scramblingTime (r_s : ℝ) (S : ℝ) (hr : r_s > 0) (hS : S > 0) : ℝ :=

proof body

Definition body.

 158  (r_s / c) * log S
 159
 160/-- Black holes are the fastest scramblers in nature! -/

depends on (1)

Lean names referenced from this declaration's body.