module module

`IndisputableMonolith.Verification.Dimension`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Patterns module_import
IndisputableMonolith.RecogSpec.Spec module_import

declarations in this module (13)

def DimensionalRigidityWitness L20
def RSCounting_Gap45_Absolute L28
theorem dimension_is_three L34
theorem onlyD3_satisfies_RSCounting_Gap45_Absolute L41
theorem dimension_three_of_cover_and_sync L50
theorem rs_counting_gap45_absolute_iff_dim3 L58
def H_D2NoLinking L105
def H_D4TrivialLinking L114
def phi L120
theorem phi_fixed_point L122
def hopf_linking_penalty L129
def H_ThreeDimensionalLinkingUnique L135
theorem dimension_three_from_linking_requirement L141