Gravity Seven Gaps Wick Three Two Hinges Product Form Crossing Value Mixed

A negative result, made exact

In the Recognition Science framework's study of quantum gravity, researchers often work with a simplified model of spacetime called a causal 4-simplex, a four-dimensional building block with ten triangular faces, or hinges. A proposed shortcut, called the product-form transcription, would replace a complicated expression for each hinge with the square root of a product of two simpler terms. The declaration product_form_crossing_value_mixed is a machine-checked proof that this shortcut fails for one class of hinges, the mixed class, at a specific interior point of the calculation's path.

The proof pins down the failure with an exact number. At a particular point on the path, the product of the two terms equals -40, a negative number. A square root of a negative number is not a real number, so the proposed simplification cannot produce a real-valued result there. This is not an approximation or a numerical estimate; it is a theorem in the framework's machine-checked library of formal theorems, meaning the calculation is verified step-by-step by a computer. The point where this happens is given by a formula involving the arccosine function, and its value is approximately 0.6368, which lies strictly between 0 and 1, confirming it is inside the valid range of the path.

This negative result is part of a larger effort to map out where the product-form shortcut fails. A companion theorem, product_form_crossing_value_upper, proves a similar failure for another class of hinges, the upper-pair class, where the product equals -48 at a different interior point. Together, these two results, along with a previously established failure for the fourOne crossing, show that the shortcut fails for all ten hinges of this particular simplex type. The framework's library memorializes these failures as certificates, so future work does not repeat the attempt.

What the declaration does not claim is just as important as what it proves. It does not claim that the product-form shortcut fails everywhere; it only proves failure at one specific point for one class of hinges. It also does not claim anything about the physical validity of the overall approach to quantum gravity. The proof is a mathematical statement about a specific algebraic expression, not a statement about the actual structure of spacetime. The framework explicitly leaves open the next step: continuing the action itself, which would involve the full geometric structure of the simplex, not just the hinge angles.

/-- 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 tStarMixed_mem_Ioo : tStarMixed ∈ Set.Ioo (0 : ℝ) 1 := by
  have hpi := Real.pi_pos
  have h1 : 0 < Real.arccos (5 / 12) := Real.arccos_pos.mpr (by norm_num)
  have h2 : Real.arccos (5 / 12) ≤ Real.pi / 2 :=
    Real.arccos_le_pi_div_two.mpr (by norm_num)
  constructor
  · have hle : Real.arccos (5 / 12) / Real.pi ≤ 1 / 2 := by
      rw [div_le_iff₀ hpi]
      linarith
    unfold tStarMixed
    linarith
  · have hgt : 0 < Real.arccos (5 / 12) / Real.pi := div_pos h1 hpi
    unfold tStarMixed
    linarith

/-- 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 product-form shortcut fails everywhere for the mixed hinge class. The failure of the shortcut has any physical consequence for spacetime. The action-level continuation of the simplex has been completed.

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: