evaporationFractionAtTick
plain-language theorem explainer
For an operator-level Page process, the evaporation fraction after n ticks is the ratio of n to the process's total tick budget. Anyone equating discrete ledger-tick capacities to the continuous unitarity Page curve cites this bridge. It is a one-line wrapper that reuses the tick-count fraction on the process field totalTicks.
Claim. Given an operator Page process $P$ (closed bulk-radiation ledger with initial black-hole entropy $S_{BH}$, finite positive tick budget $N$, unitary tick, and initial state) and a natural number $n$, the evaporation fraction at tick $n$ is $n/N\in\mathbb{R}$.
background
Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterized by a fraction $t\in[0,1]$: bulk capacity falls as $S_{BH}(1-t)$ and radiation capacity grows as $S_{BH},t$. For a pure joint state on bulk $\otimes$ radiation, Schmidt forces equal reduced entropies bounded by $\min$ of the two capacities, which is the Page curve peaking at $t=1/2$.
The continuous layer uses that fraction $t$ directly. The discrete layer counts emitted ticks $n$ out of a budget $N$, with evaporation fraction $n/N$. An operator Page process packages $S_{BH}$, a positive total tick budget, a reversible linear tick operator, and an initial bulk-radiation ledger state, without committing to a microscopic Hamiltonian entropy readout.
This definition simply reads the process budget and applies the same tick-induced fraction used by the capacity-transfer layer.
proof idea
One-line definitional wrapper. It applies evaporationFractionFromTicks to the process field totalTicks and the tick index $n$, i.e. returns $(n:\mathbb{R})/(N:\mathbb{R})$ with $N=P.\mathrm{totalTicks}$. No tactics or lemmas beyond that field projection.
why it matters
This is the discrete-to-continuous glue for operator processes in Gravity Track 3.C. Downstream equalities rewrite tick-indexed capacities and the ledger Page curve in continuous language: radiation capacity at tick $n$ equals radiation capacity at this fraction (by rfl); bulk capacity at tick $n$ matches bulk capacity of the fraction under $n\le N$; and the ledger-tick Page curve equals the unitarity Page curve evaluated at the same fraction.
Without a shared evaporation coordinate, the structural min-of-capacities theorem and the operator tick surface would stay in separate units. The module status is structural closure (0 sorry): the triangular shape emerges from purity plus linear capacity transfer, not from a kinematic ansatz. This def does not itself invoke T0-T8 or the RCL; it sits inside the gravity Page-curve derivation that those foundations ultimately underwrite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.