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)

  68noncomputable def pageTime : ℝ := 1 / 2

proof body

Definition body.

  69
  70/-- The entanglement entropy of the radiation (the Page curve).
  71
  72    Before Page time (f < 1/2):
  73      S_rad = S_0 × f  (grows linearly)
  74
  75    After Page time (f > 1/2):
  76      S_rad = S_0 × (1 - f)  (decreases linearly)
  77
  78    This forms the "Page curve" - a tent-shaped function. -/

used by (12)

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
pageTime 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

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
entropy in IndisputableMonolith.Foundation.InitialCondition decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
Before in IndisputableMonolith.Foundation.PreTemporalForcingOrder decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
pageTime in IndisputableMonolith.Gravity.BlackHoleInformationPreservation decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
entropy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
entropy in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use