hingeCosPath_zero
plain-language theorem explainer
At the Lorentzian endpoint t=0 of the physical Wick arc, the split-form complex dihedral cosine of the traced fourOne hinge equals -(3/8) in ℂ. Gravity and Regge-calculus workers cite this as the Lorentzian boundary value of the C11 hinge-data continuation. The proof rewrites the path through its Möbius closed form, plugs in the arc endpoint, and evaluates by norm_num.
Claim. Let $C^{\mathrm{split}}(t)$ be the split-form complex dihedral cosine of the traced fourOne hinge (opposite pair $(2,3)$, unit edge scales) along the upper-half-plane Wick arc. Then at the Lorentzian endpoint, $C^{\mathrm{split}}(0) = -\frac{3}{8}$ in $\mathbb{C}$.
background
Module C11 formalizes a 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))$ on $t\in[0,1]$, with $z(0)$ Lorentzian and $z(1)$ Euclidean, interior strictly in the open upper half-plane.
The split-form cosine path is $t\mapsto C_{pq}/(\sqrt{C_{pp}}\sqrt{C_{qq}})$ at hinge $(0,1,4)$, opposite pair $(2,3)$, type fourOne, $a=\alpha=1$. A prior branch-collapse theorem identifies this path with the cut-free rational function $(1-2z)/(6z-2)$ everywhere on the arc (the two split square roots multiply back to the product of cofactors). The module is hinge-data only: action-level continuation of a full interior-hinge complex is the separate C12 question and remains open in the ledger.
proof idea
Term-mode, three steps. Rewrite the path via the Möbius identity hingeCosPath_eq_moebius, so the claim becomes evaluation of $(1-2z)/(6z-2)$ at the arc parameter $t=0$. Substitute the Lorentzian endpoint of the arc via zArc_zero. Finish with norm_num on the resulting complex rational constant, obtaining $-(3/8)$.
why it matters
Supplies the Lorentzian boundary value in the boundary-continuation receipt wick_boundary_continuation_fourOne_hinge, which asserts continuity of the split cosine on $[0,1]$ together with endpoints $-(3/8)$ at $t=0$ and $-(1/4)$ at $t=1$ (the regular unit 4-simplex Euclidean value in the $+C_{pq}$ convention).
Also feeds lorentzian_endpoint_sign_factor, which documents that at this endpoint both cofactors are negative ($C_{pp}=C_{qq}=-8$), so the split denominator is $-8$ rather than $\mathrm{Real.sqrt},64=+8$; the split form therefore equals $(-1)$ times the real product-form value $+3/8$. That sign factor is part of the S4 convention package for the C11 lane (panel P1-remainder, QG Seven-Gaps). It does not close the FullTheoryLedger gap wick_action_continuation_4d; that remains open pending C12.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.