Gravity Seven Gaps Causal Simplex Wick Cm3 Euclidean Degenerate At Min

The degenerate threshold

In the framework of Recognition Science, a discrete record of events, the basic building blocks of a 3D spacetime are tetrahedra, four-pointed shapes with triangular faces. These tetrahedra come in two types, distinguished by how many of their vertices lie on a given time slice: the (3,1) type has three vertices on one slice and one on the next, while the (2,2) type has two on each. Each tetrahedron is characterized by a parameter alpha that controls the squared length of its timelike edges, those that connect different time slices. When alpha is small, the tetrahedron is squashed flat and has zero volume; the theorem cm3_euclidean_degenerate_at_min establishes the exact threshold at which this collapse happens.

The theorem proves that the Cayley-Menger polynomial cm3, which equals 288 times the square of the volume for a realizable tetrahedron, vanishes precisely when alpha equals the minimum value for each type. For the (3,1) type, that minimum is 1/3; for the (2,2) type, it is 1/2. Below these values, the tetrahedron is degenerate, meaning it has no volume at all. Above them, it becomes non-degenerate, with a positive volume. This threshold is exact: the theorem does not merely show that degeneracy occurs at these values, it proves that it occurs exactly at these values and nowhere else. The result is certified by a machine-checked library of formal theorems, meaning the proof has been verified step by step by a computer.

The theorem is part of a larger effort to build a Lorentzian, or causal, sector of discrete gravity. In the Euclidean regime, where all edges have positive squared length, the tetrahedra are well-defined for alpha above the threshold. But in the Lorentzian regime, where timelike edges have negative squared length, the same tetrahedra are never Euclidean-realizable, as the Cayley-Menger polynomial is always negative there. This is why a Wick rotation, a mathematical transformation that flips the sign of timelike squared lengths, is needed to connect the two regimes. The theorem cm3_euclidean_degenerate_at_min is a key step in showing that this rotation produces non-degenerate Euclidean tetrahedra, which are the building blocks of the theory.

What the theorem does not claim is just as important as what it does. It does not claim that the physical universe is actually made of these tetrahedra, or that this discrete model is a complete description of gravity. It is a mathematical statement about a specific definitional choice, the choice to model spacetime as a causal triangulation. The theorem does not address the action-level Lorentzian continuation, such as complex dihedral angles or the sinh-action sector, which remains open. It also does not prove that the dihedral angles are real for all alpha above the threshold, only at the specific physical point alpha = 1, where the tetrahedra coincide with the regular tetrahedron. These are targets for future work, not claims of this theorem.

/-- THEOREM (threshold exactness): at `alpha = alphaMin ty` the Euclideanized
simplex is degenerate, `cm3 = 0`. -/
theorem cm3_euclidean_degenerate_at_min (ty : CausalTetType) (a : ℝ) :
    cm3 (euclideanSqEdges ty a (alphaMin ty)) = 0 := by
  cases ty
  · rw [alphaMin_threeOne, cm3_euclidean_threeOne]
    norm_num
  · rw [alphaMin_twoTwo, cm3_euclidean_twoTwo]
    norm_num

theorem alphaMin_threeOne : alphaMin CausalTetType.threeOne = 1 / 3 := rfl

theorem alphaMin_twoTwo : alphaMin CausalTetType.twoTwo = 1 / 2 := rfl

/-- THEOREM (threshold exactness): at `alpha = alphaMin ty` the Euclideanized
simplex is degenerate, `cm3 = 0`. -/
theorem cm3_euclidean_degenerate_at_min (ty : CausalTetType) (a : ℝ) :
    cm3 (euclideanSqEdges ty a (alphaMin ty)) = 0 := by
  cases ty
  · rw [alphaMin_threeOne, cm3_euclidean_threeOne]
    norm_num
  · rw [alphaMin_twoTwo, cm3_euclidean_twoTwo]
    norm_num

What this page does not claim

The theorem does not claim that physical spacetime is actually composed of these discrete tetrahedra. The theorem does not address the action-level Lorentzian continuation, such as complex dihedral angles or the sinh-action sector. The theorem does not prove that the dihedral angles are real for all alpha above the threshold, only at the specific point alpha = 1.

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