Gravity Page Curve Nontrivial Nontrivial Page Curve One Statement

A page curve that actually rises

A Page curve describes how the entropy of a black hole's radiation changes as the hole evaporates. The expected shape is a rise to a peak at half-evaporation, then a fall back to zero. That shape matters because it encodes whether information escapes. Earlier framework work had proved the shape theorems but only on a trivial process with no peak. The declaration nontrivial_page_curve_one_statement closes that gap: it proves, for any positive tick budget, that a genuine process exists whose entropy readout starts at zero, peaks at half-evaporation with value S_BH/2, and returns to zero at full evaporation.

In plain terms, the theorem constructs a concrete model with two independent bulk and two independent radiation states. The tick, the basic step of evolution, is a reversible linear operator. The entropy readout is not assigned ad hoc; it is derived from a capacity-transfer law that links bulk and radiation capacities. The proof is machine-checked in the framework's library of formal theorems, with no unproved axioms. This means the rise/peak/fall shape is not an assumption but a forced consequence of the model's structure.

What the declaration does not claim is just as important. It does not derive the capacity-transfer law from a microscopic recognition Hamiltonian; that remains open. It does not claim that this model is the physical black hole; it is a mathematical proof of existence within the framework. The theorem removes a specific defect, the degenerate witness, but it does not close the frontier of deriving capacities from first principles.

/-- **NONTRIVIAL PAGE CURVE ONE-STATEMENT.**  A nondegenerate Page process on
`Fin 2 ⊗ Fin 2` exists; its derived entropy readout starts at zero, peaks at
`S_BH/2` at half-evaporation, returns to zero, rises monotonically before the
peak and falls monotonically after it, and the master-theorem Page hypothesis
is inhabited by the strong witness. -/
theorem nontrivial_page_curve_one_statement :
    nontrivialPageCurveProp ∧
    Nonempty (OperatorPageEntropyReadout (Fin 2) (Fin 2)) ∧
    Nonempty Gravity.MasterTheorem.PageCurveDerived :=
  ⟨nontrivialPageCurveProp_holds,
   ⟨nontrivialReadout 2 (by norm_num) 2 (by norm_num)⟩,
   ⟨nontrivialPageCurveDerivedWitness⟩⟩

/-- **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 recognition Hamiltonian. The model is not claimed to be the physical black hole. The theorem does not prove uniqueness of the Page curve shape.

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: