module module

`IndisputableMonolith.Gravity.SevenGaps.CausalSimplexWick`

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 (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