Gravity Page Curve Nontrivial Page Curve Anti Fall

The falling half of the Page curve

A Page curve describes how the entropy of a black hole and its radiation changes as the hole evaporates. The standard picture, named after Don Page, has three phases: entropy starts at zero, climbs to a peak at the halfway point of evaporation, and then falls back to zero as the last of the hole disappears. The falling half matters because it encodes information preservation: if entropy never returned to zero, radiation would carry less information than the original hole held.

The theorem pageCurve_anti_fall proves the falling half for a specific discrete model. In this model, time advances in ticks, and the evaporated fraction is a ratio of ticks passed to total ticks. The theorem states: for any nonnegative starting entropy, any positive tick budget, and any two tick counts m and n with m before n but both after the halfway point, the entropy at n is no greater than the entropy at m. In plain terms, once past the peak, entropy never rises again; it only falls or stays flat.

The proof rests on a monotonicity property of the underlying unitarity-based readout. The model's entropy readout is not an ad-hoc assignment but is derived from a capacity transfer law: the entropy at any tick is the smaller of the bulk capacity and the radiation capacity. After the halfway point, the radiation capacity dominates, and the bulk capacity shrinks monotonically as evaporation proceeds. The theorem chains the evaporation-fraction monotonicity with the capacity-transfer law to deliver the anti-monotonicity of the readout.

In Recognition Science, this theorem is part of a larger effort to supply a nontrivial witness for the Page-curve master theorem. Earlier witnesses were degenerate: they had no interior peak and identically zero entropy. This work constructs a process on a two-by-two state space with a genuine rise, peak, and fall, and proves the full shape for an arbitrary positive tick budget. The anti-fall theorem is the post-peak half of that shape.

What the theorem does not claim is as important as what it proves. It does not derive the capacity-transfer law from a microscopic Hamiltonian; that derivation remains open. It does not claim that the model's entropy values match measured black-hole radiation, which has never been observed. It establishes a structural property of a discrete, reversible tick process, not a physical prediction about real black holes.

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

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

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

What this page does not claim

The theorem does not derive the capacity-transfer law from a microscopic Hamiltonian. The theorem does not assert that real black holes follow this exact entropy curve. The theorem does not claim the model's entropy values match any measured radiation.

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: