cmMatrixC_hingeEdges32
plain-language theorem explainer
The bordered complex Cayley–Menger matrix built from the (3,2) two-value edge tuple (spacelike edges 1, timelike edges z) equals the explicit 6×6 hinge matrix for that simplex. Anyone computing (3,2) hinge cofactors or Wick-continued Regge angles cites this identification. The proof is pure matrix extensionality: case-split on Fin 6 indices and definitional equality.
Claim. For every complex parameter $z$, the bordered $6\times 6$ complex Cayley–Menger matrix of the (3,2) edge assignment (timelike squared lengths equal to $z$, spacelike squared lengths equal to $1$) coincides with the explicitly written hinge matrix whose lower-slice block is vertices $0,1,2$ and upper-slice block is vertices $3,4$.
background
Lane B2 of the QG Seven-Gaps campaign treats the 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. The (3,2) type has lower slice ${0,1,2}$, upper slice ${3,4}$, and exactly six timelike cross edges.
The general constructor cmMatrixC builds the bordered $6\times 6$ complex Cayley–Menger matrix from any 10-tuple of complex squared edge lengths (complexification of the $n=4$ real Cayley–Menger matrix). The specialized edge map hingeEdges32C z sets every timelike edge of the (3,2) type to $z$ and every spacelike edge to $1$. The companion definition hingeMatrix32C z writes the same matrix by hand, with rows/cols $1..3$ the lower triple and $4..5$ the upper pair (mirror of the real pentagon matrix at $p=1$, $q=z$).
This lemma simply equates the two presentations so later cofactor and minor calculations can rewrite through the explicit matrix.
proof idea
Term-mode proof by matrix extensionality. After ext i j, both indices range over Fin 6. Nested fin_cases exhausts all 36 entry pairs; each residual goal is definitional equality of the corresponding match-clause in cmMatrixC applied to hingeEdges32C z versus the hard-coded clause in hingeMatrix32C z, discharged by rfl. No algebraic lemmas are required.
why it matters
Every closed-form cofactor for the ten triangular hinges of the (3,2) simplex rewrites through this identity. Downstream theorems cof32_12, cof32_13, cof32_14, cof32_15, cof32_23, cof32_24, and their siblings unfold the general CM cofactor, replace the abstract matrix by hingeMatrix32C via this lemma, then evaluate the corresponding $5\times 5$ minor determinant. Those cofactors supply the split-form branch certificates ($C_{pp}$, $C_{qq}$, $C_{pq}$, area squares) that match the executed Wick-arc trace table for all three hinge classes: spacelike opposite pair $(3,4)$, six mixed pairs, and three upper-pair hinges.
In the broader Recognition gravity stack this is scaffolding for the complex-first Wick continuation of Regge deficit angles on causal 4-simplices, not a forcing-chain (T0–T8) step. It closes the matrix-identification gap that lets the kernel-checked minor algebra proceed without repeatedly expanding the general Cayley–Menger constructor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.