BranchRegularOn
plain-language theorem explainer
Predicate of branch regularity for a split-form hinge path: along a real parameter set, both diagonal Cayley–Menger cofactors stay in the complex slit plane (off the principal square-root cut) and the split dihedral cosine stays off the arccos cuts. Cited by every fourOne hinge certificate on the open Wick arc. Pure definitional Prop, no proof content.
Claim. For a path $x:\mathbb{R}\to(\mathrm{Fin}\,10\to\mathbb{C})$ of complex squared edge lengths of a 4-simplex, opposite vertices $p,q\in\{0,\ldots,4\}$, and a parameter set $s\subseteq\mathbb{R}$, branch regularity on $s$ means: for every $t\in s$, the diagonal Cayley–Menger cofactors $C_{pp}(x(t))$ and $C_{qq}(x(t))$ lie in the complex slit plane, and the split-form dihedral cosine of the hinge opposite $(p,q)$ lies off the arccos branch cuts.
background
Module C11 formalizes complex-first 4D Wick continuation of Regge hinge data (areas-squared and dihedral cosines) for causal 4-simplex classes. The physical arc is $z(t)=\alpha a^2\exp(i\pi(1-t))$ on $t\in[0,1]$, Lorentzian at $t=0$ and Euclidean at $t=1$, with open interior in the upper half-plane. Scope is hinge-data only; full action-level continuation remains open (C12 / ledger gap).
Squared edges are packaged as SqEdges10C ($\mathrm{Fin},10\to\mathbb{C}$). Diagonal cofactors $C_{rr}$ come from the bordered $6\times 6$ Cayley–Menger matrix; they feed the principal square root csqrt, continuous precisely on the slit plane. The split cosine is the ratio of the off-diagonal cofactor to the product of those square roots. Branch cuts of csqrt and arccos are the only analytic obstacles on the arc.
proof idea
Definitional abbreviation: the body is the universal quantification over $t\in s$ of the three-way conjunction (both diagonal cofactors in Complex.slitPlane, and the split cosine off the arccos cut). No tactics, no lemmas applied. Downstream theorems inhabit the predicate by proving the three conjuncts pointwise on the open interval $(0,1)$.
why it matters
S3 model predicate for the C11 branch certificate. Every fourOne hinge theorem is an inhabitation of this Prop: the single traced hinge opposite $(2,3)$ on $(0,1)$; the parametric timelike and spacelike pair lemmas; and the B1 headline that all ten unordered opposite pairs are branch-regular on the full open arc at $a=\alpha=1$. Symmetry in the opposite pair is proved directly from the definition.
It encodes the gate requirement that the split-sqrt denominator stay continuous and the dihedral cosine avoid arccos cuts, matching the numeric interior margins in the Wick arc trace. It does not close the open ledger gap on genuine action-level continuation of a full interior-hinge complex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.