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

ARTICLE 3 claims 3 theorems

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

A machine-checked proof shows a certain simplified formula for quantum gravity angles fails at a precise point; here is what that failure means and what it does not prove.

Verify this page

A specific obstruction

A ledger, in this framework, is a discrete record of events. In a quantum gravity calculation, one often needs to continue a formula from imaginary time back to real time, a process called a Wick rotation. The declaration product_form_crossing_threeTwo_mixed concerns a specific four-dimensional simplex, a shape with five vertices, and a particular simplified way of writing its geometry.

The shape in question is the (3,2) causal 4-simplex, which has a lower slice of three vertices and an upper slice of two. Its six cross edges are timelike, meaning they point along time. The calculation asks whether a certain product formula, which multiplies two cofactors together under a single square root, correctly describes the angles of this simplex as time is continued. The declaration proves that this product formula fails: at a specific point on the continuation path, the product of the two cofactors equals exactly -40, a negative number. The square root of a negative number is not real, so the formula crosses a branch cut and cannot be used there.

The failure point is not arbitrary. It occurs at a time parameter t* = 1 - arccos(5/12)/pi, approximately 0.6368, which lies strictly between 0 and 1. At this point, the cosine of the continuation angle equals 5/12, a rational number. This is a precise, kernel-checked result: the theorem product_form_crossing_value_mixed states that (8z - 4)(6z - 2) = -40 at the relevant complex point z. The proof is sorry-free, meaning it relies only on the machine-checked library's standard axioms.

What this does not claim is just as important. The declaration does not prove that the full, unsimplified theory fails. It only kills this particular single-square-root transcription. The framework explicitly leaves open the action-level continuation, which involves the full simplicial complex and deficit angles. The result is a negative certificate, a memorialized obstruction that tells researchers which simplified route does not work, not a statement that no route works.

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 tStarMixed_mem_Ioo · IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean
tStarMixed_mem_Ioo · IndisputableMonolith/Gravity/SevenGaps/WickThreeTwoHinges.lean:1203 
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 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

What this page does not claim

The full theory of quantum gravity is not proven to fail. No claim is made that the action-level continuation is impossible. The result does not establish any physical prediction about the real universe.

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