Pith. sign in
def

Track3TickCapacityEndpoint

definition
show as:
module
IndisputableMonolith.Gravity.MasterTheoremHandoffIntegration
domain
Gravity
line
1645 · github
papers citing
none yet

plain-language theorem explainer

Fork D packages nine identities equating discrete recognition-tick bulk/radiation capacities to the continuous Page-curve capacities at the induced evaporation fraction. Total capacity is conserved, each tick transfers S_BH/N, and the ledger Page curve matches the unitarity (Schmidt min) curve, vanishing at the endpoints and equaling S_BH/2 at half evaporation. Gravity integration cites this as the Track 3.C handoff. The object is a pure Prop conjunction; the companion theorem discharges it by named lemmas from PageCurveDynamical.

Claim. The following hold simultaneously for black-hole entropy capacity $S_{BH}$ and tick counts $N,n$: radiation (resp. bulk) capacity from ticks equals continuous radiation (resp. bulk) capacity at evaporation fraction $n/N$; bulk plus radiation capacities sum to $S_{BH}$; each successive tick raises radiation capacity and lowers bulk capacity by $S_{BH}/N$; the ledger-tick Page curve equals the unitarity Page curve at that fraction; the ledger curve is $0$ at $n=0$ and at $n=N$; and when the fraction is $1/2$ the ledger curve equals $S_{BH}/2$.

background

Track 7 is the integration-lane receipt for parallel fork handoffs in the gravity master theorem. Fork D is Track 3.C: discrete recognition-tick Page-capacity transfer. It does not upgrade the discovery claim; it records what the new endpoints prove.

In PageCurveDynamical, evaporation fraction from ticks is $n/N$. Bulk capacity from ticks is $S_{BH}\cdot(N-n)/N$, the remaining-tick share; radiation capacity is the complementary emitted share. The continuous counterparts are linear: bulk capacity $S_{BH}(1-t)$ and radiation capacity $S_{BH},t$ at fraction $t$. The Page curve from unitarity is the Schmidt min curve; the ledger-tick version evaluates the same curve on the tick-induced fraction.

Spatial dimension $D=3$ (forced by T8/T9) sits in the broader gravity stack but is not a free parameter of these capacity identities. The endpoint is the Prop that the tick layer is faithful to the continuous Page layer.

proof idea

This declaration is a definition: a bare Prop equal to a nine-fold conjunction of universal statements. There is no proof body to walk. The companion theorem track3_tick_capacity_endpoint_holds is the one-line (tuple) discharge, assembling named lemmas from PageCurveDynamical: equality of tick and continuous radiation/bulk capacities, the sum invariant, the one-tick forward differences $\pm S_{BH}/N$, equality of ledger and unitarity Page curves, the two endpoint vanishings, and the half-evaporation evaluation $S_{BH}/2$.

why it matters

Fork D is the discrete recognition-tick bridge into the Page curve: finite emitted ticks induce bulk/radiation capacity transfer, conserve total capacity, and land on the existing Schmidt min curve at the tick-induced fraction. That is the gravity-side reading of ledger ticks as the evaporation clock.

Downstream, track3_tick_capacity_endpoint_holds proves the Prop; ForkHandoffIntegrationCert stores it as a field; and fork_A_B_C_D_E_F_handoffs_integrated_one_statement conjoins it with Forks A–C, E, F and the structural master certificate. The integration statement deliberately does not assert the fully unconditional discovery theorem. Within RS landmarks, the construction sits on the eight-tick/octave timing culture (T7) only as ambient discrete time; the identities themselves are linear capacity bookkeeping, not a new forcing step.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.