threePentComplex
plain-language theorem explainer
The three-pent complex is the finite set of three 4-simplices on six vertices that all contain a fixed hinge triangle. Anyone working the positive half of the interior-hinge gate (Regge deficit at a genuine interior hinge) cites this as the ambient complex. The body is a three-element set literal built from the named pents.
Claim. Let the three 4-simplices on vertex set $\{0,\ldots,5\}$ be $P_A=\{0,1,2,3,4\}$, $P_B=\{0,1,2,4,5\}$, and $P_C=\{0,1,2,3,5\}$. The three-pent complex is the finite set $\{P_A,P_B,P_C\}$ of maximal simplices.
background
This module supplies the positive half of the interior-hinge gate for glued-pent Regge expressions (panel P1-remainder, live bet C12). The hinge triangle is ${0,1,2}$. Each pent is a 4-simplex containing that hinge, with residual pair the two vertices outside the hinge: $P_A$ residual ${3,4}$, $P_B$ residual ${4,5}$, $P_C$ residual ${3,5}$.
The two-pent module already showed that a path link (boundary hinge) arises from two pents and proved the counting lower bound that any interior hinge needs at least three pents. Here the three pents glue face-to-face: each adjacent pair shares exactly one tetrahedron containing the hinge, and the triple intersection is exactly the hinge triangle.
The complex is presented by its maximal simplices (the three pents). Downstream objects (tetrahedra of the complex, link vertices, link edges) are read off this set by filtering powersets and residual pairs.
proof idea
Pure definition: the complex is the three-element finset whose members are the already-defined pents $P_A$, $P_B$, and $P_C$. No proof obligations; cardinality and membership are immediate from the set literal and are later discharged by decide in the witness theorems.
why it matters
This is the ambient complex for the main positive witness theorems of the module. tets takes all 4-subsets of members of the complex; linkVerts and linkEdges filter vertices and pairs whose union with the hinge lands in those faces or in the complex. The residual identification linkEdges_eq_pent_residues equates link edges with $P\setminus\mathrm{hinge}$ over the complex.
The main cycle theorem threePent_hinge_is_interior asserts that the residual link-edge set satisfies IsCycleLink, so the hinge is a genuine interior hinge (exactly the incidence condition for a Regge deficit $2\pi-\sum\theta$ that closes around the hinge). threePent_minimality packages card $=3$ with the committed lower bound interior_hinge_needs_three_pents, so this configuration attains the bound and is the minimal interior-hinge complex. Together with the two-pent path witness, it gates when glued-pent expressions may be called Regge action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.