branchRegular_threeTwo_mixed_pair
plain-language theorem explainer
For mixed opposite pairs on the (3,2) causal 4-simplex, the class-B branch certificate holds on the open Wick arc: both Cayley-Menger cofactors stay off the slit plane and the split cosine stays off the arccos cuts. Gravity/QG workers cite it when discharging the six mixed hinges at the physical point a=α=1. The proof tracks imaginary parts of 8z−4 and 6z−2 along zArc, places both square roots in Q1, and invokes the mixed cosine path identity.
Claim. Let $p,q\in\{0,1,2,3,4\}$. Suppose the Cayley-Menger cofactors of the complex hinge edge matrix satisfy $C_{pp}(z)=8z-4$, $C_{qq}(z)=6z-2$, and $C_{pq}(z)=-1$ for all $z\in\mathbb{C}$. Then the Wick-continued edge data of the $(3,2)$ causal 4-simplex at the physical point $a=1$, $\alpha=1$ is branch-regular for the opposite pair $(p,q)$ on the open parameter interval $(0,1)$: both principal cofactors lie in the slit plane and the dihedral cosine stays off the arccos branch cuts.
background
Lane B2 of the QG Seven-Gaps campaign treats all-hinge complex-first Wick continuation of the $(3,2)$ causal 4-simplex. Vertices split into a lower triple ${0,1,2}$ and upper pair ${3,4}$; the six cross edges are the timelike ones. Opposite pairs fall into three classes. Mixed pairs (one lower, one upper vertex) give the six hinges with two timelike triangle edges; their closed cofactor forms are asymmetric: $C_{pp}=8z-4$ on the lower member, $C_{qq}=6z-2$ on the upper member, and $C_{pq}=-1$, with squared area $z/4-1/16$.
Branch regularity on an open set means both principal cofactors avoid the nonpositive real axis (so principal square roots are holomorphic) and the split dihedral cosine $-C_{pq}/(\sqrt{C_{pp}}\sqrt{C_{qq}})$ avoids the arccos cuts $\mathbb{R}\setminus(-1,1)$. The continuation path is the canonical upper-half-plane arc $z_{\mathrm{Arc}}(t)$ of the complex-first Wick action, restricted here to the open interior $t\in(0,1)$ where $\mathrm{Im},z_{\mathrm{Arc}}(t)>0$.
Closed cofactor identities are kernel-checked by explicit $5\times5$ minors against the executed per-hinge trace table. The physical edge map continuationEdgesC at type threeTwo with $a=\alpha=1$ reduces to the hinge edge matrix evaluated on $z_{\mathrm{Arc}}$.
proof idea
Fix $t\in(0,1)$. Positivity of $\mathrm{Im},z_{\mathrm{Arc}}(t)$ is immediate from the arc lemma. Imaginary parts of the two principal cofactors expand as $\mathrm{Im}(8z-4)=8,\mathrm{Im},z$ and $\mathrm{Im}(6z-2)=6,\mathrm{Im},z$, both strictly positive. After rewriting the physical continuation edges via the threeTwo identity, each cofactor lands in the slit plane by the imaginary-part criterion.
For the cosine, the mixed-path identity equates the dihedral cosine to $-1/(\sqrt{8z-4},\sqrt{6z-2})$. Both square roots lie in the open first quadrant (positive imaginary part of the radicand), so their product has strictly positive imaginary part by the Q1-product lemma. Negating the reciprocal of a number with positive imaginary part keeps the result off the real axis, hence off the arccos cuts. The three conjuncts assemble into branch regularity.
why it matters
This is the single parametric engine for all six mixed hinges of the $(3,2)$ simplex. Downstream one-line specializations discharge pairs $(0,3)$, $(0,4)$, $(1,3)$, $(1,4)$, $(2,3)$, and $(2,4)$ by plugging in the corresponding closed cofactor lemmas. Together with the spacelike and upper-pair classes, they complete the split-form branch certificate for every triangular hinge at the physical point, which is the second deliverable of lane B2 in the finishing charter.
In the broader Recognition gravity stack this feeds the complex-first Wick continuation of Regge-type hinge actions: without branch regularity the dihedral angles cannot be continued off the Lorentzian section, and the Euclidean-to-Lorentzian matching of the executed arc trace fails. The result is interior-only by design; endpoint cut contact is handled separately for the spacelike hinge and is allowed under the gate. No open scaffolding remains on this lemma itself: it is fully proved and only consumes already-certified cofactor polynomials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.