Encyclopedia Gravity Gravity Seven Gaps Wick Three Two Hinges Branch Regular Three Two Spacelike

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Wick Three Two Hinges Branch Regular Three Two Spacelike

A machine-checked proof shows that a particular angle in a four-dimensional simplex can be followed smoothly through time, and that a naive shortcut fails.

Verify this page

A branch without a cut

In the geometry of curved spacetime, a simplex is the simplest building block: a triangle in two dimensions, a tetrahedron in three, and in four dimensions a shape with five corners. The dihedral angle between two faces of such a simplex is a number that changes as the simplex evolves. The declaration branchRegular_threeTwo_spacelike concerns one specific dihedral angle in one specific kind of four-dimensional simplex, and it proves that this angle can be followed continuously through a full interval of time without hitting a mathematical obstruction.

The simplex in question has a particular arrangement of its five corners, called the threeTwo type: three corners form one slice, two form another, and the six edges connecting the slices are the timelike ones, meaning they represent the flow of time. The angle in question is the one opposite the pair of corners in the two-slice, which is called the spacelike hinge. The theorem proves that as a parameter t runs from 0 to 1, the cosine of this angle traces a smooth, continuous path with no branch cut, no point where the formula would jump or become ambiguous. This is a statement about the complex continuation of the angle, a technique used to connect quantum and classical regimes.

The proof is not just a hand-waving argument. It is a machine-checked theorem in the framework's library of formal theorems, meaning every step has been verified by a computer. The declaration also pins down the boundary values: at the start of the interval the cosine is exactly -11/8, and at the end it is -1/4. The starting value sits precisely on a known mathematical cut, the place where the arccos function is not smooth, so the theorem is careful to state regularity only on the open interval, not at the endpoints. The endpoint values themselves are still exact, because the formula simplifies to a rational function there.

The theorem also establishes a negative result, a kind of memorialized failure. A naive way to write the angle's formula would use a single square root of a product of two factors. The declaration proves this naive product form fails for two other classes of hinges in the same simplex: at a specific time t* ≈ 0.6368 the product equals -40, and at exactly t = 2/3 it equals -48, both crossing into a region where the branch cut would appear. This means the simple transcription is not valid, and the more careful split form proved here is necessary.

In Recognition Science, this result is a step in a larger campaign to understand how gravity emerges from a discrete ledger of events. The framework models spacetime as a collection of such simplices, and the angles between their faces carry the geometric information. This theorem establishes that one particular angle behaves well under continuation, a necessary check for the framework's approach to be consistent. It does not, however, claim that the full quantum action, the quantity that would sum over all such angles, is itself well-defined. That remains an open target.

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 · 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
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'

What this page does not claim

The full action-level continuation, including deficit angles and the continued Regge action, is not established by this declaration. The theorem does not claim that the spacelike hinge angle is regular at the endpoints t = 0 and t = 1, only on the open interval between them. This result does not provide a physical interpretation of the framework's ledger; it is a mathematical consistency check.

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