denom_ne
plain-language theorem explainer
On the unit-modulus Wick arc the Cayley–Menger cofactor $6z-2$ never vanishes, endpoints included. Continuity and closed-form identities for the traced $(4,1)$ hinge cosine cite this non-vanishing denominator. Proof is a short contradiction: $|z|=1$ forces $|6z|^2=36\neq 4=|2|^2$.
Claim. For every real $t$, writing $z(t)$ for the complex Wick-arc edge value (with $|z(t)|=1$), one has $6z(t)-2\neq 0$. Equivalently the traced $(4,1)$ hinge cofactor never hits zero on the closed arc, since the only candidate root $z=1/3$ lies off the unit circle.
background
Module C11 formalizes 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))$ for $t\in[0,1]$, with Lorentzian endpoint $z(0)=-\alpha a^2$ and Euclidean endpoint $z(1)=+\alpha a^2$. For the traced unit hinge one takes $\alpha=a=1$, so $|z(t)|=1$ everywhere.
The split-form dihedral cosine is a rational function of $z$ whose denominator is the cofactor $6z-2$ (opposite vertex pair on the fourOne hinge triangle $(0,1,4)$). Downstream continuity and Möbius collapse identities require that this denominator stay off zero on the whole closed interval. The module is deliberately hinge-data only: full action-level continuation remains the open C12 ledger gap.
proof idea
Proof by contradiction. Assume $6,z(t)-2=0$, rewrite as $6z(t)=2$ over $\mathbb{C}$, and equate squared moduli. Multiplicativity of Complex.normSq plus the arc identity $|z(t)|^2=1$ (and $|n|^2=n^2$ for natural $n$) yields $36\cdot 1=4$. norm_num discharges the numerical absurdity. No case split on $t$; the argument is uniform on all of $\mathbb{R}$.
why it matters
This is the algebraic gate that lets the split cosine collapse to the cut-free Möbius form $(1-2z)/(6z-2)$ on the whole arc and stay continuous on the closed interval $[0,1]$. Downstream consumers include the branch-regularity certificate for the traced fourOne timelike hinge on $(0,1)$, the closed-interval continuity of the hinge cosine path, the Möbius identification itself, and the parametric fourOne/threeTwo boundary and branch theorems in the sibling all-hinges modules.
In the QG Seven-Gaps C11 lane it underwrites the PATH-SELECTED continuation with a proved interior branch certificate (trace margin $0.625$ on this hinge). It does not close the ledger gap wick_action_continuation_4d: that still needs a genuine interior-hinge complex (C12).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.