schmidtSaturated_entropy_zero
plain-language theorem explainer
Radiation entropy of a Schmidt-saturated operator Page process is zero at tick zero, before any evaporation. Boundary-condition arguments for the operator-derived Page curve cite this. The proof rewrites through the saturation-equals-Page-curve identity at n = 0, then applies the ledger Page curve's zero-tick vanishing lemma.
Claim. Let $P$ be a Schmidt-saturated operator Page process on finite bulk and radiation types. Then the state-derived radiation entropy of $P$ after zero unitary ticks equals $0$: $S(\Psi_0) = 0$, where $\Psi_0$ is the initial bulk-radiation ledger state.
background
Gravity Track 3.C derives the Page entropy readout from an operator process rather than supplying readout_eq_page_curve as a field. A Schmidt-saturated operator process extends an ordinary operator Page process by a state-to-entropy map entropyFromState that is forced, by the saturation hypothesis, to equal the Schmidt capacity bound at every tick up to total evaporation.
stateAfterOperatorTicks iterates a reversible Page tick unitary on a bulk-radiation ledger; at zero ticks it returns the initial state unchanged. The triangular Page curve from ledger ticks vanishes when no ticks have been emitted: pageCurveFromLedgerTicks S_BH N 0 = 0 under the standing nonnegativity and positivity hypotheses on black-hole entropy and total tick count.
The sibling result that radiation entropy equals the Page curve at every admissible tick is the derived readout theorem: saturation alone forces the equality, with no independent readout field.
proof idea
Term-mode, two steps. Rewrite the left-hand side by the derived readout theorem at $n = 0$ (using $0 \le$ totalTicks from arithmetic), which replaces state-derived entropy by pageCurveFromLedgerTicks at zero emitted ticks. Discharge the resulting goal by the upstream zero-tick identity for the ledger Page curve, feeding the process's black-hole entropy nonnegativity and positive total tick count.
why it matters
Closes the early-time boundary of the operator-derived Page curve: the readout starts at zero, matching the classical Page curve before radiation is emitted. Together with the full-evaporation and peak siblings, it pins the triangular shape once Schmidt saturation is assumed.
The module's point is structural: master-theorem witnesses route through derived equalities rather than a supplied readout_eq_page_curve field. This lemma is one of those derived equalities at the $n = 0$ endpoint. No downstream consumers are recorded yet; it stands as a boundary check inside Track 3.C's operator entropy package.
It does not invoke RS forcing landmarks (T5–T8, RCL, phi-ladder) directly; the content is quantum-information structure for evaporating black holes under a discrete tick ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.