continuousOn_hingeCosPath
plain-language theorem explainer
The split-form complex dihedral cosine along the Wick arc is continuous on the closed unit interval. Continuity is the missing piece for the fourOne hinge boundary-continuation receipt, which also pins the Lorentzian and Euclidean endpoint values. The proof identifies the path with a cut-free Möbius function of the arc and invokes ordinary complex division continuity once the denominator is known never to vanish.
Claim. The split-form cosine path $t \mapsto \mathrm{hingeCos}(t)$ is continuous on the closed interval $[0,1]$. On that interval it agrees with the rational (Möbius) function $(1-2z(t))/(6z(t)-2)$ of the upper-half-plane arc $z(t)$, whose denominator is nowhere zero.
background
This sits in the C11 complex-first Wick lane for Regge hinge data of a single causal 4-simplex. 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 $z(0)=-\alpha a^2$ and Euclidean endpoint $z(1)=+\alpha a^2$. Interior points lie in the open upper half-plane.
The object under study is the split-form complex dihedral cosine of a traced fourOne timelike hinge, built from complex Cayley-Menger areas-squared and cofactor cosines. Module scope is deliberately hinge-data only: action-level continuation for a full interior-hinge complex is the separate C12 question and remains open on the ledger.
A prior identity equates the path on $[0,1]$ with the cut-free rational function of $z(t)$. A separate non-vanishing lemma guarantees the denominator $6z(t)-2$ never hits zero on the real parameter interval, so ordinary complex division is continuous there.
proof idea
First prove that $t\mapsto(1-2z(t))/(6z(t)-2)$ is continuous on $\mathbb{R}$ (hence on $[0,1]$) by Continuous.div: numerator and denominator are affine in the continuous arc $z(t)$, and the denominator never vanishes by the existing denom_ne fact. Restrict to continuous-on $[0,1]$, then rewrite via pointwise congruence with the identity that the hinge cosine path equals this Möbius expression on the interval. No analytic continuation or branch cuts appear; the argument is pure continuity of rational functions once the cut-free representative is in hand.
why it matters
Downstream, wick_boundary_continuation_fourOne_hinge packages this continuity with the two endpoint evaluations into the S4 boundary-continuation receipt: a continuous path on $[0,1]$ from the Lorentzian value $-(3/8)$ at $t=0$ to the Euclidean regular-4-simplex value $-(1/4)$ at $t=1$. That theorem is the panel-locked C11 flagship deliverable for hinge-data Wick continuation.
In the broader Seven-Gaps gravity campaign this closes the continuity half of the path-selected continuation certificate for dihedral cosines. It does not touch the FullTheoryLedger gap on genuine action-level 4D continuation, which still requires an interior-hinge complex (C12). Framework-wise it is analytic infrastructure for Lorentzian Regge data, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.