module module

`IndisputableMonolith.Holography.HorizonOneSidedCut`

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

declarations in this module (38)

abbrev CutCfg L85
def cutSum L89
def cutClosed L93
def closedSet L99
def spike L107
theorem sum_spike L110
def compA L119
def compB L123
def compAB L127
theorem compA_closed L131
theorem compB_closed L137
theorem compAB_closed L143
def projA L152
def projB L156
def projAB L160
def projSeam L165
theorem card_fun_zmod L168
theorem margA_image_univ L173
theorem margB_image_univ L181
theorem margAB_image_univ L189
theorem margA_card L198
theorem margB_card L203
theorem margAB_card L208
theorem margA_bits L214
theorem margB_bits L218
theorem margAB_bits L222
theorem seam_posted_by_A L231
theorem seam_posted_by_B L243
theorem seam_card L253
theorem seam_identity L264
def HorizonSumsPerSide L277
theorem horizon_record_double_posts_seam L285
theorem severed_edge_seam_is_two L296
theorem kappa_per_pixel_is_four L306
theorem domino_face_capacity L312
def horizon_carries_one_side L326
theorem horizon_carries_one_side_holds L337
theorem horizonOneSidedCutCert L342