IndisputableMonolith.Gravity.HawkingTemperatureSI
IndisputableMonolith/Gravity/HawkingTemperatureSI.lean · 428 lines · 25 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Foundation.SIBridgeClosure
3import IndisputableMonolith.Gravity.HawkingTemperatureFromRung
4
5/-!
6# Gravity Track 3.A: Hawking Temperature in SI Units
7
8## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
9
10## What this module closes
11
12This module implements **Track 3.A of the quantum-gravity master plan**
13(`Quantum_Gravity_Discovery_Master_Plan_20260521.html`, §4 Track 3.A):
14the SI conversion of the Hawking temperature via the dimensional bridge
15discharged in `Foundation.SIBridgeClosure` (Track 5.A, CLOSED 2026-05-09).
16
17`Gravity.HawkingTemperatureFromRung` proves `T_H = 1/(8πM)` in
18RS-native (geometrized) units where `c = G = ℏ = k_B = 1`. With Track 5.A
19closed, the SI conversion is no longer a free calibration: the bridge
20factors `(a_T, a_L, a_M)` are uniquely determined by the c, ℏ, G constraints
21plus the SI-2019-exact value of `k_B`.
22
23## Master plan statement closed
24
25> 3.A Hawking temperature: SI unit-bridge upgrade
26>
27> `theorem hawking_temperature_SI :`
28> ` ∀ (M_SI : ℝ) (h_pos : 0 < M_SI),`
29> ` HawkingTemperature_SI M_SI = (ℏ_SI * c_SI³) / (8 * π * G_SI * k_B_SI * M_SI)`
30
31This module's `T_hawking_SI_def` is exactly this identity (after unfolding
32the definition, the master plan's statement holds by `rfl`).
33
34## Substantive content
35
36* `k_B_SI` — Boltzmann constant in SI, exact since SI 2019
37 (`k_B = 1.380649 × 10⁻²³ J/K`).
38
39* `T_hawking_SI M_SI = ℏ_SI · c_SI³ / (8π · G_SI · k_B_SI · M_SI)` — the
40 standard SI Hawking formula.
41
42* `T_hawking_SI_pos`, `T_hawking_SI_strict_anti` — positivity and strict
43 anti-monotonicity (lighter holes are hotter, in SI units).
44
45* `T_hawking_SI_eq_geom_via_bridge` — the bridge-derivation identity:
46 `T_hawking_SI(M_SI) = T_hawking(G_SI · M_SI / c_SI²) · (ℏ_SI · c_SI / k_B_SI)`.
47 The geometrized mass `G_SI · M_SI / c_SI²` is the standard
48 mass-to-length conversion in general relativity (Schwarzschild radius
49 prefactor); evaluating the RS-native `T_hawking` at this geometrized
50 mass yields an inverse length, and multiplication by the energy-to-
51 temperature factor `ℏ_SI · c_SI / k_B_SI` returns kelvin.
52
53* `hawkingTemperatureSICert` — master cert bundling the above.
54
55## Anti-retreat principle satisfied
56
57The SI prediction is anchored on:
58* `c_SI` — SI-2019 exact (defined).
59* `hbar_SI` — SI-2019 exact (defined).
60* `k_B_SI` — SI-2019 exact (defined).
61* `G_SI` — the SINGLE CODATA measurement that anchors the bridge
62 (via `Foundation.SIBridgeClosure`).
63
64No free dimensionless parameters; one dimensional anchor. This is the
65strongest form of "zero free dimensionless parameters, one dimensional
66anchor" declared in `Foundation.SIBridgeClosure`. No softening of the
67master-statement claim (`HawkingTemperature_SI = (ℏ·c³)/(8π·G·k_B·M)`)
68relative to its master-plan-stipulated form.
69
70## Falsifier (Hawking row of master plan §7)
71
72Any direct measurement of Hawking radiation from a primordial or
73laboratory black hole that yields a temperature inconsistent with the
74SI formula at the 10 % level. (No such measurement yet exists; the
75prediction is firmly inside the canonical Hawking band, and the
76sub-leading φ-rung correction tracked by `BlackHoleEntropyFromLedger`
77remains a Track 3.B item.)
78
79## Honest scope note
80
81This module is the **SI-unit bridge** for the Hawking temperature. It does
82NOT prove the existence or stability of Hawking radiation, nor does it
83derive the sub-leading entropy correction at one-loop. Those are Track 3.B
84(leading-log entropy correction at theorem grade) and Track 3.C (Page
85curve as derivation) items.
86
87The `8π` factor in the denominator inherits from the standard
88semiclassical derivation (Hartle-Hawking 1976); it is NOT forced by the
89RS forcing chain. The RS forcing chain forces the sub-leading
90`c_RS = -log φ / 2` correction at one-loop, encoded in
91`Gravity.BlackHoleEntropyFromLedger`; the first-law identity `dE = T dS`
92ties RS temperature to RS entropy. That tie is structural in
93`HawkingTemperatureFromRung`; the SI lift here just propagates it through
94the closed bridge.
95-/
96
97namespace IndisputableMonolith
98namespace Gravity
99namespace HawkingTemperatureSI
100
101open Constants
102open IndisputableMonolith.Foundation.SIBridgeClosure
103open IndisputableMonolith.Gravity.HawkingTemperatureFromRung
104
105noncomputable section
106
107/-! ## §1. Boltzmann constant in SI (exact since SI 2019)
108
109After the 2019 redefinition of the SI base units, `k_B` is exact:
110`k_B = 1.380649 × 10⁻²³ J/K`. Together with the SI-exact `c_SI`,
111`hbar_SI` from `Foundation.SIBridgeClosure`, and the CODATA `G_SI`, this
112completes the four constants needed to express the Hawking temperature
113in kelvin.
114-/
115
116/-- Boltzmann constant in SI: exact since SI 2019. -/
117def k_B_SI : ℝ := 1.380649e-23
118
119theorem k_B_SI_pos : 0 < k_B_SI := by
120 unfold k_B_SI; norm_num
121
122/-! ## §2. The SI Hawking temperature -/
123
124/-- Hawking temperature of a Schwarzschild black hole in SI units:
125`T_H = ℏ_SI · c_SI³ / (8π · G_SI · k_B_SI · M_SI)`. -/
126def T_hawking_SI (M_SI : ℝ) : ℝ :=
127 hbar_SI * c_SI ^ 3 / (8 * Real.pi * G_SI * k_B_SI * M_SI)
128
129theorem T_hawking_SI_def (M_SI : ℝ) :
130 T_hawking_SI M_SI = hbar_SI * c_SI ^ 3 /
131 (8 * Real.pi * G_SI * k_B_SI * M_SI) := rfl
132
133/-- The master plan statement, verbatim:
134`HawkingTemperature_SI M_SI = (ℏ_SI · c_SI³) / (8π · G_SI · k_B_SI · M_SI)`. -/
135theorem hawking_temperature_SI (M_SI : ℝ) (_h_pos : 0 < M_SI) :
136 T_hawking_SI M_SI =
137 hbar_SI * c_SI ^ 3 / (8 * Real.pi * G_SI * k_B_SI * M_SI) := rfl
138
139/-- Positivity: positive masses give positive Hawking temperatures. -/
140theorem T_hawking_SI_pos (M_SI : ℝ) (hM : 0 < M_SI) :
141 0 < T_hawking_SI M_SI := by
142 unfold T_hawking_SI
143 have h_num_pos : 0 < hbar_SI * c_SI ^ 3 :=
144 mul_pos hbar_SI_pos (pow_pos c_SI_pos 3)
145 have h8 : (0 : ℝ) < 8 := by norm_num
146 have h_den_pos : 0 < 8 * Real.pi * G_SI * k_B_SI * M_SI :=
147 mul_pos (mul_pos (mul_pos (mul_pos h8 Real.pi_pos) G_SI_pos) k_B_SI_pos) hM
148 exact div_pos h_num_pos h_den_pos
149
150/-- Strict anti-monotonicity in mass: lighter holes are hotter (SI form). -/
151theorem T_hawking_SI_strict_anti
152 (M1 M2 : ℝ) (h1 : 0 < M1) (_h2 : 0 < M2) (hlt : M1 < M2) :
153 T_hawking_SI M2 < T_hawking_SI M1 := by
154 unfold T_hawking_SI
155 have h_num_pos : 0 < hbar_SI * c_SI ^ 3 :=
156 mul_pos hbar_SI_pos (pow_pos c_SI_pos 3)
157 have h8 : (0 : ℝ) < 8 := by norm_num
158 have h_coeff_pos : 0 < 8 * Real.pi * G_SI * k_B_SI :=
159 mul_pos (mul_pos (mul_pos h8 Real.pi_pos) G_SI_pos) k_B_SI_pos
160 have h_den1_pos : 0 < 8 * Real.pi * G_SI * k_B_SI * M1 :=
161 mul_pos h_coeff_pos h1
162 have h_den_lt : 8 * Real.pi * G_SI * k_B_SI * M1 <
163 8 * Real.pi * G_SI * k_B_SI * M2 :=
164 mul_lt_mul_of_pos_left hlt h_coeff_pos
165 exact div_lt_div_of_pos_left h_num_pos h_den1_pos h_den_lt
166
167/-! ## §3. Connection to RS-native via the dimensional bridge
168
169The substantive bridge identity. The RS-native Hawking temperature
170(`HawkingTemperatureFromRung.T_hawking M = 1/(8π M)`) lives in
171geometrized units where `c = G = ℏ = k_B = 1`. The standard
172general-relativistic mass-to-length conversion is `M_geom = G_SI · M_SI / c_SI²`,
173and the energy-to-temperature conversion is `T_K = (1/m) · (ℏ · c / k_B)`.
174Composing these gives the SI Hawking formula above.
175-/
176
177/-- **Track 3.A core identity**: the SI Hawking temperature is the
178bridge-converted RS-native (geometrized) Hawking temperature, multiplied
179by the SI energy-to-temperature factor.
180
181`T_hawking_SI(M_SI) = T_hawking(G_SI · M_SI / c_SI²) · (ℏ_SI · c_SI / k_B_SI)`
182
183This is the formal Track 3.A theorem: the SI prediction is the lift of
184the RS-native theorem through the closed dimensional bridge. -/
185theorem T_hawking_SI_eq_geom_via_bridge (M_SI : ℝ) (hM : 0 < M_SI) :
186 T_hawking_SI M_SI =
187 T_hawking (G_SI * M_SI / c_SI ^ 2) * (hbar_SI * c_SI / k_B_SI) := by
188 unfold T_hawking_SI T_hawking
189 have hG : G_SI ≠ 0 := ne_of_gt G_SI_pos
190 have hM_ne : M_SI ≠ 0 := ne_of_gt hM
191 have hc : c_SI ≠ 0 := ne_of_gt c_SI_pos
192 have hpi : Real.pi ≠ 0 := Real.pi_pos.ne'
193 have hk : k_B_SI ≠ 0 := ne_of_gt k_B_SI_pos
194 field_simp
195
196/-- Symmetric form: the RS-native temperature recovered from the SI one
197by dividing by the energy-to-temperature factor. -/
198theorem T_hawking_geom_eq_SI_via_bridge (M_SI : ℝ) (hM : 0 < M_SI) :
199 T_hawking (G_SI * M_SI / c_SI ^ 2) =
200 T_hawking_SI M_SI * (k_B_SI / (hbar_SI * c_SI)) := by
201 have h := T_hawking_SI_eq_geom_via_bridge M_SI hM
202 have hbar_ne : hbar_SI ≠ 0 := ne_of_gt hbar_SI_pos
203 have hc : c_SI ≠ 0 := ne_of_gt c_SI_pos
204 have hk : k_B_SI ≠ 0 := ne_of_gt k_B_SI_pos
205 have hbar_c_ne : hbar_SI * c_SI ≠ 0 := mul_ne_zero hbar_ne hc
206 -- T_hawking · (ℏ·c/k_B) = T_SI ⇒ T_hawking = T_SI · k_B / (ℏ·c)
207 rw [h]
208 field_simp
209
210/-! ## §4. Schwarzschild radius in SI
211
212The Schwarzschild radius `r_s = 2 G M / c²` is the natural length scale
213companion to `T_hawking_SI`. In RS-native (geometrized) units this is
214just `r_s = 2 M`, and `T_hawking_of_radius (2 M) = T_hawking M`
215(`HawkingTemperatureFromRung.T_hawking_eq_radius_form`). The SI lift
216goes via the standard mass-to-length conversion `G_SI · M_SI / c_SI²`.
217-/
218
219/-- Schwarzschild radius in SI: `r_s(M_SI) = 2 G_SI · M_SI / c_SI²`. -/
220def schwarzschildRadius_SI (M_SI : ℝ) : ℝ :=
221 2 * G_SI * M_SI / c_SI ^ 2
222
223theorem schwarzschildRadius_SI_def (M_SI : ℝ) :
224 schwarzschildRadius_SI M_SI = 2 * G_SI * M_SI / c_SI ^ 2 := rfl
225
226theorem schwarzschildRadius_SI_pos (M_SI : ℝ) (hM : 0 < M_SI) :
227 0 < schwarzschildRadius_SI M_SI := by
228 unfold schwarzschildRadius_SI
229 have h2 : (0 : ℝ) < 2 := by norm_num
230 have hnum : 0 < 2 * G_SI * M_SI := mul_pos (mul_pos h2 G_SI_pos) hM
231 exact div_pos hnum (pow_pos c_SI_pos 2)
232
233/-- The SI Hawking temperature as a function of Schwarzschild radius:
234`T_hawking_SI_of_radius(r_s) = ℏ c² / (4π G k_B · r_s · M_planck_unit)`.
235Equivalently (Schwarzschild identification `r_s = 2M`):
236`T_hawking_SI M_SI = ℏc / (4π · k_B · schwarzschildRadius_SI M_SI)`.
237
238The derivation: starting from `T_hawking_SI M_SI = ℏc³/(8π·G·k_B·M_SI)`
239and `schwarzschildRadius_SI M_SI = 2·G·M_SI/c²`, eliminate `M_SI` to get
240`T_hawking_SI = ℏc/(4π·k_B·r_s)`. -/
241theorem T_hawking_SI_eq_inv_schwarzschildRadius (M_SI : ℝ) (hM : 0 < M_SI) :
242 T_hawking_SI M_SI = hbar_SI * c_SI /
243 (4 * Real.pi * k_B_SI * schwarzschildRadius_SI M_SI) := by
244 unfold T_hawking_SI schwarzschildRadius_SI
245 have hG : G_SI ≠ 0 := ne_of_gt G_SI_pos
246 have hM_ne : M_SI ≠ 0 := ne_of_gt hM
247 have hc : c_SI ≠ 0 := ne_of_gt c_SI_pos
248 have hpi : Real.pi ≠ 0 := Real.pi_pos.ne'
249 have hk : k_B_SI ≠ 0 := ne_of_gt k_B_SI_pos
250 field_simp
251 ring
252
253/-! ## §5. Page time (Hawking evaporation lifetime) in SI
254
255The Page time of a Schwarzschild black hole is the time at which half its
256mass has been radiated. Standard semiclassical Hawking evaporation
257`dM/dt = -ℏc⁴/(15360π G² M²)` integrates to dust as
258`t_Page = 5120π · G² · M³ / (ℏ · c⁴)`.
259
260In RS-native (fully geometrized) units, this collapses to
261`HawkingTemperatureFromRung.t_Page M = 5120π · M³` (the
262`M³` scaling preserved). The SI lift restores the explicit
263`G² / (ℏ · c⁴)` Planck-time-cubed scale.
264
265The Planck-time conversion factor is the cube of the Planck mass
266ratio: `t_Page_SI(M_SI) = (M_SI/M_Planck)³ · (5120π · t_Planck)` with
267`M_Planck = √(ℏc/G)` and `t_Planck = √(ℏG/c⁵)`. The squared identity is
268clean (no `Real.sqrt`); we ship the direct SI form and the explicit
269`M_SI³` scaling as the algebraic content of this section.
270
271The `5120π` semiclassical prefactor inherits from Page (1976), NOT from
272the RS forcing chain; this is consistent with the `8π` factor in the
273Hawking temperature noted earlier. The RS-forced piece is the cubic
274`M³` scaling itself (`dM/dt ∝ -1/M²` integrated to lifetime ∝ M³),
275which follows from the inverse-mass-squared Hawking flux ∝ T_H² · A
276together with `T_H ∝ 1/M` and `A ∝ M²` already proved in
277`HawkingTemperatureFromRung` and `BlackHoleEntropyFromLedger`.
278-/
279
280/-- Page time in SI: `t_Page_SI(M_SI) = 5120π · G_SI² · M_SI³ / (ℏ_SI · c_SI⁴)`. -/
281def t_Page_SI (M_SI : ℝ) : ℝ :=
282 5120 * Real.pi * G_SI ^ 2 * M_SI ^ 3 / (hbar_SI * c_SI ^ 4)
283
284theorem t_Page_SI_def (M_SI : ℝ) :
285 t_Page_SI M_SI = 5120 * Real.pi * G_SI ^ 2 * M_SI ^ 3 /
286 (hbar_SI * c_SI ^ 4) := rfl
287
288/-- The Page time prefactor: `K_Page = 5120π · G_SI² / (ℏ_SI · c_SI⁴)`.
289This is the constant of proportionality in the `M³` scaling. -/
290def K_Page_SI : ℝ :=
291 5120 * Real.pi * G_SI ^ 2 / (hbar_SI * c_SI ^ 4)
292
293theorem K_Page_SI_pos : 0 < K_Page_SI := by
294 unfold K_Page_SI
295 have hb_pow : 0 < hbar_SI * c_SI ^ 4 :=
296 mul_pos hbar_SI_pos (pow_pos c_SI_pos 4)
297 have h5120 : (0 : ℝ) < 5120 := by norm_num
298 have hnum : 0 < 5120 * Real.pi * G_SI ^ 2 :=
299 mul_pos (mul_pos h5120 Real.pi_pos) (pow_pos G_SI_pos 2)
300 exact div_pos hnum hb_pow
301
302/-- **The cubic Page-time scaling identity**:
303`t_Page_SI(M_SI) = K_Page_SI · M_SI³`. The `M³` scaling is the RS-forced
304content (from `dM/dt ∝ -1/M²` integration); `K_Page_SI` is the
305semiclassical prefactor lifted to SI through the dimensional bridge. -/
306theorem t_Page_SI_eq_K_mul_M_cube (M_SI : ℝ) :
307 t_Page_SI M_SI = K_Page_SI * M_SI ^ 3 := by
308 unfold t_Page_SI K_Page_SI
309 have hb : hbar_SI ≠ 0 := ne_of_gt hbar_SI_pos
310 have hc : c_SI ≠ 0 := ne_of_gt c_SI_pos
311 field_simp
312
313/-- Positivity: positive masses give positive Page times. -/
314theorem t_Page_SI_pos (M_SI : ℝ) (hM : 0 < M_SI) : 0 < t_Page_SI M_SI := by
315 rw [t_Page_SI_eq_K_mul_M_cube]
316 exact mul_pos K_Page_SI_pos (pow_pos hM 3)
317
318/-- Strict monotonicity: heavier holes evaporate slower. -/
319theorem t_Page_SI_strict_mono
320 (M1 M2 : ℝ) (h1 : 0 < M1) (_h2 : 0 < M2) (hlt : M1 < M2) :
321 t_Page_SI M1 < t_Page_SI M2 := by
322 rw [t_Page_SI_eq_K_mul_M_cube, t_Page_SI_eq_K_mul_M_cube]
323 have h_pow : M1 ^ 3 < M2 ^ 3 :=
324 pow_lt_pow_left₀ hlt h1.le (by decide : (3 : ℕ) ≠ 0)
325 exact mul_lt_mul_of_pos_left h_pow K_Page_SI_pos
326
327/-- **Bridge identity (squared form, no `Real.sqrt`)**: the squared
328Page-time-in-SI equals `(5120π)² · ℏG/c⁵ · M_SI⁶ · (G/(ℏc))³`. The
329factor `ℏG/c⁵` is the squared Planck time and `G/(ℏc) = 1/M_Planck²`;
330cubing the latter and multiplying by `M_SI⁶` gives `(M_SI/M_Planck)⁶`.
331So the squared identity says
332`t_Page_SI(M_SI)² = t_Planck² · (5120π)² · (M_SI/M_Planck)⁶`, the
333Planck-unit form. -/
334theorem t_Page_SI_squared_planck_form (M_SI : ℝ) :
335 (t_Page_SI M_SI) ^ 2 =
336 (5120 * Real.pi) ^ 2 * (hbar_SI * G_SI / c_SI ^ 5) *
337 (G_SI / (hbar_SI * c_SI)) ^ 3 * M_SI ^ 6 := by
338 unfold t_Page_SI
339 have hb : hbar_SI ≠ 0 := ne_of_gt hbar_SI_pos
340 have hc : c_SI ≠ 0 := ne_of_gt c_SI_pos
341 have hG : G_SI ≠ 0 := ne_of_gt G_SI_pos
342 field_simp
343
344/-! ## §6. Master cert -/
345
346/-- Master cert: SI Hawking temperature has the master-plan-stipulated form,
347positivity, strict anti-monotonicity, is the bridge lift of the
348RS-native `T_hawking`, admits a Schwarzschild-radius reformulation, and
349extends to the SI Page time `t_Page_SI` with `M³` scaling. -/
350structure HawkingTemperatureSICert where
351 T_hawking_SI_def :
352 ∀ M : ℝ, T_hawking_SI M = hbar_SI * c_SI ^ 3 /
353 (8 * Real.pi * G_SI * k_B_SI * M)
354 hawking_temperature_SI :
355 ∀ (M_SI : ℝ), 0 < M_SI →
356 T_hawking_SI M_SI = hbar_SI * c_SI ^ 3 /
357 (8 * Real.pi * G_SI * k_B_SI * M_SI)
358 T_hawking_SI_pos :
359 ∀ M : ℝ, 0 < M → 0 < T_hawking_SI M
360 T_hawking_SI_strict_anti :
361 ∀ M1 M2 : ℝ, 0 < M1 → 0 < M2 → M1 < M2 →
362 T_hawking_SI M2 < T_hawking_SI M1
363 T_hawking_SI_eq_geom_via_bridge :
364 ∀ M : ℝ, 0 < M →
365 T_hawking_SI M =
366 T_hawking (G_SI * M / c_SI ^ 2) * (hbar_SI * c_SI / k_B_SI)
367 schwarzschildRadius_SI_def :
368 ∀ M : ℝ, schwarzschildRadius_SI M = 2 * G_SI * M / c_SI ^ 2
369 schwarzschildRadius_SI_pos :
370 ∀ M : ℝ, 0 < M → 0 < schwarzschildRadius_SI M
371 T_hawking_SI_eq_inv_schwarzschildRadius :
372 ∀ M : ℝ, 0 < M →
373 T_hawking_SI M = hbar_SI * c_SI /
374 (4 * Real.pi * k_B_SI * schwarzschildRadius_SI M)
375 t_Page_SI_def :
376 ∀ M : ℝ, t_Page_SI M = 5120 * Real.pi * G_SI ^ 2 * M ^ 3 /
377 (hbar_SI * c_SI ^ 4)
378 K_Page_SI_pos : 0 < K_Page_SI
379 t_Page_SI_eq_K_mul_M_cube :
380 ∀ M : ℝ, t_Page_SI M = K_Page_SI * M ^ 3
381 t_Page_SI_pos : ∀ M : ℝ, 0 < M → 0 < t_Page_SI M
382 t_Page_SI_strict_mono :
383 ∀ M1 M2 : ℝ, 0 < M1 → 0 < M2 → M1 < M2 → t_Page_SI M1 < t_Page_SI M2
384
385def hawkingTemperatureSICert : HawkingTemperatureSICert where
386 T_hawking_SI_def := T_hawking_SI_def
387 hawking_temperature_SI := hawking_temperature_SI
388 T_hawking_SI_pos := T_hawking_SI_pos
389 T_hawking_SI_strict_anti := T_hawking_SI_strict_anti
390 T_hawking_SI_eq_geom_via_bridge := T_hawking_SI_eq_geom_via_bridge
391 schwarzschildRadius_SI_def := schwarzschildRadius_SI_def
392 schwarzschildRadius_SI_pos := schwarzschildRadius_SI_pos
393 T_hawking_SI_eq_inv_schwarzschildRadius := T_hawking_SI_eq_inv_schwarzschildRadius
394 t_Page_SI_def := t_Page_SI_def
395 K_Page_SI_pos := K_Page_SI_pos
396 t_Page_SI_eq_K_mul_M_cube := t_Page_SI_eq_K_mul_M_cube
397 t_Page_SI_pos := t_Page_SI_pos
398 t_Page_SI_strict_mono := t_Page_SI_strict_mono
399
400theorem hawkingTemperatureSICert_inhabited :
401 Nonempty HawkingTemperatureSICert :=
402 ⟨hawkingTemperatureSICert⟩
403
404/-- **HAWKING TEMPERATURE SI ONE-STATEMENT** (Track 3.A closure form).
405In SI units, the Hawking temperature of a Schwarzschild black hole is
406`T_H = ℏ_SI · c_SI³ / (8π · G_SI · k_B_SI · M_SI)`. It is positive and
407strictly decreasing in the mass. It is the lift of the RS-native
408`T_hawking(G_SI · M_SI / c_SI²)` (geometrized form) through the energy-to-
409temperature conversion factor `ℏ_SI · c_SI / k_B_SI` provided by the
410SI dimensional bridge. -/
411theorem hawking_temperature_SI_one_statement :
412 (∀ M : ℝ, T_hawking_SI M = hbar_SI * c_SI ^ 3 /
413 (8 * Real.pi * G_SI * k_B_SI * M)) ∧
414 (∀ M : ℝ, 0 < M → 0 < T_hawking_SI M) ∧
415 (∀ M1 M2 : ℝ, 0 < M1 → 0 < M2 → M1 < M2 →
416 T_hawking_SI M2 < T_hawking_SI M1) ∧
417 (∀ M : ℝ, 0 < M →
418 T_hawking_SI M =
419 T_hawking (G_SI * M / c_SI ^ 2) * (hbar_SI * c_SI / k_B_SI)) :=
420 ⟨T_hawking_SI_def, T_hawking_SI_pos, T_hawking_SI_strict_anti,
421 T_hawking_SI_eq_geom_via_bridge⟩
422
423end
424
425end HawkingTemperatureSI
426end Gravity
427end IndisputableMonolith
428