Pith. sign in
theorem

boundary_threeTwo_mixed_pair

proved
show as:
module
IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges
domain
Gravity
line
800 · github
papers citing
none yet

plain-language theorem explainer

For any mixed opposite pair (one lower-slice vertex, one upper-slice vertex) of the (3,2) causal 4-simplex, the split-form cosine path along the canonical upper-half-plane Wick arc is continuous on the closed unit interval, with Lorentzian endpoint √6/24 and Euclidean endpoint −1/4. Gravity and Regge-calculus workers cite it as the class-B boundary certificate for all six mixed hinges. The proof reduces the path to an explicit quotient of complex square roots, then checks continuity and the two endpoint evaluations by direct algebra.

Claim. Let $p,q\in\{0,1,2,3,4\}$. Suppose the Cayley–Menger cofactors of the complexified (3,2) hinge edge matrix satisfy $C_{pp}(z)=8z-4$, $C_{qq}(z)=6z-2$, and $C_{pq}(z)=-1$ for all $z\in\mathbb{C}$. Then the split cosine path $t\mapsto\cos_{3,2}(p,q;t)$ along the canonical upper-half-plane arc is continuous on $[0,1]$, equals $\sqrt{6}/24$ 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 Wick continuation of every triangular hinge of the (3,2) causal 4-simplex at the physical point $a=1$, $\alpha=1$. Vertices split into a lower triple ${0,1,2}$ and an upper pair ${3,4}$; the six cross edges are the only timelike ones. Mixed opposite pairs (one lower, one upper) give the six hinges with two timelike triangle edges. Their Cayley–Menger cofactors are asymmetric: $C_{pp}=8z-4$ on the lower member, $C_{qq}=6z-2$ on the upper member, and off-diagonal $C_{pq}=-1$, with squared area $z/4-1/16$.

The cosine of a hinge is realized in split form as the normalized cofactor quotient $C_{pq}/\sqrt{C_{pp}C_{qq}}$. Continuation is performed along the canonical upper-half-plane arc $z_{\mathrm{Arc}}$ of the complex-first Wick package, which runs from the Lorentzian point $z=-1$ at $t=0$ to the Euclidean point $z=1$ at $t=1$, staying in the closed upper half-plane. Complex square-root branches are chosen so that imaginary parts remain non-negative on the arc, keeping the path off the branch cut except at controlled endpoint contact.

proof idea

First apply the algebraic identity that rewrites the mixed cosine path as $$t\mapsto -1\big/\bigl(\sqrt{8z_{\mathrm{Arc}}(t)-4},\sqrt{6z_{\mathrm{Arc}}(t)-2}\bigr).$$ Continuity on $[0,1]$ follows by composing continuous affine maps in $z_{\mathrm{Arc}}$ with the continuous complex square-root (justified by non-vanishing denominators and non-negative imaginary parts along the arc), then dividing. At $t=0$ one substitutes $z=-1$, obtains pure-negative reals $-12$ and $-8$, takes principal square roots $i\sqrt{12}$ and $i\sqrt{8}$, and reduces the quotient by the identity $\sqrt{12}\sqrt{8}=4\sqrt{6}$ to $\sqrt{6}/24$. At $t=1$ one substitutes $z=1$, both radicands become $4$, and $\sqrt{4}\sqrt{4}=4$ yields $-1/4$.

why it matters

This is the single parametric class-B boundary certificate for all six mixed hinges of the (3,2) simplex. Downstream it is instantiated once per pair as the six theorems for opposite pairs $(0,3)$, $(0,4)$, $(1,3)$, $(1,4)$, $(2,3)$, $(2,4)$, each supplying the matching closed-form cofactor lemmas. Together with the spacelike-hinge and upper-pair certificates in the same module, it completes the all-hinge continuous Wick continuation demanded by lane B2 of the Seven-Gaps finishing charter.

In the broader Recognition gravity stack this feeds the complex-first Regge action on causal 4-simplices: continuous cosine paths on the closed arc guarantee that the hinge deficit angles (and thus the Einstein–Hilbert discrete action) remain well-defined through the Lorentzian-to-Euclidean transition. The Lorentzian value $\sqrt{6}/24\approx 0.102$ is the exact classical boost cosine at a mixed hinge; the Euclidean value $-1/4$ is the corresponding spherical cosine. No scaffolding remains on this class.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.