module module

`IndisputableMonolith.Holography.RecognitionMultiplicity`

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

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.RecognitionLedgerFloor module_import
IndisputableMonolith.Holography.CoefficientBridge module_import
IndisputableMonolith.Holography.PixelGluedPlaquette module_import

declarations in this module (19)

def cellLedger L99
def recognitionMultiplicity L106
theorem recognitionMultiplicity_eq L112
def dominoLeftClosed L125
def dominoRightClosed L129
def dominoLocalMap L134
def dominoRank L138
def dominoNullity L142
theorem dominoRank_eq_two L145
theorem dominoNullity_eq_four L147
theorem domino_image_times_kernel L151
theorem multiplicity_eq_rank_one L161
theorem multiplicity_eq_rank_two L167
theorem multiplicity_ne_nullity_two L177
theorem bekenstein_selector_derived L191
theorem coefficient_is_one_quarter_derived L200
def target_recognition_multiplicity L209
theorem target_recognition_multiplicity_holds L219
theorem recognitionMultiplicityCert L224