branchRegular_threeTwo_upper_pair
plain-language theorem explainer
For opposite vertices of an upper-pair hinge on the (3,2) causal 4-simplex, if the Cayley-Menger cofactors equal the closed forms 8z-4 on both diagonals and 3-4z off-diagonal, the physical Wick edge data stay branch-regular on the open arc (0,1). Seven-Gaps lane-B2 hinge certificates cite this parametric lemma for the three lower-triple pairs. The proof reduces regularity to slit-plane membership of 8z-4 and a strictly nonzero imaginary part of the collapsed cosine via the upper-pair cosine-path identity.
Claim. Let $p,q\in\{0,1,2,3,4\}$. Suppose the Cayley-Menger cofactors of the complex hinge-edge matrix satisfy $C_{pp}(z)=C_{qq}(z)=8z-4$ and $C_{pq}(z)=3-4z$ for every $z\in\mathbb{C}$. Then the physical Wick continuation of the $(3,2)$ causal 4-simplex edges (parameters $a=\alpha=1$) is branch-regular for the opposite pair $(p,q)$ on the open interval $(0,1)$.
background
Lane B2 of the QG Seven-Gaps campaign treats all-hinge complex-first Wick continuation of the (3,2) causal 4-simplex at the physical point $a=1$, $\alpha=1$, along the canonical upper-half-plane arc $z_{\mathrm{arc}}$. The threeTwo type has lower slice ${0,1,2}$ and upper slice ${3,4}$; timelike edges are exactly the six cross edges.
Hinges are classified by the opposite vertex pair. Pairs inside the lower triple give the three upper-pair hinges $(0,3,4)$, $(1,3,4)$, $(2,3,4)$, with closed cofactor forms $C_{pp}=C_{qq}=8z-4$, $C_{pq}=3-4z$, and squared area $z/4-1/16$. These forms are kernel-checked by explicit $5\times 5$ minors against the executed trace table.
Branch regularity on an open parameter set demands that both diagonal cofactors lie in the complex slit plane and that the collapsed (dihedral) cosine has nonzero imaginary part, so the arccos branch stays off the cut. The certificate is interior-only: the worst interior-attained trace margin quoted for this class is $0.4167$.
proof idea
Fix $t\in(0,1)$. Positivity of $\mathrm{Im}(z_{\mathrm{arc}}(t))$ is immediate from the arc lemma. A short imaginary-part computation gives $\mathrm{Im}(8z-4)=8,\mathrm{Im} z>0$, so $8z-4$ lies in the slit plane.
BranchRegularOn is discharged in three goals. The two diagonal goals rewrite the physical continuation edges to the assumed cofactors $8z-4$ and reuse slit-plane membership. The off-diagonal goal invokes the upper-pair cosine-path identity, collapsing the dihedral cosine to the rational $(3-4z)/(8z-4)$. Expanding the quotient imaginary part yields $-8,\mathrm{Im} z/|8z-4|^2$; the numerator is strictly negative on the open arc and the denominator is positive by the nonzero-denominator lemma for this class.
why it matters
This is the single parametric class-C branch certificate for every upper-pair hinge of the (3,2) simplex. It is instantiated three times downstream: for opposite pairs $(0,1)$, $(0,2)$, and $(1,2)$, each supplying the matching closed cofactor lemmas and obtaining interior branch regularity of the physical continuation edges.
Together with the spacelike and mixed-pair certificates in the same module, it completes the split-form branch side of lane B2 (all ten triangular hinges). The module also memorializes the two remaining product-form kill certificates from the executed Wick-arc trace. The result sits inside the gravity finishing charter rather than the T0-T8 forcing chain, but it is required infrastructure for a fully certified complex-first Wick path on the causal 4-simplex used in the discrete gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.