dihedralDenomSplitC
plain-language theorem explainer
Split-form denominator of the complex cofactor dihedral cosine at the hinge opposite vertices p and q on a 4-simplex: product of two separate complex square roots of the diagonal Cayley-Menger cofactors C_pp and C_qq. Anyone formalizing the 4D Wick arc of Regge hinge data cites it. Pure definitional construction, forced by the hour-0 gate that the single-sqrt product form crosses the branch cut mid-arc.
Claim. Given complex squared edge lengths $x$ of a 4-simplex and opposite vertices $p,q\in\{0,\ldots,4\}$, the split denominator is $\sqrt{C_{pp}(x)}\,\sqrt{C_{qq}(x)}$, where $C_{ii}$ denotes the complex Cayley-Menger cofactor at the CM vertex index of $i$.
background
Module C11 builds a complex-first formalization of the 4D Lorentzian Wick continuation of hinge data (complex Cayley-Menger areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The arc on the timelike squared edge is $z(t)=\alpha a^2\exp(i\pi(1-t))$ for $t\in[0,1]$, running from the Lorentzian endpoint $z(0)=-\alpha a^2$ to the Euclidean endpoint $z(1)=+\alpha a^2$, with open-arc interior in the upper half-plane.
SqEdges10C is the type of complex squared edge lengths indexed by Fin 10 (lex order on the 4-simplex edges). The real 3D ancestor is dihedralCos3Sq, the tetrahedral dihedral cosine from Cayley-Menger cofactors: $C_{pq}/\mathrm{denom}$. In 4D the same $+C_{pq}$ numerator convention is kept.
The hour-0 numeric gate mandates a split square-root denominator. The product form $\sqrt{C_{pp}C_{qq}}$ crosses the principal branch cut mid-arc (certificate: product-form crossing value equals $-32$ at the critical $t^*$).
proof idea
Definitional, not a proof. Body is the product of two applications of the complex square root csqrt to the diagonal cofactors cmCofactorC x (cmVertexIndexC p) (cmVertexIndexC p) and the same at $q$. No lemmas are invoked; the split is written by construction so later equalities can multiply the roots back without traversing a cut.
why it matters
Feeds the split-form cosine dihedralCosSplitC (numerator $C_{pq}$ over this denominator) and every path identity that unfolds it: hingeCosPath_eq_moebius (branch collapse to the cut-free Möbius map $(1-2z)/(6z-2)$ on the full arc), pentHingeCosPath_eq_moebius in the interior-hinge confinement module, and the 4+1 hinge theorems fourOneCosPath_eq_spacelike / fourOneCosPath_eq_timelike plus symmetry dihedralCosSplitC_symm.
This is the concrete embodiment of mandate S2 in the C11 lane: without the split, the product-form denominator argument hits a negative real mid-arc (product_form_crossing_value), so path-selected continuation would be ill-defined. The FullTheoryLedger gap on genuine action-level continuation (wick_action_continuation_4d) stays open; this object only underwrites hinge-data continuation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.