schmidtCapacityBound_at_page_fraction
plain-language theorem explainer
At the Page midpoint (evaporation fraction exactly 1/2), the Schmidt capacity bound of an operator Page process equals half the initial black-hole entropy. Anyone deriving the triangular Page curve from operator dynamics rather than a supplied readout field would cite this identity. The proof unfolds the capacity definition and applies the ledger-tick midpoint lemma.
Claim. Let $P$ be an operator Page process with initial black-hole entropy $S_{BH}$ and total tick count $N>0$. If $n\le N$ satisfies the evaporation-fraction condition that the fraction of ticks elapsed equals $1/2$, then the Schmidt capacity bound of $P$ at tick $n$ equals $S_{BH}/2$.
background
This module sits in Gravity Track 3.C: operator-derived Page entropy. The dynamical Page-curve module already packages the triangular Page curve as a Schmidt-capacity minimum and supplies a master-theorem witness that still carries readout equality as a structure field. Here the readout is meant to be derived: define a capacity bound from the operator process, prove that Schmidt saturation (entropy equals that bound) forces the Page curve, and route the witness through the derived equality.
An operator Page process packages a black-hole entropy $S_{BH}$, a positive total tick count, and the discrete evaporation timeline. The evaporation fraction at tick $n$ is the elapsed share of that timeline. The Schmidt capacity bound is the triangular min-curve built from $S_{BH}$ and that fraction: it rises linearly to the midpoint and falls symmetrically afterward. The Page fraction is the unique half-evaporated tick where the bound should peak at $S_{BH}/2$.
Upstream, the ledger-tick Page-curve lemmas already establish the same midpoint identity at the level of abstract tick counts and entropy scales; this declaration specializes that fact to the operator-process packaging.
proof idea
One-line term wrapper. Unfold the definition of the Schmidt capacity bound (so the goal becomes the abstract ledger-tick midpoint statement), then apply pageCurveFromLedgerTicks_at_page_fraction to $S_{BH}$, the total tick count, $n$, positivity of the total, the inequality $n\le N$, and the hypothesis that the evaporation fraction equals $1/2$. No additional algebraic work.
why it matters
The midpoint identity is the peak of the triangular Page curve: radiation entropy reaches half the initial black-hole entropy exactly when half the ticks have elapsed, then declines. Together with the zero-tick and full-evaporation endpoint lemmas in this module, it pins the three canonical values of the Schmidt capacity bound.
Those bounds feed the Schmidt-saturation principle introduced immediately below: if the entropy functional is derived from the operator state and saturates the capacity bound at every tick, the readout is forced to equal the Page curve. The module's stated goal is to supersede field-based witnesses that literally assume readout_eq_page_curve, so no load-bearing theorem depends on a supplied equality field.
No downstream consumers are recorded yet; the declaration is infrastructure for the saturated-process theorems and the operator-derived Page-curve proposition in the same file. Framework-wise it is pure structural gravity bookkeeping, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.