IndisputableMonolith.Gravity.SevenGaps.WickActionInteriorHingeConfinement

declarations in this module (25)

• theorem continuationEdgesC_threeTwo L41
• theorem normSq_arcZ_one L51
• theorem denom_ne_of_causal L63
• theorem arcZ_im_eq L82
• theorem arcZ_im_pos_of_causal L90
• theorem pentHingeCosPath_eq_moebius L103
• theorem pentHingeCosPath_eq_moebius_one L114
• theorem pentHingeCosPath_one_eq_threeTwo L119
• theorem euclidCos_one L122
• theorem lorentzCos_one L125
• theorem pentHingeCosPath_eq_euclidCos L128
• theorem pentHingeCosPath_eq_lorentzCos L133
• theorem pentHingeCosPath_one_zero L150
• theorem pentHingeCosPath_one_one L154
• theorem im_pentHingeCosPath_eq L160
• theorem im_pentHingeCosPath_neg L172
• theorem im_pentHingeCosPath_neg_one L181
• theorem branchRegularSum_of_causal L187
• theorem branchRegularSum_one L198
• def carccos_tendsto_at_cut_one L209
• def carccos_tendsto_at_cut_family L215
• def lorentzAnchor_one L222
• theorem rapidityPinned_one L228
• theorem lorentz_endpoint_im_eq L233
• theorem lorentz_endpoint_not_real L241