module module moderate

`IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst`

Infrastructure for a complex-first Wick continuation of the 4-simplex gravitational action: squared edge lengths in ℂ, Cayley–Menger minors over ℂ, a principal complex square root, and the split dihedral denominator. Gravity and CDT workers cite it when lifting Lorentzian (4,1) and (3,2) simplices off the real axis. The module is mostly definitions and elementary complex identities, not a single theorem.

claimFor a causal 4-simplex, equip the ten edges (lex order) with complex squared lengths $s_e \in \mathbb{C}$, form the complex Cayley–Menger matrix and its cofactors, and define a principal square root $\sqrt{\cdot}_{\mathbb{C}}$ so that dihedral and volume factors of the Regge–Wick action admit a holomorphic split-form continuation off the Lorentzian locus.

background

The QG Seven-Gaps campaign treats Lorentzian causal dynamical triangulations in $D=4$. Upstream, CausalSimplex4D classifies CDT-style 4-simplices (notably the $(4,1)$ and $(3,2)$ types) and sets the kinematical stage for a Wick rotation that stays faithful to the causal gluing, rather than a naive Euclidean replacement of the metric signature.

This module works complex-first: edge data are promoted to ten complex squared lengths indexed by $\mathrm{Fin},10$ in the lexicographic order of the pentachoron edge list. From those lengths one builds the complex Cayley–Menger matrix, its minors and signed cofactors, and a complex square root used in volume and dihedral expressions. The point is to keep branch choices and denominators under explicit algebraic control before any real-section specialization.

Sibling objects include the realized edge tuple, squared-distance helpers, CM index/vertex maps, cofactor signs, csqrt with $z\cdot z = w$ when $z=\sqrt{w}$, and a split form of the dihedral denominator that later proofs use for hinge regularity.

proof idea

Definition-and-identity module, not a single end-to-end theorem. It introduces complex edge arrays and Cayley–Menger scaffolding over $\mathbb{C}$, then proves elementary facts (e.g. csqrt_mul_self, cofactor sign conventions, the dihedral denominator split). Downstream hinge certificates import these objects and specialize them on the upper-half-plane arc at the physical point; the hard analytic work lives in those consumers, not here.

why it matters in Recognition Science

Lane B of the finishing charter needs a single complex chart in which every triangular hinge of both causal 4-simplex types can be continued. This module is that chart: squared edges, CM cofactors, and the split dihedral denominator that make branch regularity checkable.

It is imported by the all-hinge $(4,1)$ continuation (ten hinges at $a=1$, $\alpha=1$ on the canonical arc), the all-hinge $(3,2)$ continuation (ten hinges plus residual product-form kills), and the completeness conjunction over both types and all twenty hinges. Without the complex-first edge and CM layer, those certificates would re-derive branch algebra ad hoc. In the broader RS gravity lane this is kinematical scaffolding for Lorentzian Regge calculus under Wick rotation, not a mass or $\alpha$ claim.

scope and limits

Does not prove full Wick continuation of the 4-simplex action for all hinges.
Does not classify causal 4-simplex types; that lives in CausalSimplex4D.
Does not fix physical edge lengths or the $(a,\alpha)=(1,1)$ specialization.
Does not address dynamical equations, measure, or path-integral convergence.
Does not claim Euclidean CDT equivalence beyond the complex chart setup.

used by (3)

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

IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges module_import
IndisputableMonolith.Gravity.SevenGaps.WickHingeDataComplete module_import
IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D module_import

declarations in this module (67)

theorem realized L29
abbrev SqEdges10C L154
def pentDistSqC L158
def cmIndexVertexC L185
def cmMatrixC L190
def cmMinorC L200
def cmCofactorSignC L204
def cmCofactorC L209
def cmVertexIndexC L214
def csqrt L227
theorem csqrt_mul_self L231
def dihedralDenomSplitC L242
def dihedralCosSplitC L251
def triCMMatrixC L258
def triangleAreaSqC L277
def hingeAreaSqC L282
def arcZ L293
def continuationEdgesC L298
theorem arcZ_zero L303
theorem arcZ_one L311
theorem continuationEdgesC_zero L320
theorem continuationEdgesC_one L332
def zArc L345
theorem zArc_eq_exp L347
theorem zArc_re L352
theorem zArc_im L356
theorem zArc_zero L360
theorem zArc_one L365
theorem normSq_zArc L371
theorem zArc_im_pos L378
theorem continuous_zArc L388
theorem denom_ne L400
def hingeEdgesC L417
theorem continuationEdgesC_physical L422
def hingeMatrixC L434
theorem cmMatrixC_hingeEdges L457
def minorPPC L464
def minorPQC L483
theorem submatrix_pp L500
theorem submatrix_qq L506
theorem submatrix_pq L512
theorem det_minorPPC L523
theorem det_minorPQC L535
theorem cofactor_pp L542
theorem cofactor_qq L550
theorem cofactor_pq L558
theorem hingeAreaSqC_closed L569
def OffArccosCut L587
def BranchRegularOn L594
def hingeCosPath L603
theorem hingeCosPath_eq_moebius L611
theorem branchRegular_fourOne_hinge L628
theorem hingeAreaSq_interior_off_cut L673
theorem continuousOn_hingeCosPath L691
theorem hingeCosPath_zero L702
theorem hingeCosPath_one L709
theorem wick_boundary_continuation_fourOne_hinge L720
def realLorentzianProductCos L729
theorem realLorentzianProductCos_eq L732
theorem lorentzian_endpoint_sign_factor L745
theorem endpoint_cofactor_on_sqrt_cut L757
def tStar L773
theorem tStar_mem_Ioo L775
theorem arg_tStar L790
theorem cos_arg_tStar L797
theorem product_form_crossing_value L805
theorem product_form_crossing L840