IndisputableMonolith.Gravity.PageCurveNontrivial
Collects the elementary inequalities that make the dynamical Page curve nontrivial: the tick-induced evaporation fraction stays in [0,1], equals 1/2 at the Page time, and the curve rises then falls with a unique peak. Gravity auditors cite it when they need the readout to be strictly non-flat. Proofs are short order and min/max arguments on the Schmidt-capacity formula from the dynamical and operator-entropy modules.
claimLet $f(t)$ be the tick-induced evaporation fraction and $S(t)$ the Page entropy built as a Schmidt-capacity minimum. Then $0 \le f(t) \le 1$, $f$ is monotone in the natural tick parameter, $f = 1/2$ exactly at the Page time, $S$ is monotone increasing before that time and monotone decreasing after, and $S$ attains a unique peak. The associated nontrivial readout vanishes at the empty and full extremes and is positive in between.
background
Recognition Science Gravity Track 3.C derives the black-hole Page curve from Schmidt-balanced ledger dynamics rather than a kinematic ansatz. The upstream module PageCurveDynamical replaces the Session-101 piecewise-linear triangle by a capacity minimum coming from the ledger; PageCurveOperatorEntropy then supplies the operator-derived entropy and the master-theorem witness via recognition ticks.
The evaporation fraction $f$ is the tick-normalized share of degrees of freedom that have left the interior. The Page entropy is the min of interior and exterior Schmidt capacities, so its shape is controlled by when $f$ crosses one half. This module isolates the order-theoretic facts about $f$ and $S$ that certify the curve is not constant and has the classic rise-peak-fall profile.
Local setting: pure structural theorems (no RS-internal axioms, no sorry) sitting between the dynamical construction and the unconditional master-theorem closure surface.
proof idea
The module is a cluster of short lemmas, not a single deep argument. Non-negativity, upper bound one, and the half-crossing identities for the evaporation fraction are direct from its definition as a normalized tick count (nonnegativity, monotonicity in the tick parameter, and comparison with $1/2$).
Monotone rise of the Page curve before the Page time and monotone fall after follow by feeding those fraction comparisons into the Schmidt-capacity $\min$: before half, the interior capacity is the binding constraint and grows; after half, the exterior capacity binds and shrinks. The peak lemma is the conjunction of the two mono facts at the unique half-crossing.
Nontrivial readout is the residual that vanishes at the empty and fully evaporated endpoints and is assembled so the master theorem can quote a single non-degeneracy witness.
why it matters in Recognition Science
MasterTheoremUnconditional imports this module to install theorem-built witnesses for the older conditional quantum-gravity master theorem. Without a proved non-flat Page profile, the D-series convergence and information-recovery routes would still carry a kinematic hypothesis.
In the broader RS gravity stack this is the last elementary filter between Schmidt-balanced ledger dynamics and the zero-argument closure surface: it turns the dynamical triangle into a package of named inequalities (fraction bounds, rise/fall, peak, nontrivial readout) that downstream master theorems can cite by name.
It does not itself derive $D=3$ or the eight-tick octave; those sit earlier in the forcing chain. Its job is narrower and essential: certify that the operator-derived Page entropy is a genuine Page curve, not a constant or monotone stub.
scope and limits
- Does not derive the Page curve from Einstein equations or semiclassical QFT.
- Does not fix numerical Page time in SI units; only tick-normalized fraction identities.
- Does not prove unitarity of evaporation beyond the Schmidt-capacity ledger model.
- Does not discharge master-theorem inputs other than the nontriviality/readout package.
- Does not address higher-genus or charged black-hole variants.
used by (1)
depends on (2)
declarations in this module (20)
-
theorem
evapFrac_nonneg -
theorem
evapFrac_mono -
theorem
evapFrac_le_half -
theorem
evapFrac_ge_half -
theorem
evapFrac_le_one -
theorem
evapFrac_eq_half -
theorem
pageCurve_mono_rise -
theorem
pageCurve_anti_fall -
theorem
pageCurve_peak -
def
nontrivialReadout -
theorem
nontrivialReadout_zero -
theorem
nontrivialReadout_full -
theorem
nontrivialReadout_peak -
def
nontrivialPageCurveProp -
theorem
nontrivialPageCurveProp_holds -
def
nontrivialPageCurveDerivedWitness -
structure
NontrivialPageCurveCert -
def
nontrivialPageCurveCert -
theorem
nontrivialPageCurveCert_inhabited -
theorem
nontrivial_page_curve_one_statement