Cm4SignNotActionLevelCertificate
plain-language theorem explainer
S3 separation certificate: the three-pent Cayley–Menger sign fact (cm4 < 0 on each induced pent for all a > 0 and α ≥ 0) is packaged with a trivial arithmetic witness so it cannot be read as action-level Wick continuation. Gravity auditors cite it when checking that gap6 lookalikes stay separated from the V2 close. The Prop is a pure conjunction; the companion theorem discharges it via threePent_lorentzian_cm4_neg and norm_num.
Claim. The proposition that (i) for every scale $a > 0$ and every $\alpha \ge 0$, the sign-normalized 4-simplex Cayley–Menger determinant of the squared-edge data induced on each of the three pent charts $A$, $B$, $C$ is strictly negative, and (ii) $\neg(7/12 < 0)$.
background
Gap6 in the SevenGaps campaign is the 4D Wick action-continuation claim, closed by wick_action_continuation_4d_v2. This module (Wave C4 R0) retains lookalike mathematics that a later session might mis-promote into the ledger terminal, and packages each lookalike with a post-close separation certificate: the lookalike holds, yet a witness shows it would not have sufficed for the V2 close.
Here cm4 is the sign-normalized 4-simplex Cayley–Menger determinant on a 10-tuple of squared edge lengths: cm4 > 0 on non-degenerate Euclidean 4-simplices, with cm4 = 9216 V^2. The three charts pentAVert, pentBVert, pentCVert embed the faces $A={0,1,2,3,4}$, $B={0,1,2,4,5}$, $C$ into the global 6-vertex complex; inducedSqEdges pulls back the causal squared-length assignment at scale $a$ and parameter $\alpha$ onto each chart.
The first conjunct is therefore a pure sign fact on those three induced pents. The second conjunct is a trivial true arithmetic statement used as the post-close separation marker.
proof idea
Definition only: the body is the Prop itself, a conjunction of a universal sign statement and a trivial arithmetic negation. No tactics run here. The companion theorem cm4SignNotActionLevelCertificate proves the Prop by pairing threePent_lorentzian_cm4_neg (the three-pent Lorentzian cm4 < 0 lemma) with a one-line norm_num discharge of $\neg(7/12 < 0)$.
why it matters
Earns its place as the S3 arm of the gap6 lookalike-falsify residual. Downstream, the theorem of the same name (camelCase) inhabits this Prop, and TypedResidual_gap6_lookalike_decoys_fail conjoins it with the other separation certificates (3D continuation, 4D kinematical continuation, hinge-data, branch-regular, etc.) so the DAG residual records that lookalikes are separated by content from the V2 ledger close.
Doc-comment binding: per-pent cm4 < 0 holds for all $\alpha \ge 0$, including outside CertV2's causal range (witness $\alpha = 0$), so the sign fact alone would not have closed wick_action_continuation_4d_v2. That is the honesty patch after F3 succession (gap6 closed via V2): obsolete "gap6 stays false" conjuncts are replaced by post-close-compatible separation. No direct T0–T8 landmark; this is gravity-side ledger hygiene around the Wick action continuation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.