dihedralCosSplitC
plain-language theorem explainer
Defines the complex cofactor dihedral cosine of a 4-simplex hinge in split-sqrt form: the off-diagonal Cayley–Menger cofactor C_pq divided by csqrt(C_pp)·csqrt(C_qq). Anyone tracing Wick-continued Regge hinge angles on the fourOne arc cites this as the cosine path. It is a one-line ratio of the already-defined complex cofactor and the mandatory split denominator.
Claim. For complex squared edge lengths $x$ of a 4-simplex and vertices $p,q\in\{0,\ldots,4\}$, the split-form complex dihedral cosine opposite the hinge is $C_{p'q'}/(\sqrt{C_{p'p'}}\,\sqrt{C_{q'q'}})$, where $p',q'$ are the bordered Cayley–Menger indices of $p,q$, and $C_{rs}$ is the complex CM cofactor. The numerator uses the $+C_{pq}$ convention (regular unit tetrahedron $\to +1/3$; regular unit 4-simplex $\to -1/4$).
background
Module C11 formalizes complex-first 4D Wick continuation of Regge hinge data (triangular areas-squared and dihedral cosines) for causal 4-simplex classes. The physical path is the upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ from Lorentzian to Euclidean endpoints. Scope is hinge-data only; full action-level continuation remains open (C12).
SqEdges10C is the complexification of the ten squared edge lengths of a 4-simplex. The bordered $6\times 6$ Cayley–Menger matrix yields cofactors cmCofactorC; vertex labels $0..4$ map to CM rows $1..5$ via cmVertexIndexC. The classical real dihedral cosine is a cofactor ratio; here the same formula is complexified.
The denominator is forced into split form csqrt(C_pp)·csqrt(C_qq) rather than csqrt(C_pp C_qq). The hour-0 gate showed the product-under-one-sqrt form crosses the branch cut mid-arc; the split form does not. That is exactly dihedralDenomSplitC.
proof idea
Pure definitional abbreviation: numerator is the off-diagonal complex CM cofactor at the CM indices of $p$ and $q$; denominator is the already-defined split product of principal-cofactor square roots. No lemmas are applied; the body is the single quotient that downstream paths and branch-regularity predicates unfold.
why it matters
This is the cosine object whose analytic continuation is certified on the open arc. hingeCosPath is literally this definition along the fourOne physical edges at opposite pair $(2,3)$. hingeCosPath_eq_moebius collapses it to the cut-free Möbius function $(1-2z)/(6z-2)$ once the split square roots multiply back. BranchRegularOn requires the split cosine to stay off the arccos cuts, and branchRegular_fourOne_hinge proves that on all of $(0,1)$.
Downstream, WickFourOneAllHinges reuses it for spacelike- and timelike-pair branch certificates and for the symmetry lemma dihedralCosSplitC_symm. In the Seven-Gaps campaign this is the C11 hinge cosine that makes PATH-SELECTED Wick continuation of dihedral data a proved, branch-certified object—without claiming the still-open ledger gap wick_action_continuation_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.