module module high

`IndisputableMonolith.Gravity.SevenGaps.CausalSimplexWick`

Catalogues the two causal tetrahedron types of 3d causal dynamical triangulations between adjacent time slices: (3,1) with three vertices on slice t and one on t+1, and (2,2) with two on each. Supplies slice membership, timelike/spacelike edge predicates, and edge-count identities under a Lorentzian squared-length signature. Gravity and CDT workers cite it when wiring combinatorial carriers to Regge edge data. The body is definitional enumeration plus elementary counting equalities.

claimIn 3d CDT, a causal tetrahedron between adjacent slices is either of type $(3,1)$ (three vertices on slice $t$, one on $t+1$; time reflection $(1,3)$ shares the same edge data) or of type $(2,2)$ (two vertices on each slice). For each type one records slice membership of vertices, which edges are timelike versus spacelike under a Lorentzian squared-length assignment, and the resulting timelike and spacelike edge counts.

background

Causal dynamical triangulations (CDT) build Lorentzian path integrals from piecewise-flat simplicial manifolds with a preferred foliation by discrete time slices. In three dimensions the elementary building blocks between consecutive slices are tetrahedra whose vertices lie on at most two adjacent slices. Only two combinatorial types appear: $(3,1)$ (and its time reflection $(1,3)$) and $(2,2)$.

The module sits inside the SevenGaps gravity campaign and imports the Cayley-Menger / Regge stack (CayleyMengerPolynomial, DihedralCayleyMenger, ReggeRigorousFoundation). Those modules supply the Euclidean squared-edge polynomial and dihedral cosines needed later to compare Regge second-variation coefficients to face areas. Here the focus is purely causal and combinatorial: which edges cross the slice and which stay inside it, once a Lorentzian sign pattern is chosen on squared lengths.

Sibling definitions introduce an inductive type of causal tetrahedra, a slice-membership map, a timelike predicate, and explicit counts of timelike versus spacelike edges for each type, together with a Lorentzian squared-edge assignment.

proof idea

This is primarily a definition module. CausalTetType enumerates the two CDT tetrahedron classes. sliceOf and isTimelike are pure data and predicates on vertices and edges. The equalities isTimelike_threeOne_eq_crossSlice and isTimelike_twoTwo_eq_crossSlice identify the timelike edges with the cross-slice edges by case analysis on the type. The remaining declarations are arithmetic identities: how many edges lie in each slice and how many are timelike or spacelike for $(3,1)$ and $(2,2)$, obtained by direct counting under the fixed Lorentzian squared-edge pattern lorentzianSqEdges. No deep analytic argument is required.

why it matters in Recognition Science

The SevenGaps campaign tracks scoped quantum-gravity increments that are not yet full-strength closures. This module supplies the causal simplex vocabulary that downstream ledgers and blockers import. CampaignLedger records machine-checked status of each gap and pulls this file as part of the combinatorial carrier layer. MetricRefinementCarrierBlocker uses the same stack to certify a P2.5 obstruction: path-sum measures and triangulation classes only see cardinalities and incidence, not metric geometries, so distinct positive edge-length assignments on a one-tetrahedron complex remain unidentified.

In the broader Recognition gravity program the file bridges discrete causal structure to the Regge foundation (Cayley-Menger polynomials and dihedral cofactors) that aims at the component identity $M_{ij}=-\mathrm{area}(f_{ij})$. It does not itself close that identity; it fixes the Lorentzian edge typing against which metric refinement and second-variation comparisons are later stated.

scope and limits

Does not prove the Regge component identity $M_{ij}=-\mathrm{area}(f_{ij})$.
Does not construct continuum limits, measures, or full CDT partition functions.
Does not treat higher-dimensional simplices or non-foliated triangulations.
Does not assign numerical edge lengths beyond a Lorentzian sign pattern on squares.
Does not flip any full-strength QGScopeAudit closure flag.

used by (2)

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

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import
IndisputableMonolith.Gravity.SevenGaps.MetricRefinementCarrierBlocker module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMengerPolynomial module_import
IndisputableMonolith.Geometry.DihedralCayleyMenger module_import
IndisputableMonolith.Geometry.ReggeRigorousFoundation module_import

declarations in this module (50)

inductive CausalTetType L107
def sliceOf L114
def isTimelike L121
theorem isTimelike_threeOne_eq_crossSlice L129
theorem isTimelike_twoTwo_eq_crossSlice L137
theorem slice_count_threeOne L146
theorem slice_count_twoTwo L154
theorem timelike_count_threeOne L162
theorem spacelike_count_threeOne L168
theorem timelike_count_twoTwo L174
theorem spacelike_count_twoTwo L180
def lorentzianSqEdges L193
def euclideanSqEdges L199
def LorentzianClass L204
theorem euclideanSqEdges_pos L209
def wick L224
theorem wick_wick L229
theorem wick_involutive L238
theorem wick_lorentzian L244
theorem lorentzian_continuation L253
theorem wick_eq_continuation L264
theorem wick_image_euclidean L270
theorem cm3_euclidean_threeOne L291
theorem cm3_euclidean_twoTwo L310
theorem cm3_lorentzian_threeOne L326
theorem cm3_lorentzian_twoTwo L344
theorem euclideanSqEdges_scale L363
theorem cm3_euclidean_scale L377
def alphaMin L387
theorem alphaMin_threeOne L391
theorem alphaMin_twoTwo L393
theorem alphaMin_pos L395
theorem alphaMin_lt_one L398
theorem cm3_euclidean_pos_iff L405
theorem cm3_euclidean_pos L437
theorem cm3_euclidean_pos_joint L444
theorem cm3_euclidean_degenerate_at_min L455
theorem lorentzian_cm3_neg_threeOne L470
theorem lorentzian_cm3_neg_twoTwo L479
def euclideanCausalTet L492
theorem wick_lorentzian_nondegenerate L504
def physicalCausalTet L512
theorem euclideanSqEdges_alpha_one L530
theorem dihedralCos3Sq_alpha_one L543
theorem dihedralCos3Sq_alpha_one_mem_Ioo L550
theorem dihedralAngle3_physical L559
theorem dihedralAngle3_physical_mem_Ioo L565
structure LorentzianSectorStatus L584
def lorentzianSectorStatus L591
theorem lorentzianSectorStatus_flags L598