TwoPentNotInteriorActionCertificate
plain-language theorem explainer
Packages two combinatorial facts as a single Prop: the two-pentachoron complex has no cyclic edge-link around the shared hinge triangle, and any cyclic hinge link needs at least three pentachora. Gravity/QG auditors cite it as the two-pent decoy kill inside the gap-6 lookalike residual. Pure definitional packaging; the content is proved by the companion theorem.
Claim. The following hold jointly: (i) the edge-link of the two-pentachoron complex around the hinge triangle $\{0,1,2\}$ is not a cycle link (not every incident vertex has degree exactly 2); (ii) for every finite collection of pentachora on vertex set $\mathrm{Fin}\,6$, if the edge-links around that same hinge form a cycle link, then the collection has cardinality at least $3$.
background
Module Wave C4 R0 packages post-close separation certificates for gap-6 lookalikes: each lookalike is true mathematics that nonetheless fails to discharge wick_action_continuation_4d_v2 (domain mismatch, action-field kill, or distinct closer). Gap 6 itself is already closed via the V2 ledger; these certificates keep the decoy mathematics honest.
The hinge is the triangle ${0,1,2}$, a 2-face of the shared tetrahedron in the glued-pents complex. A cycle link is a nonempty set of 2-edges in which every incident vertex has degree exactly 2; that is the combinatorial condition for the link of a triangle to close around the hinge, so the angle deficit $2\pi-\sum\theta$ becomes an interior curvature quantity.
The two-pent complex is the pair of maximal simplices ${\mathrm{pentA},\mathrm{pentB}}$. Its image under $P\mapsto P\setminus\mathrm{hinge}$ is the candidate edge-link around the hinge.
proof idea
Definitional packaging only: the Prop is the conjunction of a negated cycle-link assertion on the two-pent complex and a universal counting lower bound (any cycle link around the hinge forces at least three pentachora). No tactics. The companion theorem twoPentNotInteriorActionCertificate discharges both conjuncts by pairing two_pent_interior_impossible with the banked counting lemma interior_hinge_needs_three_pents_banked.
why it matters
Feeds the gap-6 lookalike residual TypedResidual_gap6_lookalike_decoys_fail, which conjoins several separation certificates so that decoy constructions cannot be mistaken for a V2 action-level close. Parent theorem twoPentNotInteriorActionCertificate is the proved instance of this Prop.
In the Recognition gravity stack this blocks a natural Regge-style decoy: two glued pentachora look like a local 4-simplex fragment, but their hinge link never closes, so they cannot supply interior deficit curvature of the kind needed for a 4d Wick action continuation. The counting half records the minimal three-pent threshold for any genuine interior hinge. Landmark contact is the discrete curvature / action side of the gravity campaign (gap-6 close via wick_action_continuation_4d_v2), not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.