IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidenceM2Eval4D

declarations in this module (15)

• theorem m2PathB_meanLocal_axisTTPlus_symbolDir L34
• theorem m2PathB_meanLocal_axisTTCross_symbolDir L39
• theorem m2PathB_meanLocal_axisTTPlus_e0Dir L44
• theorem m2PathB_meanLocal_axisTTCross_e0Dir L49
• theorem m2PathB_meanLocal_plus_cross_disagree_e0Dir L54
• lemma symbolDir_normSq L60
• theorem continuumFace_meanLocal_normalizedPlus_symbolDir L64
• theorem meanLocal_pinned_face_ne_eh L73
• theorem pathB_vs_distinctHinge_witness_table L81
• theorem pathB_positionResolved_does_not_close_eh L105
• theorem pathB_does_not_inhabit_eh L109
• structure ReggeBlochLocalIncidenceM2Eval4DStatus L113
• def reggeBlochLocalIncidenceM2Eval4DStatus L120
• theorem reggeBlochLocalIncidenceM2Eval4DStatus_flags L128
• theorem does_not_flip_gap_action_recovery L141