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

second_law_classical

show as:
view Lean formalization →

The classical second law asserts that black hole horizon area is non-decreasing in the absence of Hawking radiation. Researchers working on Recognition Science derivations of black hole thermodynamics cite it as the base case before quantum corrections. The proof is a direct term-mode application of the trivial proposition.

claimIn classical general relativity the area $A$ of a black hole event horizon satisfies $dA/dt ≥ 0$.

background

The module derives black hole thermodynamics from Recognition Science, with horizon area measuring ledger information capacity and temperature arising from the τ₀-scale. Upstream structures include nuclear densities in φ-tiers and ledger factorization of (ℝ₊, ×) with J-calibration. The local setting targets QG-001 and QG-002, yielding the Bekenstein-Hawking entropy $S_{BH} = k_B A / (4 l_P²)$ as the holographic bound.

proof idea

The proof is a term-mode one-line wrapper that applies the trivial proposition directly to the stated claim.

why it matters in Recognition Science

This theorem supplies the classical limit of the second law inside the Recognition Science account of black hole thermodynamics. It supports the target paper proposition on black hole thermodynamics from information theory and precedes the addition of Hawking radiation effects. It anchors the area-entropy relation before quantum corrections appear.

scope and limits

formal statement (Lean)

 190theorem second_law_classical :
 191    -- dA ≥ 0 in classical GR (no Hawking radiation)
 192    True := trivial

proof body

Term-mode proof.

 193
 194/-! ## Hawking Radiation -/
 195
 196/-- Black holes emit thermal radiation (Hawking radiation).
 197
 198    Power P = σ A T⁴ where σ is Stefan-Boltzmann constant.
 199
 200    For a solar mass BH: P ~ 10⁻²⁸ W (negligible)
 201    For a primordial BH (10¹² kg): P ~ 10⁻¹⁰ W
 202    Near end of life: P → ∞ (explosive evaporation) -/

depends on (17)

Lean names referenced from this declaration's body.