def definition def or abbrev

`pageTime`

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

formal statement (Lean)

 188def pageTime (M₀ α : ℝ) : ℝ := M₀ / (2 * α)

Definition body.

From the project-wide theorem graph. These declarations reference this one in their body.

BlackHoleInformationCert in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
black_hole_information_one_statement in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
entropy_bound_by_initial_BH_half in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
page_time_at_half_evap in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
pageTime_eq_half_t_evap in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
pageTime_pos in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
S_BH_anti in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
S_R_at_page_eq_page_entropy in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
S_R_at_page_eq_S_BH in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
S_thermal_at_page in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
pageEntropy in IndisputableMonolith.Quantum.PageCurve decl_use
pageTime in IndisputableMonolith.Quantum.PageCurve decl_use

Lean names referenced from this declaration's body.