Encyclopedia Gravity Gravity Seven Gaps Wick Three Two Hinges

ARTICLE 5 claims 4 theorems 1 open

Gravity Seven Gaps Wick Three Two Hinges

A machine-checked proof verifies the analytic continuation of a quantum gravity model across all ten hinges of a causal 4-simplex, and kills two simpler candidate formulas along the way.

Verify this page

The Wick continuation check

A causal 4-simplex is the four-dimensional analogue of a triangle: five points, with some edges marked timelike. In the (3,2) type, three points lie in a lower slice and two in an upper slice, and the six cross edges are the timelike ones. The subject here is the Wick continuation, a standard technique that rotates a time coordinate into the complex plane to turn a difficult oscillating problem into a tractable one. Here the rotation is applied to the dihedral angles, the angles between triangular faces, of this simplex.

The classical question is whether the continuation is well-behaved: does it stay on the correct branch of a square root, or does it hit a cut and become ambiguous? The answer is provided for all ten hinges, the triangular faces where two tetrahedra meet. For each hinge there are closed-form expressions for the relevant cofactors and areas, and the branch is proved regular on the open interior of the continuation path. The spacelike hinge (0,1,2) touches the arccos cut exactly at the Lorentzian endpoint t = 0, where the split cosine equals -11/8, but the interior is clean and the endpoint value itself is still exact.

Two negative results are also recorded. A naive product formula for the square root, using the product of two cofactors, fails on this simplex type. The product crosses the branch cut twice more, at specific interior points: once where the product equals -40 at t ≈ 0.6368, and once where it equals -48 at t = 2/3 exactly. These are memorialized as kill certificates, so future work does not repeat the attempt.

In Recognition Science, this is a lane B deliverable of the Seven-Gaps campaign, the finishing charter's second item. The framework's library proves the branch regularity and the boundary values as theorems. The definitions of the hinge edges and matrices are modeling choices, inherited from a prior complexification. What remains open, explicitly, is the action-level continuation: the full simplicial complex of interior hinges, deficit angles, and the continued Regge action. That is a target, not a result.

The practical consequence is a certificate. Anyone building on this simplex type now knows the split-form continuation is sound on the interior, and knows two product-form shortcuts that are not. The next step is to extend the continuation to the action itself, which is not attempted here.

THEOREM branchRegular_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'
THEOREM boundary_threeTwo_spacelike · IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean
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 · 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
THEOREM product_form_crossing_value_upper · IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean
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

The action-level continuation is not proved, only the hinge-level branch certificates. The product-form kill certificates do not rule out all possible product transcriptions, only the single-sqrt form tested. The FullTheoryLedger flag is not touched, and a complete theory of quantum gravity is not claimed.

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