Gravity Seven Gaps Causal Simplex4 D Is Timelike Four One Eq Cross Slice

Counting the edges of time

In the causal set approach to quantum gravity, spacetime is assembled from discrete building blocks called 4-simplices, the four-dimensional analog of a triangle. A standard 4-simplex has five vertices and ten edges. The Recognition Science framework's declaration isTimelike_fourOne_eq_crossSlice is a formal, machine-checked statement about one specific type of these building blocks, the (4,1) simplex, which has four vertices on one spatial slice and one vertex on the next.

The declaration proves that exactly four of the ten edges in a (4,1) simplex are timelike, meaning they connect the two different spatial slices and therefore point across time. The other six edges are spacelike, lying entirely within a single slice. This is not an empirical observation or a heuristic assumption; it is a theorem verified by computation in the framework's machine-checked library of formal theorems, with no gaps in the proof. The result is stated as isTimelike_fourOne_eq_crossSlice, and it is one of several such counting lemmas that together confirm the combinatorial structure of the causal 4-simplex classes.

The significance of this count is that it anchors the geometric definition of the (4,1) simplex. The framework models the simplex with a specific assignment of which vertices lie on which slice, and this theorem verifies that the assignment produces the expected mix of edge types: six spacelike and four timelike. This is the combinatorial foundation on which the framework then builds more substantial results, such as the Wick rotation map and the exact thresholds for when the simplex is non-degenerate.

What the declaration does not claim is any physical content beyond this combinatorial fact. It does not assert that these edge counts correspond to any measurable property of spacetime, nor does it imply that the (4,1) simplex is the only valid building block. It is a precise, self-contained statement about a definitional choice, verified by computation, and it is the kind of foundational check that gives the framework's larger claims their footing.

/-- THEOREM (by `decide`): type (4,1) has exactly 4 timelike edges. -/
theorem timelike_count_fourOne :
    (Finset.univ.filter fun e : Fin 10 =>
      isTimelike CausalPentType.fourOne e = true).card = 4 := by
  decide

/-- THEOREM (by `decide`): type (4,1) has exactly 6 spacelike edges. -/
theorem spacelike_count_fourOne :
    (Finset.univ.filter fun e : Fin 10 =>
      isTimelike CausalPentType.fourOne e = false).card = 6 := by
  decide

/-- THEOREM (by `decide`): type (4,1) has exactly 4 timelike edges. -/
theorem timelike_count_fourOne :
    (Finset.univ.filter fun e : Fin 10 =>
      isTimelike CausalPentType.fourOne e = true).card = 4 := by
  decide

What this page does not claim

The declaration does not assert any physical content beyond the combinatorial edge count. It does not imply that the (4,1) simplex is the only valid building block of spacetime. It does not establish that the edge count corresponds to any measurable property.

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