cof32_34
plain-language theorem explainer
For every complex z, the Cayley-Menger cofactor C_{3,4} of the (3,2) two-value edge tuple equals -1. Mixed-hinge certificates on the Wick arc cite this constant off-diagonal entry when building the split cosine C_pq / sqrt(C_pp C_qq). The proof multiplies the odd cofactor sign by a unit 5x5 minor determinant and simplifies.
Claim. For every $z \in \mathbb{C}$, the complex Cayley-Menger cofactor $C_{3,4}$ of the bordered $6\times 6$ matrix built from the threeTwo edge tuple (spacelike squared lengths $1$, timelike squared lengths $z$) equals $-1$.
background
Lane B2 of the QG Seven-Gaps campaign continues all ten triangular hinges of the threeTwo causal 4-simplex along the complex-first Wick arc. Edges are the two-value tuple hingeEdges32C z: timelike cross edges carry z, spacelike edges carry 1. The bordered 6x6 Cayley-Menger matrix of that tuple is written out explicitly by cmMatrixC_hingeEdges32.
Cofactors are the usual signed 5x5 minors: cmCofactorC multiplies cmMinorC by the sign (-1)^{r+c} (cmCofactorSignC). Mixed opposite pairs (one lower-slice vertex, one upper-slice vertex) are predicted to have constant off-diagonal cofactor $C_{pq}=-1$, with asymmetric diagonals $C_{pp}=8z-4$ and $C_{qq}=6z-2$. Indices $(3,4)$ in Fin 6 are one such mixed pair; the corresponding minor is named submatrix32_34 / minor32_34C, and det_minor32_34C already records that its determinant is identically 1.
proof idea
Term-mode proof by unfolding and rewriting. Expand the cofactor into sign times minor. Replace the abstract CM matrix by the explicit hinge matrix (cmMatrixC_hingeEdges32), identify the deleted submatrix with submatrix32_34, and insert det_minor32_34C so the minor equals 1. The sign clause is the odd case: $3+4=7$ is not even, so cmCofactorSignC 3 4 = -1 by decide. A final ring yields $(-1)\cdot 1=-1$.
why it matters
Closes the off-diagonal cofactor slot for mixed pair $(2,3)$ (hinge $(0,1,4)$) in the per-hinge table of the module doc. Downstream, branchRegular32_pair23 feeds this constant together with the two diagonal cofactors into branchRegular_threeTwo_mixed_pair, certifying that the split cosine stays off the arccos cut on the open Wick interval. boundary32_pair23 reuses the same triple to pin continuous endpoint values of the cosine path on $[0,1]$. Together these discharge one of the six mixed-hinge rows required for the all-hinge branch and boundary certificates of the (3,2) simplex under the finishing charter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.