threeTwoCosPath_eq_mixed
plain-language theorem explainer
On the Wick arc for a mixed (3,2) hinge, the split dihedral cosine equals -1 over the product of principal square roots of the lower cofactor 8z-4 and the upper cofactor 6z-2. Gravity and QG workers cite it when certifying class-B mixed hinges of the causal 4-simplex. The proof unfolds the split cosine and rewrites with the three cofactor identities plus the physical edge continuation.
Claim. Fix opposite vertices $p,q\in\{0,\ldots,4\}$ of a mixed hinge of the $(3,2)$ causal 4-simplex. Assume that for every complex $z$, the Cayley-Menger cofactors of the hinge edge matrix satisfy $C_{pp}(z)=8z-4$, $C_{qq}(z)=6z-2$, and $C_{pq}(z)=-1$. Then for every real parameter $t$ on the canonical upper-half-plane arc $z=z_{\mathrm{arc}}(t)$, the split-form dihedral cosine equals $-1\big/\bigl(\sqrt{8z-4}\,\sqrt{6z-2}\bigr)$, with principal complex square roots.
background
Lane B2 of the QG Seven-Gaps campaign treats all-hinge complex-first Wick continuation of the $(3,2)$ causal 4-simplex at the physical point $a=1$, $\alpha=1$, along the canonical upper-half-plane arc $z_{\mathrm{arc}}$ of WickActionComplexFirst. Hinges are classified by opposite vertex pairs: mixed pairs (one lower-slice vertex, one upper) have two timelike triangle edges and asymmetric closed cofactors $C_{pp}=8z-4$ (lower), $C_{qq}=6z-2$ (upper), $C_{pq}=-1$, with area-squared $z/4-1/16$.
The split cosine is the dihedral cosine written as numerator over a product of principal square roots of the two principal cofactors (rather than a single square root of a product). For mixed hinges the two radicands have different arguments, so the expression does not collapse to a rational function of $z$. Cofactors are extracted as $5\times 5$ Cayley-Menger minors of the complexified hinge edge matrix, kernel-checked against the per-hinge trace table.
proof idea
Short tactic proof. Unfold the definitions of the mixed-path cosine and of the split dihedral cosine and denominator. Rewrite the edge matrix to the physical $(3,2)$ continuation, then substitute the three parametric cofactor hypotheses: diagonal lower $8z-4$, diagonal upper $6z-2$, off-diagonal $-1$. After substitution the split form is exactly $-1/(\mathrm{csqrt}(8z_{\mathrm{arc}}(t)-4),\mathrm{csqrt}(6z_{\mathrm{arc}}(t)-2))$. No analytic estimates; pure definitional reduction under the closed-form cofactor assumptions.
why it matters
This is the class-B split-form identity for mixed hinges. It feeds two immediate parents in the same module: the interior branch-regularity certificate (both cofactors stay in the open upper half-plane, each principal square root in the open first quadrant, so the cosine stays off the arccos cuts) and the closed-interval boundary continuation (Lorentzian value $\sqrt{6}/24$, Euclidean value $-1/4$). Together those close the mixed-pair half of the all-hinge Wick certificate for the $(3,2)$ simplex under the Seven-Gaps finishing charter. The asymmetric radicands are the structural reason mixed hinges need a genuine two-root split rather than a rational collapse, distinguishing them from the spacelike and upper-pair classes treated elsewhere in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.