module module

`IndisputableMonolith.Gravity.SevenGaps.ThreePentInteriorHingeWitness`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.GluedPentsHingeWitness module_import

declarations in this module (20)

def pentA L82
def pentB L85
def pentC L88
def threePentComplex L91
def tets L95
def linkVerts L100
def linkEdges L106
def linkDegree L111
theorem pents_are_distinct_foursimplices L119
theorem pairwise_shared_tets L127
theorem pairwise_shared_tets_unique L138
theorem triple_intersection L149
theorem residual_edges L155
theorem linkVerts_eq L162
theorem linkEdges_eq L167
theorem linkEdges_eq_pent_residues L173
theorem linkDegrees L179
theorem threePent_hinge_is_interior L189
theorem hinge_link_is_cycle L196
theorem threePent_minimality L205