Pith. sign in
theorem

hingeCosPath_one

proved
show as:
module
IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst
domain
Gravity
line
709 · github
papers citing
none yet

plain-language theorem explainer

At the Euclidean endpoint of the canonical Wick arc, the split-form complex dihedral cosine of the traced fourOne hinge equals -1/4 in C. Cite this for the C11 boundary-continuation receipt that pins the regular unit 4-simplex value under the +C_pq convention. The proof rewrites the path as a cut-free Möbius rational, specializes the arc coordinate at t=1, and finishes by numeric evaluation.

Claim. Along the physical Wick arc for the fourOne causal 4-simplex (unit edge scales), the split-form complex dihedral cosine of the traced hinge equals $-1/4$ at the Euclidean endpoint $t=1$.

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 path on the timelike squared edge is the upper-half-plane arc $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 object evaluated here is the split-form cosine path: $t\mapsto C_{pq}/(\sqrt{C_{pp}}\sqrt{C_{qq}})$ at hinge $(0,1,4)$, opposite pair $(2,3)$, type fourOne, $a=\alpha=1$. Split square roots in the denominator are mandatory on the arc (gate S2). An upstream identity collapses that split form, everywhere on the arc, to the cut-free rational $(1-2z)/(6z-2)$.

Convention note from the doc-comment: $-1/4$ is the regular unit 4-simplex value in the $+C_{pq}$ convention (textbook interior dihedral cosine is $+1/4$ under the opposite $-C$ sign).

proof idea

Term-mode, three steps. Rewrite the path via the branch-collapse identity that equates the split-form cosine to the Möbius rational $(1-2z)/(6z-2)$ in the arc coordinate. Specialize the arc at the Euclidean endpoint with the $t=1$ evaluation of $z$. Close by norm_num on the resulting complex rational, which yields $-1/4$.

why it matters

This is the Euclidean endpoint conjunct of the S4 boundary-continuation receipt. Downstream, wick_boundary_continuation_fourOne_hinge packages continuity on $[0,1]$ with the two endpoint values: Lorentzian $-(3/8)$ at $t=0$ and Euclidean $-(1/4)$ at $t=1$. Without this identity the receipt does not close.

In the Seven-Gaps campaign this sits in panel-locked lane C11 (hinge-data continuation only). The module doc is explicit that action-level continuation remains open under C12 / wick_action_continuation_4d; no FullTheoryLedger flag is discharged here. The value matches the RESULTS.txt endpoint table and the regular 4-simplex dihedral cosine under the repo's $+C_{pq}$ sign convention.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.