module module moderate

`IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges`

Supplies complex-first Wick edge tuples, hinge matrices, and minors for the (3,2) causal 4-simplex at unit spacelike length and timelike arc value z. Complements the (4,1) all-hinges package so both causal types can be conjoined. Downstream completeness over all twenty hinges cites this data. Mostly definitional edge/matrix construction parallel to the (4,1) lane.

claimComplex edge data, Cayley-Menger-style hinge matrices, and principal minors for the $(3,2)$ causal $4$-simplex under complex-first Wick continuation, at unit spacelike edge length and timelike parameter $z$ on the upper-half-plane arc $z=\mathrm{zArc}(t)$.

background

The QG Seven-Gaps campaign formalizes 4D Lorentzian Wick continuation of Regge hinge data in a complex-first style. Causal 4-simplices split into two types, $(4,1)$ and $(3,2)$. Edge lengths live in $\mathbb{C}$, continue along a canonical upper-half-plane arc, and hinge regularity is read from determinants of Cayley-Menger-type matrices built from those edges.

Upstream, WickActionComplexFirst builds the complex-first 4D framework (lane C11) and certifies split-form branch regularity plus boundary continuation for a single traced hinge. WickFourOneAllHinges extends those certificates to all ten triangular hinges of the $(4,1)$ type at the physical point $a=1$, $\alpha=1$.

This module is the $(3,2)$ data counterpart: the complex edge tuple at unit spacelike value and timelike $z$ (continuation of the threeTwo pattern at those parameters), together with the associated hinge matrix, submatrices, and lower minors used in the same determinant tests.

proof idea

Definition-and-construction module, not a single theorem. It introduces the $(3,2)$ complex edge tuple at the physical point, the hinge matrix assembled from those edges, named submatrices (principal blocks and complementary blocks), and the corresponding minors and their determinants. The pattern mirrors the $(4,1)$ all-hinges package: fix $a=1$, continue timelike edges on the arc, then expose the matrix algebra needed for branch-regularity and boundary-continuation certificates on the $(3,2)$ side.

why it matters in Recognition Science

Lane B of the finishing charter needs both causal types before completeness. Downstream WickHingeDataComplete (lane B3) is the conjunction of per-type certificates into one statement over both causal 4-simplex types and all twenty hinges. Without the $(3,2)$ edge/matrix/minor package, that conjunction has nothing to conjoin on the threeTwo side.

Together with the $(4,1)$ all-hinges module and the complex-first base, this closes the hinge-data half of the Wick program for Regge calculus in the Seven-Gaps campaign. It does not itself state the global completeness theorem; it supplies the missing type so that theorem can be stated honestly.

scope and limits

Does not treat $(4,1)$ hinges; those live in the sibling all-hinges module.
Does not state the two-type completeness conjunction; that is the downstream complete module.
Does not reconstruct full continuum GR or Einstein equations from hinge data alone.
Does not claim numeric gate receipts; those sit in the campaign RESULTS artifacts.
Does not extend off the physical point $a=1$ or off the canonical arc without further work.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.WickHingeDataComplete module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst module_import
IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges module_import

declarations in this module (99)

def hingeEdges32C L97
theorem continuationEdgesC_physical32 L102
def hingeMatrix32C L116
theorem cmMatrixC_hingeEdges32 L139
theorem submatrix32_44 L149
theorem submatrix32_55 L157
def minor32LowerC L166
theorem submatrix32_11 L184
theorem submatrix32_22 L190
theorem submatrix32_33 L196
theorem det_minor32LowerC L206
def minor32_45C L216
theorem submatrix32_45 L231
theorem det_minor32_45C L239
def minor32_14C L245
theorem submatrix32_14 L262
theorem det_minor32_14C L270
def minor32_15C L276
theorem submatrix32_15 L293
theorem det_minor32_15C L301
def minor32_24C L307
theorem submatrix32_24 L324
theorem det_minor32_24C L332
def minor32_25C L338
theorem submatrix32_25 L355
theorem det_minor32_25C L363
def minor32_34C L369
theorem submatrix32_34 L386
theorem det_minor32_34C L394
def minor32_35C L400
theorem submatrix32_35 L417
theorem det_minor32_35C L425
def minor32_12C L431
theorem submatrix32_12 L448
theorem det_minor32_12C L456
def minor32_13C L462
theorem submatrix32_13 L479
theorem det_minor32_13C L487
def minor32_23C L493
theorem submatrix32_23 L510
theorem det_minor32_23C L518
theorem cof32_d1 L525
theorem cof32_d2 L531
theorem cof32_d3 L537
theorem cof32_d4 L543
theorem cof32_d5 L549
theorem cof32_45 L555
theorem cof32_14 L561
theorem cof32_15 L567
theorem cof32_24 L573
theorem cof32_25 L579
theorem cof32_34 L585
theorem cof32_35 L591
theorem cof32_12 L597
theorem cof32_13 L603
theorem cof32_23 L609
theorem denom32_ne L619
def threeTwoCosPath L632
theorem threeTwoCosPath_symm L635
theorem threeTwoCosPath_apply_symm L639
theorem boundary32_symm L644
theorem threeTwoCosPath_eq_spacelike L656
theorem branchRegular_threeTwo_spacelike L670
theorem boundary_threeTwo_spacelike L716
theorem threeTwoCosPath_eq_mixed L738
theorem branchRegular_threeTwo_mixed_pair L754
theorem boundary_threeTwo_mixed_pair L800
theorem threeTwoCosPath_eq_upper L894
theorem branchRegular_threeTwo_upper_pair L910
theorem boundary_threeTwo_upper_pair L959
theorem branchRegular32_pair03 L985
theorem branchRegular32_pair04 L992
theorem branchRegular32_pair13 L999
theorem branchRegular32_pair14 L1006
theorem branchRegular32_pair23 L1013
theorem branchRegular32_pair24 L1020
theorem branchRegular32_pair01 L1027
theorem branchRegular32_pair02 L1034
theorem branchRegular32_pair12 L1041
theorem boundary32_pair03 L1047

… and 19 more