u0
plain-language theorem explainer
Defines the complex limit log-argument at a causal parameter α as −k(α)+√(k(α)²−1), with k the positive Lorentzian cosine scale. Anyone proving cut-limits of the Wick-rotated pent-hinge path cites this point. It is a pure definitional packaging of the L2+L3 endpoint, generalizing the fixed α=1 value −11/8+√57/8.
Claim. For $\alpha\in\mathbb{R}$, set $u_0(\alpha):=-k(\alpha)+\sqrt{k(\alpha)^2-1}\in\mathbb{C}$, where $k(\alpha)=(5+6\alpha)/(2+6\alpha)$ is the positive Lorentzian cosine scale on the causal range.
background
The module builds a parameterized cut-limit family for causal $\alpha>7/12$, generalizing the six-lemma $\alpha=1$ route in WickActionCutLimit. All arguments are pointwise in $\alpha$; there is no uniform-in-$\alpha$ bound because $k(\alpha)\to 1$ as $\alpha\to\infty$.
The scale $k(\alpha)=(5+6\alpha)/(2+6\alpha)$ is the absolute value of the Lorentzian cosine on that range. For $\alpha=1$ one recovers $k=11/8$ and $\sqrt{k^2-1}=\sqrt{57}/8$, matching the fixed complex point used in the original cut-limit lemmas.
The quantity $u_0(\alpha)$ is the candidate limit of the log-argument $z+\sqrt{z^2-1}$ along the pent-hinge cosine path as the path hits the branch cut from the upper half-plane.
proof idea
Definitional. Cast $-k(\alpha)$ and $\sqrt{k(\alpha)^2-1}$ from $\mathbb{R}$ into $\mathbb{C}$ and add. No lemmas or tactics; the body is exactly the sum of the L2 and L3 limit values written in the $\alpha=1$ module.
why it matters
This is the $\alpha$-family replacement for the fixed complex endpoint that anchors every cut-limit argument in Wave C4. Downstream lemmas (norm of $u_0$, $\log|u_0|=-\mathrm{arcosh},k$, tendsto of the log-argument into a neighborhood of $u_0$ with nonnegative imaginary part, and the complex-arccos cut limit) all evaluate or approach this point.
It sits inside the Gravity/SevenGaps stack that closes the Wick-action continuation certificates. It does not itself inhabit the F2 continuation certificate or flip F3 ledger Bools; it only supplies the geometric target those later steps need. Framework-wise it is local analytic scaffolding for the gravity cut, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.