radiationEntropyAtTick_full
plain-language theorem explainer
At full evaporation (tick count equal to totalTicks), the operator-level radiation entropy readout is exactly zero. Anyone citing the dynamical Page curve endpoint or the operator-process certificate needs this boundary fact. The proof rewrites the readout via the structural bridge to the ledger-tick Page curve, then applies the already-proved full-tick vanishing lemma.
Claim. Let $P$ be an operator-level Page entropy readout on bulk and radiation carriers. Then the radiation entropy at the final tick equals zero: $S_{\mathrm{rad}}(N) = 0$ where $N$ is the total number of evaporation ticks.
background
Gravity Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterized by a tick count $n \in {0,\ldots,N}$, with bulk capacity $S_{\mathrm{BH}}(1-t)$ and radiation capacity $S_{\mathrm{BH}} t$ for fraction $t = n/N$. 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$ of the two capacities; saturating that bound yields the Page triangle, which returns to zero at $t=1$.
OperatorPageEntropyReadout is the remaining structural bridge: it packages an operator Page process together with a function radiationEntropyAtTick and the axiom that this readout equals pageCurveFromLedgerTicks for every admissible tick. Upstream, pageCurveFromLedgerTicks_at_full already states that the ledger-tick Page curve vanishes at full emitted-tick count when $S_{\mathrm{BH}} \ge 0$ and $N > 0$.
proof idea
Term-mode rewrite proof in two steps. First apply the readout bridge readout_eq_page_curve at $n = N = \texttt{totalTicks}$, using reflexivity of $\le$ to discharge $N \le N$. The goal becomes an instance of the ledger-tick identity. Second rewrite by pageCurveFromLedgerTicks_at_full, feeding nonnegativity of $S_{\mathrm{BH}}$ and positivity of total ticks from the process fields. No further case analysis.
why it matters
Closes the late-time boundary of the operator entropy interface: radiation entropy starts at zero and must finish at zero after complete evaporation, matching unitarity and the triangular Page shape forced by Schmidt balance (peak at half-evaporation forced, not chosen).
Downstream it is used by operator_page_process_interface_one_statement (the one-statement operator-level Page process interface), by pageCurveOperatorProcessCert (certificate packaging carrier, unitary tick, and readout), and by nontrivialReadout_full in PageCurveNontrivial, which specializes the same endpoint to an explicit nontrivial readout. The module status is structural closure (0 sorry); deriving the readout from a concrete microscopic Hamiltonian remains open, as the interface theorem notes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.