module module moderate

`IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst`

Complex-first Wick substrate for causal 4-simplices: ten complex squared edge lengths, Cayley-Menger matrix/minors/cofactors over ℂ, a principal complex square root, and the split-form dihedral denominator. CDT and Lorentzian-sector workers cite it when continuing hinge data through the upper half-plane. The module is mostly definitions plus short complex identities; deep hinge theorems live downstream.

claimInfrastructure for a causal 4-simplex with complex squared edge lengths $s_e\in\mathbb{C}$ on the ten edges (lexicographic order), the Cayley-Menger matrix and cofactors over $\mathbb{C}$, a complex square root satisfying $(\sqrt{z})^2=z$ on the working branch, and the split-form denominator for dihedral (hinge) continuation along a canonical upper-half-plane arc.

background

In the QG Seven-Gaps Lorentzian lane, Phase 3a lifts kernel-checked 3D causal-simplex Wick machinery to $D=4$. Upstream CausalSimplex4D fixes CDT-style causal 4-simplex classes (notably the $(4,1)$ and $(3,2)$ types) and the real combinatorial edge indexing.

Wick continuation of triangular hinges needs squared lengths and Cayley-Menger volume/dihedral formulae promoted from $\mathbb{R}$ to $\mathbb{C}$, so a path in the upper half-plane can connect Lorentzian to Euclidean signature without premature branch cuts. This module supplies those objects: complex edge squares on $\mathrm{Fin},10$, complex Cayley-Menger data, and a complex square root with the self-square identity.

Convention is complex-first: identities are proved in $\mathbb{C}$, then specialized downstream at the physical point $a=1$, $\alpha=1$ on a fixed arc.

proof idea

Definition-and-identity module, not a deep theorem package. It mirrors CausalSimplex4D combinatorics in $\mathbb{C}$: complex squared edges, Cayley-Menger matrix/minors/cofactors with index bookkeeping, a complex square root with $(\sqrt{z})^2=z$, and the split-form dihedral denominator used later for branch regularity. Any proofs are short algebraic or Mathlib complex-analysis facts (cofactor signs, square-root multiplication, $\mathrm{Fin},10$ reindexing), not geometric existence or full hinge continuation.

why it matters in Recognition Science

Shared analytic substrate for lane B of the finishing charter. Downstream, the $(4,1)$ all-hinge module extends the one-hinge split-form branch regularity and boundary continuation certified against this data to all ten triangular hinges at the physical point on the canonical arc. The $(3,2)$ hinge module does the same for that causal type (plus product-form kill certificates). The completeness module conjoins both into one statement over both types and all twenty hinges.

Without complex-first edges and Cayley-Menger cofactors, those all-hinge Wick certificates have nothing to continue. The module sits after 4D causal-simplex classification in the Lorentzian gravity lane; it does not itself close the Seven-Gaps campaign.

scope and limits

Does not prove all-hinge Wick continuation; that is downstream.
Does not choose physical (4,1) versus (3,2) geometry; only complex data.
Does not claim a unique global dihedral branch off the chosen arc.
Does not treat dynamical Regge or Einstein-Hilbert extremization.
Does not depend on the 3D CausalSimplexWick import path.

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