evaporationFractionFromTicks
plain-language theorem explainer
Maps a discrete emitted-tick count n and total tick budget N to the continuous evaporation fraction n/N in [0,1] (when n ≤ N and N > 0). Gravity Track 3.C cites it as the bridge from ledger ticks to the continuous Page-curve parameter t. The body is a one-line real division of natural numbers.
Claim. For natural numbers $N$ (total recognition-tick budget) and $n$ (emitted ticks), the induced evaporation fraction is $\frac{n}{N}$ as a real number.
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterised by a continuous fraction $t \in [0,1]$: bulk capacity falls as $S_{\mathrm{BH}}(1-t)$ and radiation capacity grows as $S_{\mathrm{BH}},t$. Unitary evolution from a pure bulk state keeps the joint bulk⊗radiation state pure, so Schmidt forces equal reduced entropies bounded by $\min$ of the two capacities; that $\min$ is the Page curve.
The continuous parameter $t$ must still be tied to the discrete recognition ledger. Horizon and thermodynamic entropy readings elsewhere in the stack (defect totals, Boltzmann $S = k\beta\langle E\rangle + k\ln Z$, log microstate counts) motivate counting emitted recognition ticks. This definition supplies the normalised tick ratio that plays the role of $t$.
proof idea
Pure definition: cast $n$ and $N$ to $\mathbb{R}$ and divide. No lemmas, no tactics. Downstream equalities unfold this name and discharge $N \neq 0$ from a positivity hypothesis on $N$.
why it matters
Central discrete-to-continuous bridge in Track 3.C. Downstream, bulkCapacityFromTicks_eq_bulkCapacity and the radiation twin identify tick capacities with the linear capacities evaluated at this fraction; bulkCapacityFromTicks_next shows each tick removes $S_{\mathrm{BH}}/N$. The ledger Page curve theorems (at zero, at full evaporation, at half-fraction peak, and equality with the unitarity Page curve) all route through it. Operator-level evaporationFractionAtTick reuses the same ratio. MasterTheoremHandoffIntegration packages the fork as Track3TickCapacityEndpoint: finite emitted ticks induce capacity transfer, conserve total capacity, and recover the Schmidt $\min$ curve at this fraction. Closes the Session-101 gap where the triangle was a kinematic ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.