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

A complete check

In four-dimensional geometry, a simplex is the simplest shape with four spatial dimensions and five corners. The specific object here is a causal 4-simplex, meaning its edges are classified as timelike (connecting events that can influence each other) or spacelike (connecting events that cannot). This particular shape, called the fourOne type, has exactly four timelike edges, all touching a single apex vertex. The declaration branchRegular_fourOne_allHinges (a machine-checked theorem in the framework's library of formal proofs) establishes that for every one of the ten triangular faces, or hinges, a certain mathematical condition holds across the entire open interior of a parameter range from 0 to 1.

That condition concerns a technique called Wick rotation, which converts a geometry with a time dimension into one with only spatial dimensions by rotating the time coordinate into the imaginary axis. This is a standard tool in physics for simplifying calculations. The theorem verifies that as the rotation parameter moves through its allowed range, the square root functions involved never hit a problematic branch cut, the line where a multi-valued function jumps discontinuously. The proof works by checking all ten triangular faces individually, using explicit five-by-five determinant calculations for each one. It confirms that the geometry remains regular, or non-degenerate, throughout the rotation.

The companion theorem, wick_boundary_continuation_fourOne_allHinges, goes further. It proves that the cosine of the dihedral angle (the angle between two faces) along each split-form path is continuous on the closed interval from 0 to 1, and that at the endpoint where the rotation is complete, it always reaches the same value of negative one quarter. This is the value expected for a perfectly regular Euclidean 4-simplex, the fully rotated version of the shape. The result means the rotation connects the causal, Lorentzian geometry smoothly to its Euclidean counterpart without any mathematical singularities appearing along the way.

In Recognition Science, this result is a step in a larger program to build a quantum theory of gravity from discrete geometry. The framework models spacetime as a collection of such simplexes, and this theorem provides a rigorous check that a fundamental building block behaves correctly under a key mathematical transformation. It does not, however, claim to have constructed the full quantum gravity action. The continuation of the action itself, involving deficit angles and the interior of the simplicial complex, remains an open question. The theorem also does not claim any physical measurement or prediction; it is a purely mathematical result about the consistency of a geometric model.

/-- 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 (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

What this page does not claim

The theorem does not construct the full quantum gravity action or its continuation. The theorem makes no statement about the physical reality of the 4-simplex, only its mathematical consistency. The theorem does not claim the branch regularity holds at the Lorentzian endpoint, which lies on the branch cut.

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: