module module high

`IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D`

Defines the two causal 4-simplex types of 4d CDT between adjacent slices: (4,1) with four vertices on slice t and one on t+1, and (3,2) with three on t and two on t+1 (reflections share edge data). Supplies edge-vertex incidence, slice membership, timelike predicates, and explicit timelike/spacelike edge counts. Downstream SevenGaps gravity modules import these carriers for causal length assignments and Wick-continued Regge data. Definitional scaffolding plus finite counting lemmas.

claimThe module introduces the two causal 4-simplex types of 4-dimensional causal dynamical triangulations between adjacent time slices: the $(4,1)$-simplex (four vertices on slice $t$, one on $t+1$) and the $(3,2)$-simplex (three on $t$, two on $t+1$), with time reflections $(1,4)$ and $(2,3)$ sharing the same edge data, together with ten-edge incidence, slice membership, and counts of timelike (cross-slice) versus spacelike (in-slice) edges.

background

In 4d Causal Dynamical Triangulations (CDT), discrete Lorentzian spacetime is assembled from 4-simplices whose vertices sit on successive proper-time slices. Causality restricts the allowed bipartitions of the five vertices across adjacent slices to two combinatorial types: $(4,1)$ and $(3,2)$ (and their time reflections, which carry identical edge data).

This Gravity.SevenGaps module imports the dimension-parametric Cayley-Menger matrix infrastructure (full CM matrix and determinant for an $n$-simplex) as geometric substrate for later metric work. Locally it fixes notation for the two-type enumeration, the ten edges of a 4-simplex, slice-of maps on vertices, and a timelike predicate that marks cross-slice edges.

Counting lemmas then record how many edges of each type are timelike versus spacelike, and identify the timelike set with the cross-slice set for both bipartitions.

proof idea

This is a definition module with elementary counting lemmas, not a deep existence argument. It introduces the two-value causal type, a fixed ten-edge index set, edge-to-vertex incidence, and slice membership; defines timelike as cross-slice; then proves by finite case analysis on Fin that the $(4,1)$ and $(3,2)$ timelike predicates coincide with cross-slice membership and that the resulting timelike and spacelike cardinalities match the expected CDT tallies. No metric or gluing construction appears here.

why it matters in Recognition Science

Supplies the combinatorial carriers consumed by three SevenGaps parents. MetricRefinementCarrierBlocker uses them when certifying that PathSumMeasure quotients identify triangulation types rather than metric geometries (the P2.5 obstruction). ThreePentCausalConsistency needs the edge taxonomy to place an explicit admissible causal edge-length assignment on the minimal interior-hinge complex (gap6-a, W3-2). WickActionComplexFirst builds the complex-first 4D Lorentzian Wick continuation of Regge hinge data on the same $(4,1)/(3,2)$ edge skeleton (C11 lane). Without a clean bipartition and timelike/spacelike split, those causal-length and Wick constructions have no discrete substrate.

scope and limits

Does not assign numerical edge lengths or a Lorentzian metric to either simplex type.
Does not construct or prove existence of a global CDT triangulation.
Does not treat gluing consistency of $(3,2)$ hinges beyond local edge counts.
Does not evaluate Regge actions, deficit angles, or continuum Einstein limits.
Does not address non-adjacent slices or higher-codimension strata.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.MetricRefinementCarrierBlocker module_import
IndisputableMonolith.Gravity.SevenGaps.ThreePentCausalConsistency module_import
IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMengerN module_import

declarations in this module (63)

inductive CausalPentType L131
abbrev SqEdges10 L137
def pentEdgeVertices L142
def sliceOf L157
def isTimelike L164
theorem isTimelike_fourOne_eq_crossSlice L174
theorem isTimelike_threeTwo_eq_crossSlice L182
theorem slice_count_fourOne L191
theorem slice_count_threeTwo L200
theorem timelike_count_fourOne L208
theorem spacelike_count_fourOne L214
theorem timelike_count_threeTwo L220
theorem spacelike_count_threeTwo L227
def lorentzianSqEdges L240
def euclideanSqEdges L246
def LorentzianClass L251
theorem euclideanSqEdges_pos L256
theorem euclideanSqEdges_scale L269
def wick L284
theorem wick_wick L289
theorem wick_involutive L298
theorem wick_lorentzian L304
theorem lorentzian_continuation L313
theorem wick_eq_continuation L324
theorem wick_image_euclidean L331
def pentDistSq L349
theorem pentDistSq_edge L375
def pentDistances L380
def cm4 L391
theorem simplexVolumeSqN_eq_cm4_div L397
def pentMatrix41 L415
def pentMatrix32 L439
theorem det_pentMatrix41 L465
theorem det_pentMatrix32 L479
theorem cmMatrixN_euclidean_fourOne L488
theorem cmMatrixN_lorentzian_fourOne L496
theorem cmMatrixN_euclidean_threeTwo L504
theorem cmMatrixN_lorentzian_threeTwo L512
theorem cm4_euclidean_fourOne L522
theorem cm4_euclidean_threeTwo L533
theorem cm4_lorentzian_fourOne L543
theorem cm4_lorentzian_threeTwo L552
theorem cm4_euclidean_scale L563
theorem euclideanSqEdges_alpha_one L574
theorem cm4_regular_unit L586
def alphaMin L595
theorem alphaMin_fourOne L599
theorem alphaMin_threeTwo L601
theorem alphaMin_pos L603
theorem alphaMin_lt_one L606
theorem cm4_euclidean_pos_iff L615
theorem cm4_euclidean_pos L647
theorem cm4_euclidean_pos_joint L654
theorem cm4_euclidean_degenerate_at_min L665
theorem lorentzian_cm4_neg_fourOne L681
theorem lorentzian_cm4_neg_threeTwo L690
structure NonDegeneratePent L703
def euclideanCausalPent L713
theorem wick_lorentzian_nondegenerate L726
def physicalCausalPent L734
structure CausalSimplex4DStatus L748
def causalSimplex4DStatus L755
theorem causalSimplex4DStatus_flags L764