hingeCosPath
plain-language theorem explainer
Defines the complex split-form dihedral cosine of the traced fourOne hinge along the physical Wick arc z(t). For each real parameter t it evaluates C_pq/(csqrt C_pp · csqrt C_qq) on the continued edge data at opposite pair (2,3) with a=α=1. Cited by the branch-regularity, continuity, Möbius-collapse, and endpoint theorems in the C11 Wick lane. Body is a one-line specialization of the split cosine to the fourOne continuation path.
Claim. For each real $t$, let $E(t)$ be the complex squared-edge data of the causal $4$-simplex of type fourOne continued along the upper-half-plane arc with $a=\alpha=1$. The hinge cosine path is the split-form dihedral cosine of the opposite pair $(2,3)$ on $E(t)$: $\mathrm{hingeCos}(t) := C_{pq}/(\sqrt{C_{pp}}\sqrt{C_{qq}})\in\mathbb{C}$, where the square roots are the principal complex branches.
background
Module C11 formalizes complex-first 4D Wick continuation of Regge hinge data (Cayley–Menger areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The physical arc is $z(t)=\alpha a^2\exp(i\pi(1-t))$ for $t\in[0,1]$, with Lorentzian endpoint $z(0)=-\alpha a^2$ and Euclidean endpoint $z(1)=+\alpha a^2$; the open interior lies in the upper half-plane.
The split-form cosine is mandatory: dihedral cosine is written $C_{pq}/(\mathrm{csqrt},C_{pp}\cdot\mathrm{csqrt},C_{qq})$ rather than a single product-form square root, so that branch cuts can be tracked separately and later collapsed. Here the hinge is triangle $(0,1,4)$ with opposite pair $(2,3)$, type fourOne, and unit scales $a=\alpha=1$. Upstream edge continuation supplies the complex squared lengths; the split cosine and denominator helpers assemble the cofactor ratio.
proof idea
Pure definitional specialization. The body applies the split-form dihedral cosine helper to the fourOne continuation edge path at scales $a=1$, $\alpha=1$, with opposite vertex pair $(2,3)$. No proof obligations; noncomputable only because complex square roots and the continuation path are noncomputable.
why it matters
Anchor object for the C11 hinge-data Wick lane. Downstream theorems identify it with the cut-free Möbius function $(1-2z)/(6z-2)$ on the whole real line, prove continuity on the closed interval $[0,1]$, evaluate the Lorentzian endpoint as $-3/8$ and the Euclidean endpoint as $-1/4$, certify branch regularity on the open interior $(0,1)$, and document the Lorentzian sign factor $-1$ versus the real product form. The all-hinges cofactor lane also consumes it.
This is hinge-data continuation only. The FullTheoryLedger gap on genuine action-level 4D Wick continuation (interior-hinge simplicial complex, C12) remains open; no ledger flag is closed here. Framework role: supplies the concrete complex path whose branch certificate and boundary values underwrite the panel-locked C11 receipt.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.