Encyclopedia Gravity Gravity Seven Gaps Wick Four One All Hinges Boundary Four One Timelike Pair

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Wick Four One All Hinges Boundary Four One Timelike Pair

A machine-checked proof shows that a specific quantum gravity path integral, the (4,1) causal 4-simplex, can be smoothly continued from Lorentzian to Euclidean geometry without hitting a mathematical obstruction.

Verify this page

The boundary continuation

The (4,1) causal 4-simplex is the simplest building block of a spacetime with one time dimension and four space dimensions. Its name encodes the split: one vertex is the apex, connected to the other four by timelike edges, while the edges among the base four vertices are spacelike. In quantum gravity, one often wants to compute a path integral by starting with a Lorentzian geometry (with its familiar minus sign for time) and rotating to a Euclidean geometry (all plus signs), a procedure called Wick rotation. The question is whether this rotation can be done smoothly, without the square roots in the geometry hitting a branch cut where the calculation becomes undefined.

The declaration boundary_fourOne_timelike_pair, proved in the framework's machine-checked library of formal theorems, answers that question for all ten triangular hinges of this simplex. A hinge is a triangle within the 4-simplex, and its opposite pair is the complementary two vertices. The proof establishes two facts. First, on the open interior of the rotation path, the square-root branch is regular: the calculation never touches the forbidden cut. Second, on the closed interval including the endpoints, the cosine of the dihedral angle is continuous and ends at the value -(1/4), which is the Euclidean regular-4-simplex value. The Lorentzian endpoint values are also computed: -(3/8) for hinges whose opposite pair lies in the base, and the purely imaginary value (sqrt 2 / 8) * I for hinges whose opposite pair includes the apex.

The significance is that this removes a potential obstruction for one specific building block. The proof is not a numerical approximation; it is a formal theorem, checked by the kernel, with no gaps. The closed forms for the ten hinge areas-squared are also derived, showing they avoid the square-root cut everywhere except at the allowed Lorentzian endpoint. This is a necessary step, but it is not the whole story.

What the declaration does not claim is equally important. It does not establish the action-level continuation: the full Regge action, with deficit angles summed over the interior hinges, is not constructed here. That remains an open target in the framework's campaign. The declaration also does not touch any global ledger flag, meaning it does not claim to have completed the entire theory. It is a local, technical result about one simplex, not a proof of quantum gravity.

THEOREM branchRegular_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
branchRegular_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean:1011 
/-- THEOREM (B1 headline, branch certificates): for EVERY hinge of the
fourOne causal 4-simplex (every unordered opposite vertex pair, both
orientations), the split-form continuation is branch-regular on the FULL
open arc interior at the physical point `a = 1`, `alpha = 1`.  The ten
hinges: (0,1,2)|(3,4), (0,1,3)|(2,4), (0,1,4)|(2,3), (0,2,3)|(1,4),
(0,2,4)|(1,3), (0,3,4)|(1,2), (1,2,3)|(0,4), (1,2,4)|(0,3),
(1,3,4)|(0,2), (2,3,4)|(0,1). -/
theorem branchRegular_fourOne_allHinges :
    ∀ p q : Fin 5, p ≠ q →
      BranchRegularOn
        (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t) p q
        (Set.Ioo 0 1) := by
  intro p q hpq
  fin_cases p <;> fin_cases q
  · exact absurd rfl hpq
  · exact branchRegular_pair01
  · exact branchRegular_pair02
  · exact branchRegular_pair03
  · exact branchRegular_pair04
  · exact branchRegularOn_symm branchRegular_pair01
  · exact absurd rfl hpq
  · exact branchRegular_pair12
  · exact branchRegular_pair13
  · exact branchRegular_pair14
  · exact branchRegularOn_symm branchRegular_pair02
  · exact branchRegularOn_symm branchRegular_pair12
  · exact absurd rfl hpq
  · exact branchRegular_pair23
  · exact branchRegular_pair24
  · exact branchRegularOn_symm branchRegular_pair03
  · exact branchRegularOn_symm branchRegular_pair13
  · exact branchRegularOn_symm branchRegular_pair23
  · exact absurd rfl hpq
  · exact branchRegular_pair34
  · exact branchRegularOn_symm branchRegular_pair04
  · exact branchRegularOn_symm branchRegular_pair14
  · exact branchRegularOn_symm branchRegular_pair24
  · exact branchRegularOn_symm branchRegular_pair34
  · exact absurd rfl hpq
