dihedralSumPath
plain-language theorem explainer
Defines the complex deficit-angle sum on the three-pent hinge as three times the complex arccos of the shared pent-hinge cosine path. Gravity and Wick-continuation proofs cite it as the angle factor inside the complex Regge action along the Euclidean–Lorentz arc. The body is a one-line structural collapse: all three dihedrals share one cosine chart, so Σθ = 3 θ(t).
Claim. For real parameters $\alpha$ and $t$, the complex dihedral-sum path is $3\,\mathrm{carccos}\bigl(c_{\alpha}(t)\bigr)$, where $c_{\alpha}(t)$ is the cosine of the shared three-pent hinge along the Wick arc and $\mathrm{carccos}$ is the complex arccos $-i\log\bigl(w+i\sqrt{1-w^2}\bigr)$.
background
Module Wave C4 R2 freezes the Wick-action continuation schema for a 4d three-pent complex. Arc convention is binding: $t=0$ Lorentzian, $t=1$ Euclidean. The shared hinge is the all-spacelike triangle ${0,1,2}$; the three induced pent cosine paths collapse definitionally to one chart pair, so the deficit sum is exactly three copies of a single complex angle.
Complex angle uses the repo lift $\mathrm{carccos},w:=-I\log(w+I,\mathrm{csqrt}(1-w^2))$, with half-power only on $1-w^2$. Upstream hinge language (codimension-2 curvature carrier with real deficit) and the glued-pents hinge witness ${0,1,2}$ fix the geometric object whose three dihedrals are being summed.
Hinge area is separately frozen as the constant real $\sqrt{3/16}$ along the arc; the present definition supplies only the angle factor of the complex Regge action.
proof idea
Pure definition, not a proof. Body multiplies the complex arccos of pentHingeCosPath α t by the constant 3, encoding the structural identity $\Sigma\theta=3\theta(t)$ forced by the three-pent chart collapse. No tactics, no lemmas discharged here.
why it matters
Angle factor inside wickActionPath, the complex Regge action along the Wick arc. Downstream continuity theorems (continuousOn_wickActionPath_Ioc_one, continuousOn_wickActionPath_Ioc_of_causal) factor the constant-3 multiplier off continuous carccos∘pent. Lorentz cut-limit anchors (lorentzAnchor_one_holds, lorentzAnchor_of_causal) unfold through this sum to obtain the $2\pi-3\theta_L$ real part and $3\times$ rapidity imaginary part. Euclidean matching (wickActionPath_eq_euclidRegge) likewise expands the $t=1$ value as hinge area times $2\pi-3,\mathrm{euclidAngle}$.
Sits in the Gap-6 / seven-gaps gravity stack that prepares a Wick-continued 4d action; it does not itself flip gap6_lorentzian_action or inhabit the terminal wick_action_continuation_4d Prop. Supports the Regge deficit bookkeeping that Recognition Science needs before linking continuum curvature to the J-cost / ledger layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.