theorem
proved
tactic proof
temp_halves_on_double
show as:
view Lean formalization →
formal statement (Lean)
180theorem temp_halves_on_double (bh₁ bh₂ : RSBH)
181 (h : bh₂.mass = 2 * bh₁.mass) :
182 rs_hawkingTemp bh₂ = rs_hawkingTemp bh₁ / 2 := by
proof body
Tactic-mode proof.
183 unfold rs_hawkingTemp
184 rw [h]
185 have hM : bh₁.mass > 0 := bh₁.mass_pos
186 have hpi : Real.pi > 0 := Real.pi_pos
187 have hdenom : 8 * Real.pi * bh₁.mass ≠ 0 := by positivity
188 field_simp [hdenom]
189
190/-! ## Theorem 4: Hamiltonian Approximation Bound -/
191
192/-- The Hamiltonian Ĥ emerges from the recognition operator R̂ only in the
193 small-strain regime. For strain ε with |ε| ≤ 1/2:
194
195 J(1 + ε) = ε²/2 + c·ε³ where |c| ≤ 2
196
197 The ε²/2 term gives the quadratic Hamiltonian. The cubic correction
198 is the R̂-specific term that standard physics misses. Near an
199 ultramassive BH's accretion disk, ε is NOT small, so the Eddington
200 limit (derived from the Hamiltonian approximation) underestimates
201 the dynamics that R̂ permits. -/