zArc_re
plain-language theorem explainer
The real part of the physical Wick arc equals cos(π(1−t)) for every real t. Anyone proving the arc stays on the unit circle (or tracking the Lorentzian-to-Euclidean edge path) cites this identity. The proof rewrites the arc into exponential form and applies the standard real-part formula for exp(iθ).
Claim. For every real $t$, if $z(t)=\exp\bigl(i\pi(1-t)\bigr)$ denotes the physical-point Wick arc (unit lattice spacing), then $\operatorname{Re} z(t)=\cos\bigl(\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-simplices. The continuation path on the timelike squared edge is the 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 physical-point specialization (unit spacing, $\alpha=1$) is the complex function $z(t)=\exp(i\pi(1-t))$. An upstream lemma records the exponential form exactly: $z(t)=\exp\bigl((\pi(1-t))\cdot i\bigr)$. The present result extracts the real part of that value.
This is hinge-data continuation only; full action-level continuation of an interior-hinge complex remains the open C12 question and is not claimed here.
proof idea
Term-mode, two steps. First rewrite the goal via the exponential characterization of the physical arc. The goal becomes $\operatorname{Re}\bigl(\exp((\pi(1-t))\cdot i)\bigr)=\cos(\pi(1-t))$. Discharge by the Mathlib identity that the real part of $\exp(i\theta)$ is $\cos\theta$, applied at $\theta=\pi(1-t)$.
why it matters
Feeds the unit-circle theorem for the physical arc: that result expands $|z(t)|^2$ into real and imaginary parts, substitutes this cosine identity together with the companion sine identity, and closes by $\sin^2+\cos^2=1$. Unit-circle control keeps the open-arc interior strictly in the upper half-plane and underwrites the path-selected branch certificate on the full open arc.
Within the QG Seven-Gaps C11 lane this is elementary analytic scaffolding for the Lorentzian-to-Euclidean hinge continuation, not a ledger-closing step: the FullTheoryLedger gap on action-level 4D continuation stays open. No T0–T8 forcing, RCL, or mass-ladder claim is touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.