module module

`IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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