pageCurveFromLedgerTicks_at_zero
plain-language theorem explainer
At zero emitted ticks the ledger Page curve equals zero: radiation entropy vanishes before evaporation starts. Gravity Track 3.C and the operator-entropy readouts cite this as the left endpoint of the triangular Page curve. The proof rewrites to the unitarity form, shows the evaporation fraction at tick 0 is zero, and applies min(S_BH, 0) = 0 under nonnegativity of black-hole entropy.
Claim. For black-hole entropy $S_{\mathrm{BH}} \ge 0$ and total tick count $N > 0$, the Page curve built from ledger ticks at emitted-tick count $0$ equals $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 fraction $t \in [0,1]$ of total entropy transferred from bulk to radiation. Bulk capacity falls as $S_{\mathrm{BH}}(1-t)$; radiation capacity grows as $S_{\mathrm{BH}}, t$. The joint bulk-radiation state stays pure under unitary evolution, so Schmidt's theorem forces equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}}, \log d_{\mathrm{rad}})$.
Under maximal Schmidt balance the radiation entropy saturates that bound and equals $\min(\mathrm{bulk\ capacity}, \mathrm{radiation\ capacity})$. That minimum of two monotone linear bounds is the triangular Page curve, with forced peak at half evaporation. The ledger-tick form discretises the same recipe by counting emitted ticks against a positive total tick budget $N$, with evaporation fraction zero when no ticks have been emitted.
The module is a structural theorem (zero sorry, no RS-internal axiom). The continuous unitarity form and the tick-parameterised capacities are the immediate upstream ingredients used here.
proof idea
Rewrite the ledger-tick Page curve at emitted count 0 into the unitarity form via the equality that identifies the two presentations (using $N > 0$ and $0 \le N$). A short unfold-and-simp shows the evaporation fraction at zero emitted ticks is $0$. Substitute that fraction, unfold the unitarity Page curve into bulk and radiation capacities, and finish with $\min(S_{\mathrm{BH}}\cdot(1-0), S_{\mathrm{BH}}\cdot 0) = \min(S_{\mathrm{BH}}, 0) = 0$ by the right-min identity under $S_{\mathrm{BH}} \ge 0$.
why it matters
This is the left endpoint of the derived Page curve: no radiation entropy before any evaporation. It is consumed by the operator readout that radiation entropy at tick 0 is zero, by the Schmidt capacity bound at tick 0, and by the saturated-process statement that entropy after zero unitary ticks is zero. The nontriviality package uses it as one of the concrete endpoint witnesses (together with the full-evaporation return to zero and the mid-curve peak).
On the integration lane it feeds the Track 3 tick-capacity endpoint bundle handed to the master theorem. Within Recognition Science gravity this closes the $t=0$ corner of the dynamical recipe that replaced the Session 101 kinematic ansatz: the triangular shape, including both endpoints, is forced by purity plus Schmidt balance rather than drawn by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.