EvolvingBlackHole
plain-language theorem explainer
EvolvingBlackHole is a structure that parameterizes a black hole by its initial Bekenstein-Hawking entropy and evaporated mass fraction, subject to positivity and interval constraints. Researchers modeling black hole evaporation under Recognition Science ledger dynamics would cite it to compute radiation entanglement entropy. The declaration is a direct structure definition that supplies the typed parameters used by downstream entropy functions.
Claim. An evolving black hole consists of a pair $(S_0, f)$ with $S_0 > 0$ the initial entropy in bits and $0 ≤ f ≤ 1$ the evaporated mass fraction, together with the explicit constraints $S_0 > 0$ and $0 ≤ f ≤ 1$.
background
The module derives the Page curve for black hole evaporation from Recognition Science ledger conservation, where entanglement is identified with shared ledger entries and information is redistributed rather than lost. Entropy of any configuration is defined as its total defect, with the zero-defect state being the minimum-entropy initial condition. Upstream structures supply the J-cost functional, phi-ladder discretization of physical quantities, and ledger factorization that calibrate the entropy scale.
proof idea
The declaration is a structure definition with no proof body. It directly introduces the two real parameters and their two validity fields, serving as the typed carrier for all subsequent entropy calculations in the module.
why it matters
The structure is the input type for pageEntropy, radiationEntropyNaive and remainingEntropy, which together realize the Page curve: linear growth of radiation entropy up to the midpoint followed by linear decrease. It supplies the concrete object needed for the module's target derivation of the Page curve from ledger dynamics and supports the claim that information is preserved by the curve. The construction sits inside the T7 eight-tick octave and ledger-based information accounting of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.