HingeDataNotActionLevelCertificate
plain-language theorem explainer
Separation certificate packaging single-simplex hinge continuation (branch regularity and cosine paths for all opposite pairs on both causal 4-simplex types) together with failure of continuity of the deficit-weighted Wick action path on the closed unit interval. Gravity auditors cite it to keep hinge-level data from being renamed into the action-level ledger target. The body is a pure Prop conjunction, not a proved theorem.
Claim. The proposition that for every pair of distinct vertices of a 4-simplex, both the $(4,1)$ and $(3,2)$ Wick edge continuations are branch-regular on $(0,1)$, the corresponding split cosine paths are continuous on $[0,1]$ and equal $-1/4$ at the Euclidean endpoint $t=1$, and yet the deficit-weighted Regge action path at parameter $\alpha=1$ fails to be continuous on $[0,1]$.
background
Module Wave C4 R0 packages post-close separation certificates for gap-6 lookalikes: each lookalike holds as mathematics, yet a witness shows it does not discharge (and would not have sufficed for) the action-level target closed by wick_action_continuation_4d_v2.
Causal 4-simplices in 4d CDT come in two types between adjacent slices: $(4,1)$ (four vertices on slice $t$, one on $t+1$) and $(3,2)$ (three and two). Squared edges continue along the Wick arc via continuationEdgesC: timelike edges follow the complex arc, spacelike edges stay real. Branch regularity on a parameter set means both diagonal Cayley-Menger cofactors stay off the square-root branch cut and the split cosine stays off the arccos cuts.
The cosine paths are the split dihedral cosines of those continued edges for each opposite pair. The action path is the deficit-weighted Regge action (hinge area times $2\pi$ minus the dihedral sum) along the same arc. The doc-comment stresses that hinge-data completeness quantifies only single-simplex opposite pairs and does not inhabit a deficit-weighted three-pent action.
proof idea
Definition only: the Prop is the conjunction of (i) a universal quantification over distinct vertex pairs $p,q\in\mathrm{Fin},5$, requiring for both causal types branch regularity of the continued edges on $(0,1)$, continuity of the cosine path on $[0,1]$, and Euclidean endpoint value $-1/4$, with (ii) the negation of continuity of the deficit-weighted action path at $\alpha=1$ on $[0,1]$. No tactics; the inhabiting theorem later pairs the banked hinge-data completeness result with the V1 action-field unsatisfiability witness.
why it matters
Earns its place as the S2 lookalike separator in the gap-6 residual DAG. Downstream, the theorem of the same name inhabits this Prop by pairing hinge-data continuation completeness with action-path non-continuity at $\alpha=1$. That certificate is then conjoined into the typed residual that records all lookalike decoys failing to match the action-level close.
After F3, gap-6 is closed via the V2 Lorentzian action bound; this certificate keeps hinge-level mathematics from being misread as that close. The doc-comment is explicit: hinge data alone would not have sufficed for the action-level target, which needed Ioc-domain plus cut-limit family assembly. In the broader gravity campaign this is ledger hygiene, not a new dynamical law: it protects the distinction between kinematical hinge continuation and the deficit-weighted three-pent action that feeds the Einstein-Hilbert continuum limit side of the Seven Gaps stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.