Encyclopedia Gravity Gravity Seven Gaps Wick Three Two Hinges Branch Regular Three Two Upper Pair

ARTICLE 3 claims 2 theorems 1 open

Gravity Seven Gaps Wick Three Two Hinges Branch Regular Three Two Upper Pair

A machine-checked certificate that a specific quantum gravity path avoids a mathematical branch cut, and the exact limits of that certificate.

Verify this page

The upper-pair branch certificate

In the Recognition Science framework's study of quantum gravity, the declaration branchRegular_threeTwo_upper_pair is a machine-checked certificate. It concerns a specific mathematical object: a path traced by a complex number as a parameter t runs from 0 to 1. The path is associated with a particular geometric configuration called a (3,2) causal 4-simplex, a five-point object with a lower slice of three points and an upper slice of two. The certificate proves that for the three hinges in the upper pair, this path stays within a region where the mathematical function involved is well-behaved, specifically avoiding a branch cut. This is a technical but important result: it ensures that a certain calculation in the framework's approach to gravity does not hit a discontinuity.

The declaration is part of a larger effort, the Seven-Gaps campaign, which aims to check the framework's predictions against established physics. In this case, the work concerns the Wick rotation, a technique used to connect quantum mechanics with statistical mechanics. The framework models this rotation as a complex path, and the branch certificate is a guarantee that this path is valid for the upper-pair hinges. The certificate is not a physical measurement; it is a formal mathematical proof, verified by a computer, that a specific calculation is consistent.

The certificate does not claim that the entire physical theory is complete. The framework explicitly states that the action-level continuation, which would involve the full geometric structure and the continued Regge action, is not claimed. This is listed as an open problem. The certificate also does not touch any global ledger flag, meaning it does not assert that the broader theory is fully validated. It is a narrow, precise result about a specific mathematical path, not a sweeping statement about quantum gravity.

The value of this certificate is in its exactness. It is not an approximation or a heuristic argument; it is a formal proof that the path is regular. This is the kind of result that builds confidence in the framework's internal consistency, even as the larger physical questions remain open. It shows that the framework's machinery can produce rigorous, checkable statements about complex geometric calculations.

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 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 certificate does not prove that the framework's approach to quantum gravity is physically correct. The certificate does not claim that the Wick rotation path is valid for all possible configurations, only for the specific (3,2) type. The certificate does not establish the full theory of quantum gravity within the framework.

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