THEOREM wick_boundary_continuation_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
wick_boundary_continuation_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean:1111 
/-- THEOREM (B1 headline, boundary continuation): every split-form cosine
path of the fourOne type is continuous on the CLOSED interval `[0, 1]` and
ends at the Euclidean regular-4-simplex value `-(1/4)` (`+C_pq` numerator
convention of the landed module; textbook `-C` interior cosine `+1/4`). -/
theorem wick_boundary_continuation_fourOne_allHinges :
    ∀ p q : Fin 5, p ≠ q →
      ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
        ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ) := by
  intro p q hpq
  fin_cases p <;> fin_cases q
  · exact absurd rfl hpq
  · exact ⟨boundary_pair01.1, boundary_pair01.2.2⟩
  · exact ⟨boundary_pair02.1, boundary_pair02.2.2⟩
  · exact ⟨boundary_pair03.1, boundary_pair03.2.2⟩
  · exact ⟨boundary_pair04.1, boundary_pair04.2.2⟩
  · exact boundary_symm ⟨boundary_pair01.1, boundary_pair01.2.2⟩
  · exact absurd rfl hpq
  · exact ⟨boundary_pair12.1, boundary_pair12.2.2⟩
  · exact ⟨boundary_pair13.1, boundary_pair13.2.2⟩
  · exact ⟨boundary_pair14.1, boundary_pair14.2.2⟩
  · exact boundary_symm ⟨boundary_pair02.1, boundary_pair02.2.2⟩
  · exact boundary_symm ⟨boundary_pair12.1, boundary_pair12.2.2⟩
  · exact absurd rfl hpq
  · exact ⟨boundary_pair23.1, boundary_pair23.2.2⟩
  · exact ⟨boundary_pair24.1, boundary_pair24.2.2⟩
  · exact boundary_symm ⟨boundary_pair03.1, boundary_pair03.2.2⟩
  · exact boundary_symm ⟨boundary_pair13.1, boundary_pair13.2.2⟩
  · exact boundary_symm ⟨boundary_pair23.1, boundary_pair23.2.2⟩
  · exact absurd rfl hpq
  · exact ⟨boundary_pair34.1, boundary_pair34.2.2⟩
  · exact boundary_symm ⟨boundary_pair04.1, boundary_pair04.2.2⟩
  · exact boundary_symm ⟨boundary_pair14.1, boundary_pair14.2.2⟩
  · exact boundary_symm ⟨boundary_pair24.1, boundary_pair24.2.2⟩
  · exact boundary_symm ⟨boundary_pair34.1, boundary_pair34.2.2⟩
  · exact absurd rfl hpq
THEOREM det_minor41_15C · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
det_minor41_15C · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean:547 
theorem det_minor41_15C (z : ℂ) : Matrix.det (minor41_15C z) = -1 := by
  unfold minor41_15C
  simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
  ring
THEOREM fourOne_areaSq_interior_off_cut · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
fourOne_areaSq_interior_off_cut · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean:1255 
/-- THEOREM: the constant spacelike-class area-squared `3/16` avoids the
sqrt cut EVERYWHERE (both endpoints included), and the timelike-class
area-squared `z/4 - 1/16` avoids it on the full open interior (its
Lorentzian endpoint value `-5/16` sits ON the cut boundary, the ALLOWED
endpoint contact documented in the landed module). -/
theorem fourOne_areaSq_interior_off_cut {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) :
    ((3 / 16 : ℂ) ∈ Complex.slitPlane)
      ∧ (zArc t / 4 - 1 / 16 ∈ Complex.slitPlane) := by
  constructor
  · exact Complex.mem_slitPlane_iff.mpr (Or.inl (by norm_num))
  · apply Complex.mem_slitPlane_iff.mpr
    right
    have hy : 0 < (zArc t).im := zArc_im_pos ht
    have him : (zArc t / 4 - 1 / 16).im = (zArc t).im / 4 := by
      simp only [Complex.sub_im, Complex.div_ofNat_im, Complex.one_im]
      ring
    rw [him]
    exact (div_pos hy (by norm_num : (0 : ℝ) < 4)).ne'

What this page does not claim

The action-level continuation with deficit angles and the continued Regge action itself is not established. No claim is made about the full quantum gravity theory or any global ledger flag. The result does not prove that the Wick rotation is valid for any other simplex type.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND