Pith. sign in
def

k_B_SI

definition
show as:
module
IndisputableMonolith.Gravity.HawkingTemperatureSI
domain
Gravity
line
117 · github
papers citing
none yet

plain-language theorem explainer

Fixes the Boltzmann constant at its SI-2019 exact value 1.380649e-23 J/K. Gravity and thermodynamics authors cite it whenever Hawking temperature or Bekenstein-Hawking entropy is lifted from RS-native units into SI. The body is a one-line numeric definition; no proof obligations.

Claim. The Boltzmann constant in SI units is the exact constant $k_B = 1.380649 \times 10^{-23}\,\mathrm{J/K}$, as fixed by the 2019 SI redefinition.

background

Track 3.A of the quantum-gravity master plan converts the RS-native Hawking temperature $T_H = 1/(8\pi M)$ (geometrized units $c = G = \hbar = k_B = 1$) into SI. The conversion uses the dimensional bridge from Foundation.SIBridgeClosure, whose scale factors are fixed by the SI values of $c$, $\hbar$, $G$, and $k_B$.

Since the 2019 SI reform, $k_B$ is an exact defining constant rather than a measured quantity. This module therefore hard-codes that exact value and builds the standard SI Hawking formula $T = \hbar c^3 / (8\pi G k_B M)$ and the related positivity and bridge identities around it.

Downstream, the same constant multiplies the leading Bekenstein-Hawking entropy when area is expressed in SI, so black-hole entropy statements inherit this definition directly.

proof idea

Pure definition: the real constant is assigned the literal SI-2019 value $1.380649 \times 10^{-23}$. No tactics, lemmas, or axioms are involved.

why it matters

Without an exact $k_B$, the SI Hawking temperature and the SI Bekenstein-Hawking entropy cannot be stated as closed identities. Downstream, S_BH_SI is defined as $k_B$ times area times $c^3/(4 G \hbar)$, and the Track 3.B cert BlackHoleEntropySICert requires S_BH_SI_def and the bridge identity S_BH_SI = k_B \cdot S_{\mathrm{lead}}(A/\ell_P^2). The one-statement theorem black_hole_entropy_SI_one_statement likewise opens with the same formula. In the RS framework this constant is the last SI anchor that turns the geometrized $T_H = 1/(8\pi M)$ and $S = A/4$ into laboratory units after the $c$, $\hbar$, $G$ bridge is closed.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.