IndisputableMonolith.Gravity.SevenGaps.WickActionCertAssembly

declarations in this module (24)

• lemma sqrt57_div_eight L69
• lemma arcosh_eleven_over_eight L79
• theorem carccos_at_lorentz_cut_one L92
• theorem carccos_cut_limit_value_one L165
• theorem carccos_value_ne_cut_limit_one L172
• lemma wickActionPath_zero_ne_lorentz_limit L198
• lemma tendsto_Ioi_of_continuousOn_Icc L235
• theorem contAction_not_satisfiable_at_one L257
• structure WickActionContinuationCertV2 L277
• def wick_action_continuation_v2_family L319
• def wick_action_continuation_v2_at_one L325
• theorem offArccosCut_pentHingeCosPath_Ioc_one L330
• theorem continuousOn_pentHingeCosPath_Ioc_one L341
• theorem continuousOn_carccos_comp_pent_Ioc_one L348
• theorem continuousOn_wickActionPath_Ioc_one L356
• theorem chartsAgree_one L382
• theorem euclidAnchor_one L391
• theorem wickActionContinuationCertV2_one L399
• theorem wick_action_continuation_v2_at_one_holds L415
• theorem decoy_euclidean_only_falsified L423
• theorem decoy_interior_nhds_not_cutLimit_filter L430
• structure WickActionCertAssemblyStatus L442
• def wickActionCertAssemblyStatus L449
• theorem wickActionCertAssemblyStatus_flags L456