module module

`IndisputableMonolith.Gravity.SevenGaps.GluedPentsHingeWitness`

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.Gravity.SevenGaps.ThreePentInteriorHingeWitness module_import

declarations in this module (30)

def pentA L90
def pentB L93
def sharedTet L96
def hinge L99
def twoPentComplex L102
def tets L106
def hingeTets L110
def linkVerts L115
def linkEdges L120
def linkDegree L125
theorem pents_are_distinct_foursimplices L132
theorem shared_face_data L138
theorem shared_tets_unique L145
theorem hingeTets_eq L153
theorem hingeTets_card_and_shared L160
theorem pentA_hinge_tets L165
theorem pentB_hinge_tets L171
theorem boundary_tets_belong_to_one_pent L178
theorem linkVerts_eq L190
theorem linkEdges_eq L195
theorem linkEdges_eq_pent_residues L202
theorem link_edges_chain_through_shared L210
theorem linkDegrees L218
def IsPathLinkOn L225
theorem hinge_link_is_path L235
def IsCycleLink L243
theorem cycleLink_three_edges L253
theorem interior_hinge_needs_three_pents L312
theorem twoPent_hinge_never_interior L321
theorem hinge_link_not_cycle L330