interior_hinge_needs_three_pents_banked
plain-language theorem explainer
Any collection of 4-simplices whose residual pairs around the fixed hinge triangle form a cyclic link must contain at least three simplices. Gravity and discrete-curvature workers cite it to rule out two-pent “interior hinge” lookalikes. The proof is a one-line re-export of the counting lemma that a cycle needs three edges and image cannot raise cardinality.
Claim. Let $\mathrm{hinge}=\{0,1,2\}\subset\mathrm{Fin}\,6$. For a finite set $\mathcal{P}$ of subsets of $\mathrm{Fin}\,6$, if the residual pairs $\{P\setminus\mathrm{hinge}:P\in\mathcal{P}\}$ form a cyclic link (nonempty 2-edge set in which every incident vertex has degree exactly 2), then $|\mathcal{P}|\ge 3$.
background
This module banks Gap-6 lookalike separation certificates: positive theorems that a decoy construction holds yet fails to discharge the real 4D Wick-action continuation close. The local setting is combinatorial hinge geometry on six labeled vertices, used to model discrete curvature around a shared triangle.
The hinge is the fixed 2-face ${0,1,2}$. Each candidate 4-simplex ("pent") containing that face contributes exactly one residual pair $P\setminus\mathrm{hinge}$, an edge in the link. A cyclic link is the combinatorial model of an interior hinge: a nonempty set of 2-element edges in which every incident vertex has degree exactly two, so the link closes and the angle deficit $2\pi-\sum\theta$ is an interior curvature quantity.
Upstream, the counting lemma states that any cyclic link needs at least three edges, and the image map $P\mapsto P\setminus\mathrm{hinge}$ cannot increase cardinality, so at least three pents are required for a genuine interior hinge.
proof idea
One-line term wrapper: apply the upstream theorem interior_hinge_needs_three_pents to the same pents and cycle hypothesis. That lemma itself is le_trans of (i) a cycle-link needs $\ge 3$ edges and (ii) Finset.card_image_le on the residual-pair map. No extra arithmetic or case split is introduced here; the banked name is only a re-export into the Gap-6 receipt module.
why it matters
Feeds the S6 kill certificate twoPentNotInteriorActionCertificate, which packages that a two-pent complex cannot present an interior hinge together with this $\ge 3$ lower bound. In the Wave C4 Gap-6 residual DAG, that separation shows the two-pent lookalike does not supply the interior-hinge structure needed for a 4D action-level close of wick_action_continuation_4d_v2.
Within Recognition gravity scaffolding, interior curvature on glued simplices is the discrete stand-in for Einstein–Hilbert content; forcing three (not two) 4-simplices around a hinge is the minimal combinatorial gate before any continuum or Lorentzian continuation claim. The result is proved with no sorry and sits as a banked positive theorem retained after Gap-6 closed, so later ledger renames can cite a stable name without reopening the counting argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.