branchRegularSum_one
plain-language theorem explainer
At the physical coupling α = 1, the three-pent hinge cosine path stays off the arccos cuts on (0,1), and both diagonal cofactors of the split-form continuation lie in the slit plane. Anyone assembling the Wick-action continuation certificate at α = 1 cites this. The proof is a one-line specialization of the causal-range branch-regularity theorem, since 1 > 7/12.
Claim. For every real $t \in (0,1)$, writing $c(t)$ for the three-pent hinge cosine path at coupling $\alpha = 1$: $c(t)$ lies off the classical arccos cuts (either $\mathrm{Im}\,c(t)\neq 0$ or $-1 < \mathrm{Re}\,c(t) < 1$), the cofactor $1 - c(t)^2$ lies in the complex slit plane, and the split sum $c(t) + i\sqrt{1 - c(t)^2}$ (principal square root) also lies in the slit plane.
background
Module Wave C4 closes N3 (Moebius confinement and branch-regular sum on the causal α-range) and packages N4 cut-boundary fallbacks. It does not inhabit the terminal Wick certificate, flip gap6, or touch Schläfli.
The shared path pentHingeCosPath α t is the dihedral cosine split on chart pair (3,4) of the three-two continuation edges at structural collapse a = 1. Branch regularity for the split-form hinge means three simultaneous conditions: the cosine stays in OffArccosCut (open set where any principal complex arccos is continuous: imaginary part nonzero, or real part strictly inside (−1,1)); the cofactor 1 − c² lies in Mathlib’s slitPlane (ℂ minus (−∞,0], the continuity region of principal cpow (1/2)); and the split sum c + i·csqrt(1 − c²) likewise stays in the slit plane. Here csqrt z := z^(1/2) is the principal-branch substitute for the missing Complex.sqrt.
Upstream, branchRegularSum_of_causal already proves the full triple for every α > 7/12 and every t ∈ (0,1). The physical coupling α = 1 sits strictly above that threshold.
proof idea
One-line term wrapper: apply branchRegularSum_of_causal at α = 1, discharging the hypothesis α > 7/12 by norm_num. No further analytic work; the general causal-range argument already supplies OffArccosCut, slit-plane membership of 1 − c², and slit-plane membership of the split sum along the open parameter interval.
why it matters
Feeds the banked partial receipt wickActionContinuationCertV2_one, which packages the repaired V2 Wick-action continuation certificate at the physical coupling α = 1 (causal range, chart agreement, branch-regular sum, and interior continuity of the action path). That certificate explicitly sets branchRegularSum := branchRegularSum_one.
Within the SevenGaps gravity stack this is the α = 1 instance of N3 branch-regularity: the split-form hinge continuation is free of arccos and square-root cuts on the open interior of the parameter interval, so the complex action path is well-defined before any cut-boundary limit is taken. N4 cut-boundary Tendsto at α = 1 remains a named open Prop; this lemma only closes the interior field-shape obligation. It does not inhabit the terminal four-dimensional Wick continuation or flip gap6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.