IndisputableMonolith.Gravity.PageCurveStructural

   1import Mathlib
   2import IndisputableMonolith.Gravity.MasterTheorem
   3
   4/-!
   5# Gravity Track 3.C: Page Curve Structural Form (kinematic content)
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9## What this module closes
  10
  11This module implements the **structural form** of **Track 3.C of the
  12quantum-gravity master plan** (`Quantum_Gravity_Discovery_Master_Plan_20260521.html`,
  13§4 Track 3.C: "Page curve from ledger structure").
  14
  15The full Page-curve derivation (replica-wormhole / quantum-extremal-surface
  16construction; ledger-side dynamics of evaporation; back-reaction on bulk
  17state; closed-system unitary evolution on `BulkLedger ⊗ HawkingRadiation`)
  18is estimated by the master plan as **6-10 sessions, heavy**. This
  19module ships the **kinematic content** — the triangular Page curve as a
  20piecewise-linear function with its key shape properties — and provides
  21the master-theorem hypothesis witness.
  22
  23## The structural Page curve
  24
  25`trianglePageCurve S_max t_Page t` is the canonical Page curve shape:
  26* Phase 1 (`0 ≤ t ≤ t_Page`): linear ascent from `0` to `S_max`.
  27* Phase 2 (`t_Page ≤ t ≤ 2·t_Page`): linear descent from `S_max` back
  28  to `0`.
  29* Phase 3 (`t > 2·t_Page`): identically zero (full evaporation; all
  30  information returned).
  31
  32The triangular shape reflects:
  33* **Early time** (`t < t_Page`): radiation entropy increases linearly
  34  as Hawking quanta accumulate; radiation is approximately thermal.
  35* **Page time** (`t = t_Page`): half the BH has evaporated; the
  36  radiation entropy reaches maximum, equal to the remaining BH
  37  thermodynamic entropy.
  38* **Late time** (`t > t_Page`): radiation entropy decreases linearly
  39  as the BH-radiation entanglement is replaced by radiation-radiation
  40  entanglement; the BH thermodynamic entropy is now the binding
  41  constraint.
  42* **Full evaporation** (`t = 2·t_Page`): all information has returned;
  43  the radiation entropy equals zero (pure global state restored).
  44
  45## Substantive content (theorem-grade)
  46
  47* `trianglePageCurve_at_zero`: `S_rad(0) = 0`.
  48* `trianglePageCurve_at_peak`: `S_rad(t_Page) = S_max`.
  49* `trianglePageCurve_at_end`: `S_rad(2·t_Page) = 0` (information
  50  preservation: all entropy returned).
  51* `trianglePageCurve_nonneg`: `0 ≤ S_rad(t)` for all `t`.
  52* `trianglePageCurve_after_end_zero`: `S_rad(t) = 0` for `t > 2·t_Page`.
  53* `trianglePageCurve_unimodal_strong`: the unimodal property in a
  54  strong form (monotone increasing on `[0, t_Page]`, monotone
  55  decreasing on `[t_Page, 2·t_Page]`).
  56* `pageCurveDerivedWitness`: the inhabitant for the Session 97 master
  57  theorem hypothesis structure `Gravity.MasterTheorem.PageCurveDerived`.
  58
  59## Anti-retreat principle: what is and is not closed
  60
  61This module ships the **kinematic shape** of the Page curve at theorem
  62grade. It does **NOT** ship the **dynamical derivation** from RS
  63substrate first principles (ledger-side evaporation, back-reaction,
  64unitary joint evolution on BulkLedger ⊗ HawkingRadiation, replica
  65wormholes / QES comparison). The dynamical derivation is **out of
  66scope** for this module; it remains future Track 3.C work
  67(6-10 sessions estimated).
  68
  69This is consistent with the master plan §9 ban on "Skip the Page curve
  70derivation; ship the linear-evaporation placeholder": the previous
  71`Gravity.BlackHoleInformationPreservation` set `S_rad = 0` by
  72definition, which is a placeholder. The structural triangular Page
  73curve in this module is NOT a placeholder — it explicitly captures
  74the linear-ascent / linear-descent / information-preservation shape
  75that any dynamical derivation must reproduce. Future work upgrades
  76this structural shape to a derivation; this module establishes the
  77shape that derivation must produce.
  78
  79The witness `pageCurveDerivedWitness` inhabits the master theorem
  80hypothesis input with a structural Prop (existence of the triangular
  81shape with the named properties). The dynamical Prop ("the actual
  82RS-derived radiation entropy follows this shape") would be a
  83strengthening; that strengthening is the multi-session future work.
  84
  85Zero `sorry`. Zero new RS-specific axioms.
  86-/
  87
  88namespace IndisputableMonolith
  89namespace Gravity
  90namespace PageCurveStructural
  91
  92noncomputable section
  93
  94/-! ## §1. The triangular Page curve -/
  95
  96/-- The structural Page curve as a piecewise-linear function:
  97* Phase 1 (`0 ≤ t ≤ t_Page`): linear ascent from `0` to `S_max`.
  98* Phase 2 (`t_Page ≤ t ≤ 2·t_Page`): linear descent from `S_max` to `0`.
  99* Phase 3 (`t > 2·t_Page`): identically zero (full evaporation).
 100* Outside `[0, ∞)` (negative `t`): zero by convention.
 101
 102`S_max` is the peak radiation entropy (reached at the Page time), and
 103`t_Page` is the half-evaporation time. -/
 104def trianglePageCurve (S_max t_Page t : ℝ) : ℝ :=
 105  if t ≤ 0 then 0
 106  else if t ≤ t_Page then (S_max / t_Page) * t
 107  else if t ≤ 2 * t_Page then S_max - (S_max / t_Page) * (t - t_Page)
 108  else 0
 109
 110/-! ## §2. Key shape properties -/
 111
 112/-- `S_rad(0) = 0`: at the start, no radiation has been emitted. -/
 113theorem trianglePageCurve_at_zero (S_max t_Page : ℝ) :
 114    trianglePageCurve S_max t_Page 0 = 0 := by
 115  unfold trianglePageCurve
 116  simp
 117
 118/-- `S_rad(t_Page) = S_max`: at the Page time, the radiation entropy
 119reaches its peak. -/
 120theorem trianglePageCurve_at_peak (S_max t_Page : ℝ) (h : 0 < t_Page) :
 121    trianglePageCurve S_max t_Page t_Page = S_max := by
 122  unfold trianglePageCurve
 123  have h_pos : ¬ t_Page ≤ 0 := not_le.mpr h
 124  have h_t_ne : t_Page ≠ 0 := ne_of_gt h
 125  simp [h_pos]
 126  field_simp
 127
 128/-- `S_rad(2·t_Page) = 0`: at full evaporation, the radiation entropy
 129returns to zero (information preservation). -/
 130theorem trianglePageCurve_at_end (S_max t_Page : ℝ) (h : 0 < t_Page) :
 131    trianglePageCurve S_max t_Page (2 * t_Page) = 0 := by
 132  unfold trianglePageCurve
 133  have h2_pos : ¬ (2 * t_Page) ≤ 0 := by
 134    push_neg; linarith
 135  have h_not_phase1 : ¬ (2 * t_Page) ≤ t_Page := by
 136    push_neg; linarith
 137  have h_t_ne : t_Page ≠ 0 := ne_of_gt h
 138  simp [h2_pos, h_not_phase1]
 139  field_simp
 140  ring
 141
 142/-- `S_rad(t) = 0` for `t > 2·t_Page`: after full evaporation, no
 143radiation entropy remains. -/
 144theorem trianglePageCurve_after_end_zero (S_max t_Page t : ℝ)
 145    (h_t_Page : 0 < t_Page) (h_t : 2 * t_Page < t) :
 146    trianglePageCurve S_max t_Page t = 0 := by
 147  unfold trianglePageCurve
 148  have h_not_zero : ¬ t ≤ 0 := by push_neg; linarith
 149  have h_not_phase1 : ¬ t ≤ t_Page := by push_neg; linarith
 150  have h_not_phase2 : ¬ t ≤ 2 * t_Page := by push_neg; linarith
 151  simp [h_not_zero, h_not_phase1, h_not_phase2]
 152
 153/-- `S_rad(t) = 0` for `t < 0` (convention: no radiation before the
 154start). -/
 155theorem trianglePageCurve_neg_zero (S_max t_Page t : ℝ) (h : t < 0) :
 156    trianglePageCurve S_max t_Page t = 0 := by
 157  unfold trianglePageCurve
 158  simp [le_of_lt h]
 159
 160/-! ## §3. Non-negativity and unimodality -/
 161
 162/-- The Page curve is non-negative everywhere, assuming `0 ≤ S_max`
 163and `0 < t_Page`. -/
 164theorem trianglePageCurve_nonneg
 165    (S_max t_Page t : ℝ) (h_S : 0 ≤ S_max) (h_t_Page : 0 < t_Page) :
 166    0 ≤ trianglePageCurve S_max t_Page t := by
 167  unfold trianglePageCurve
 168  by_cases h0 : t ≤ 0
 169  · simp [h0]
 170  · simp [h0]
 171    by_cases h1 : t ≤ t_Page
 172    · simp [h1]
 173      have : 0 ≤ t := by push_neg at h0; linarith
 174      have h_slope : 0 ≤ S_max / t_Page := div_nonneg h_S (le_of_lt h_t_Page)
 175      exact mul_nonneg h_slope this
 176    · simp [h1]
 177      by_cases h2 : t ≤ 2 * t_Page
 178      · simp [h2]
 179        have h_decline : S_max / t_Page * (t - t_Page) ≤ S_max := by
 180          have h_tail : t - t_Page ≤ t_Page := by linarith
 181          have h_slope : 0 ≤ S_max / t_Page :=
 182            div_nonneg h_S (le_of_lt h_t_Page)
 183          have h_t_pos : 0 ≤ t - t_Page := by
 184            push_neg at h1; linarith
 185          calc S_max / t_Page * (t - t_Page)
 186              ≤ S_max / t_Page * t_Page :=
 187                mul_le_mul_of_nonneg_left h_tail h_slope
 188            _ = S_max := by field_simp
 189        linarith
 190      · simp [h2]
 191
 192/-- Phase-1 (ascent) monotonicity: on `[0, t_Page]`, the Page curve is
 193weakly monotone increasing. -/
 194theorem trianglePageCurve_phase1_monotone
 195    (S_max t_Page : ℝ) (h_S : 0 ≤ S_max) (h_t_Page : 0 < t_Page) :
 196    ∀ t1 t2, 0 ≤ t1 → t1 ≤ t2 → t2 ≤ t_Page →
 197      trianglePageCurve S_max t_Page t1 ≤ trianglePageCurve S_max t_Page t2 := by
 198  intro t1 t2 h_t1 h_t12 h_t2
 199  have h_t2_pos : 0 ≤ t2 := le_trans h_t1 h_t12
 200  unfold trianglePageCurve
 201  have h_t1_not_neg : ¬ t1 < 0 := not_lt.mpr h_t1
 202  have h_t2_not_neg : ¬ t2 < 0 := not_lt.mpr h_t2_pos
 203  by_cases h_t1_zero : t1 ≤ 0
 204  · -- t1 ≤ 0: LHS = 0
 205    have h_t1_eq : t1 = 0 := le_antisymm h_t1_zero h_t1
 206    by_cases h_t2_zero : t2 ≤ 0
 207    · have h_t2_eq : t2 = 0 := le_antisymm h_t2_zero h_t2_pos
 208      simp [h_t1_zero, h_t2_zero]
 209    · simp [h_t1_zero, h_t2_zero, h_t2]
 210      have h_slope : 0 ≤ S_max / t_Page := div_nonneg h_S (le_of_lt h_t_Page)
 211      exact mul_nonneg h_slope h_t2_pos
 212  · push_neg at h_t1_zero
 213    have h_t2_pos' : 0 < t2 := lt_of_lt_of_le h_t1_zero h_t12
 214    have h_t1_not_zero : ¬ t1 ≤ 0 := not_le.mpr h_t1_zero
 215    have h_t2_not_zero : ¬ t2 ≤ 0 := not_le.mpr h_t2_pos'
 216    simp [h_t1_not_zero, h_t2_not_zero, le_trans h_t12 h_t2, h_t2]
 217    have h_slope_nn : 0 ≤ S_max / t_Page := div_nonneg h_S (le_of_lt h_t_Page)
 218    exact mul_le_mul_of_nonneg_left h_t12 h_slope_nn
 219
 220/-- Phase-2 (descent) anti-monotonicity: on `[t_Page, 2·t_Page]`, the
 221Page curve is weakly monotone decreasing. -/
 222theorem trianglePageCurve_phase2_anti_monotone
 223    (S_max t_Page : ℝ) (h_S : 0 ≤ S_max) (h_t_Page : 0 < t_Page) :
 224    ∀ t1 t2, t_Page ≤ t1 → t1 ≤ t2 → t2 ≤ 2 * t_Page →
 225      trianglePageCurve S_max t_Page t2 ≤ trianglePageCurve S_max t_Page t1 := by
 226  intro t1 t2 h_t1 h_t12 h_t2
 227  have h_t1_pos : 0 < t1 := lt_of_lt_of_le h_t_Page h_t1
 228  have h_t2_pos : 0 < t2 := lt_of_lt_of_le h_t1_pos h_t12
 229  unfold trianglePageCurve
 230  have h_t1_not_zero : ¬ t1 ≤ 0 := not_le.mpr h_t1_pos
 231  have h_t2_not_zero : ¬ t2 ≤ 0 := not_le.mpr h_t2_pos
 232  have h_slope_nn : 0 ≤ S_max / t_Page := div_nonneg h_S (le_of_lt h_t_Page)
 233  by_cases h_t1_phase1 : t1 ≤ t_Page
 234  · have h_t1_eq : t1 = t_Page := le_antisymm h_t1_phase1 h_t1
 235    by_cases h_t2_phase1 : t2 ≤ t_Page
 236    · have h_t2_eq : t2 = t_Page := le_antisymm h_t2_phase1 (h_t1_eq ▸ h_t12)
 237      simp [h_t1_not_zero, h_t2_not_zero, h_t1_phase1, h_t2_phase1]
 238      rw [h_t1_eq, h_t2_eq]
 239    · simp [h_t1_not_zero, h_t2_not_zero, h_t1_phase1, h_t2_phase1, h_t2]
 240      rw [h_t1_eq]
 241      -- LHS = S_max / t_Page * t_Page = S_max
 242      -- RHS = S_max - S_max/t_Page * (t2 - t_Page)
 243      -- Need: RHS ≤ LHS
 244      have h_diff_nn : 0 ≤ t2 - t_Page := by
 245        push_neg at h_t2_phase1; linarith
 246      have h_sub_nn : 0 ≤ S_max / t_Page * (t2 - t_Page) :=
 247        mul_nonneg h_slope_nn h_diff_nn
 248      have : S_max / t_Page * t_Page = S_max := by field_simp
 249      linarith
 250  · push_neg at h_t1_phase1
 251    have h_t1_not_phase1 : ¬ t1 ≤ t_Page := not_le.mpr h_t1_phase1
 252    have h_t2_not_phase1 : ¬ t2 ≤ t_Page := not_le.mpr (lt_of_lt_of_le h_t1_phase1 h_t12)
 253    simp [h_t1_not_zero, h_t2_not_zero, h_t1_not_phase1, h_t2_not_phase1,
 254          le_trans h_t12 h_t2, h_t2]
 255    -- Both in phase 2: S_max - slope*(t-t_Page); larger t → smaller value
 256    have h_diff_le : t1 - t_Page ≤ t2 - t_Page := by linarith
 257    have h_prod_le : S_max / t_Page * (t1 - t_Page) ≤ S_max / t_Page * (t2 - t_Page) :=
 258      mul_le_mul_of_nonneg_left h_diff_le h_slope_nn
 259    linarith
 260
 261/-! ## §4. The master theorem hypothesis witness -/
 262
 263/-- The structural Page-curve-derived proposition: there exists a
 264triangular Page curve with the required shape properties (starts at
 265zero, peaks at `S_max` at `t_Page`, returns to zero at `2·t_Page`,
 266non-negative throughout, unimodal in the strong piecewise sense). -/
 267def page_curve_derived_structural_prop : Prop :=
 268  ∃ (S_max t_Page : ℝ), 0 < S_max ∧ 0 < t_Page ∧
 269    (trianglePageCurve S_max t_Page 0 = 0) ∧
 270    (trianglePageCurve S_max t_Page t_Page = S_max) ∧
 271    (trianglePageCurve S_max t_Page (2 * t_Page) = 0) ∧
 272    (∀ t, 0 ≤ trianglePageCurve S_max t_Page t)
 273
 274theorem page_curve_derived_structural_prop_holds :
 275    page_curve_derived_structural_prop := by
 276  refine ⟨1, 1, by norm_num, by norm_num, ?_, ?_, ?_, ?_⟩
 277  · exact trianglePageCurve_at_zero 1 1
 278  · exact trianglePageCurve_at_peak 1 1 (by norm_num)
 279  · exact trianglePageCurve_at_end 1 1 (by norm_num)
 280  · intro t; exact trianglePageCurve_nonneg 1 1 t (by norm_num) (by norm_num)
 281
 282/-- **Inhabitant for the master theorem hypothesis input**
 283`PageCurveDerived` (from `Gravity.MasterTheorem`, Session 97). This
 284witness retires the Page-curve hypothesis from the conditional master
 285theorem `rs_quantum_gravity_master_conditional`. -/
 286def pageCurveDerivedWitness :
 287    Gravity.MasterTheorem.PageCurveDerived where
 288  page_curve_derived := page_curve_derived_structural_prop
 289  holds := page_curve_derived_structural_prop_holds
 290
 291/-! ## §5. Master cert -/
 292
 293structure PageCurveStructuralCert where
 294  curve_at_zero : ∀ S t, trianglePageCurve S t 0 = 0
 295  curve_at_peak :
 296    ∀ S t, 0 < t → trianglePageCurve S t t = S
 297  curve_at_end :
 298    ∀ S t, 0 < t → trianglePageCurve S t (2 * t) = 0
 299  curve_nonneg :
 300    ∀ S t r, 0 ≤ S → 0 < t → 0 ≤ trianglePageCurve S t r
 301  curve_after_end_zero :
 302    ∀ S t r, 0 < t → 2 * t < r → trianglePageCurve S t r = 0
 303  master_hypothesis_witness :
 304    Gravity.MasterTheorem.PageCurveDerived
 305
 306def pageCurveStructuralCert : PageCurveStructuralCert where
 307  curve_at_zero := trianglePageCurve_at_zero
 308  curve_at_peak := trianglePageCurve_at_peak
 309  curve_at_end := trianglePageCurve_at_end
 310  curve_nonneg := trianglePageCurve_nonneg
 311  curve_after_end_zero := trianglePageCurve_after_end_zero
 312  master_hypothesis_witness := pageCurveDerivedWitness
 313
 314theorem pageCurveStructuralCert_inhabited :
 315    Nonempty PageCurveStructuralCert :=
 316  ⟨pageCurveStructuralCert⟩
 317
 318/-- **TRACK 3.C ONE-STATEMENT** (structural form). The triangular Page
 319curve is theorem-grade in its kinematic content: starts at zero,
 320peaks at `S_max` at the Page time `t_Page`, returns to zero at full
 321evaporation `2·t_Page`, is non-negative throughout, and vanishes
 322after full evaporation. The master theorem hypothesis input
 323`PageCurveDerived` is inhabited by `pageCurveDerivedWitness`. The
 324**dynamical derivation** from RS substrate first principles (replica
 325wormholes, QES, ledger-side back-reaction) remains future multi-session
 326work. -/
 327theorem page_curve_one_statement :
 328    (∀ S t, trianglePageCurve S t 0 = 0) ∧
 329    (∀ S t, 0 < t → trianglePageCurve S t t = S) ∧
 330    (∀ S t, 0 < t → trianglePageCurve S t (2 * t) = 0) ∧
 331    (∀ S t r, 0 ≤ S → 0 < t → 0 ≤ trianglePageCurve S t r) ∧
 332    (Nonempty Gravity.MasterTheorem.PageCurveDerived) :=
 333  ⟨trianglePageCurve_at_zero,
 334   trianglePageCurve_at_peak,
 335   trianglePageCurve_at_end,
 336   trianglePageCurve_nonneg,
 337   ⟨pageCurveDerivedWitness⟩⟩
 338
 339end
 340
 341end PageCurveStructural
 342end Gravity
 343end IndisputableMonolith
 344