Gravity Seven Gaps Wick Action Complex First Real Lorentzian Product Cos Eq

The endpoint sign factor

In complex analysis, a function that is smooth in a region can often be extended along a path, but the extension's value at the path's end depends on which branch of a multi-valued function you chose along the way. The declaration realLorentzianProductCos fixes one such endpoint for a specific geometric object: the cosine of the dihedral angle of a triangular hinge in a four-dimensional simplex, computed at the Lorentzian (real, timelike) end of a continuation arc.

The theorem lorentzian_endpoint_sign_factor proves that the complex continuation's value at the start of the arc equals -1 times the real formula's value at that same point. In plain terms: the machine-checked library shows that the complex path and the real formula agree in magnitude but differ in sign at the Lorentzian endpoint. The real formula gives +3/8; the complex path gives -3/8. The factor of -1 is not an error or an inconsistency; it is a proved consequence of the definitional choice to use a split square root in the denominator.

The split form is mandatory. The library proved that the alternative, a single square root of a product, crosses the branch cut of the complex square root at an interior point of the arc, making the continuation discontinuous there. The split form avoids that crossing on the full open arc interior, and the endpoint sign factor is the price of that regularity. The theorem is sorry-free and kernel-checked, so the sign is not a matter of convention; it is forced by the definitions.

What the declaration does not claim is broader. It does not claim that the complex continuation equals the real formula in general; the equality is only at the Lorentzian endpoint, and even there only up to the sign factor. It does not claim that this hinge-data continuation is an action-level continuation of gravity; that would require an interior-hinge simplicial complex, which is a separate open question. The theorem is a precise, narrow statement about one endpoint value, not a license to replace real formulas with complex ones elsewhere.

/-- THEOREM (S4 documented sign convention): at the Lorentzian endpoint,
where both cofactors are negative (`C_pp = C_qq = -8`), the split form
equals `(-1) *` (the real product-form value): `csqrt w * csqrt w = w`,
not `|w|`, so the split denominator is `-8` where `Real.sqrt 64 = +8`.
The sign factor is exactly `-1` on this hinge (trace: split `-3/8` vs
real-formula `+3/8`, RESULTS.txt §3 endpoint note). -/
theorem lorentzian_endpoint_sign_factor :
    hingeCosPath 0 = (-1 : ℂ) * ((realLorentzianProductCos : ℝ) : ℂ) := by
  rw [hingeCosPath_zero, realLorentzianProductCos_eq]
  push_cast
  ring

/-- THEOREM (exact crossing value): at `tStar` the arc point is
`z = 1/3 + i * sin(arccos(1/3))` and the product-form denominator argument
`C_pp * C_qq = (6z - 2)^2` equals `-32` EXACTLY: a real negative value in
the interior of the arc. -/
theorem product_form_crossing_value :
    (6 * zArc tStar - 2) * (6 * zArc tStar - 2) = -32 := by
  have hz : zArc tStar = ((1 / 3 : ℝ) : ℂ)
      + ((Real.sin (Real.pi * (1 - tStar)) : ℝ) : ℂ) * Complex.I := by
    rw [zArc_eq_exp, Complex.exp_mul_I, ← Complex.ofReal_cos,
      ← Complex.ofReal_sin, cos_arg_tStar]
  have h6z : 6 * zArc tStar - 2
      = ((Real.sin (Real.pi * (1 - tStar)) : ℝ) : ℂ) * Complex.I * 6 := by
    rw [hz]
    push_cast
    ring
  have hprod : (6 * zArc tStar - 2) * (6 * zArc tStar - 2)
      = -(36 : ℂ) * ((Real.sin (Real.pi * (1 - tStar)) : ℝ) : ℂ) ^ 2 := by
    rw [h6z]
    linear_combination (36 * ((Real.sin (Real.pi * (1 - tStar)) : ℝ) : ℂ) ^ 2)
      * Complex.I_sq
  have hs2 : Real.sin (Real.pi * (1 - tStar)) ^ 2 = 8 / 9 := by
    rw [Real.sin_sq, cos_arg_tStar]
    norm_num
  have hcast : ((Real.sin (Real.pi * (1 - tStar)) : ℝ) : ℂ) ^ 2
      = ((8 / 9 : ℝ) : ℂ) := by
    rw [← Complex.ofReal_pow, hs2]
  rw [hprod, hcast]
  push_cast
  norm_num

/-- THEOREM (S4 documented sign convention): at the Lorentzian endpoint,
where both cofactors are negative (`C_pp = C_qq = -8`), the split form
equals `(-1) *` (the real product-form value): `csqrt w * csqrt w = w`,
not `|w|`, so the split denominator is `-8` where `Real.sqrt 64 = +8`.
The sign factor is exactly `-1` on this hinge (trace: split `-3/8` vs
real-formula `+3/8`, RESULTS.txt §3 endpoint note). -/
theorem lorentzian_endpoint_sign_factor :
    hingeCosPath 0 = (-1 : ℂ) * ((realLorentzianProductCos : ℝ) : ℂ) := by
  rw [hingeCosPath_zero, realLorentzianProductCos_eq]
  push_cast
  ring

What this page does not claim

The complex continuation equals the real Lorentzian formula at any point other than the arc's endpoint. The hinge-data continuation is an action-level continuation of the Regge action. The sign factor is a matter of convention rather than a proved consequence.

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/WickActionComplexFirst.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: