Gravity Page Curve Nontrivial Nontrivial Readout Peak

The half-evaporation peak

The Page curve describes how the entropy of radiation emitted by an evaporating black hole changes over time. It starts at zero, rises as the hole radiates, peaks at the midpoint of evaporation, and then falls back to zero when the hole is gone, ensuring information is preserved. The theorem nontrivialReadout_peak establishes the middle of that story: at the precise tick when half the evaporation is complete, the radiation entropy equals exactly half of the black hole's initial entropy, S_BH / 2.

The result is part of a machine-checked library of formal theorems in the Recognition Science framework. The framework models physical processes as a discrete ledger, a record of recognition events where each step is a reversible operation. In this model, the entropy readout is not assigned by hand but derived from a capacity-transfer law: it is the smaller of the bulk capacity and the radiation capacity at each step. The theorem holds for any nonnegative initial entropy S_BH and any positive tick budget N, provided the peak tick is exactly half of N, so that 2 * peak = N.

The theorem is one of several that together prove the full nontrivial Page curve shape. The readout starts at zero, rises monotonically before the peak, falls monotonically after it, and returns to zero at full evaporation. The peak value itself is the key quantitative claim: at half-evaporation, the entropy is S_BH / 2. This is a theorem in the formal library, proved with no unproved assumptions and no framework-specific axioms.

The theorem does not claim that the capacity-transfer law itself is derived from a microscopic Hamiltonian. That derivation remains open. It also does not claim that any particular physical black hole follows this curve; it establishes the mathematical shape for a model process with two independent bulk and two independent radiation states. The theorem removes a defect in an earlier witness that had no interior peak, but it does not close the frontier of deriving capacities from first principles.

/-- The nontrivial readout peaks at `S_BH / 2` at the half-evaporation tick. -/
theorem nontrivialReadout_peak
    (S_BH : ℝ) (hS : 0 ≤ S_BH) (N peak : ℕ) (hN : 0 < N)
    (hpeak : 0 < peak) (hbal : 2 * peak = N) :
    (nontrivialReadout S_BH hS N hN).radiationEntropyAtTick peak = S_BH / 2 := by
  show pageCurveFromLedgerTicks S_BH N peak = S_BH / 2
  exact pageCurve_peak S_BH N peak hN hpeak hbal

theorem nontrivialPageCurveProp_holds : nontrivialPageCurveProp := by
  refine ⟨2, 1, 2, le_refl 2, by norm_num, by norm_num, by norm_num,
    ⟨nontrivialReadout 2 (by norm_num) 2 (by norm_num)⟩, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · exact pageCurveFromLedgerTicks_at_zero 2 2 (by norm_num) (by norm_num)
  · exact pageCurveFromLedgerTicks_at_full 2 2 (by norm_num) (by norm_num)
  · exact pageCurve_peak 2 2 1 (by norm_num) (by norm_num) (by norm_num)
  · rw [pageCurveFromLedgerTicks_at_zero 2 2 (by norm_num) (by norm_num),
        pageCurve_peak 2 2 1 (by norm_num) (by norm_num) (by norm_num)]
    norm_num
  · rw [pageCurveFromLedgerTicks_at_full 2 2 (by norm_num) (by norm_num),
        pageCurve_peak 2 2 1 (by norm_num) (by norm_num) (by norm_num)]
    norm_num
  · intro m n hmn hn
    exact pageCurve_mono_rise 2 (by norm_num) 2 m n (by norm_num) hmn hn
  · intro m n hhalf hmn hnN
    exact pageCurve_anti_fall 2 (by norm_num) 2 m n (by norm_num) hhalf hmn hnN

/-- **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⟩

/-- The nontrivial readout peaks at `S_BH / 2` at the half-evaporation tick. -/
theorem nontrivialReadout_peak
    (S_BH : ℝ) (hS : 0 ≤ S_BH) (N peak : ℕ) (hN : 0 < N)
    (hpeak : 0 < peak) (hbal : 2 * peak = N) :
    (nontrivialReadout S_BH hS N hN).radiationEntropyAtTick peak = S_BH / 2 := by
  show pageCurveFromLedgerTicks S_BH N peak = S_BH / 2
  exact pageCurve_peak S_BH N peak hN hpeak hbal

What this page does not claim

The theorem does not derive the capacity-transfer law from a Hamiltonian. The theorem does not assert that any observed black hole follows this exact curve. The theorem does not prove information preservation for all possible evaporation processes.

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: