Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.ThreePentInteriorHingeWitness

show as:
view Lean formalization →

Combinatorial witness for the minimal three-pent complex with a genuine interior hinge: three 4-simplices whose pairwise tetrahedron gluings produce a cyclic link rather than a path. Gravity and discrete-Regge workers cite it as the combinatorial half of gap6-a (W3-2). The module builds the complex by explicit vertex sets, checks distinctness and unique pairwise shared tets, and records the triple intersection and link degree.

claimThere exist three distinct 4-simplices $P_A,P_B,P_C$ on a finite vertex set such that each pair shares exactly one tetrahedron, the three shared tetrahedra meet in a common interior hinge (triangle or edge as specified by the link), and the dual link of that hinge is a cycle of length three rather than a path.

background

In the SevenGaps gravity campaign, a "pent" is a 4-simplex. Gluing two pents along a tetrahedron yields a path-shaped dual link (the upstream GluedPentsHingeWitness): that configuration is not yet an interior hinge in the Regge sense, because the deficit angle does not close around a bulk edge.

An interior hinge requires at least three 4-simplices arranged so their dual link is a cycle. This module supplies the smallest such complex: three labeled pents (vertex sets built from ${0,1,2,3,4}$ and residual pairs), the list of tetrahedra, the link vertices and edges, and the link degree.

The local setting is pure combinatorics of simplicial complexes. No metric, no edge lengths, and no curvature assignment appear here; those are deferred to the causal-consistency layer.

proof idea

Definition-and-lemma module, not a single deep proof. It names three concrete 4-simplices pentA, pentB, pentC, assembles threePentComplex, and extracts tets, linkVerts, linkEdges, and linkDegree. Short lemmas then discharge: the three pents are distinct 4-simplices; each pair shares a unique tetrahedron; the triple intersection is the expected hinge skeleton; and the dual link is a 3-cycle. All arguments are finite enumeration on fixed vertex labels, inheriting the two-pent path witness as the pairwise building block.

why it matters in Recognition Science

Closes the combinatorial half of gap6-a / Wave-3 lane W3-2: existence of a minimal genuine interior hinge. Downstream, ThreePentCausalConsistency imports this module and supplies an admissible causal edge-length assignment on the same complex, exactly the missing piece named in the honest-scope clause ("consistent causal edge lengths around the cycle"). Together they gate whether three-pent expressions may enter the discrete Regge action with a bulk deficit. In the broader RS gravity stack this is the smallest bulk hinge on which curvature and causal structure can be tested before scaling to larger triangulations.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (20)