zArc_im
plain-language theorem explainer
The imaginary part of the unit physical Wick arc equals sin(π(1−t)) for every real t. Anyone proving the arc stays in the closed upper half-plane, or that its modulus is one, cites this identity. The argument is a one-line rewrite to the exponential form plus the standard Im(e^{iθ}) formula.
Claim. For every real $t$, if $z(t)=\exp\bigl(i\pi(1-t)\bigr)$ denotes the unit physical Wick arc, then $\operatorname{Im} z(t)=\sin\bigl(\pi(1-t)\bigr)$.
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 physical-point specialization used here takes unit lattice spacing and $\alpha=1$, so the arc collapses to $z(t)=\exp(i\pi(1-t))$. An upstream equality records exactly that this definition coincides with the complex exponential of $i\pi(1-t)$. The present lemma extracts the imaginary part of that exponential.
Honest scope of the module: this is hinge-data continuation only. Action-level continuation of a full interior-hinge complex remains open (C12 / ledger gap).
proof idea
Rewrite the arc via the upstream exponential identity, reducing the claim to $\operatorname{Im}\bigl(\exp(i\theta)\bigr)=\sin\theta$ with $\theta=\pi(1-t)$. Discharge by the Mathlib lemma that the imaginary part of $\exp(x\cdot i)$ for real $x$ is $\sin x$. Term-mode, two steps, no case splits.
why it matters
This identity is the Im half of the polar decomposition of the physical arc. Downstream it feeds the unit-circle theorem (norm-squared equals 1 via $\sin^2+\cos^2$), the strict upper-half-plane positivity on the open interval $(0,1)$, and the closed-interval nonnegativity used in the all-hinges 4-1 panel. Together those facts certify the PATH-SELECTED branch of the Wick arc interior for hinge data in the QG Seven-Gaps C11 lane.
It does not touch the still-open ledger gap on genuine action-level continuation; that remains a separate C12 question. Within Recognition gravity scaffolding it is a local analytic hinge, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.