pith. machine review for the scientific record. sign in
theorem proved term proof

hawkingTemp_inv_mass

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 140theorem hawkingTemp_inv_mass {M₁ M₂ : ℝ} (h₁ : 0 < M₁) (h₂ : 0 < M₂)
 141    (hM : M₁ < M₂) : hawkingTemp M₂ < hawkingTemp M₁ := by

proof body

Term-mode proof.

 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. -/

depends on (16)

Lean names referenced from this declaration's body.