radiationCapacityFromTicks_eq_radiationCapacity
plain-language theorem explainer
Tick-parameterised radiation capacity equals the continuous linear radiation capacity evaluated at the evaporation fraction induced by emitted ledger ticks. Gravity and Page-curve workers cite it when bridging discrete recognition-tick bookkeeping to the Schmidt min-of-capacities curve. The proof is pure definitional equality (rfl).
Claim. For any black-hole entropy scale $S_{\mathrm{BH}}\in\mathbb{R}$ and natural numbers $N,n$, the radiation capacity computed from $N$ total ticks with $n$ emitted equals the continuous radiation capacity $S_{\mathrm{BH}}\cdot t$ at the tick-induced evaporation fraction $t=t(N,n)$.
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt purification on bulk ⊗ radiation, rather than postulating it kinematically. Evaporation is parameterised by a fraction $t\in[0,1]$: bulk capacity falls as $S_{\mathrm{BH}}(1-t)$ and radiation capacity rises as $S_{\mathrm{BH}}\cdot t$. Unitary evolution from a pure bulk state keeps the joint state pure, so Schmidt forces equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$; under maximal entanglement the radiation entropy saturates that min and yields the triangle peaking at $t=1/2$.
The discrete side counts emitted ledger ticks. A tick is the RS atomic time quantum ($\tau_0=1$). The map evaporationFractionFromTicks turns a pair $(N,n)$ into the continuous fraction $t$, and radiationCapacityFromTicks is the corresponding discrete radiation capacity. This lemma identifies that discrete object with the continuous linear capacity at the induced $t$.
proof idea
One-line definitional equality: rfl. By construction, radiation capacity from ticks is defined as the continuous linear radiation capacity evaluated at the tick-induced evaporation fraction, so the two sides are definitionally equal with no rewriting or arithmetic required.
why it matters
This is the radiation half of the first discrete-to-continuous bridge in Track 3.C (Page curve from Schmidt-balanced ledger dynamics). It is consumed by tick_capacity_sum_invariant (tick capacities conserve $S_{\mathrm{BH}}$), by the main bridge pageCurveFromLedgerTicks_eq_pageCurveFromUnitarity (ledger-tick curve equals the Schmidt min-of-capacities curve at the induced fraction), and by the integration endpoint track3_tick_capacity_endpoint_holds in MasterTheoremHandoffIntegration. Together with the twin bulk identity, it closes the handoff from emitted recognition ticks to the continuous Page-curve parameter without extra axioms. Framework context: discrete time advances in ticks (eight-tick octave at the foundation layer); here ticks only supply the evaporation clock for the capacity ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.