wickActionPath
plain-language theorem explainer
Deficit-weighted Regge action along the Wick arc: complex path equal to fixed hinge area times (2π minus the three-pent dihedral sum). Gap-6 and Wick-continuation authors cite it as the action-level object whose continuity, Euclidean anchor, and closed-interval no-go are certified downstream. Definition is the one-line product of banked √(3/16) with the deficit from the dihedral-sum path.
Claim. For real $\alpha,t$, the Wick-arc Regge action is the complex value $S(\alpha,t):=A\bigl(2\pi-\Sigma\theta(\alpha,t)\bigr)$, where $A=\sqrt{3/16}$ is the constant spacelike hinge area and $\Sigma\theta(\alpha,t)=3\,\mathrm{carccos}(c_{\mathrm{hinge}}(\alpha,t))$ is the three-pent dihedral-angle sum along the arc.
background
Module Wave C4 R2 freezes the wick_action_continuation_4d schema for a three-pent Regge complex under Wick rotation. Binding arc convention: $t=0$ Lorentzian, $t=1$ Euclidean. On this object the shared hinge is the same-slice all-spacelike triangle; structural collapse forces the dihedral sum to be three times a single complex angle, and hinge area squared equal to the constant real $3/16$.
The complex angle uses the repo lift $\mathrm{carccos},w:=-I\log(w+I\sqrt{1-w^2})$ (half-power only on $1-w^2$). Upstream, the dihedral-sum path is exactly $3\cdot\mathrm{carccos}$ of the pent hinge cosine path; the hinge area is the real constant $\sqrt{3/16}$. Classical Regge action is area times angular deficit $2\pi-\sum\theta$; this definition is that product, complexified along the arc.
proof idea
Pure definitional abbreviation. Cast the real hinge area $\sqrt{3/16}$ into $\mathbb{C}$, subtract the already-defined dihedral-sum path from $2\pi$, and multiply. No lemmas, no tactics: the body is the product of those two upstream defs.
why it matters
This is the action-level path that Gap-6 certificates deliberately separate from mere hinge-data continuation. Downstream, WickActionCertAssembly proves continuous-on-$(0,1]$ at $\alpha=1$, the Euclidean endpoint identity matching real Regge, and the named no-go that continuous-on-$[0,1]$ is unsatisfiable at $\alpha=1$ (Lorentz cut). Status flags record V1 unsatisfiability and V2 closure at $\alpha=1$. Lookalike receipts use it to show hinge-data completeness does not inhabit a deficit-weighted three-pent action. It sits inside the frozen continuation schema without flipping action-level Bools or claiming Schläfli or half-plane confinement (N3/N4 still open).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.