boundary_threeTwo_upper_pair
plain-language theorem explainer
Parametric class-C boundary continuation for upper-pair hinges of the (3,2) causal 4-simplex. Under the closed cofactor forms C_pp = C_qq = 8z−4 and C_pq = 3−4z, the split cosine path is continuous on the closed unit interval, with Lorentzian value −7/12 and Euclidean value −1/4. Cited by the three concrete lower-triple pair instantiations. Proof equates the path to a rational function of the Wick arc, then checks continuity and endpoints by direct evaluation.
Claim. Let $p,q\in\{0,1,2,3,4\}$. Suppose the complex Cayley–Menger cofactors of the $(3,2)$ hinge-edge matrix satisfy $C_{pp}(z)=C_{qq}(z)=8z-4$ and $C_{pq}(z)=3-4z$ for all $z\in\mathbb{C}$. Then the split cosine path of the opposite pair $\{p,q\}$ along the canonical upper-half-plane Wick arc is continuous on $[0,1]$, equals $-7/12$ at the Lorentzian endpoint $t=0$, and equals $-1/4$ at the Euclidean endpoint $t=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$. The lower slice is ${0,1,2}$, the upper slice ${3,4}$; the six cross edges are the timelike ones. Opposite pairs fall into three classes. Pairs inside the lower triple give the three upper-pair hinges $(0,3,4)$, $(1,3,4)$, $(2,3,4)$, with closed cofactors $C_{pp}=C_{qq}=8z-4$, $C_{pq}=3-4z$ and squared area $z/4-1/16$.
The cosine path is the split form built from those cofactors along the canonical upper-half-plane arc $z_{\mathrm{Arc}}$ of the complex-first Wick module. Continuity is demanded on the closed interval $[0,1]$, including both Lorentzian ($t=0$) and Euclidean ($t=1$) endpoints. The cofactor identities themselves are kernel-checked by explicit $5\times 5$ minors elsewhere in the module.
proof idea
First apply the algebraic identity equating the upper-pair cosine path to the rational function $(3-4z_{\mathrm{Arc}}(t))/(8z_{\mathrm{Arc}}(t)-4)$ under the three cofactor hypotheses. Continuity on $[0,1]$ follows by rewriting that quotient as a continuous division: numerator and denominator are affine in the continuous arc $z_{\mathrm{Arc}}$, and the denominator never vanishes (the dedicated non-vanishing lemma for the $8z-4$ factor). The two endpoint equalities are then one-line rewrites: substitute $t=0$ and $t=1$, use the arc endpoint lemmas $z_{\mathrm{Arc}}(0)$ and $z_{\mathrm{Arc}}(1)$, and finish by numeric simplification to $-7/12$ and $-1/4$.
why it matters
This is the parametric engine for the three upper-pair boundary certificates in the same module: the concrete pairs $(0,1)$, $(0,2)$, and $(1,2)$ are discharged by feeding the matching cofactor lemmas into this theorem. Together with the mixed-pair and spacelike-hinge branches, those certificates complete the all-ten-hinge boundary continuation demanded by lane B2 of the finishing charter (split-form branch certificate plus boundary continuation on the physical Wick arc).
In the broader Recognition gravity stack this sits inside the Regge/TT hinge analysis that feeds the complex-first Wick program: continuous cosine paths with exact Lorentzian and Euclidean endpoint values are the raw data for the executed arc-trace kill and survival certificates. The upper-pair class is the symmetric $C_{pp}=C_{qq}=8z-4$ case, complementary to the asymmetric mixed hinges and the spacelike hinge whose Lorentzian endpoint sits on the arccos cut.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.