SqEdges10C
plain-language theorem explainer
Type of complex squared edge lengths for a causal 4-simplex: maps from the ten lexicographic edges into the complex numbers. Every complex Cayley-Menger matrix, cofactor, split dihedral cosine, and Wick-arc edge path in the C11 hinge-data lane is typed over this table. Pure type abbreviation of Fin 10 to C; no proof content.
Claim. Let $\mathrm{SqEdges10}^{\mathbb{C}}$ be the type of maps $\{0,\ldots,9\}\to\mathbb{C}$, i.e. complex squared edge lengths of a 4-simplex on five vertices, indexed in the fixed lexicographic edge order.
background
A Euclidean or Lorentzian 4-simplex has five vertices and $\binom{5}{2}=10$ edges. In the real causal-simplex layer, those squared lengths live in a ten-slot real table, and pentDistSq rebuilds the symmetric $5\times 5$ squared-distance matrix from that table by the same lexicographic edge order.
This module (C11, complex-first Wick continuation of Regge hinge data) complexifies that table so the timelike squared edges can travel the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ from the Lorentzian endpoint $t=0$ to the Euclidean endpoint $t=1$, while spacelike edges stay real and positive. All subsequent hinge quantities (bordered Cayley-Menger matrix, minors, cofactors, split-form dihedral cosines, triangle areas-squared) are functions of one such complex table.
The module is explicitly hinge-data only: dihedral cosines and areas of triangular hinges of a single causal 4-simplex. Full action-level continuation on an interior-hinge complex is deferred to the separate C12 lane.
proof idea
Definitional abbreviation only: the type is identified with Fin 10 → ℂ. No lemmas, no tactics, no computational content beyond the type equality.
why it matters
This is the ambient edge-data type for the entire C11 complex-first stack. Downstream constructors and predicates all take an argument of this type: the complex Cayley-Menger matrix and its minors/cofactors, the split dihedral cosine and its denominator, hinge area-squared, the Wick-arc path continuationEdgesC, and the branch-regularity predicate that keeps diagonal cofactors off the square-root cut and the cosine ratio off the arccos cuts.
Without a single complex edge table, the PATH-SELECTED boundary continuation of hinge data along the canonical upper-half-plane arc cannot even be stated. The declaration therefore sits at the base of the proved branch certificate on the open arc interior, while leaving the FullTheoryLedger gap on genuine action-level 4D continuation untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.