radiationEntropyAtTick_page_fraction
plain-language theorem explainer
At any tick where the ledger evaporation fraction is exactly one half, the operator readout's radiation entropy equals half the black-hole entropy. Gravity and Page-curve workers cite this for the forced peak of the triangular curve under Schmidt balance. The proof is two rewrites: the readout equals the ledger Page curve, which itself equals S_BH/2 at half evaporation.
Claim. Let $P$ be an operator Page entropy readout on bulk and radiation spaces, with black-hole entropy $S_{\mathrm{BH}}$ and total tick count $N$. If $n \le N$ and the evaporation fraction at tick $n$ equals $1/2$, then the radiation entropy at tick $n$ equals $S_{\mathrm{BH}}/2$.
background
Gravity Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterised by a fraction $t \in [0,1]$ of total entropy moved from bulk to radiation. Bulk capacity falls as $S_{\mathrm{BH}}(1-t)$ and radiation capacity rises as $S_{\mathrm{BH}} t$. Unitary evolution from a pure initial bulk state keeps the joint bulk$\otimes$radiation state pure, so Schmidt forces equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$.
Under maximal Schmidt entanglement the radiation entropy saturates that bound and becomes $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$, which is the triangular Page curve with a forced peak at $t=1/2$.
An operator Page entropy readout extends the operator process by a tick-indexed radiation entropy map required to match the ledger-tick Page curve: for every admissible tick, readout entropy equals pageCurveFromLedgerTicks of $S_{\mathrm{BH}}$ and the total tick budget. The fundamental RS time quantum is one tick ($\tau_0=1$).
proof idea
Term-mode proof by two rewrites. First apply the readout axiom: radiation entropy at tick $n$ equals the ledger Page curve at that tick (using $n \le$ total ticks). Second apply the ledger half-fraction lemma: whenever the evaporation fraction from the total tick count at $n$ is $1/2$, that ledger Page value is exactly $S_{\mathrm{BH}}/2$ (using positivity of the total tick count and the half-fraction hypothesis). No further case splits.
why it matters
Closes the operator-level statement of the Page peak inside Track 3.C. The module status is a structural theorem (zero sorry, zero RS-internal axiom): the triangular shape, including the peak at half evaporation, is derived from purity plus Schmidt balance rather than inserted by hand as in the earlier kinematic ansatz of PageCurveStructural.
This lemma specialises the readout bridge at the unique forced maximum of $\min(S_{\mathrm{BH}}(1-t), S_{\mathrm{BH}} t)$. Downstream consumers of the operator interface can quote half black-hole entropy without re-opening capacity arithmetic. No used_by edges are recorded yet; the declaration is a terminal citation point for the half-evaporation identity on the dynamical curve. It sits in the gravity domain and does not itself invoke the T0–T8 forcing chain, RCL, or the $\alpha$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.