BranchRegularOnNotDeficitSumCertificate
plain-language theorem explainer
Packages the S4+S9 separation certificate: at three interior Wick-arc parameters (mixed and pure hinges), the product of Cayley–Menger cofactors is a negative real outside the slit plane, so the product-form complex square root is branch-killed. Gravity residual auditors cite it to show a branch-regular-on lookalike is not a deficit-sum closer. The body is a pure Prop conjunction of three numeric cofactor identities.
Claim. The following hold simultaneously: (i) the mixed three-two crossing $t_\star^{\mathrm{mix}}\in(0,1)$ has $C_{11}C_{44}=-40\notin\mathbb{C}\setminus(-\infty,0]$ on the Wick-continued edges; (ii) at $t=2/3\in(0,1)$ the same three-two family has $C_{11}C_{22}=-48$ off the slit plane; (iii) the four-one crossing $t_\star\in(0,1)$ has $C_{33}C_{44}=-32$ off the slit plane. Thus product-form $\sqrt{C_{pp}C_{qq}}$ is kernel-killed at these interior arc points.
background
Module Wave C4 R0 banks gap-6 lookalike separation certificates after the F3 close of wick_action_continuation_4d_v2. Each certificate records that a tempting decoy holds on its own terms yet fails to supply the Lorentzian 4d action bound (domain mismatch, V1 kill, or distinct closer).
Causal 4-simplices come in two CDT types: four-one (four vertices on slice $t$, one on $t+1$) and three-two (three and two). Squared edges are Wick-continued by continuationEdgesC: timelike edges follow the arc, spacelike edges stay $a^2$. Complex Cayley–Menger cofactors $C_{r,c}$ are the bordered $6\times 6$ minors used to build dihedral data and the product-form square root that would feed a deficit sum.
The named interior parameters are exact crossings: $t_\star=1-\arccos(1/3)/\pi$ on the four-one hinge and $t_\star^{\mathrm{mix}}=1-\arccos(5/12)/\pi$ on the mixed three-two product form. The slit-plane membership tests detect when $C_{pp}C_{qq}$ lands on the branch cut.
proof idea
Definitional Prop only: no proof obligations here. The body is the conjunction of three blocks, each asserting an open-interval membership for an arc parameter, an equality of a product of two cmCofactorC values on continuationEdgesC for the indicated CausalPentType, and that the resulting negative real lies outside Complex.slitPlane. Numeric targets are $-40$ (three-two at $t_\star^{\mathrm{mix}}$, indices 1,4), $-48$ (three-two at $2/3$, indices 1,2), and $-32$ (four-one at $t_\star$, indices 3,4). The inhabiting theorem later discharges the Prop by citing the memorialized product-form kill and the product-form crossing lemmas.
why it matters
Fills the S4+S9 slot in the gap-6 lookalike receipt: product-form $\mathrm{csqrt}(C_{pp}C_{qq})$ is killed at interior arc parameters, so a branch-regular-on reading cannot serve as a deficit-sum closer for the 4d Wick action. Downstream, the theorem branchRegularOnNotDeficitSumCertificate inhabits this Prop, and the DAG residual TypedResidual_gap6_lookalike_decoys_fail conjoins it with the other separation certificates (3d continuation, 4d kinematical, hinge-data, cm4-sign). After F3, gap-6 is closed via the V2 ledger; this certificate remains as post-close separation so a renamed lookalike cannot be mistaken for the action-level bound. Sits in the SevenGaps gravity stack that feeds the continuum EH limit, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.