triple_intersection
plain-language theorem explainer
The triple intersection of the three 4-simplices in the minimal interior-hinge complex equals the shared hinge triangle and nothing more. Anyone citing the three-pent cyclic hinge witness, link-cycle identification, or interior-hinge minimality needs this face identity. The proof is a one-line kernel decision on concrete finite sets.
Claim. Let $A=\{0,1,2,3,4\}$, $B=\{0,1,2,4,5\}$, and $C=\{0,1,2,3,5\}$ be the three 4-simplices on vertex set $\mathrm{Fin}\,6$, and let the hinge triangle be $H=\{0,1,2\}$. Then $A \cap B \cap C = H$.
background
In the SevenGaps gravity stack, glued-pent expressions may be called Regge action only when the hinge link is a genuine cycle (panel P1-remainder, live bet C12). The committed two-pent path witness already proves three pents are necessary for an interior hinge. This module supplies the matching positive half: a minimal complex whose hinge link is a cycle.
The complex lives on six vertices. The hinge is the triangle ${0,1,2}$. Each pent is a 4-simplex containing that triangle plus a residual pair: $A$ adds ${3,4}$, $B$ adds ${4,5}$, $C$ adds ${3,5}$. Adjacent pairs share exactly one tetrahedron containing the hinge ($A\cap B={0,1,2,4}$, and cyclic). The present identity closes the gluing picture: the common triple face is exactly the hinge, so the three pents wrap the hinge and nothing more.
proof idea
The three pents and the hinge are concrete finite subsets of a six-element type. Equality of finite sets is decidable, so the kernel tactic decide checks $A \cap B \cap C = {0,1,2}$ by exhaustive computation. No algebraic lemmas or inductive arguments are used; it is a pure finite check.
why it matters
This identity is a structural brick of the three-pent interior hinge witness. Together with the pairwise shared-tet lemmas, it lets the module identify the hinge link as the triangle cycle $3\text{—}4\text{—}5\text{—}3$, prove every link vertex has degree two, and conclude the hinge is a genuine interior hinge (threePent_hinge_is_interior, hinge_link_is_cycle). Combined with the counting lemma that any interior presentation needs at least three pents, the complex attains the lower bound and is therefore the minimal interior-hinge configuration.
That positive gate is what authorizes treating glued-pent expressions as Regge action in the SevenGaps program. No external used_by edges are recorded yet; consumers sit in the same module as later cycle and minimality theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.