module module

`IndisputableMonolith.Gravity.PageCurveNontrivial`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

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

IndisputableMonolith.Gravity.MasterTheoremUnconditional module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.PageCurveDynamical module_import
IndisputableMonolith.Gravity.PageCurveOperatorEntropy module_import

declarations in this module (20)

theorem evapFrac_nonneg L61
theorem evapFrac_mono L66
theorem evapFrac_le_half L73
theorem evapFrac_ge_half L82
theorem evapFrac_le_one L91
theorem evapFrac_eq_half L99
theorem pageCurve_mono_rise L111
theorem pageCurve_anti_fall L125
theorem pageCurve_peak L136
def nontrivialReadout L150
theorem nontrivialReadout_zero L163
theorem nontrivialReadout_full L169
theorem nontrivialReadout_peak L175
def nontrivialPageCurveProp L192
theorem nontrivialPageCurveProp_holds L208
def nontrivialPageCurveDerivedWitness L228
structure NontrivialPageCurveCert L237
def nontrivialPageCurveCert L249
theorem nontrivialPageCurveCert_inhabited L255
theorem nontrivial_page_curve_one_statement L263