module module high

`IndisputableMonolith.Gravity.PageCurveDynamical`

Defines the dynamical Page curve for black-hole evaporation in Recognition gravity: bulk and radiation Hilbert-space entropy capacities as linear functions of the evaporation fraction, with their sum fixed by unitarity. Supplies the triangular Page curve (Schmidt min) and the recognition-tick lift used as the Track 3.C master-theorem witness. Anyone citing the discrete Page-capacity transfer or operator-derived Page entropy depends on this module.

claimAt evaporation fraction $t\in[0,1]$, bulk capacity is $S_{\mathrm{bulk}}(t)=(1-t)S_{\mathrm{BH}}$ and radiation capacity is $S_{\mathrm{rad}}(t)=t\,S_{\mathrm{BH}}$, so $S_{\mathrm{bulk}}(t)+S_{\mathrm{rad}}(t)=S_{\mathrm{BH}}$. The Page curve is the unitary envelope $S_{\mathrm{Page}}(t)=\min\{S_{\mathrm{bulk}}(t),S_{\mathrm{rad}}(t)\}$. The same capacities are realized from discrete recognition-ledger tick counts.

background

Track 3.C of the quantum-gravity master plan asks for a Page curve that is not merely kinematic but dynamical: entropy capacities that evolve with evaporation and still obey unitarity. The structural sibling module fixes the kinematic form; this module supplies the time-dependent capacities.

Bulk capacity decreases linearly from the initial black-hole entropy $S_{\mathrm{BH}}$ at $t=0$ to zero at complete evaporation $t=1$. Radiation capacity does the opposite. Their sum is invariant, which is the ledger expression of unitary information conservation. The observed Page curve is the Schmidt-capacity minimum of the two branches, yielding the classic triangular shape.

Upstream, MacroscopicLedger gives the Hilbert carrier on which these capacities live, and MasterTheorem states the conditional master claim that consumes a Page witness. Recognition ticks convert continuous $t$ into discrete ledger steps so the same curve can be fed to the master theorem without continuum hypotheses.

proof idea

The module is largely definitional plus elementary real analysis. Bulk and radiation capacities are defined as affine maps in the evaporation fraction; endpoint lemmas check the boundary values $S_{\mathrm{BH}}$ and $0$. The capacity-sum identity is a one-line algebraic cancellation. The Page curve is the pointwise minimum of the two capacities (unitarity envelope). A second layer maps discrete recognition-ledger tick counts to an evaporation fraction and pushes the same capacities and Page curve through that map, producing the tick-native witness consumed downstream.

why it matters in Recognition Science

This is the dynamical half of Track 3.C. Downstream, PageCurveOperatorEntropy records that this module "ships the triangular Page curve as a Schmidt-capacity min and supplies the master-theorem witness via pageCurveDerivedWitness_recognitionTicks." PageCurveNontrivial uses that witness to close referee F3 (nontrivial Page process). MasterTheoremHandoffIntegration lists Fork D as the "discrete recognition-tick Page-capacity transfer," and MasterTheoremUnconditional routes the zero-argument master theorem through the same Page input. Without these capacities, the master theorem has no unitary Page curve to cite.

scope and limits

Does not derive $S_{\mathrm{BH}}$ from microstate counting; treats it as an input scale.
Does not prove semiclassical Hawking dynamics; only the unitary capacity envelope.
Does not address firewalls, islands, or bulk reconstruction beyond Schmidt capacities.
Does not close the full master theorem alone; only the Page-curve input leg.
Does not claim continuum QFT entanglement entropy equals the ledger tick capacities.

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.MasterTheoremHandoffIntegration module_import
IndisputableMonolith.Gravity.MasterTheoremUnconditional module_import
IndisputableMonolith.Gravity.PageCurveNontrivial module_import
IndisputableMonolith.Gravity.PageCurveOperatorEntropy module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.MacroscopicLedger module_import
IndisputableMonolith.Gravity.MasterTheorem module_import
IndisputableMonolith.Gravity.PageCurveStructural module_import

