Gravity Page Curve Nontrivial Nontrivial Readout Zero

The zero point of the Page curve

The Page curve describes how the entropy of radiation emitted by an evaporating black hole changes over time. The curve rises as the black hole radiates, peaks at the halfway point of evaporation, and then falls back to zero when the black hole is gone. This shape is a standard expectation from quantum information theory: the radiation starts out with no information about the black hole's interior, becomes maximally entangled at the midpoint, and ends with all the information carried away in the radiation.

The theorem nontrivialReadout_zero proves the starting point of this curve. It states that for any positive tick budget, the radiation entropy readout at the very first tick is exactly zero. In plain terms, before any evaporation has happened, the emitted radiation carries no entropy. This is the formal anchor for the intuitive statement that a black hole's radiation begins in a pure, zero-entropy state.

This result matters because it closes a gap in the framework's earlier work. A previous construction of the Page curve used a degenerate process that never actually rose or fell; its entropy was zero at every tick. That witness satisfied the formal requirements but did not represent a real Page curve. The new theorem is part of a package that builds a genuinely nontrivial process, one with two independent bulk and radiation states, and proves the full rise-peak-fall shape for it. The zero at the start is the first of those proven properties.

In Recognition Science, the framework models the evaporation as a discrete ledger of recognition events, where each tick is a reversible linear operation on a two-state system. The entropy readout is not assigned by hand; it is derived from a capacity-transfer law that governs how information moves from the bulk to the radiation. The theorem nontrivialReadout_zero is a theorem in the machine-checked library of formal theorems, proved with no unproven assumptions and no framework-specific axioms.

What the theorem does not claim is equally important. It does not say that the entropy readout is zero at any later tick, nor does it say that the capacity-transfer law itself is derived from a microscopic Hamiltonian. That derivation remains open. The theorem also does not claim that the process is physical in the sense of matching a specific observed black hole; it is a mathematical construction that satisfies the formal requirements of a Page curve.

/-- The nontrivial readout's entropy starts at zero. -/
theorem nontrivialReadout_zero
    (S_BH : ℝ) (hS : 0 ≤ S_BH) (N : ℕ) (hN : 0 < N) :
    (nontrivialReadout S_BH hS N hN).radiationEntropyAtTick 0 = 0 :=
  (nontrivialReadout S_BH hS N hN).radiationEntropyAtTick_zero

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⟩

What this page does not claim

The theorem does not claim the entropy readout is zero at any tick other than the first. The theorem does not claim the capacity-transfer law is derived from a microscopic Hamiltonian; that derivation remains open. The theorem does not claim the process matches a specific observed black hole.

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: