Pith. sign in
def

hingeMatrix32C

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

plain-language theorem explainer

Explicit bordered 6×6 Cayley–Menger matrix over ℂ for the (3,2) causal 4-simplex at spacelike edge-value 1 and timelike value z. Gravity and Regge-calculus workers cite it as the concrete kernel for all ten triangular-hinge minors on the Wick arc. The body is a pure pattern-match table: border of ones, lower-triple and upper-pair blocks filled by 1, cross-slice entries equal to z.

Claim. For $z \in \mathbb{C}$, define the bordered $6 \times 6$ complex matrix $H(z)$ with indices $\{0,\ldots,5\}$ by: $H_{00}=0$ and $H_{0j}=H_{i0}=1$ for $i,j\ge 1$; diagonal entries $H_{ii}=0$; mutual entries among the lower-slice block $\{1,2,3\}$ equal to $1$; the upper-slice pair entry $H_{45}=H_{54}=1$; and every remaining cross-slice entry equal to $z$. Rows/cols $1..3$ index lower-slice vertices $0..2$, rows/cols $4..5$ index upper-slice vertices $3..4$.

background

Lane B2 of the QG Seven-Gaps campaign treats the all-hinge complex-first Wick continuation of the (3,2) causal 4-simplex. The simplex splits into a lower spacelike triple ${0,1,2}$ and an upper spacelike pair ${3,4}$; the six cross edges are the timelike ones. Hinge classes are labelled by opposite edge pairs and carry closed cofactor formulae ($C_{pp}$, $C_{qq}$, $C_{pq}$) and squared areas that must be kernel-checked via $5\times 5$ minors.

The classical object behind those minors is the bordered Cayley–Menger (CM) matrix of squared edge lengths. Here the two-value tuple is fixed at spacelike length-squared $1$ and complex timelike parameter $z$, mirroring CausalSimplex4D.pentMatrix32 at $(p,q)=(1,z)$. Index $0$ is the CM border; indices $1..3$ and $4..5$ are the two slices.

The ambient module works on the canonical upper-half-plane arc of the complex-first Wick action, at the physical point $a=1$, $\alpha=1$, and aims at split-form branch certificates for all ten triangular hinges plus two product-form kill certificates.

proof idea

Pure definition by exhaustive pattern match on (i.val, j.val). The border row/column is hard-coded to the standard CM pattern (corner $0$, off-border $1$). All six diagonal slots are $0$. The three lower-slice off-diagonals and the single upper-slice off-diagonal are set to the spacelike value $1$. Every unmatched pair falls through to the timelike parameter $z$. No lemmas are invoked; the table is the object.

why it matters

This matrix is the single explicit kernel that the rest of the lane factors through. The theorem cmMatrixC_hingeEdges32 identifies the abstract complex CM matrix of the threeTwo edge tuple with this table, so every later minor computation can work with concrete entries. Downstream submatrix32_ij theorems peel off each $5\times 5$ principal or off-principal block (e.g. minor32LowerC, minor32_12C, …) by Fin.succAbove and rfl, feeding the kernel checks that match the per-hinge cofactor table in the executed Wick-arc trace.

Those minors underwrite the closed forms for all three hinge classes (spacelike opposite pair, six mixed pairs, three upper-pair hinges) and the honest endpoint disclosure that the spacelike hinge cosine sits on the arccos cut at the Lorentzian endpoint while remaining branch-certifiable on the open arc. In the broader Recognition gravity stack this is scaffolding for Regge deficit angles on the (3,2) 4-simplex, not a forcing-chain (T0–T8) step.

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