radiationEntropyAtTick_zero
plain-language theorem explainer
At tick zero, before any evaporation, the operator-level radiation entropy readout is exactly zero. Anyone citing the dynamical Page-curve interface or the operator-process certificate needs this boundary condition. The proof is a two-line rewrite: the readout equals the ledger-tick Page curve, which vanishes at the initial tick.
Claim. For any operator-level Page entropy readout $P$ on bulk and radiation carriers, the radiation entropy at tick $0$ equals $0$: $P.\mathrm{radiationEntropyAtTick}(0) = 0$.
background
Gravity Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterised by a tick count $n$ from $0$ to $N = \mathrm{totalTicks}$. Bulk capacity falls as $S_{BH}(1-t)$ and radiation capacity grows as $S_{BH},t$, with $t = n/N$. Unitarity of the joint bulk-radiation state plus Schmidt balance force radiation entropy to equal $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$, which is the triangular Page curve.
OperatorPageEntropyReadout packages an operator process (unitary tick on an explicit bulk-radiation carrier) together with a real-valued radiation-entropy function of the tick index. Its structural bridge axiom states that this readout agrees with pageCurveFromLedgerTicks at every admissible tick. Upstream, pageCurveFromLedgerTicks_at_zero already records that zero emitted ticks give zero radiation entropy on the ledger side.
proof idea
Two rewrites. First apply the readout bridge readout_eq_page_curve at $n=0$, using Nat.zero_le totalTicks to discharge the side condition $0 \le N$. The goal becomes equality of the ledger-tick Page curve at tick zero with zero. That is exactly pageCurveFromLedgerTicks_at_zero, fed $S_{BH}$, $N$, nonnegativity of $S_{BH}$, and positivity of $N$ from the process fields. No further arithmetic is needed.
why it matters
This is the initial boundary condition for the operator-level Page process. Downstream, pageCurveOperatorProcessCert wires it in as readout_starts_zero, and operator_page_process_interface_one_statement packages the full interface (carrier, unitary tick, entropy readout, tick evolution, and this zero start). The nontrivial track reuses it as nontrivialReadout_zero.
In the module narrative the Page curve must start at zero (pure bulk, empty radiation) and return to zero at full evaporation. This lemma closes the start endpoint at the operator-readout layer. The remaining open item, flagged by the one-statement interface, is deriving the readout from a concrete microscopic Hamiltonian or recognition update; the zero-at-tick-zero fact itself is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.