submatrix32_14
plain-language theorem explainer
Removing row index 1 and column index 4 from the bordered 6×6 complex hinge matrix of the (3,2) causal 4-simplex yields the explicit 5×5 mixed off-diagonal minor at Cayley–Menger slot (1,4). Anyone computing the (1,4) cofactor for the mixed hinge opposite pair (0,3) cites this equality. The proof is a pure index exhaustion: extensionality plus fin_cases on both Fin 5 indices, each cell reducing by rfl.
Claim. For every $z \in \mathbb{C}$, the $5 \times 5$ submatrix of the bordered complex hinge matrix of the $(3,2)$ simplex obtained by deleting row $1$ and column $4$ (0-based) equals the explicitly tabulated mixed off-diagonal minor associated to Cayley–Menger entry $(1,4)$ (opposite vertex pair $(0,3)$).
background
Lane B2 of the QG Seven-Gaps campaign continues all ten triangular hinges of the threeTwo causal 4-simplex through the complex-first Wick arc. The lower slice is vertices ${0,1,2}$, the upper slice ${3,4}$; the six cross edges are the timelike ones. Hinges fall into three classes by opposite pair: one spacelike hinge, six mixed hinges, and three upper-pair hinges.
The bordered $6 \times 6$ matrix hingeMatrix32C z encodes the threeTwo edge data with spacelike length squared $1$ and timelike length squared $z$, mirroring the real pentagon matrix at $(p,q)=(1,z)$. Its first row and column are the usual Cayley–Menger border of ones (diagonal zero). The mixed off-diagonal minor at CM slot $(1,4)$ is the $5 \times 5$ matrix obtained by striking that row and column; it is written out entrywise as minor32_14C and corresponds to opposite pair $(0,3)$.
Cofactors of these minors supply the closed-form $C_{pp}$, $C_{qq}$, $C_{pq}$ that enter the split cosine and area-squared formulae for each hinge class.
proof idea
Term-mode equality of two $5 \times 5$ complex matrices. Apply matrix extensionality to reduce to pointwise equality on indices $i,j : \mathrm{Fin},5$. Exhaust both indices by fin_cases; each of the twenty-five cells is definitionally identical to the corresponding entry of the explicit minor, so rfl closes every branch. No algebraic rewriting or determinant lemmas are required.
why it matters
Feeds directly into cof32_14, which unfolds the Cayley–Menger cofactor at $(1,4)$ and rewrites via this submatrix identity plus the determinant of the minor to obtain the constant value $-1$. That constant is the mixed-hinge off-diagonal cofactor $C_{pq}=-1$ recorded in the module charter for all six mixed pairs (one lower, one upper vertex).
Those closed cofactors are the algebraic input to the split-form branch certificates on the physical Wick arc $z_{\mathrm{Arc}}$ at $a=\alpha=1$. They sit inside the broader Recognition gravity program that forces $D=3$ (T8) and the eight-tick octave (T7), here specialized to the Lorentzian geometry of a single $(3,2)$ 4-simplex. The equality is a bookkeeping lemma, but without it the cofactor pipeline cannot discharge the mixed-hinge table against the executed trace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.