module module moderate

`IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges`

Library of complex-analytic and matrix lemmas for the 4–1 causal type in the 4D Wick continuation of Regge hinge data. It pins non-vanishing and quadrant placement of the principal square root, imaginary-part signs on the Wick arc, and symmetry of the complex Cayley–Menger matrix, minors, and cofactors. Downstream cut-limit and hinge-completeness certificates import it as shared infrastructure. Proofs are short complex-analysis and matrix identities, not a single terminal theorem.

claimFor the 4–1 causal 4-simplex hinges under complex-first Wick rotation: the principal square root $\sqrt{z}$ is nonzero for $z\neq 0$, lands in the closed first quadrant on the relevant rays, and the complex Cayley–Menger matrix $C$, its minors, and cofactors are symmetric. Imaginary parts along the Wick arc stay nonnegative where required for the $\mathrm{carccos}$ branch.

background

This sits in the QG Seven-Gaps campaign, complex-first lane for 4D Lorentzian Wick continuation of Regge hinge data (panel C11). The parent module builds the complex-first formalization: edge lengths and dihedral data are continued through a complex arc so that Lorentzian anchors arise as boundary values of holomorphic (or continuous-on-slit) functions rather than as ad hoc real formulas.

Regge calculus stores simplex geometry in Cayley–Menger determinants; after Wick rotation those entries become complex. The principal branch $\mathrm{csqrt}$ and a complex arccos must stay on controlled sides of their cuts. Sibling lemmas here record that $\sqrt{z}\neq 0$ off the origin, place $\sqrt{x}$ for real $x$, control $\mathrm{Im}$ along the arc, and prove symmetry of the complex Cayley–Menger matrix and its minors/cofactors so hinge volumes and angles are well-defined for every 4–1 hinge.

Notation follows Mathlib complex analysis: principal square root, open quadrant conditions, and ContinuousOn compositions used later by cut-limit arguments.

proof idea

Not a single proof: a bundle of short lemmas. Non-vanishing of $\mathrm{csqrt}$ is the standard principal-branch fact off $0$. Quadrant and real-ray lemmas reduce to Mathlib square-root and argument bounds. Imaginary-part positivity on the Wick arc is a direct computation from the arc parametrization and product rules in the first quadrant. Continuity of $\mathrm{csqrt}\circ f$ is ContinuousOn composition on sets avoiding the branch cut. Matrix, minor, and cofactor symmetry are entrywise or determinant identities for the complex Cayley–Menger array (transpose invariance). No deep tactic automation; algebraic and library facts.

why it matters in Recognition Science

4–1 hinges are one of the two causal 4-simplex types that must be continued before the campaign can claim completeness over all twenty hinges. This module is the shared substrate imported by WickActionInteriorHinge (frozen continuation schema and carccos lift), WickActionCutLimit and WickActionCutLimitFamily (N4 cut-boundary limits and the $\alpha>7/12$ family), WickActionCertAssembly (certificate assembly at $\alpha=1$), WickHingeDataComplete (conjunction over both causal types), WickThreeTwoHinges (the companion 3–2 type), and the gap6 lookalike-falsify receipt.

Without controlled $\mathrm{csqrt}$ and symmetric complex Cayley–Menger data, the carccos cut limits and the terminal wick_action_continuation_4d schema have nothing well-defined to evaluate. It does not itself close gap6 or flip ledger Bools; it removes analytic and linear-algebra blockers so those receipts can cite hinge values safely.

scope and limits

Does not prove the terminal wick_action_continuation_4d proposition or close gap6 ledgers.
Does not treat 3–2 hinges; that lives in the companion WickThreeTwoHinges module.
Does not establish uniform-in-α cut limits; only pointwise complex-sqrt and matrix facts.
Does not choose physical units or fix G, c, ħ; pure complex geometry of hinge data.
Does not claim holomorphicity across the arccos cut; only off-cut and arc-side control.

used by (7)

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

IndisputableMonolith.Gravity.SevenGaps.Gap6LookalikeReceipt module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionCertAssembly module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimit module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimitFamily module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHinge 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.WickActionComplexFirst module_import

declarations in this module (97)

theorem csqrt_ne_zero L106
theorem csqrt_mem_Q1 L114
theorem csqrt_ofReal_nonneg L155
theorem csqrt_four L163
theorem csqrt_ofReal_neg L173
theorem neg_one_div_im_pos L205
theorem mul_im_pos_of_Q1 L221
theorem zArc_im_nonneg L228
theorem continuousOn_csqrt_comp L244
theorem cmMatrixC_symm L288
theorem cmMinorC_symm L294
theorem cmCofactorC_symm L305
theorem dihedralCosSplitC_symm L311
theorem branchRegularOn_symm L317
theorem submatrix41_11 L338
theorem submatrix41_22 L345
def minor41_55C L353
theorem submatrix41_55 L363
theorem det_minor41_55C L373
def minor41_12C L381
theorem submatrix41_12 L396
theorem det_minor41_12C L404
def minor41_13C L410
theorem submatrix41_13 L425
theorem det_minor41_13C L433
def minor41_14C L439
theorem submatrix41_14 L454
theorem det_minor41_14C L462
def minor41_23C L468
theorem submatrix41_23 L483
theorem det_minor41_23C L491
def minor41_24C L497
theorem submatrix41_24 L512
theorem det_minor41_24C L520
def minor41_15C L526
theorem submatrix41_15 L539
theorem det_minor41_15C L547
def minor41_25C L553
theorem submatrix41_25 L566
theorem det_minor41_25C L574
def minor41_35C L580
theorem submatrix41_35 L593
theorem det_minor41_35C L601
def minor41_45C L607
theorem submatrix41_45 L620
theorem det_minor41_45C L628
theorem cofactor41_d1 L638
theorem cofactor41_d2 L644
theorem cofactor41_d5 L650
theorem cofactor41_12 L656
theorem cofactor41_13 L662
theorem cofactor41_14 L668
theorem cofactor41_23 L674
theorem cofactor41_24 L680
theorem cofactor41_15 L686
theorem cofactor41_25 L692
theorem cofactor41_35 L698
theorem cofactor41_45 L704
def fourOneCosPath L715
theorem fourOneCosPath_symm L718
theorem fourOneCosPath_apply_symm L722
theorem boundary_symm L727
theorem fourOneCosPath_eq_timelike L738
theorem fourOneCosPath_eq_spacelike L752
theorem branchRegular_fourOne_timelike_pair L765
theorem branchRegular_fourOne_spacelike_pair L816
theorem boundary_fourOne_timelike_pair L856
theorem boundary_fourOne_spacelike_pair L884
theorem branchRegular_pair01 L943
theorem branchRegular_pair02 L950
theorem branchRegular_pair03 L957
theorem branchRegular_pair12 L964
theorem branchRegular_pair13 L971
theorem branchRegular_pair23 L978
theorem branchRegular_pair04 L984
theorem branchRegular_pair14 L991
theorem branchRegular_pair24 L998
theorem branchRegular_pair34 L1005
theorem branchRegular_fourOne_allHinges L1018
theorem boundary_pair01 L1051

… and 17 more