arcZ_zero
plain-language theorem explainer
At the Lorentzian endpoint of the Wick arc, the complex continuation of the timelike squared edge equals the negative real value $-(\alpha a^{2})$. Workers on the C11 hinge-data Wick continuation cite this to pin the $t=0$ boundary against the repo Lorentzian sign convention. The proof unfolds the arc, reduces the phase to $\pi$, and applies $\exp(i\pi)=-1$.
Claim. For all real $a$ and $\alpha$, the canonical upper-half-plane Wick path on the timelike squared edge evaluates at the Lorentzian endpoint $t=0$ to $-(\alpha a^{2})$ in $\mathbb{C}$.
background
Module C11 formalizes a complex-first 4D Wick continuation of Regge hinge data (Cayley-Menger areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The path on the timelike squared edge is the upper-half-plane arc
$z(t)=\alpha a^{2},\exp\bigl(i\pi(1-t)\bigr)$, $t\in[0,1]$,
with $z(0)=-(\alpha a^{2})$ Lorentzian and $z(1)=+(\alpha a^{2})$ Euclidean, matching lorentzianSqEdges / euclideanSqEdges and the executed gate RESULTS.txt §1. Interior points lie in $\mathrm{Im}>0$.
The arc definition is exactly that formula: real scale $\alpha a^{2}$ times $\exp(i\pi(1-t))$. This lemma is the $t=0$ endpoint identity for that definition. Scope is hinge-data only; full action-level continuation remains the open C12 / ledger gap.
proof idea
Tactic proof. Unfold the arc definition. A one-line ring step gives $\pi(1-0)=\pi$. Rewrite with that identity and Complex.exp_pi_mul_I ($e^{i\pi}=-1$). push_cast aligns real and complex coercions; a final ring closes $-(\alpha a^{2})$ on both sides.
why it matters
Pins the Lorentzian boundary of the S1 arc against the repo sign convention and the hour-0 numeric gate. Downstream, continuationEdgesC_zero uses it so that at $t=0$ the full complex edge tuple equals the kernel-checked real Lorentzian tuple coerced to $\mathbb{C}$. The normalized path lemma zArc_zero rewrites through this fact to get $z_{\mathrm{arc}}(0)=-1$.
In the Seven-Gaps C11 lane this is the first endpoint certificate on the PATH-SELECTED continuation; without it the branch certificate on the open arc interior has no fixed Lorentzian anchor. It does not close the ledger gap wick_action_continuation_4d (action-level continuation stays open).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.