declarations in this module (84)

def bulkCapacity L86
def radiationCapacity L90
theorem bulkCapacity_at_zero L92
theorem bulkCapacity_at_one L96
theorem radiationCapacity_at_zero L100
theorem radiationCapacity_at_one L105
theorem capacity_sum_invariant L112
def pageCurveFromUnitarity L121
def evaporationFractionFromTicks L128
def bulkCapacityFromTicks L131
def radiationCapacityFromTicks L135
def pageCurveFromLedgerTicks L140
theorem radiationCapacityFromTicks_eq_radiationCapacity L145
theorem bulkCapacityFromTicks_eq_bulkCapacity L153
theorem tick_capacity_sum_invariant L164
theorem radiationCapacityFromTicks_next L173
theorem bulkCapacityFromTicks_next L185
theorem pageCurveFromLedgerTicks_eq_pageCurveFromUnitarity L201
theorem pageCurveFromLedgerTicks_at_zero L210
theorem pageCurveFromLedgerTicks_at_full L223
theorem pageCurveFromLedgerTicks_at_page_fraction L237
abbrev BulkLedger L251
abbrev HawkingRadiationLedger L256
abbrev BulkRadiationLedger L261
structure PageTickUnitary L272
theorem tick_injective L284
theorem tick_surjective L290
def identityPageTickUnitary L299
theorem pageTickUnitary_inhabited L307
def stateAfterOperatorTicks L313
theorem stateAfterOperatorTicks_zero L320
theorem stateAfterOperatorTicks_succ L326
structure OperatorPageProcess L340
def stateAtTick L354
theorem stateAtTick_zero L358
theorem stateAtTick_succ L362
def evaporationFractionAtTick L368
theorem radiationCapacityAtTick_eq L371
theorem bulkCapacityAtTick_eq L376
theorem capacityAtTick_sum_invariant L382
theorem pageCurveAtTick_eq_unitarity_curve L388
structure OperatorPageEntropyReadout L400
theorem radiationEntropyAtTick_zero L412
theorem radiationEntropyAtTick_full L417
theorem radiationEntropyAtTick_page_fraction L422
def canonicalOperatorPageEntropyReadout L435
def operator_level_page_process_structural_prop L450
theorem operator_level_page_process_structural_prop_holds L453
structure PageCurveOperatorProcessCert L458
def pageCurveOperatorProcessCert L475
theorem pageCurveOperatorProcessCert_inhabited L483
theorem operator_page_process_interface_one_statement L494
theorem pageCurveFromUnitarity_at_zero L515
theorem pageCurveFromUnitarity_at_one L521
theorem pageCurveFromUnitarity_at_half L530
theorem pageCurveFromUnitarity_phase1 L540
theorem pageCurveFromUnitarity_phase2 L551
theorem pageCurveFromUnitarity_nonneg L560
theorem information_preservation L574
theorem pageCurveFromUnitarity_mono_phase1 L579
theorem pageCurveFromUnitarity_anti_mono_phase2 L590
structure PageCurveDynamicalProcess L618
def canonicalProcess L633
theorem S_rad_at_zero L646
theorem S_rad_at_one L649
theorem S_rad_at_page_time L655
theorem S_rad_information_returned L659
theorem S_rad_phase1 L662
theorem S_rad_phase2 L668
theorem S_rad_nonneg L674
theorem S_rad_mono_phase1 L681
theorem S_rad_anti_mono_phase2 L688
def page_curve_derived_dynamical_prop L703
theorem page_curve_derived_dynamical_prop_holds L710
def pageCurveDerivedWitness_dynamical L724
def recognition_tick_capacity_transfer_prop L735
theorem recognition_tick_capacity_transfer_prop_holds L749
def page_curve_derived_from_recognition_ticks_prop L765
theorem page_curve_derived_from_recognition_ticks_prop_holds L768
def pageCurveDerivedWitness_recognitionTicks L774

… and 4 more