cmMatrixC_hingeEdges
plain-language theorem explainer
For any complex timelike squared length z, the general bordered Cayley–Menger matrix built from the fourOne two-value edge tuple (spacelike edges 1, timelike edges z) equals the explicit 6×6 hinge matrix. Gravity and Regge-calculus workers cite it to replace the abstract CM constructor by a concrete matrix before taking minors. The proof is pure matrix extensionality plus Fin-case exhaustion to definitional equality.
Claim. For every $z \in \mathbb{C}$, the bordered $6 \times 6$ complex Cayley–Menger matrix of the fourOne edge tuple with spacelike squared lengths $1$ and timelike squared length $z$ equals the explicit hinge matrix whose off-border entries are $0$, $1$, or $z$ according to the fourOne incidence pattern.
background
Module C11 formalizes complex-first 4D Wick continuation of Regge hinge data (areas-squared and dihedral cosines) for causal 4-simplex classes. 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.
The complex Cayley–Menger matrix cmMatrixC is the bordered $6 \times 6$ complexification of the real $n=4$ construction: border row/column of ones, zero corner, and squared edge lengths in the vertex block. The two-value tuple hingeEdgesC z sets every fourOne-timelike edge to $z$ and every spacelike edge to $1$. The explicit matrix hingeMatrixC z hard-codes that same pattern by index cases (mirror of the real pentMatrix41 at $p=1$, $q=z$).
This lemma identifies the two presentations so later cofactor and determinant work can rewrite through the explicit matrix.
proof idea
Tactic proof by matrix extensionality: ext i j, then nested fin_cases over both Fin 6 indices. Each of the $36$ cells reduces by rfl because the match-on-vertex-index definition of the general CM matrix, evaluated on the two-value edge tuple, is definitionally the same as the case-split definition of the explicit hinge matrix.
why it matters
This equality is the rewrite bridge used by every closed-form cofactor on the fourOne hinge. Downstream, cofactor_pp, cofactor_qq obtain $C_{pp}=C_{qq}=6z-2$, and cofactor_pq obtains $C_{pq}=1-2z$; the all-hinges suite (cofactor41_12 through related entries) rewrites the same way before evaluating $5 \times 5$ minors. Those cofactors feed complex dihedral cosines and the path-selected Wick continuation on the open arc interior.
In the QG Seven-Gaps C11 lane this is scaffolding for hinge-data continuation, not a claim that an interior-hinge simplicial complex exists (that is C12). The ledger gap wick_action_continuation_4d stays open. No direct contact with T0–T8 forcing, RCL, or the alpha band; the link is Regge geometry under complex edge lengths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.