naive_entropy_sum
plain-language theorem explainer
The theorem shows that black-hole entropy at time t plus naive thermal entropy of radiation emitted by t equals initial black-hole entropy. Physicists studying the information paradox cite it as the baseline naive relation before the Page curve is imposed. The proof unfolds the entropy definitions and reduces the equality by algebraic simplification.
Claim. Let $S_{BH}(M_0, alpha, t) = M(t)/4$ where $M(t) = M_0 - alpha t$. Let $S_{thermal}(alpha, t) = alpha t / 4$. Then $S_{BH}(M_0, alpha, t) + S_{thermal}(alpha, t) = S_{BH}(M_0, alpha, 0)$.
background
In this module the black-hole entropy at time t is S_BH_at(M0, alpha, t) := S_lead(bhMass(M0, alpha, t)), where S_lead(A) = A/4 is the leading-order ledger entropy. The naive thermal entropy S_thermal_at(alpha, t) := alpha * t / 4 counts the entropy contributed by mass lost to radiation under the assumption of complete thermalization. The module contrasts this conserved sum with the actual radiation entropy defined as the minimum of the two quantities, which produces the Page curve while keeping the joint von Neumann entropy identically zero.
proof idea
The proof is a one-line wrapper that unfolds S_BH_at, S_thermal_at, S_lead and bhMass, then applies the ring tactic to obtain the algebraic identity.
why it matters
This supplies the naive entropy-conservation relation that the module uses to set up the contrast with S_radiation_at = min(S_thermal, S_BH). It anchors the baseline step in the information-preservation argument, where the joint state on the recognition Hilbert space remains pure while reduced entropies track each other up to the Page time. The result therefore marks the transition from the standard thermal puzzle to the unitary resolution via recognition-rung emission.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.