pairwise_shared_tets_unique
plain-language theorem explainer
Each adjacent pair among three 4-simplices on six vertices shares exactly one tetrahedral face: the 4-subset families of A and B meet only at {0,1,2,4}, of B and C only at {0,1,2,5}, and of A and C only at {0,1,2,3}. Anyone building the three-pent interior-hinge witness cites this uniqueness. The proof is a pure kernel decide on finite set equalities.
Claim. Let $A=\{0,1,2,3,4\}$, $B=\{0,1,2,4,5\}$, $C=\{0,1,2,3,5\}$ be 4-simplices in the vertex set $\mathrm{Fin}\,6$. Then the family of 4-element subsets of $A$ intersects that of $B$ in exactly $\{\{0,1,2,4\}\}$; likewise $B\cap C$ yields exactly $\{\{0,1,2,5\}\}$ and $A\cap C$ yields exactly $\{\{0,1,2,3\}\}$.
background
This module builds the minimal cyclic hinge link for Regge-style discrete gravity in the Recognition Science seven-gaps program. Three 4-simplices ("pents") sit on vertex set $\mathrm{Fin},6$, each containing the fixed hinge triangle ${0,1,2}$ imported from the two-pent witness: $A={0,1,2,3,4}$, $B={0,1,2,4,5}$, $C={0,1,2,3,5}$.
Face-to-face gluing means each adjacent pair shares a tetrahedron of four vertices that still contains the hinge. The 4-element powerset of a pent enumerates its candidate tetrahedral faces; intersecting two such families isolates the shared faces. The companion statement that those intersections are nonempty is the non-unique listing; the present result sharpens each intersection to a singleton.
The local setting is the positive half of panel P1-remainder live bet C12: a complex whose hinge link is a genuine cycle, complementing the counting lemma that three pents are necessary for an interior hinge.
proof idea
One-line term proof by decide. All three pents are concrete finite subsets of Fin 6, so the 4-element powersets, their pairwise intersections, and equality to the named singletons are fully decidable propositions in the Lean kernel. No algebraic lemmas are invoked; the decision procedure exhausts the finite combinatorics.
why it matters
Uniqueness of the shared tetrahedra is the face-to-face half of the three-pent gluing story. Together with the non-unique pairwise listing and the triple-intersection theorem (triple meet equals the hinge triangle), it certifies that the three pents wrap cleanly around ${0,1,2}$ and nothing more.
That clean wrap is required before residual link edges can be identified with the triangle cycle $3-4-5-3$, before every link vertex has degree two, and before the hinge can be declared a genuine interior hinge via the imported cyclic-link predicate. The module then closes minimality: any complex presenting the hinge as interior needs at least three pents, and this complex attains the bound.
In the broader gravity stack this is scaffolding for whether glued-pent expressions may be called Regge action. No downstream consumers are wired yet in the graph; the declaration is a local structural gate inside the three-pent witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.