Pith. sign in
theorem

cof32_24

proved
show as:
module
IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges
domain
Gravity
line
573 · github
papers citing
none yet

plain-language theorem explainer

For every complex edge parameter z, the Cayley–Menger cofactor C_{2,4} of the (3,2) two-value hinge tuple equals −1 constantly. This is the mixed-pair off-diagonal C_{pq} for opposite vertices (1,3). Cited by the branch-regularity and boundary-continuation certificates for that mixed hinge. Proof unfolds the cofactor, inserts the explicit 5×5 minor, and reduces by the already-proved determinant identity det = −1 with even sign.

Claim. For every $z \in \mathbb{C}$, the complex Cayley–Menger cofactor $C_{2,4}$ of the bordered $6\times 6$ matrix built from the (3,2) two-value edge tuple (spacelike edges $1$, timelike edges $z$) equals $-1$.

background

Lane B2 of the QG Seven-Gaps campaign treats the complex-first Wick continuation of all ten triangular hinges of the causal (3,2) 4-simplex at the physical point $a=\alpha=1$. Edges are encoded by the two-value tuple hingeEdges32C z: each of the six timelike cross-edges carries the complex value $z$, and every spacelike edge is fixed at $1$.

Dihedral data are read from complex Cayley–Menger cofactors of the bordered $6\times 6$ matrix. The cofactor $C_{r,c}$ is the signed $5\times 5$ minor obtained by deleting row $r$ and column $c$; the sign is $(-1)^{r+c}$. Vertex indices $0..4$ sit in CM rows/columns $1..5$, so CM indices $(2,4)$ are the opposite pair of vertices $(1,3)$.

For mixed opposite pairs (one lower-slice vertex, one upper-slice vertex) the module records the closed form $C_{pq}=-1$, independent of $z$. The upstream identity det_minor32_24C already evaluates that particular $5\times 5$ minor to $-1$; the present theorem only assembles the signed cofactor.

proof idea

Term-mode proof by unfolding and rewriting. Unfold the cofactor into sign times minor. Replace the abstract CM matrix by the explicit hinge matrix via cmMatrixC_hingeEdges32, identify the deleted submatrix with submatrix32_24, and insert det_minor32_24C (determinant equals $-1$). The parity test Even(2+4) succeeds, so the cofactor sign is $+1$. A final ring yields $+1\cdot(-1)=-1$.

why it matters

Supplies the constant off-diagonal cofactor $C_{pq}=-1$ required by every mixed-hinge certificate in the (3,2) table. Downstream, branchRegular32_pair13 feeds it (with the two diagonal cofactors) into branchRegular_threeTwo_mixed_pair to obtain branch regularity of the cosine path for opposite pair $(1,3)$ on the open arc $(0,1)$. Likewise boundary32_pair13 uses it for continuous boundary values at the Euclidean and Lorentzian endpoints.

This is one kernel-checked entry in the per-hinge closed-form table of the Wick-arc trace: mixed hinges have asymmetric diagonals $C_{pp}=8z-4$, $C_{qq}=6z-2$ and constant $C_{pq}=-1$. Closing all ten hinges (plus the two product-form kill certificates) completes Lane B2 of the finishing charter for the complex-first Wick continuation of the causal 4-simplex.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.