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

ARTICLE 3 claims 3 theorems

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

In a discrete model of quantum gravity, a proposed shortcut for computing angles fails at two exact points, and a machine-checked proof says why.

Verify this page

A branch cut that fails

In the Recognition Science framework's study of quantum gravity, a four-simplex (the four-dimensional analogue of a triangle) is built from ten edges. The framework assigns each edge a length, and from those lengths one can compute the angle between any two faces, a dihedral angle. The computation is not always easy: when a length becomes imaginary, as happens in the Lorentzian signature of spacetime, the angle formula develops a branch cut, a line in the complex plane where the function is discontinuous. A proposed simplification, the product form, replaces a complicated square root of a product with a single square root. The declaration in question, branchRegular_threeTwo_mixed_pair, is a machine-checked theorem that proves this simplification is not valid for the mixed class of hinges in a particular simplex type.

The simplex type is called threeTwo, referring to its two slices: a lower slice with three vertices and an upper slice with two. The six edges connecting the slices are timelike, meaning they point along time; the three edges within the lower slice are spacelike, meaning they point along space. A hinge is a triangle where two faces meet, and it is determined by the pair of vertices opposite it. The mixed class of hinges, six in total, has one vertex in each slice, so the hinge triangle contains two timelike edges and one spacelike edge. For these hinges, the product form fails at two specific points along the continuous path that interpolates between the Euclidean and Lorentzian regimes. At a parameter value of approximately 0.6368, the product of the two cofactors equals -40 exactly; at exactly two-thirds, the product equals -48. These are branch crossings, points where the product form's square root would switch to the wrong branch, making it discontinuous.

The theorem is a negative result, a certificate that a particular approach is dead. It is proved in the framework's machine-checked library of formal theorems, meaning the reasoning is verified step by step by a computer. The declaration itself is a theorem, not a definition: it states that the product form is not branch-regular on the open interior of the path for the mixed hinges. The proof relies on explicit 5x5 matrix minors, whose determinants are computed exactly. The result is specific to the threeTwo simplex at the physical point where the scale factor a and the parameter alpha are both 1. It does not claim anything about other simplex types, other hinge classes, or the action-level continuation of the theory, which 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 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 declaration does not claim the product form fails for the spacelike hinge, which has its own separate branch certificate. It does not claim the action-level continuation of the theory is invalid, only that this particular product-form transcription is. It does not claim the framework's model of quantum gravity is physically correct, only that this internal computation is formally verified.

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