submatrix32_15
plain-language theorem explainer
Deleting row 1 and column 5 from the complex 6×6 bordered hinge matrix of the (3,2) causal 4-simplex recovers the explicit 5×5 mixed off-diagonal minor at Cayley–Menger slot (1,5), opposite pair (0,4). Authors of the Wick-continuation cofactor table cite it when computing that entry. Proof is entrywise Fin-case exhaustion with reflexivity.
Claim. For every $z\in\mathbb{C}$, the $5\times 5$ submatrix of the bordered $(3,2)$ hinge matrix at $z$ obtained by deleting row index $1$ and column index $5$ equals the explicitly tabulated mixed off-diagonal minor for Cayley–Menger position $(1,5)$ (opposite vertex pair $(0,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$. The lower slice is vertices ${0,1,2}$, the upper slice ${3,4}$; the six cross edges are the timelike ones.
The bordered $6\times 6$ hinge matrix places a zero-border row/column and encodes spacelike edge length $1$ with timelike length $z$, mirroring the real pentagon matrix at $(p,q)=(1,z)$. Mixed off-diagonal minors arise when the deleted pair straddles the two slices; the minor at CM $(1,5)$ is the opposite pair $(0,4)$, one of the six mixed hinges whose closed cofactor forms are $C_{pp}=8z-4$, $C_{qq}=6z-2$, $C_{pq}=-1$.
That minor is supplied as an explicit $5\times 5$ match-table (border zero, selected $z$ and $0$ entries). The present equality identifies the abstract Matrix.submatrix deletion with that table.
proof idea
Pointwise matrix extensionality on the two Fin 5 indices. Nested fin_cases exhausts all twenty-five entries; each residual goal is definitional equality of the corresponding match-clause in the hinge matrix against the tabulated minor, discharged by rfl. No algebraic lemmas beyond the two definitions.
why it matters
Feeds the cofactor identity that the Cayley–Menger cofactor at $(1,5)$ equals $-1$ for every complex $z$. That constant $C_{pq}=-1$ is the closed form quoted in the module for all six mixed (one-lower, one-upper) hinges, and is kernel-checked against the executed Wick-arc trace table. Together with the matching $5\times 5$ determinant evaluations, it closes the split-form branch certificate for those hinges on the upper-half-plane arc. Inside the broader RS gravity stack this is bookkeeping for the $(3,2)$ simplex geometry that underwrites the eight-tick / $D=3$ forcing chain’s continuum limit, not a new dynamical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.