Encyclopedia Gravity Gravity Seven Gaps Wick Four One All Hinges

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Wick Four One All Hinges

A machine-checked proof that every one of the ten triangular joints in a five-vertex spacetime building block behaves regularly as the geometry rotates from Lorentzian to Euclidean.

Verify this page

The all-hinge continuation

In the Recognition Science framework's quantum gravity program, the basic object is a fourOne causal 4-simplex: a five-vertex building block of spacetime, four of whose edges are timelike (they touch a chosen apex vertex) and six of which are spacelike. The module WickFourOneAllHinges certifies a specific mathematical property of this object. A hinge is a triangular face of the simplex, defined by choosing three of its five vertices; the opposite pair is the remaining two vertices. There are ten such hinges in total.

The property being certified concerns a Wick rotation, a standard technique in physics that rotates a time coordinate into an imaginary one to convert a Lorentzian spacetime (with its distinct time and space directions) into a Euclidean one (where all directions behave alike). The module works with a parameter t that interpolates between these two regimes. The core result, proved in a machine-checked library of formal theorems, is that for every one of the ten hinges, the relevant geometric quantity is well-behaved throughout this interpolation. Specifically, the branch of the complex square root used in the calculation is regular on the open interval 0 < t < 1, and the cosine path is continuous on the closed interval [0, 1], ending at the same value, -(1/4), for all hinges.

The ten hinges split into two classes. Six contain the apex vertex and have two timelike edges; four avoid it and have none. The module proves that these classes have distinct endpoint behaviors. The timelike-class hinges end at a Lorentzian value of -(3/8), while the spacelike-class hinges end at a purely imaginary value, (sqrt 2 / 8) * i, reflecting the imaginary dihedral angle characteristic of a spacelike hinge. The area-squared of each hinge is also given in closed form: a constant 3/16 for the spacelike class, and t/4 - 1/16 for the timelike class on the open interior.

The significance of this result is that it extends a previously established certificate for a single hinge to all ten hinges of the fourOne simplex. This is a necessary step toward the larger goal of defining a complete quantum gravity action on this building block. The module explicitly does not claim to have achieved that goal: the continuation of the full action, involving deficit angles and the Regge action itself, remains an open problem. The module also notes a discrepancy in a trace document, where the counts of the two hinge classes are swapped; the per-hinge table and the combinatorics agree that the correct counts are four spacelike and six timelike.

THEOREM branchRegular_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
branchRegular_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean:1011 
/-- THEOREM (B1 headline, branch certificates): for EVERY hinge of the
fourOne causal 4-simplex (every unordered opposite vertex pair, both
orientations), the split-form continuation is branch-regular on the FULL
open arc interior at the physical point `a = 1`, `alpha = 1`.  The ten
hinges: (0,1,2)|(3,4), (0,1,3)|(2,4), (0,1,4)|(2,3), (0,2,3)|(1,4),
(0,2,4)|(1,3), (0,3,4)|(1,2), (1,2,3)|(0,4), (1,2,4)|(0,3),
(1,3,4)|(0,2), (2,3,4)|(0,1). -/
theorem branchRegular_fourOne_allHinges :
    ∀ p q : Fin 5, p ≠ q →
      BranchRegularOn
        (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t) p q
        (Set.Ioo 0 1) := by
  intro p q hpq
  fin_cases p <;> fin_cases q
  · exact absurd rfl hpq
  · exact branchRegular_pair01
  · exact branchRegular_pair02
  · exact branchRegular_pair03
  · exact branchRegular_pair04
  · exact branchRegularOn_symm branchRegular_pair01
  · exact absurd rfl hpq
  · exact branchRegular_pair12
  · exact branchRegular_pair13
  · exact branchRegular_pair14
  · exact branchRegularOn_symm branchRegular_pair02
  · exact branchRegularOn_symm branchRegular_pair12
  · exact absurd rfl hpq
  · exact branchRegular_pair23
  · exact branchRegular_pair24
  · exact branchRegularOn_symm branchRegular_pair03
  · exact branchRegularOn_symm branchRegular_pair13
  · exact branchRegularOn_symm branchRegular_pair23
  · exact absurd rfl hpq
  · exact branchRegular_pair34
  · exact branchRegularOn_symm branchRegular_pair04
  · exact branchRegularOn_symm branchRegular_pair14
  · exact branchRegularOn_symm branchRegular_pair24
  · exact branchRegularOn_symm branchRegular_pair34
  · exact absurd rfl hpq
THEOREM wick_boundary_continuation_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
wick_boundary_continuation_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean:1111 
/-- THEOREM (B1 headline, boundary continuation): every split-form cosine
path of the fourOne type is continuous on the CLOSED interval `[0, 1]` and
ends at the Euclidean regular-4-simplex value `-(1/4)` (`+C_pq` numerator
convention of the landed module; textbook `-C` interior cosine `+1/4`). -/
theorem wick_boundary_continuation_fourOne_allHinges :
    ∀ p q : Fin 5, p ≠ q →
      ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
        ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ) := by
  intro p q hpq
  fin_cases p <;> fin_cases q
  · exact absurd rfl hpq
  · exact ⟨boundary_pair01.1, boundary_pair01.2.2⟩
  · exact ⟨boundary_pair02.1, boundary_pair02.2.2⟩
  · exact ⟨boundary_pair03.1, boundary_pair03.2.2⟩
  · exact ⟨boundary_pair04.1, boundary_pair04.2.2⟩
  · exact boundary_symm ⟨boundary_pair01.1, boundary_pair01.2.2⟩
  · exact absurd rfl hpq
  · exact ⟨boundary_pair12.1, boundary_pair12.2.2⟩
  · exact ⟨boundary_pair13.1, boundary_pair13.2.2⟩
  · exact ⟨boundary_pair14.1, boundary_pair14.2.2⟩
  · exact boundary_symm ⟨boundary_pair02.1, boundary_pair02.2.2⟩
  · exact boundary_symm ⟨boundary_pair12.1, boundary_pair12.2.2⟩
  · exact absurd rfl hpq
  · exact ⟨boundary_pair23.1, boundary_pair23.2.2⟩
  · exact ⟨boundary_pair24.1, boundary_pair24.2.2⟩
  · exact boundary_symm ⟨boundary_pair03.1, boundary_pair03.2.2⟩
  · exact boundary_symm ⟨boundary_pair13.1, boundary_pair13.2.2⟩
  · exact boundary_symm ⟨boundary_pair23.1, boundary_pair23.2.2⟩
  · exact absurd rfl hpq
  · exact ⟨boundary_pair34.1, boundary_pair34.2.2⟩
  · exact boundary_symm ⟨boundary_pair04.1, boundary_pair04.2.2⟩
  · exact boundary_symm ⟨boundary_pair14.1, boundary_pair14.2.2⟩
  · exact boundary_symm ⟨boundary_pair24.1, boundary_pair24.2.2⟩
  · exact boundary_symm ⟨boundary_pair34.1, boundary_pair34.2.2⟩
  · exact absurd rfl hpq
THEOREM det_minor41_24C · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
det_minor41_24C · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean:520 
theorem det_minor41_24C (z : ℂ) : Matrix.det (minor41_24C z) = 1 - 2 * z := by
  unfold minor41_24C
  simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
  ring
THEOREM fourOne_areaSq_interior_off_cut · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
fourOne_areaSq_interior_off_cut · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean:1255 
/-- 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 module does not claim to have continued the full quantum gravity action for the fourOne simplex. The module does not claim to have resolved the discrepancy in the trace document's summary section, only to have identified it. The module does not claim to have proved anything about the physical interpretation of the imaginary dihedral angle.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND