branchRegularSum_of_causal
plain-language theorem explainer
For causal hinge parameters α > 7/12, the three-pent cosine path on (0,1) stays off the classical arccos cuts, and both principal-square-root inputs for complex arccos lie in the slit plane. Gravity/Wick-continuation authors cite it as the branch-regularity half of the V2 certificate. The proof is a short term argument: strict negative imaginary part yields OffArccosCut, then the general slit-plane lemma.
Claim. Let $\alpha > 7/12$. For every $t \in (0,1)$, writing $c = c_{\mathrm{pent}}(\alpha,t)$ for the shared three-pent hinge cosine path, one has $c$ off the classical arccos cuts $(\mathrm{Im}\,c \neq 0$ or $-1 < \mathrm{Re}\,c < 1)$, and both $1-c^2$ and $c + i\,\mathrm{csqrt}(1-c^2)$ lie in the complex slit plane (continuity region of the principal square root).
background
Module Wave C4 closes N3 on the causal α-family: Moebius collapse of the three-two continuation, MODEL path equality, Im < 0 confinement, and the branchRegularSum field shape. It does not inhabit the terminal certificate, flip gap6, or touch Schläfli.
The path pentHingeCosPath α t is the shared three-pent hinge cosine: chart pair (3,4) of the threeTwo continuation at structural collapse a = 1. OffArccosCut(w) means w is off the classical real cuts (−∞,−1] ∪ [1,∞), i.e. Im w ≠ 0 or −1 < Re w < 1; that is the open region where any principal log-based complex arccos is continuous. The principal square root csqrt is z^(1/2) via Complex.cpow, cut on (−∞,0], continuous precisely on the slit plane.
Upstream, im_pentHingeCosPath_neg gives Im c < 0 on the open unit interval when α > 7/12. The general lemma offArccosCut_slitPlane (N1a) then places both csqrt-inputs 1−w² and w+I·csqrt(1−w²) in the slit plane whenever OffArccosCut holds.
proof idea
Term proof, two steps. Fix t ∈ (0,1). From im_pentHingeCosPath_neg (α > 7/12) one has Im(pentHingeCosPath α t) < 0, hence Im ≠ 0, so OffArccosCut holds by the left disjunct. Apply offArccosCut_slitPlane to that witness: it returns the pair of slit-plane memberships for 1−c² and c+I·csqrt(1−c²). Package as the required triple.
why it matters
This is the branch-regularity field of the N3 package (α-family, causal range). Downstream, wickActionContinuationCertV2_of_causal installs it as the branchRegularSum field of the family-wide repaired V2 certificate on 7/12 < α, alongside chartsAgree and interior continuity of the Wick action path. The specialization branchRegularSum_one is the α = 1 instance.
In the SevenGaps Wick-action program it certifies that the split-form hinge continuation stays inside the continuity region of principal csqrt/arccos on the open parameter interval, so the complex deficit-angle sum is well-defined before any cut-boundary limit. N4 cut-boundary Tendsto remains open (Mathlib one-sided log/csqrt filter API); this result does not address the endpoint and deliberately leaves the named Props carccos_tendsto_at_cut_one / lorentzAnchor_one unresolved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.