bhMass_nonneg_in_window
plain-language theorem explainer
The theorem establishes non-negativity of black hole mass under linear evaporation up to the total lifetime. Researchers constructing the Page curve and joint entropy invariance in Recognition Science cite it to keep the mass profile physically consistent. The proof is a short tactic sequence that unfolds the mass definition, multiplies the time bound by the positive rate, substitutes the explicit evaporation time, and concludes by linear arithmetic.
Claim. Let $M_0, alpha, t in mathbb{R}$ satisfy $alpha > 0$ and $t leq t_{rm evap}(M_0, alpha)$. Then $0 leq M(t)$, where $M(t) = M_0 - alpha t$ is the black-hole mass at time $t$.
background
The Black-Hole Information Preservation module models evaporation via the linear profile $M(t) = M_0 - alpha t$ with evaporation time $t_{rm evap} = M_0 / alpha$. Black-hole entropy is taken as $S_{rm BH}(t) = M(t)/4$, lifted directly from the ledger entropy in BlackHoleEntropyFromLedger.S_lead. The local setting is the resolution of the information paradox by keeping the joint black-hole-plus-radiation state pure on the Recognition Hilbert space, so that reduced entropies match and the Page curve appears automatically.
proof idea
The proof unfolds bhMass to reduce the goal to $M_0 - alpha t geq 0$. It forms the auxiliary inequality $alpha t leq alpha (t_{rm evap} M_0 alpha)$ by mul_le_mul_of_nonneg_left applied to the hypothesis $t leq t_{rm evap}$, rewrites the right-hand side to $M_0$ via field_simp on the definition of t_evap, and finishes with linarith.
why it matters
The result supplies the mass non-negativity needed for all subsequent entropy statements in the module, including S_BH_at and the bound $S_R(t) leq M_0/8$ that caps the radiation entropy. It anchors the linear evaporation model used to derive the Page time $t_P = t_{rm evap}/2$ and the joint VN entropy zero. Within the Recognition Science chain it closes the consistency requirement between the ledger factorization and the horizon dynamics before the entropy calculations proceed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.