Gravity Page Curve Nontrivial Page Curve Mono Rise

The rising curve

In the physics of evaporating black holes, the Page curve describes how the entropy of the radiation escaping a black hole changes over time. The curve starts at zero, climbs to a peak at the halfway point of evaporation, and then falls back to zero when the hole is gone. The rising part of that curve is the subject of a theorem called pageCurve_mono_rise in the Recognition Science library, a machine-checked collection of formal theorems.

The theorem states a monotonicity property: as the evaporation fraction increases from zero up to one half, the radiation entropy never decreases. In plainer terms, before the black hole is halfway gone, the entropy of the emitted radiation only goes up or stays flat, it never dips. The proof works for any positive number of ticks, the discrete steps in which the framework's ledger (a discrete record of events) advances. The entropy readout itself is not assigned by hand; it is derived from a capacity-transfer law that connects the bulk and radiation states of the system.

This theorem matters because an earlier witness for the Page curve in the framework was degenerate: it had no interior peak and its entropy was identically zero. A referee would not accept that as a genuine Page curve. The new result supplies a nontrivial process with two independent bulk and two independent radiation states, and proves for that process the full rise, peak, and fall shape. The monotonic rise is one of the three shape theorems, alongside the monotonic fall and the peak value of S_BH / 2 at half evaporation.

The theorem does not claim that the capacity-transfer law itself is derived from a microscopic Hamiltonian. That step remains open. It also does not claim that every possible evaporation process must rise monotonically; it establishes the property for the specific nontrivial process constructed in the module, under the condition that the evaporation fraction stays at or below one half.

/-- **Monotone rise (pre-peak segment).**  On `2 * n ≤ N` the discrete
ledger Page curve is monotone non-decreasing in the emitted-tick count. -/
theorem pageCurve_mono_rise
    (S_BH : ℝ) (hS : 0 ≤ S_BH) (N m n : ℕ) (hN : 0 < N)
    (hmn : m ≤ n) (hn : 2 * n ≤ N) :
    pageCurveFromLedgerTicks S_BH N m ≤ pageCurveFromLedgerTicks S_BH N n := by
  have hnN : n ≤ N := le_trans (Nat.le_mul_of_pos_left n (by norm_num)) hn
  have hmN : m ≤ N := le_trans hmn hnN
  rw [pageCurveFromLedgerTicks_eq_pageCurveFromUnitarity S_BH N m hN hmN,
      pageCurveFromLedgerTicks_eq_pageCurveFromUnitarity S_BH N n hN hnN]
  exact pageCurveFromUnitarity_mono_phase1 S_BH _ _ hS
    (evapFrac_nonneg N m) (evapFrac_mono N m n hmn) (evapFrac_le_half N n hN hn)

/-- **Monotone rise (pre-peak segment).**  On `2 * n ≤ N` the discrete
ledger Page curve is monotone non-decreasing in the emitted-tick count. -/
theorem pageCurve_mono_rise
    (S_BH : ℝ) (hS : 0 ≤ S_BH) (N m n : ℕ) (hN : 0 < N)
    (hmn : m ≤ n) (hn : 2 * n ≤ N) :
    pageCurveFromLedgerTicks S_BH N m ≤ pageCurveFromLedgerTicks S_BH N n := by
  have hnN : n ≤ N := le_trans (Nat.le_mul_of_pos_left n (by norm_num)) hn
  have hmN : m ≤ N := le_trans hmn hnN
  rw [pageCurveFromLedgerTicks_eq_pageCurveFromUnitarity S_BH N m hN hmN,
      pageCurveFromLedgerTicks_eq_pageCurveFromUnitarity S_BH N n hN hnN]
  exact pageCurveFromUnitarity_mono_phase1 S_BH _ _ hS
    (evapFrac_nonneg N m) (evapFrac_mono N m n hmn) (evapFrac_le_half N n hN hn)

/-- **Nontrivial master-theorem Page witness.**  Bundles the
recognition-tick capacity-transfer law with the nontrivial Page-curve
proposition.  Supersedes the degenerate `operatorPageCurveDerivedWitness`. -/
def nontrivialPageCurveDerivedWitness :
    Gravity.MasterTheorem.PageCurveDerived where
  page_curve_derived :=
    recognition_tick_capacity_transfer_prop ∧ nontrivialPageCurveProp
  holds :=
    ⟨recognition_tick_capacity_transfer_prop_holds, nontrivialPageCurveProp_holds⟩

What this page does not claim

The capacity-transfer law is not derived from a microscopic Hamiltonian; that derivation remains open. The theorem does not apply to evaporation fractions beyond one half; the fall segment is covered by a separate theorem. The result does not claim that every conceivable evaporation process rises monotonically, only the specific nontrivial process constructed.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/PageCurveNontrivial.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: