 109
 110    For the fixed-point condition (demand = bandwidth), this confirms
 111    the BH is at the saturation boundary. -/
 112noncomputable def saturationRatio (M : ℝ) : ℝ :=
 113  horizonDemand M / horizonBandwidth M
 114
 115/-- The saturation ratio scales as 1/M², so larger BHs are "deeper" in saturation.
 116    Any BH with M > 0 is saturated at its horizon. -/
 117theorem saturationRatio_pos {M : ℝ} (hM : 0 < M) : 0 < saturationRatio M := by
 118  unfold saturationRatio
 119  exact div_pos
 120    (by rw [horizonDemand_eq hM]; exact div_pos one_pos (mul_pos (by linarith) Real.pi_pos))
 121    (horizonBandwidth_pos hM)
 122
 123/-! ## §5. Hawking Temperature from Bandwidth -/
 124
 125/-- Hawking temperature: T_H = 1/(8πM).
 126
 127    The factor 8π = 8 × π where:
 128    - 8 is the tick count per recognition cycle
 129    - π is the geometric factor from the horizon
 130
 131    In the bandwidth picture: T_H is the recognition "clock rate" of the horizon,
 132    set by the 8-tick cadence divided by the horizon's geometric scale. -/
 133noncomputable def hawkingTemp (M : ℝ) : ℝ := 1 / (8 * Real.pi * M)
 134
 135theorem hawkingTemp_pos {M : ℝ} (hM : 0 < M) : 0 < hawkingTemp M := by
 136  unfold hawkingTemp
 137  exact div_pos one_pos (mul_pos (mul_pos (by norm_num : (0:ℝ) < 8) Real.pi_pos) hM)
 138
 139/-- Hawking temperature is inversely proportional to mass. -/
 140theorem hawkingTemp_inv_mass {M₁ M₂ : ℝ} (h₁ : 0 < M₁) (h₂ : 0 < M₂)
 141    (hM : M₁ < M₂) : hawkingTemp M₂ < hawkingTemp M₁ := by
 142  unfold hawkingTemp

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.