continuous_zArc
plain-language theorem explainer
The unit Wick arc sending real parameter t to exp(i π (1-t)) in the complex plane is continuous on all of ℝ. Gravity and Regge analysts cite it as the analytic backbone of every closed-interval hinge-cosine path in the C11 complex-first Wick lane. The proof is a short term rewrite to the exponential form, then composition of continuous maps (exp, ofReal, affine t ↦ π(1-t)).
Claim. The map $t \mapsto \exp\bigl(i\pi(1-t)\bigr)$ from $\mathbb{R}$ to $\mathbb{C}$ is continuous.
background
Module C11 formalizes a complex-first 4D Lorentzian Wick continuation of Regge hinge data (complex Cayley-Menger areas-squared and cofactor dihedral cosines) for causal 4-simplex classes. The canonical upper-half-plane arc on the timelike squared edge is $z(t)=\alpha a^2\exp(i\pi(1-t))$ for $t\in[0,1]$, with Lorentzian endpoint $z(0)=-\alpha a^2$ and Euclidean endpoint $z(1)=+\alpha a^2$; the open interior lies in the open upper half-plane.
At the physical point (unit lattice spacing, $\alpha=1$) this reduces to the pure phase path written here as the arc map $t\mapsto\exp(i\pi(1-t))$. An upstream identity equates that definition to the complex exponential of the real affine path $\pi(1-t)$ times $i$. Continuity of this path is the elementary analytic input needed before any rational function of the arc (cofactor ratios, split-sqrt cosine paths) can be shown continuous on the closed interval.
Honest scope of the module: this is hinge-data continuation only. Action-level continuation for a full interior-hinge complex is the separate C12 question and remains open in the ledger.
proof idea
Pointwise identity: the arc equals $t\mapsto\mathrm{Complex.exp}((\pi(1-t):\mathbb{C})\cdot i)$. Lift that identity by function extensionality to an equality of maps, rewrite the goal, and discharge continuity by composition. The outer factor is continuity of complex exponential. The inner factor is continuity of multiplication by the constant $i$, applied to the continuous real-to-complex embedding of the continuous real affine map $t\mapsto\pi(1-t)$ (constant times continuous-id subtracted from a constant). No case splits and no topology beyond the standard product/composition rules.
why it matters
Every closed-interval continuity statement for hinge cosine paths in this lane factors through this lemma. Downstream, the split-form cosine path is continuous on $[0,1]$ precisely because numerator and denominator are continuous functions of the arc and the denominator $6z-2$ never vanishes on $|z|=1$. The same arc continuity is invoked in the parametric boundary-continuation theorems for four-one spacelike and timelike hinge pairs and for three-two mixed, spacelike, and upper pairs: each proves ContinuousOn on the closed interval together with explicit Lorentzian and Euclidean endpoint values.
In the QG Seven-Gaps campaign this sits in flagship lane C11 (panel-locked, proceed-with-mandate). It does not close the FullTheoryLedger gap on action-level 4D Wick continuation; that remains open and is not claimed here. Framework-wise it is pure analytic scaffolding for the Regge hinge Wick path, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.