hawking_temperature_SI_proven
plain-language theorem explainer
The SI Hawking-temperature certificate is fully discharged: temperature positive, strictly anti-correlated with mass, Page-time prefactor positive, and Page time scaling exactly as mass cubed. Gravity and black-hole auditors cite it as one of the eight closed master-theorem clauses. The proof is a pure term that packages the existing HawkingTemperatureSI certificate fields.
Claim. The SI Hawking-temperature certificate holds: Hawking temperature satisfies $T_H^{\mathrm{SI}}>0$ and is strictly decreasing in black-hole mass; the Page-time prefactor obeys $K_{\mathrm{Page}}^{\mathrm{SI}}>0$; and Page time equals $t_{\mathrm{Page}}^{\mathrm{SI}}=K_{\mathrm{Page}}^{\mathrm{SI}}\,M^3$.
background
Gravity Track 7.A authors the master quantum-gravity statement as a twelve-clause conjunction. Eight clauses are CLOSED and discharged from existing Lean certificates; five remain as hypothesis inputs for still-open tracks. The Hawking-temperature SI clause is one of the closed certificates.
In SI units the certificate records four analytic facts about evaporating black holes: positivity of $T_H$, its strict inverse-mass (anti) dependence, positivity of the Page-time constant, and the cubic mass law $t_{\mathrm{Page}}\propto M^3$. These sit alongside sibling closed props (Lorentzian $1{+}3$, cost uniqueness, $\omega_\Lambda$ from $\varphi$, QNM discriminators) that the master theorem packages together.
The local module is structural and conditional: it does not claim the discovery is finished, only that closed anchors are inhabited and open tracks are named as hypotheses.
proof idea
Term-mode packaging, not a tactic script. The goal type is a nested structure (product of the four analytic fields with a certificate witness). The proof supplies both halves by projection from Gravity.HawkingTemperatureSI.hawkingTemperatureSICert:
- positivity of $T_H^{\mathrm{SI}}$,
- strict anti-mass dependence of $T_H^{\mathrm{SI}}$,
- positivity of $K_{\mathrm{Page}}^{\mathrm{SI}}$,
- the identity $t_{\mathrm{Page}}^{\mathrm{SI}}=K,M^3$,
then wraps the same certificate object as the second component. No new analysis is performed here; the lemma is a one-shot inhabitant that re-exports an already-proved SI certificate into the master-theorem Prop namespace.
why it matters
This declaration is a load-bearing CLOSED clause of Track 7.A. Downstream, rs_quantum_gravity_master_conditional includes it among the eight clauses discharged inside the conditional master theorem (under the five open-track hypotheses). The non-circularity audit closed_certs_hold lists it explicitly in the conjunction of six closed certificate props that must hold independently of the open inputs.
In the Recognition framework it anchors the thermodynamic side of black-hole physics in SI units, complementary to entropy and echo certificates imported by the same module. It does not itself invoke the forcing chain T0–T8 or the RCL, but it sits in the gravity stack that those foundations ultimately support. Closing this clause removes one structural obligation from the path to an unconditional master theorem once Tracks 1.B/1.C, 2.C/2.D, 3.C, 6.B, and 6.C finish.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.