module module

`IndisputableMonolith.Holography.CoefficientBridge`

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 (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Holography.RecognitionMultiplicity module_import
IndisputableMonolith.Holography.RecordCostAsymmetry module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Holography.EdgeSectorBridge module_import
IndisputableMonolith.Holography.RecognitionEventCapacity module_import

declarations in this module (16)

def closureRank L59
def freeBits L62
def rawBits L66
theorem closureRank_eq_one L68
theorem freeBits_eq_three L70
theorem rawBits_eq_four L72
theorem rank_nullity_add L76
theorem closure_image_times_kernel L81
def target_coefficient_bridge L88
theorem target_coefficient_bridge_holds L97
theorem coefficient_of_multiplicity L106
theorem bekenstein_branch L111
theorem kappa_four_thirds_branch L117
def selector_multiplicity_is_closure_rank L126
theorem bekenstein_of_selector L132
theorem single_event_entropy_eq_H L141