IndisputableMonolith.Gravity.PageCurveDynamical · Recognition explainer

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