module module

`IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst`

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.WickFourOneAllHinges module_import
IndisputableMonolith.Gravity.SevenGaps.WickHingeDataComplete module_import
IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.CausalSimplex4D module_import

declarations in this module (67)

theorem realized L29
abbrev SqEdges10C L154
def pentDistSqC L158
def cmIndexVertexC L185
def cmMatrixC L190
def cmMinorC L200
def cmCofactorSignC L204
def cmCofactorC L209
def cmVertexIndexC L214
def csqrt L227
theorem csqrt_mul_self L231
def dihedralDenomSplitC L242
def dihedralCosSplitC L251
def triCMMatrixC L258
def triangleAreaSqC L277
def hingeAreaSqC L282
def arcZ L293
def continuationEdgesC L298
theorem arcZ_zero L303
theorem arcZ_one L311
theorem continuationEdgesC_zero L320
theorem continuationEdgesC_one L332
def zArc L345
theorem zArc_eq_exp L347
theorem zArc_re L352
theorem zArc_im L356
theorem zArc_zero L360
theorem zArc_one L365
theorem normSq_zArc L371
theorem zArc_im_pos L378
theorem continuous_zArc L388
theorem denom_ne L400
def hingeEdgesC L417
theorem continuationEdgesC_physical L422
def hingeMatrixC L434
theorem cmMatrixC_hingeEdges L457
def minorPPC L464
def minorPQC L483
theorem submatrix_pp L500
theorem submatrix_qq L506
theorem submatrix_pq L512
theorem det_minorPPC L523
theorem det_minorPQC L535
theorem cofactor_pp L542
theorem cofactor_qq L550
theorem cofactor_pq L558
theorem hingeAreaSqC_closed L569
def OffArccosCut L587
def BranchRegularOn L594
def hingeCosPath L603
theorem hingeCosPath_eq_moebius L611
theorem branchRegular_fourOne_hinge L628
theorem hingeAreaSq_interior_off_cut L673
theorem continuousOn_hingeCosPath L691
theorem hingeCosPath_zero L702
theorem hingeCosPath_one L709
theorem wick_boundary_continuation_fourOne_hinge L720
def realLorentzianProductCos L729
theorem realLorentzianProductCos_eq L732
theorem lorentzian_endpoint_sign_factor L745
theorem endpoint_cofactor_on_sqrt_cut L757
def tStar L773
theorem tStar_mem_Ioo L775
theorem arg_tStar L790
theorem cos_arg_tStar L797
theorem product_form_crossing_value L805
theorem product_form_crossing L840