submatrix_pp
plain-language theorem explainer
Deleting row and column index 3 from the complex 6×6 hinge Cayley–Menger matrix yields exactly the tabulated 5×5 minor used for the (3,3) cofactor. Anyone computing dihedral cosines or areas along the Wick arc cites this identification. The proof is pure index exhaustion: extensionality plus fin_cases on all 5×5 entries, each reducing by rfl.
Claim. For every $z\in\mathbb{C}$, the submatrix of the bordered $6\times 6$ complex hinge matrix obtained by deleting row and column index $3$ equals the explicitly defined $5\times 5$ minor associated to that deletion (the $pp$ minor).
background
Module C11 formalizes a complex-first 4D Wick continuation of Regge hinge data (Cayley–Menger areas-squared and cofactor dihedral cosines) for a single causal 4-simplex. The path is the upper-half-plane arc on the timelike squared edge from the Lorentzian to the Euclidean endpoint. Scope is hinge-data only; full action-level continuation remains open (C12).
The hinge matrix is the explicit bordered $6\times 6$ complex matrix for the fourOne edge tuple (spacelike edges 1, one timelike edge $z$), mirroring the real pentMatrix at $p=1$, $q=z$. The $pp$ minor is the $5\times 5$ matrix obtained by deleting row/column 3 (equivalently, by vertex symmetry, the (4,4) minor), written out entrywise for later determinant work.
Matrix.submatrix with Fin.succAbove 3 is the library operation that deletes that index on both axes. This theorem asserts that the library deletion coincides with the hand-written minor.
proof idea
Pointwise matrix equality. Apply ext on the two Fin 5 indices, then fin_cases on each index (25 residual goals). Every goal is definitional equality of a single complex entry and closes by rfl. No algebraic lemmas are needed beyond the two definitions.
why it matters
Feeds cofactor_pp, which proves the closed form $C_{pp}=6z-2$ for the Cayley–Menger cofactor at row/col 3 (vertex 2). That rewrite chain unfolds the cofactor, replaces the library submatrix by this minor via submatrix_pp, then invokes the determinant of the $pp$ minor and simplifies the sign. Without the identification, the cofactor formula cannot leave the abstract Matrix.submatrix API.
In the C11 lane this is scaffolding for path-selected boundary continuation of hinge cosines and areas along the Wick arc. It does not close the FullTheoryLedger gap on action-level continuation; that remains open by module mandate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.