Encyclopedia Gravity Gravity Seven Gaps Wick Three Two Hinges Product Form Crossing Value Upper

ARTICLE 3 claims 3 theorems

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

A machine-checked theorem shows a proposed simplification of a quantum gravity calculation fails at an exact, simple point, and the failure is itself a precise result.

Verify this page

The upper-pair crossing

In the Recognition Science framework's campaign to continue a quantum gravity amplitude from real to complex time, one proposed shortcut was to replace a complicated square root by the product of two simpler ones. The declaration product_form_crossing_value_upper is a machine-checked theorem that this shortcut fails for one class of hinges, the upper-pair class, at a specific point. It proves that at the parameter value z = zArc(2/3), the product (8z - 4)(8z - 4) equals exactly -48, not a positive value that would keep the square root on the expected branch.

The setting is a (3,2) causal 4-simplex, a five-vertex building block of spacetime with three points in one time slice and two in another. The six edges connecting the slices are timelike. The upper-pair hinges are the three triangular faces that contain both upper-slice vertices and one lower vertex. For these, the cofactor product is (8z - 4)^2. The theorem evaluates this at z = zArc(2/3), which corresponds to a time parameter t* = 2/3 exactly. At that point the product equals -48, a negative real number, so its square root is imaginary. A negative value under the square root means the product-form transcription crosses a branch cut, invalidating the simplification on the open interior of the continuation path.

The result is a negative result, memorialized as a kill certificate. It does not compute a physical quantity, nor does it describe a valid continuation. It establishes a precise obstruction: the single-square-root transcription cannot work for the upper-pair hinges. The companion theorem product_form_crossing_value_mixed proves a similar failure for the mixed hinge class at t* ≈ 0.6368, where the product equals -40. Together they close off a proposed route for the all-hinge continuation, leaving the action-level continuation open.

In Recognition Science, the declaration is a theorem, kernel-checked with no axioms beyond the standard three. It is not a model choice, not a measurement, and not a claim about the physical world. It is a statement about a specific algebraic expression within a defined complexification. The endpoint value at the Lorentzian boundary t = 0 is handled separately and is exact, but the branch certificate is stated only on the open interior, where the imaginary part of the cosine is strictly negative.

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
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
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 theorem does not compute a physical amplitude or a measurable quantity. It does not establish that the product-form transcription fails everywhere, only at the specified points. It does not claim the action-level continuation is impossible, only that this particular route is blocked.

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