hawkingTemp

formal source

 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
 143  have h8pi : 0 < 8 * Real.pi := mul_pos (by norm_num) Real.pi_pos
 144  rw [div_lt_div_iff₀
 145    (mul_pos h8pi h₂) (mul_pos h8pi h₁)]
 146  nlinarith
 147
 148/-- **THEOREM**: The 8 in 8πM is the recognition cadence.
 149
 150    T_H = 1/(8πM) = 1/((8τ₀)·π·M) where 8τ₀ is the eight-tick cadence
 151    and πM is the geometric scale of the horizon.
 152
 153    This connects Hawking radiation directly to the 8-tick structure. -/
 154theorem hawking_contains_eight_tick {M : ℝ} (hM : 0 < M) :
 155    hawkingTemp M = 1 / (eightTickCadence * Real.pi * M) := by
 156  unfold hawkingTemp eightTickCadence τ₀ tick
 157  ring
 158
 159/-! ## §6. No-Hair from Full Saturation -/
 160
 161/-- **THEOREM**: Full bandwidth saturation leaves no recognition capacity
 162    for additional structure.
 163