submatrix_pq

This module formalizes the complex-first 4D Wick continuation of Regge hinge data (Cayley–Menger areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The continuation path is the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ from the Lorentzian to the Euclidean endpoint. Scope is hinge-data only; full action-level continuation remains open (C12).

The bordered hinge matrix $H(z)$ is the $6\times 6$ Cayley–Menger matrix for the fourOne edge tuple with spacelike edges $1$ and one timelike squared length $z$ (rows/cols $1..5$ index vertices $0..4$). The named $5\times 5$ object $M_{pq}(z)$ is the minor that deletes row $3$ and column $4$, the pair needed for the off-diagonal cofactor $C_{pq}$.

Fin.succAbove k is the standard embedding that skips index $k$, so the Lean submatrix construction is exactly that deletion.

Pointwise matrix extensionality on the $5\times 5$ index set, then double fin_cases over both indices. Each of the twenty-five residual goals is definitional equality (rfl) between the corresponding entry of the submatrix of $H(z)$ and the match-table definition of $M_{pq}(z)$. No algebraic lemmas are required.

Feeds the closed-form cofactor theorem cofactor_pq, which states $C_{pq}=1-2z$ for the CM rows/cols $(3,4)$. That proof rewrites the cofactor through this identification, then applies the $5\times 5$ determinant evaluation and the odd-parity sign. Together they supply the symbolic off-diagonal cofactor on the Wick arc, matching the RESULTS.txt gate form used in the C11 hinge-data continuation. Does not close the open ledger gap on action-level 4D continuation.