arcZ_one
plain-language theorem explainer
At the Euclidean endpoint t = 1 of the canonical upper-half-plane Wick arc, the complex squared-edge value equals the real positive quantity α a² coerced to ℂ. Gravity and QG workers cite this when identifying the Wick-rotated endpoint of the timelike hinge against CausalSimplex4D.euclideansqEdges. The proof unfolds the arc definition, kills the phase factor by π(1−1)=0, and simplifies.
Claim. For all real $a$ and $\alpha$, the canonical Wick arc on the timelike squared edge satisfies $z(1)=\alpha a^{2}$ in $\mathbb{C}$, where $z(t)=\alpha a^{2}\,\exp\bigl(i\pi(1-t)\bigr)$.
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(i\pi(1-t))$, $t\in[0,1]$,
with Lorentzian endpoint $z(0)=-(α a^{2})$ and Euclidean endpoint $z(1)=+(α a^{2})$, matching lorentzianSqEdges / euclideanSqEdges and the executed gate RESULTS.txt §1. Interior points lie in Im > 0.
The definition arcZ a alpha t is exactly that formula. Parameters $a$ (edge scale) and $α$ (fine-structure scale factor in the edge tuple) are real; the result is complex. This lemma is the pure endpoint evaluation of that arc at $t=1$. Scope is hinge-data continuation only; full action-level continuation remains the open C12 / ledger gap.
proof idea
Tactic proof. Unfold arcZ to expose the product of the real scalar $α a^{2}$ with $\exp(i\pi(1-t))$. Specialize $t=1$ and prove $\pi(1-1)=0$ by ring. Rewrite the phase to zero, then simp reduces $\exp(0)=1$ and yields the coerced real $α a^{2}$. No external lemmas beyond the definition and elementary real/complex arithmetic.
why it matters
Pins the Euclidean endpoint of the S1 arc so downstream endpoint-identification theorems can match the complex continuation tuple to the kernel-checked real Euclidean edge tuple of CausalSimplex4D. Direct consumers: continuationEdgesC_one (at $t=1$ the continuation equals euclideanSqEdges coerced to ℂ) and zArc_one (normalized arc value is 1 at the Euclidean end). Together with the Lorentzian counterpart at $t=0$, this closes the boundary certificates for the PATH-SELECTED Wick continuation on hinge data in the QG Seven-Gaps C11 lane. Does not touch the still-open ledger gap wick_action_continuation_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.