Gravity Page Curve Structural Page Curve Structural Cert Inhabited

The certified curve

The Page curve describes how the entropy of radiation emitted by an evaporating black hole changes over time. In the standard account, the curve rises linearly as the black hole radiates, peaks when half the black hole has evaporated, then falls linearly back to zero as the remaining information is released. This triangular shape is a central expectation in quantum gravity, where it resolves the information paradox by showing that information is not lost.

The declaration pageCurveStructuralCert_inhabited is a theorem in the framework's machine-checked library of formal theorems. It proves that a certificate object exists, one that packages the essential shape properties of the Page curve: it starts at zero, reaches a peak value at the Page time, returns to zero at twice the Page time, stays non-negative throughout, and vanishes after full evaporation. The certificate also provides a witness that satisfies the structural hypothesis required by the framework's master theorem on quantum gravity.

In Recognition Science, this result establishes the kinematic content of the Page curve as theorem-grade. The shape is not a placeholder; it is a precisely defined piecewise-linear function with proven properties. However, the certificate does not derive this shape from the framework's deeper principles. The dynamical derivation, which would explain how the ledger structure of recognition events produces this curve through evaporation dynamics, back-reaction, and unitary evolution, remains future work estimated at six to ten sessions.

What this means practically is that the framework now has a rigorously established target shape. Any future dynamical derivation must reproduce this triangular curve. The certificate acts as a constraint and a goal, not as an explanation of why the curve has this form. It is a structural theorem about a mathematical function, not a physical derivation from first principles.

theorem pageCurveStructuralCert_inhabited :
    Nonempty PageCurveStructuralCert :=
  ⟨pageCurveStructuralCert⟩

theorem pageCurveStructuralCert_inhabited :
    Nonempty PageCurveStructuralCert :=
  ⟨pageCurveStructuralCert⟩

def pageCurveStructuralCert : PageCurveStructuralCert where
  curve_at_zero := trianglePageCurve_at_zero
  curve_at_peak := trianglePageCurve_at_peak
  curve_at_end := trianglePageCurve_at_end
  curve_nonneg := trianglePageCurve_nonneg
  curve_after_end_zero := trianglePageCurve_after_end_zero
  master_hypothesis_witness := pageCurveDerivedWitness

/-- **Inhabitant for the master theorem hypothesis input**
`PageCurveDerived` (from `Gravity.MasterTheorem`, Session 97). This
witness retires the Page-curve hypothesis from the conditional master
theorem `rs_quantum_gravity_master_conditional`. -/
def pageCurveDerivedWitness :
    Gravity.MasterTheorem.PageCurveDerived where
  page_curve_derived := page_curve_derived_structural_prop
  holds := page_curve_derived_structural_prop_holds

What this page does not claim

The theorem does not derive the Page curve from the Recognition Science substrate's first principles. The theorem does not prove that actual black hole radiation entropy follows this triangular shape. The theorem does not establish the dynamical content of the Page curve, such as evaporation dynamics or back-reaction.

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/PageCurveStructural.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: