Encyclopedia Gravity Gravity Seven Gaps Wick Three Two Hinges Wick Continuation Three Two Hinges

ARTICLE 3 claims 2 theorems 1 open

Gravity Seven Gaps Wick Three Two Hinges Wick Continuation Three Two Hinges

A machine-checked proof that all ten triangular hinges of a (3,2) causal 4-simplex can be continued from Lorentzian to Euclidean signature without branch cuts, and the two places where the simpler product formula fails.

Verify this page

The all-hinge continuation

In the Recognition Science framework's campaign to understand quantum gravity, a causal 4-simplex (the simplest building block of spacetime, a 4-dimensional triangle with a fixed time direction) comes in two types. The (3,2) type has three vertices in its lower slice and two in its upper slice. The declaration wick_continuation_threeTwo_hinges establishes that all ten triangular hinges of this simplex, the two-dimensional faces where neighboring tetrahedra meet, can be continued from Lorentzian to Euclidean signature. This is the mathematical act of rotating time into imaginary values, a standard technique in physics to make quantum amplitudes well-defined. The continuation works along a specific arc in the complex plane, at the physical point where the scale factor and the lapse are both set to 1.

The proof is fully kernel-checked in the framework's machine-checked library of formal theorems, with no gaps and no extra axioms. It works by explicit computation of 5x5 minors of a 6x6 matrix, giving closed-form expressions for the cosine of the dihedral angle at each hinge. The ten hinges fall into three classes: one spacelike hinge, six mixed hinges with two timelike edges, and three upper-pair hinges. For each class, the continuation is shown to be branch-regular on the open interior of the parameter interval, meaning the function stays on the correct sheet of the square root. At the endpoint t = 0, the spacelike hinge's cosine equals -11/8, which sits exactly on the arccos branch cut, so the certificate is stated only on the open interior; the endpoint value itself is still exact, collapsing to the rational function (5 - 6z)/(6z - 2).

The declaration also memorializes two negative results. The simpler product-form transcription, which would use a single square root of the product of two cofactors, is killed on this simplex type. At two specific interior points, the product crosses the branch cut: for the mixed class, (8z - 4)(6z - 2) equals exactly -40 at Re z = 5/12, and for the upper-pair class, (8z - 4)^2 equals exactly -48 at Re z = 1/2. These are exact, kernel-checked values, not numerical approximations. The failure of the product form at these points means the more elaborate split-form continuation is necessary, and it is this split form that the declaration establishes for all ten hinges.

What the declaration does not claim is just as important as what it proves. The action-level continuation, which would extend the result to the full Regge action with deficit angles and the interior-hinge simplicial complex, is explicitly left open. No claim is made about the physical interpretation of the continued action, and no FullTheoryLedger flag is touched. The result is a precise, self-contained statement about the analytic continuation of the hinge geometry, a necessary step toward a full quantum-gravity amplitude, but not the amplitude itself.

THEOREM branchRegular_threeTwo_spacelike · boundary_threeTwo_spacelike · IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean
branchRegular_threeTwo_spacelike · IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean:664 
/-- THEOREM (class-A branch certificate): branch regularity of the
spacelike hinge on the FULL open interior.  The Lorentzian ENDPOINT value
`-(11/8)` sits exactly ON the arccos cut (the classical boost angle); that
is an ALLOWED endpoint contact and is NOT part of this interior statement.
On the interior the cosine's imaginary part is
`-18 im z / normSq (6z - 2) ≠ 0`. -/
theorem branchRegular_threeTwo_spacelike :
    BranchRegularOn
      (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t)
      3 4 (Set.Ioo 0 1) := by
  intro t ht
  dsimp only
  have hy : 0 < (zArc t).im := zArc_im_pos ht
  have hv3 : cmVertexIndexC 3 = 4 := rfl
  have hv4 : cmVertexIndexC 4 = 5 := rfl
  have him6 : (6 * zArc t - 2).im = 6 * (zArc t).im := by
    simp only [Complex.sub_im, Complex.mul_im, Complex.re_ofNat,
      Complex.im_ofNat]
    ring
  have hslit : 6 * zArc t - 2 ∈ Complex.slitPlane := by
    apply Complex.mem_slitPlane_iff.mpr
    right
    rw [him6]
    exact (mul_pos (by norm_num : (0 : ℝ) < 6) hy).ne'
  refine ⟨?_, ?_, ?_⟩
  · rw [hv3, continuationEdgesC_physical32, cof32_d4]
    exact hslit
  · rw [hv4, continuationEdgesC_physical32, cof32_d5]
    exact hslit
  · left
    have hcos : dihedralCosSplitC
        (continuationEdgesC CausalPentType.threeTwo 1 1 t) 3 4
        = (5 - 6 * zArc t) / (6 * zArc t - 2) :=
      threeTwoCosPath_eq_spacelike t
    rw [hcos]
    have hnum : (5 - 6 * zArc t).im * (6 * zArc t - 2).re
        - (5 - 6 * zArc t).re * (6 * zArc t - 2).im
        = -18 * (zArc t).im := by
      simp only [Complex.sub_im, Complex.sub_re, Complex.mul_im,
        Complex.mul_re, Complex.re_ofNat, Complex.im_ofNat]
      ring
    have hdiv : ((5 - 6 * zArc t) / (6 * zArc t - 2)).im
        = (-18 * (zArc t).im) / Complex.normSq (6 * zArc t - 2) := by
      rw [Complex.div_im, div_sub_div_same, hnum]
    rw [hdiv]
    apply div_ne_zero
    · exact ne_of_lt (mul_neg_of_neg_of_pos (by norm_num) hy)
    · exact (Complex.normSq_pos.mpr (denom_ne t)).ne'
boundary_threeTwo_spacelike · IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean:713 
/-- THEOREM (class-A boundary continuation): continuous on the CLOSED
interval; Lorentzian value `-(11/8)` (ON the arccos cut, allowed endpoint
contact, disclosed above); Euclidean value `-(1/4)`. -/
theorem boundary_threeTwo_spacelike :
    ContinuousOn (threeTwoCosPath 3 4) (Set.Icc 0 1)
      ∧ threeTwoCosPath 3 4 0 = -(11 / 8 : ℂ)
      ∧ threeTwoCosPath 3 4 1 = -(1 / 4 : ℂ) := by
  refine ⟨?_, ?_, ?_⟩
  · have hmo : Continuous fun t => (5 - 6 * zArc t) / (6 * zArc t - 2) := by
      apply Continuous.div
      · exact continuous_const.sub (continuous_const.mul continuous_zArc)
      · exact (continuous_const.mul continuous_zArc).sub continuous_const
      · exact fun t => denom_ne t
    exact hmo.continuousOn.congr fun t _ => threeTwoCosPath_eq_spacelike t
  · rw [threeTwoCosPath_eq_spacelike 0, zArc_zero]
    norm_num
  · rw [threeTwoCosPath_eq_spacelike 1, zArc_one]
    norm_num
THEOREM product_form_crossing_value_mixed · product_form_crossing_value_upper · IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean
product_form_crossing_value_mixed · IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean:1231 
/-- THEOREM (exact crossing value, mixed class): at `tStarMixed` the
product-form denominator argument `(8z - 4)(6z - 2)` equals `-40`
EXACTLY. -/
theorem product_form_crossing_value_mixed :
    (8 * zArc tStarMixed - 4) * (6 * zArc tStarMixed - 2) = -40 := by
  have hz : zArc tStarMixed = ((5 / 12 : ℝ) : ℂ)
      + ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ) * Complex.I := by
    rw [zArc_eq_exp, Complex.exp_mul_I, ← Complex.ofReal_cos,
      ← Complex.ofReal_sin, cos_arg_tStarMixed]
  have h84 : 8 * zArc tStarMixed - 4
      = -(2 / 3 : ℂ)
        + 8 * ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ)
          * Complex.I := by
    rw [hz]
    push_cast
    ring
  have h62 : 6 * zArc tStarMixed - 2
      = (1 / 2 : ℂ)
        + 6 * ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ)
          * Complex.I := by
    rw [hz]
    push_cast
    ring
  have hprod : (8 * zArc tStarMixed - 4) * (6 * zArc tStarMixed - 2)
      = -(1 / 3 : ℂ)
        - 48 * ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ) ^ 2 := by
    rw [h84, h62]
    linear_combination
      (48 * ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ) ^ 2)
        * Complex.I_sq
  have hs2 : Real.sin (Real.pi * (1 - tStarMixed)) ^ 2 = 119 / 144 := by
    rw [Real.sin_sq, cos_arg_tStarMixed]
    norm_num
  have hcast : ((Real.sin (Real.pi * (1 - tStarMixed)) : ℝ) : ℂ) ^ 2
      = ((119 / 144 : ℝ) : ℂ) := by
    rw [← Complex.ofReal_pow, hs2]
  rw [hprod, hcast]
  push_cast
  norm_num
product_form_crossing_value_upper · IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean:1301 
/-- THEOREM (exact crossing value, upper-pair class): at `t = 2/3` the
product-form denominator argument `(8z - 4)^2 = 16 (2z - 1)^2` equals
`-48` EXACTLY. -/
theorem product_form_crossing_value_upper :
    (8 * zArc (2 / 3) - 4) * (8 * zArc (2 / 3) - 4) = -48 := by
  have hz : zArc (2 / 3) = ((1 / 2 : ℝ) : ℂ)
      + ((Real.sin (Real.pi * (1 - 2 / 3)) : ℝ) : ℂ) * Complex.I := by
    rw [zArc_eq_exp, Complex.exp_mul_I, ← Complex.ofReal_cos,
      ← Complex.ofReal_sin, cos_arg_twoThirds]
  have h84 : 8 * zArc (2 / 3) - 4
      = 8 * ((Real.sin (Real.pi * (1 - 2 / 3)) : ℝ) : ℂ) * Complex.I := by
    rw [hz]
    push_cast
    ring
  have hprod : (8 * zArc (2 / 3) - 4) * (8 * zArc (2 / 3) - 4)
      = -(64 : ℂ) * ((Real.sin (Real.pi * (1 - 2 / 3)) : ℝ) : ℂ) ^ 2 := by
    rw [h84]
    linear_combination
      (64 * ((Real.sin (Real.pi * (1 - 2 / 3)) : ℝ) : ℂ) ^ 2)
        * Complex.I_sq
  have hs2 : Real.sin (Real.pi * (1 - 2 / 3)) ^ 2 = 3 / 4 := by
    rw [Real.sin_sq, cos_arg_twoThirds]
    norm_num
  have hcast : ((Real.sin (Real.pi * (1 - 2 / 3)) : ℝ) : ℂ) ^ 2
      = ((3 / 4 : ℝ) : ℂ) := by
    rw [← Complex.ofReal_pow, hs2]
  rw [hprod, hcast]
  push_cast
  norm_num

What this page does not claim

No claim is made about the physical interpretation of the continued action. The declaration does not provide the full Regge action with deficit angles. No claim is made about the behavior of the continuation at the branch cut endpoints for the mixed or upper-pair hinges.

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/WickThreeTwoHinges.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