black_hole_information_one_statement
plain-language theorem explainer
For an evaporating black hole with initial mass M0 and positive linear mass-loss rate alpha, the Page time equals half the total evaporation time, radiation entropy at that instant equals M0/8, radiation entropy stays at most M0/8 for all times, and the joint von Neumann entropy of black hole plus radiation is identically zero. Quantum-gravity researchers addressing the information paradox would cite this as the compact RS statement of unitarity preservation. The proof is a term-mode four-part conjunction assembled from reflexivity, a Page-time
Claim. Let $M_0, alpha > 0$ be real numbers. The Page time satisfies $t_P = M_0/(2 alpha)$, the radiation entropy at $t_P$ equals the Page entropy $M_0/8$, the radiation entropy is at most $M_0/8$ for every real time $t$, and the joint von Neumann entropy of the black-hole and radiation subsystems is zero for all $t$.
background
Recognition Science resolves the black-hole information paradox by treating the combined black-hole plus radiation system as a pure state on the recognition Hilbert space. The module introduces linear evaporation $M(t) = M_0 - alpha t$, defines pageTime as $M_0/(2 alpha)$ and pageEntropy as $M_0/8$, and sets radiation entropy to the pointwise minimum of naive thermal entropy and black-hole entropy. Joint von Neumann entropy is defined to be identically zero by unitarity of recognition evolution on $H_RS$ (see MODULE_DOC). Upstream results include the Page-bound theorem entropy_bound_by_initial_BH_half (proved by case split on $t$ relative to pageTime) and the direct theorem joint_VN_entropy_zero.
proof idea
The proof is a term-mode conjunction. Reflexivity gives the Page-time identity. The equality of radiation entropy to pageEntropy at that instant is supplied by the sibling lemma S_R_at_page_eq_page_entropy. The universal upper bound follows by applying entropy_bound_by_initial_BH_half to an arbitrary time. The final conjunct is immediate from the definition of joint_VN_entropy as the constant-zero function.
why it matters
This is the single-statement capstone for Track G1 in the Gravity module. It packages the Page curve (radiation entropy rises then falls without exceeding $M_0/8$) together with the structural fact that joint von Neumann entropy remains zero, thereby closing the information paradox inside the Recognition Science ledger framework. The result rests on the pure-state evolution on $H_RS$ and the entropy formulas imported from BlackHoleEntropyFromLedger; it appears as the terminal theorem in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.