module module

`IndisputableMonolith.Holography.RecordMonotonicity`

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.Holography.LocalRecognitionHorizonCut module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Holography.CellInjection module_import

declarations in this module (44)

def recordFlux L90
def recordWeight L94
theorem recordFlux_eq_weight_sub L99
theorem recordFlux_self L121
def cellPotential L126
def stepHeatCell L129
theorem faceRecord_length L131
theorem stepHeatCell_eq_potential L134
def pathHeatCell L139
theorem books_balance L148
theorem no_free_erasure L159
theorem erasure_exports_debit L166
def RecordMonotone L173
theorem recordMonotone_of_no_export L179
def gaugeRel L191
theorem gaugeRel_equivalence L196
theorem gauge_step_zero_heat L200
theorem silent_iff_kernel L209
theorem mem_recordKernel_iff L213
theorem gauge_iff_kernel_record L218
theorem gauge_iff_kernel L225
def RecordCompatible L234
def CreatesFreeRecord L240
theorem recordCompatible_iff_no_free_record L245
def runProtocol L255
theorem no_protocol_separates L261
def Separated L274
theorem gauge_never_separated L279
def gaugeSetoid L286
def PhysState L290
def physState L293
def physRecord L296
theorem physRecord_mk L299
theorem weak_complementarity L306
theorem physRecord_mem_image L313
theorem physRecord_surjective_on_records L321
theorem physState_records_card L329
theorem holographic_bound_of_weak_comp L337
def KernelIsGauge L348
theorem weak_complementarity_of_gsl L355
theorem kernelIsGauge_falsifier L364
def target_record_monotonicity L377
theorem target_record_monotonicity_holds L387
theorem recordMonotonicityCert L392