fourOneCosPath
plain-language theorem explainer
Defines the complex split-form dihedral cosine of any opposite vertex pair along the physical (4,1) Wick arc at unit scale. CDT and quantum-gravity workers cite it when extending single-hinge branch regularity to all ten hinges of the fourOne 4-simplex. The body is a one-line composition of the fourOne edge continuation with the cofactor cosine.
Claim. For opposite vertices $p,q\in\{0,1,2,3,4\}$ and real arc parameter $t$, return the split-form complex dihedral cosine of the Wick-continued squared-edge data of the $(4,1)$ causal 4-simplex at physical point $a=1$, $\alpha=1$.
background
Lane B1 of the QG Seven-Gaps campaign extends the single-hinge Wick certificates of WickActionComplexFirst to every triangular hinge of the fourOne causal 4-simplex. A hinge is an unordered triple of vertices in Fin 5; its opposite pair is the complementary two vertices. The fourOne type has timelike edges exactly those incident to the apex vertex 4.
The complex edge continuation sends each timelike squared length along the canonical upper-half-plane arc and holds each spacelike squared length fixed at $a^2$. The split-form dihedral cosine is the ratio of the Cayley-Menger cofactor $C_{pq}$ to the split denominator built from the same complex edge data; the $+$ numerator convention matches the 3D regular-tetrahedron check $+1/3$.
This path specializes that cosine to the physical point $a=1$, $\alpha=1$ on the fourOne type, generalizing the landed single-hinge path (opposite pair $(2,3)$) to an arbitrary opposite pair $(p,q)$.
proof idea
One-line definition. Feed the complex-continued squared-edge 10-tuple of the fourOne type at $(a,\alpha)=(1,1)$ and parameter $t$ into the split-form cofactor cosine, evaluated at the opposite pair $(p,q)$. No further simplification or case split occurs at the definition site.
why it matters
This is the common path object for the all-hinge boundary program. Every concrete pair theorem (boundary_pair01 through the remaining nine pairs) and the two parametric class theorems (timelike-class and spacelike-class boundary continuation) state continuity on the closed interval $[0,1]$ and the Lorentzian/Euclidean endpoint values in terms of this path.
Downstream, the S2 lookalike receipt packages universal branch regularity together with ContinuousOn of this path on $[0,1]$ for every distinct pair, while explicitly separating hinge-data continuation from a deficit-weighted three-pent action-level target. Closing all ten hinges at the data level is the combinatorial half of lane B1; action-level assembly remains a distinct charter item.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.