Encyclopedia Gravity Gravity Page Curve Nontrivial Nontrivial Readout Full

ARTICLE 3 claims 3 theorems

Gravity Page Curve Nontrivial Nontrivial Readout Full

A machine-checked theorem proves that a model black hole's radiation entropy starts at zero, peaks at half its maximum, and returns to zero at full evaporation.

Verify this page

The full evaporation readout

The Page curve describes how the entropy of radiation emitted by an evaporating black hole changes over time. It starts at zero, rises to a maximum at the halfway point, and then falls back to zero when the black hole has completely evaporated. This shape matters because it encodes whether information is preserved during evaporation.

The declaration nontrivialReadout_full is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes the final point of that curve: for any positive number of evaporation ticks, the radiation entropy at the last tick is exactly zero. In plain terms, once the black hole is gone, the radiation carries no additional entropy beyond what it already had, which is the information-preservation condition.

The theorem is part of a larger package that proves the full shape. The same module shows the entropy starts at zero, rises monotonically before the halfway tick, peaks at exactly S_BH / 2 (half the black hole's initial entropy), and falls monotonically after. The readout is not assigned by hand; it is derived from a capacity-transfer law between bulk and radiation states, itself a proved theorem.

In Recognition Science, the framework models this process with a discrete ledger of recognition events, where each tick is a reversible linear operation on a two-state system. The theorem holds for any nonnegative real initial entropy S_BH and any positive integer tick budget N, so it is not a special-case construction.

What the theorem does not claim is equally important. It does not derive the capacity-transfer law from a microscopic Hamiltonian on the joint ledger; that remains open. It also does not claim that the model matches actual astrophysical black holes, only that the mathematical structure satisfies the Page-curve shape within the framework's axioms.

THEOREM nontrivialReadout_full · IndisputableMonolith/Gravity/PageCurveNontrivial.lean
nontrivialReadout_full · IndisputableMonolith/Gravity/PageCurveNontrivial.lean:168 
/-- The nontrivial readout's entropy returns to zero at full evaporation. -/
theorem nontrivialReadout_full
    (S_BH : ℝ) (hS : 0 ≤ S_BH) (N : ℕ) (hN : 0 < N) :
    (nontrivialReadout S_BH hS N hN).radiationEntropyAtTick N = 0 :=
  (nontrivialReadout S_BH hS N hN).radiationEntropyAtTick_full
THEOREM nontrivialReadout_zero · pageCurve_mono_rise · nontrivialReadout_peak · pageCurve_anti_fall · IndisputableMonolith/Gravity/PageCurveNontrivial.lean
nontrivialReadout_zero · IndisputableMonolith/Gravity/PageCurveNontrivial.lean:162 
/-- 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
pageCurve_mono_rise · IndisputableMonolith/Gravity/PageCurveNontrivial.lean:109 
/-- **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)
nontrivialReadout_peak · IndisputableMonolith/Gravity/PageCurveNontrivial.lean:174 
/-- 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
pageCurve_anti_fall · IndisputableMonolith/Gravity/PageCurveNontrivial.lean:122 
/-- **Monotone fall (post-peak segment).**  On the segment where the smaller
index is already past half-evaporation (`N ≤ 2 * m`) the discrete ledger
Page curve is monotone non-increasing in the emitted-tick count. -/
theorem pageCurve_anti_fall
    (S_BH : ℝ) (hS : 0 ≤ S_BH) (N m n : ℕ) (hN : 0 < N)
    (hhalf : N ≤ 2 * m) (hmn : m ≤ n) (hnN : n ≤ N) :
    pageCurveFromLedgerTicks S_BH N n ≤ pageCurveFromLedgerTicks S_BH N m := by
  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_anti_mono_phase2 S_BH _ _ hS
    (evapFrac_ge_half N m hN hhalf) (evapFrac_mono N m n hmn) (evapFrac_le_one N n hN hnN)
THEOREM nontrivialPageCurveDerivedWitness · IndisputableMonolith/Gravity/PageCurveNontrivial.lean
nontrivialPageCurveDerivedWitness · IndisputableMonolith/Gravity/PageCurveNontrivial.lean:225 
/-- **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 derive the capacity-transfer law from a microscopic Hamiltonian. The model does not claim to match observed astrophysical black hole radiation. The entropy readout is defined for this discrete model, not for general quantum gravity.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND