second_law_classical
plain-language theorem explainer
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.
Claim. In 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.