IndisputableMonolith.Gravity.SevenGaps.ThreePentCausalConsistency

declarations in this module (23)

• def slice6 L101
• def causalSqLength L109
• theorem causalSqLength_symm L113
• def pentAVert L121
• def pentBVert L125
• def pentCVert L129
• theorem pent_charts_cover L134
• theorem pent_charts_injective L142
• theorem pent_slices_match L151
• def inducedSqEdges L163
• theorem shared_face_consistency L174
• theorem induced_pentA_eq L188
• theorem induced_pentB_eq L195
• theorem induced_pentC_eq L202
• class of L211
• theorem threePent_lorentzian_class L212
• theorem threePent_lorentzian_cm4_neg L226
• theorem threePent_euclidean_admissible L239
• theorem hinge_edges_spacelike L255
• theorem link_edges_spacelike L264
• theorem cross_edges_timelike L272
• theorem physical_point_regular L288
• theorem threePent_causal_assignment L321