submatrix32_34
plain-language theorem explainer
For complex z, deleting row 3 and column 4 from the bordered 6×6 hinge matrix of the (3,2) causal simplex yields exactly the hand-written mixed minor at CM entry (3,4). Cofactor computations for the mixed opposite-pair hinges cite this identification. The proof is pointwise extensionality on Fin 5 with exhaustive fin_cases and rfl.
Claim. For every $z \in \mathbb{C}$, the $5\times 5$ submatrix of the bordered hinge matrix $H_{32}(z)$ obtained by deleting row index $3$ and column index $4$ equals the explicitly defined mixed off-diagonal minor $M_{34}(z)$.
background
Lane B2 of the QG Seven-Gaps campaign continues all ten triangular hinges of the threeTwo causal 4-simplex (lower slice ${0,1,2}$, upper ${3,4}$) in the complex-first Wick setting, at the physical point on the canonical upper-half-plane arc. Closed cofactor forms are kernel-checked by explicit $5\times 5$ minors.
The bordered hinge matrix $H_{32}(z)$ is the $6\times 6$ complex matrix mirroring the (3,2) pentagon matrix at spacelike edge $1$ and timelike edge $z$: first row/column is the usual border of ones, then lower-slice vertices occupy indices $1..3$ and upper-slice vertices $4..5$.
The target minor $M_{34}(z)$ is the mixed off-diagonal $5\times 5$ block at Cayley–Menger position $(3,4)$ (opposite pair $(2,3)$), written by cases so that its determinant can be evaluated in closed form. Mixed pairs (one lower, one upper vertex) are the six hinges with two timelike triangle edges and asymmetric cofactors.
proof idea
Pointwise matrix extensionality on the two Fin 5 indices. Each index is discharged by fin_cases, producing twenty-five residual goals; each goal is definitional equality between the corresponding entry of the submatrix (via succAbove on the hinge matrix) and the case-match body of the hand-written minor, closed by rfl. No algebraic lemmas are required beyond the definitions of the two matrices.
why it matters
Feeds the cofactor identity cof32_34, which unfolds the Cayley–Menger cofactor at $(3,4)$, rewrites through the hinge-edge matrix identification and this submatrix equality, inserts the evaluated minor determinant, applies the odd-parity sign, and obtains $C_{34}=-1$ by ring. That constant off-diagonal cofactor is the closed form quoted in the module for all six mixed hinges (one lower and one upper vertex): $C_{pp}=8z-4$, $C_{qq}=6z-2$, $C_{pq}=-1$, $\mathrm{areaSq}=z/4-1/16$. Those forms underwrite the split-form branch certificates on the Wick arc for the mixed class of the (3,2) simplex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.