Gravity Seven Gaps Wick Four One All Hinges Four One Area Sq Interior Off Cut

The interior cut check

In the Recognition Science framework's gravity program, a 4-simplex is the four-dimensional analogue of a triangle: a shape with five vertices, ten edges, and ten triangular faces. The declaration fourOne_areaSq_interior_off_cut concerns one specific type, the (4,1) causal simplex, where one vertex is the apex and the four timelike edges all touch it. The theorem checks that two closed-form expressions for the squared area of a triangular hinge, a term for one of the ten faces, never land on the branch cut of the complex square-root function.

The two expressions are the constant 3/16 and z/4 - 1/16, where z is a complex parameter running along the physical arc. The theorem states that for every interior point of the open interval (0, 1), both values lie in the slit plane, the complex plane with the negative real axis removed. That matters because the framework's Wick rotation, a method for continuing a Lorentzian spacetime into a Euclidean one, relies on taking square roots; if the argument of the square root crosses the cut, the continuation can jump discontinuously. The proof is kernel-checked, meaning a machine verified every step with no gaps in the logical chain.

The theorem is deliberately narrow. It covers the interior of the arc, not the endpoints. At the Lorentzian endpoint, the value -5/16 sits exactly on the cut, and the framework documents this as an allowed boundary contact rather than a failure. The declaration also does not extend to the full action-level continuation, which would involve deficit angles and the Regge action itself; that remains an open target. What the theorem does establish is that, away from the boundary, the area-squared formulas for all ten hinges of this simplex type remain in the safe region where the square root is single-valued and continuous.

/-- THEOREM: the constant spacelike-class area-squared `3/16` avoids the
sqrt cut EVERYWHERE (both endpoints included), and the timelike-class
area-squared `z/4 - 1/16` avoids it on the full open interior (its
Lorentzian endpoint value `-5/16` sits ON the cut boundary, the ALLOWED
endpoint contact documented in the landed module). -/
theorem fourOne_areaSq_interior_off_cut {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) :
    ((3 / 16 : ℂ) ∈ Complex.slitPlane)
      ∧ (zArc t / 4 - 1 / 16 ∈ Complex.slitPlane) := by
  constructor
  · exact Complex.mem_slitPlane_iff.mpr (Or.inl (by norm_num))
  · apply Complex.mem_slitPlane_iff.mpr
    right
    have hy : 0 < (zArc t).im := zArc_im_pos ht
    have him : (zArc t / 4 - 1 / 16).im = (zArc t).im / 4 := by
      simp only [Complex.sub_im, Complex.div_ofNat_im, Complex.one_im]
      ring
    rw [him]
    exact (div_pos hy (by norm_num : (0 : ℝ) < 4)).ne'

/-- THEOREM: the constant spacelike-class area-squared `3/16` avoids the
sqrt cut EVERYWHERE (both endpoints included), and the timelike-class
area-squared `z/4 - 1/16` avoids it on the full open interior (its
Lorentzian endpoint value `-5/16` sits ON the cut boundary, the ALLOWED
endpoint contact documented in the landed module). -/
theorem fourOne_areaSq_interior_off_cut {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) :
    ((3 / 16 : ℂ) ∈ Complex.slitPlane)
      ∧ (zArc t / 4 - 1 / 16 ∈ Complex.slitPlane) := by
  constructor
  · exact Complex.mem_slitPlane_iff.mpr (Or.inl (by norm_num))
  · apply Complex.mem_slitPlane_iff.mpr
    right
    have hy : 0 < (zArc t).im := zArc_im_pos ht
    have him : (zArc t / 4 - 1 / 16).im = (zArc t).im / 4 := by
      simp only [Complex.sub_im, Complex.div_ofNat_im, Complex.one_im]
      ring
    rw [him]
    exact (div_pos hy (by norm_num : (0 : ℝ) < 4)).ne'

/-- THEOREM: the constant spacelike-class area-squared `3/16` avoids the
sqrt cut EVERYWHERE (both endpoints included), and the timelike-class
area-squared `z/4 - 1/16` avoids it on the full open interior (its
Lorentzian endpoint value `-5/16` sits ON the cut boundary, the ALLOWED
endpoint contact documented in the landed module). -/
theorem fourOne_areaSq_interior_off_cut {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) :
    ((3 / 16 : ℂ) ∈ Complex.slitPlane)
      ∧ (zArc t / 4 - 1 / 16 ∈ Complex.slitPlane) := by
  constructor
  · exact Complex.mem_slitPlane_iff.mpr (Or.inl (by norm_num))
  · apply Complex.mem_slitPlane_iff.mpr
    right
    have hy : 0 < (zArc t).im := zArc_im_pos ht
    have him : (zArc t / 4 - 1 / 16).im = (zArc t).im / 4 := by
      simp only [Complex.sub_im, Complex.div_ofNat_im, Complex.one_im]
      ring
    rw [him]
    exact (div_pos hy (by norm_num : (0 : ℝ) < 4)).ne'

What this page does not claim

The theorem does not claim the area-squared values are defined at the endpoints of the arc. It does not claim the full action-level continuation with deficit angles is complete. It does not claim the Lorentzian endpoint value -5/16 is regular; it is an allowed boundary contact.

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