IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFamilyThreshold

declarations in this module (25)

• structure CausalWickComplex L83
• def fourOneComplex L87
• def threeTwoComplex L89
• def wickContinuationThreshold L93
• def wickContinuationThresholdOf L98
• theorem wickContinuationThreshold_eq_alphaMin L101
• theorem wickContinuationThreshold_fourOne L105
• theorem wickContinuationThreshold_threeTwo L109
• theorem wickContinuationThresholds_differ L117
• theorem wickContinuationThreshold_fourOne_lt_threeTwo L124
• theorem causalWickComplex_two_inhabitants L131
• def WickEuclideanAdmissible L141
• theorem wickEuclideanAdmissible_iff L147
• theorem wickEuclideanAdmissible_of_gt_threshold L156
• theorem wickEuclideanAdmissible_false_at_threshold L163
• theorem wickThreshold_gap_witness L177
• theorem wickContinuationThresholdOf_not_constant L199
• theorem no_common_typewise_exact_threshold L214
• theorem hardcodedConstant_eq_threeTwo_threshold L239
• theorem hardcodedConstant_gt_fourOne_threshold L246
• theorem joint_wickEuclideanAdmissible_iff L256
• theorem universal_sufficient_threshold_eq_max L273
• theorem certV2_above_threeTwo_threshold L288
• theorem no_certV2_in_fourOne_only_window L299
• theorem fourOne_only_window_witness L307