zArc_eq_exp
plain-language theorem explainer
For every real parameter t, the unit physical-point Wick arc equals the pure complex exponential exp(i π (1-t)). Continuity of the arc, its real/imaginary parts, and the exact product-form crossing certificates all rewrite through this identity. The proof is a two-line unfold of the scaled arc definition followed by norm_num.
Claim. For every real $t$, the physical-point Wick arc (unit lattice spacing, scale factor $1$) satisfies $z(t)=\exp\bigl(i\pi(1-t)\bigr)$ in $\mathbb{C}$.
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 continuation path on the timelike squared edge is the canonical upper-half-plane arc $z(t)=\alpha a^2\exp(i\pi(1-t))$ for $t\in[0,1]$, with Lorentzian endpoint at $t=0$ and Euclidean endpoint at $t=1$; the open interior lies in $\mathrm{Im}>0$.
The scaled arc arcZ a alpha t is exactly that formula. The physical-point specialization zArc t fixes unit lattice spacing and scale ($a=\alpha=1$), matching the Lean physical point of the causal pentagon. This lemma simply records that the scale prefactor collapses to $1$, so the physical arc is the pure exponential.
proof idea
Term-mode proof by definitional reduction. Unfold zArc to arcZ 1 1 t, then unfold arcZ to the product $((1\cdot 1^2:\mathbb{R}):\mathbb{C})\cdot\exp(i\pi(1-t))$. A single norm_num discharges the real prefactor identity $1\cdot 1^2=1$, leaving the pure complex exponential on the right-hand side.
why it matters
Workhorse rewrite for the entire C11 arc calculus. Downstream, continuous_zArc funexts through it and composes with Complex.continuous_exp; zArc_re and zArc_im obtain $\mathrm{Re},z(t)=\cos(\pi(1-t))$ and $\mathrm{Im},z(t)=\sin(\pi(1-t))$ by the same rewrite plus the standard Euler identities. The exact crossing theorems (product_form_crossing_value and the mixed/upper-pair analogues in WickThreeTwoHinges) open by rewriting zArc tStar via this lemma, then applying Complex.exp_mul_I to reach the certified real-negative product-form denominators ($-32$, $-40$, $-48$).
Within the Seven-Gaps campaign this sits on the hinge-data continuation path only; the FullTheoryLedger gap on genuine action-level interior-hinge continuation remains open and is not touched here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.