module module

`IndisputableMonolith.Holography.CellInjection`

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

declarations in this module (28)

abbrev CellCfg L77
def vbit L80
def closedOn L84
def faceRecord L90
def flipv L99
def xorCfg L103
def weight L107
def cell0 L110
def cellComplement L113
def faceFlip L116
theorem single_flip_posts L123
theorem single_flip_posts_three L128
theorem complement_invisible L137
theorem record_not_injective L142
def recordKernel L147
theorem recordKernel_card L150
theorem recordKernel_eq L155
theorem record_image_card L162
theorem record_rank_eq_four L165
theorem record_nullity_eq_four L170
theorem record_image_times_kernel L174
theorem record_blind_only_global L183
theorem face_flip_invisible_everywhere L189
theorem faceFlip_weight L192
theorem invisible_iff_kernel L197
def target_cell_injection L207
theorem target_cell_injection_holds L218
theorem cellInjectionCert L223