Encyclopedia Gravity Gravity Seven Gaps Wick Four One All Hinges Branch Regular Four One All Hinges

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Wick Four One All Hinges Branch Regular Four One All Hinges

A machine-checked proof that all ten triangular hinges of a specific four-dimensional simplex stay on the correct mathematical sheet during a complex rotation, and a clear statement of what that proof does not cover.

Verify this page

The all-hinge certificate

In four-dimensional geometry, a simplex is the simplest shape with five corners, the analog of a triangle in two dimensions or a tetrahedron in three. A hinge is a triangular face where two of these corners meet the opposite edge, and a 4-simplex has ten of them. The declaration branchRegular_fourOne_allHinges is a machine-checked theorem in the Recognition Science framework's library of formal proofs. It concerns a specific type of 4-simplex, called fourOne, where exactly four edges are timelike, meaning they point more in the time direction than in space, and all touch a single apex vertex.

The theorem states that for every one of the ten hinges, a certain mathematical condition called BranchRegularOn holds on the entire open interval from 0 to 1. In plain terms, this means that as a parameter t moves smoothly from 0 to 1, the complex square roots involved in the calculation never cross their branch cut, the line where the function is discontinuous. The proof works by checking each of the ten hinges individually, using explicit 5x5 determinant calculations for each one. The theorem also proves that the ten hinge areas, the squared areas of the triangular faces, avoid the branch cut throughout the interior of the interval, with one allowed contact at the endpoint.

The declaration is part of a larger effort to continue a quantum gravity action from Lorentzian to Euclidean signature, a process known as Wick rotation. The theorem establishes that this continuation is well-behaved for all hinges of this simplex type, not just one. It also proves that the boundary values at the endpoint t=1 match the expected Euclidean values, and that the Lorentzian endpoint values are correct: negative for timelike hinges and purely imaginary for spacelike ones. These are concrete, checkable facts about the geometry.

In Recognition Science, this theorem is a step toward a full theory of quantum gravity, but it is not the whole theory. The declaration does not claim that the action-level continuation, involving the full simplicial complex and deficit angles, is complete. That remains an open question in another lane of the research program. The theorem also does not claim that the physical interpretation of the Wick rotation is settled; it only certifies the mathematical consistency of this particular piece. The proof is formal and machine-checked, but it is a statement about a specific geometric configuration, not a general principle of physics.

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 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'
THEOREM wick_boundary_continuation_fourOne_allHinges · minor41_55C · 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
minor41_55C · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean:351 
/-- The apex diagonal minor (delete CM row/col 5, vertex 4): the regular
unit tetrahedron CM matrix. -/
def minor41_55C : Matrix (Fin 5) (Fin 5) ℂ :=
  fun i j =>
    match i.val, j.val with
    | 0, 0 => 0
    | 1, 1 => 0
    | 2, 2 => 0
    | 3, 3 => 0
    | 4, 4 => 0
    | _, _ => 1

What this page does not claim

The action-level continuation involving the full simplicial complex and deficit angles is not proved. The physical interpretation of the Wick rotation is not established by this theorem. The theorem does not apply to simplex types other than the fourOne configuration.

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