Gravity Seven Gaps Wick Action Complex First Lorentzian Endpoint Sign Factor

The endpoint sign factor

In the Wick rotation of a four-dimensional simplex, one often moves a squared edge length from a negative (Lorentzian) value to a positive (Euclidean) value along a semicircular arc in the complex plane. The Recognition Science declaration lorentzian_endpoint_sign_factor pins down what happens to a particular geometric cosine at the starting point of that arc, where the squared edge is negative. It states that the value of the cosine at the Lorentzian endpoint is exactly the negative of what the real-number formula would give.

The setting is a specific triangle, called the fourOne hinge, inside a causal 4-simplex. The cosine in question is built from cofactors of the Cayley-Menger matrix, a matrix whose entries are squared distances and which encodes the geometry of the simplex. The complex continuation uses a square root defined with a branch cut along the negative real axis. At the Lorentzian endpoint, the cofactors themselves land exactly on that cut, and the square root of a negative number is taken as a complex number, not as a positive real. The theorem proves that the split-form cosine, which keeps the two square roots separate in the denominator, equals minus the real product formula at that endpoint.

The theorem is a kernel-checked result, meaning it has been verified by a machine-checked library of formal theorems. The proof is short: it evaluates the path at the endpoint, substitutes the closed form of the cosine, and simplifies. The value at the Lorentzian endpoint is -(3/8), while the Euclidean endpoint gives -(1/4). The sign factor is the difference between these two conventions, and it matters because a continuation that ignores it would misstate the value at the starting point.

The declaration does not claim that the whole action, the sum of deficit angles over a simplicial complex, continues smoothly. That is a separate open question. It also does not claim an unrestricted equality with the real Lorentzian formula; the equality holds only at the endpoint, with the sign factor applied. The theorem is a precise, local statement about one hinge, not a global statement about the entire gravitational action.

/-- 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 (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: Lorentzian endpoint value of the SPLIT form: `-(3/8)`.
(The real product-form formula gives `+3/8` here; see
`lorentzian_endpoint_sign_factor` for the documented sign factor.) -/
theorem hingeCosPath_zero : hingeCosPath 0 = -(3 / 8 : ℂ) := by
  rw [hingeCosPath_eq_moebius, zArc_zero]
  norm_num

/-- THEOREM: Euclidean endpoint value: `-(1/4)`, the regular unit
4-simplex value in the `+C_pq` convention (textbook `-C` interior dihedral
cosine `+1/4`; RESULTS.txt endpoint table). -/
theorem hingeCosPath_one : hingeCosPath 1 = -(1 / 4 : ℂ) := by
  rw [hingeCosPath_eq_moebius, zArc_one]
  norm_num

What this page does not claim

The theorem does not establish the action-level continuation of the Regge action itself. It does not claim an unrestricted equality with the real Lorentzian formula away from the endpoint. It does not assert that the sign factor applies to all hinges or all simplices.

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: