module module

`IndisputableMonolith.Holography.EdgeSectorBridge`

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.CoefficientBridge module_import
IndisputableMonolith.Holography.RecordCostAsymmetry module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Holography.PixelLocal module_import

declarations in this module (9)

def closedConfigs L70
theorem closed_configs_card L75
theorem closed_free_bits L81
def sectorOf L88
theorem sectorOf_mem_admissibleSectors L96
theorem sectorOf_surjective_on_closed L105
theorem sector_is_lossy_quotient_of_closed L115
structure EdgeSectorBridgeCert L127
theorem edgeSectorBridgeCert L133