module module

`IndisputableMonolith.Holography.LocalRecognitionHorizonCut`

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.RecordFluxStress module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Holography.HorizonClockRate module_import
IndisputableMonolith.Holography.HorizonOneSidedCut module_import
IndisputableMonolith.Holography.RecordMonotonicity module_import

declarations in this module (18)

structure LocalHorizonContext L34
structure LocalCut L44
def bitReadout L50
def exteriorRecord L57
theorem exteriorRecord_length L63
def exteriorPotential L70
def exteriorStepHeat L79
theorem exteriorStepHeat_eq_potential L85
def ExteriorClausius L96
theorem exterior_record_potential_clausius L102
def exteriorPathHeat L108
theorem exterior_books_balance L116
theorem exteriorStepHeat_zero_of_same_projection L133
def ofExteriorReading L151
theorem horizonRecord_eq_joint_plus_seam L162
theorem oneSided_horizonRecord_ne_joint_marginal L172
theorem clockRateBundle L186
theorem euclideanPeriod_isLeast_for_context L195