cof32_35
plain-language theorem explainer
The complex Cayley–Menger cofactor at CM indices (3,5) of the (3,2) two-value edge tuple equals −1 for every complex z. This is the constant off-diagonal cofactor C_pq for the mixed hinge opposite vertices (2,4). Downstream branch-regularity and boundary certificates for that hinge cite it. The proof multiplies the even cofactor sign by an explicit 5×5 minor already reduced to −1.
Claim. For every $z \in \mathbb{C}$, the complex Cayley–Menger cofactor $C_{3,5}$ of the bordered $6\times 6$ matrix built from the (3,2) edge tuple (spacelike edges $1$, timelike edges $z$) equals $-1$.
background
Lane B2 of the QG Seven-Gaps campaign treats all ten triangular hinges of the (3,2) causal 4-simplex by complex-first Wick continuation at the physical point $a=1$, $\alpha=1$. Edges are the two-value tuple hingeEdges32C z: each of the six cross (timelike) edges carries $z$, each spacelike edge carries $1$.
Cayley–Menger geometry is encoded in a bordered $6\times 6$ complex matrix. The cofactor $C_{r,c}$ is the signed $5\times 5$ minor after deleting row $r$ and column $c$, with sign $(-1)^{r+c}$. Mixed opposite pairs (one lower-slice vertex, one upper-slice vertex) have closed forms $C_{pp}=8z-4$, $C_{qq}=6z-2$, and constant off-diagonal $C_{pq}=-1$.
CM indices $3$ and $5$ correspond to vertices $2$ and $4$, so this cofactor is exactly that mixed-pair $C_{pq}$. Upstream, the CM matrix of the two-value tuple is identified with an explicit matrix, and the relevant $5\times 5$ minor determinant is already proved equal to $-1$.
proof idea
Term-mode proof by unfolding the cofactor into sign times minor, then rewriting. Replace the abstract CM matrix by the explicit hinge matrix via cmMatrixC_hingeEdges32, identify the deleted submatrix with submatrix32_35, and insert det_minor32_35C which gives determinant $-1$. The cofactor sign at $(3,5)$ is $+1$ because $3+5=8$ is even (if_pos by decide). The product $(+1)\cdot(-1)$ reduces by ring to $-1$.
why it matters
Closes the constant off-diagonal cofactor identity needed for the mixed hinge opposite $(2,4)$ (triangle $(0,1,3)$). The module’s hinge classification lists $C_{pq}=-1$ for all six mixed pairs; this lemma is the kernel-checked instance at CM $(3,5)$.
It is fed directly into branchRegular32_pair24 (branch regularity of the cosine path on the open arc $(0,1)$) and boundary32_pair24 (continuous extension to the closed interval with exact endpoint values). Those certificates are part of the all-hinge split-form branch and boundary package for the (3,2) simplex under Wick continuation.
Within the Seven-Gaps finishing charter this is bookkeeping that makes the mixed-pair closed forms machine-checked rather than sympy-only, matching the per-hinge table of the executed Wick arc trace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.