IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12

declarations in this module (109)

• inductive CubeTranslate L61
• def localHingeMasks L66
• def containsHinge L70
• structure StarMember L73
• def starMembers L78
• theorem starMembers_length L82
• theorem starMembers_complete L84
• theorem star_cardinality L88
• def nearFlatSqEdges L95
• def farFlatSqEdges L98
• theorem hingeGramDet_near L102
• theorem apexDotNum_near L104
• theorem apex3NormSqNum_near L106
• theorem apex4NormSqNum_near L108
• theorem hingeGramDet_far L111
• theorem apexDotNum_far L113
• theorem apex3NormSqNum_far L115
• theorem apex4NormSqNum_far L117
• theorem cosDihedral_near_flat L120
• theorem cosDihedral_far_flat L125
• def flatAngleRight L132
• theorem flatAngleRight_eq L133
• def starFlatAngleSum L134
• theorem star_flat_angle_sum_two_pi L135
• def starFlatCosines L138
• theorem starFlatCosines_match_orbits L141
• def nearCoordPath L148
• def farCoordPath L151
• def nearCosKernel L154
• def farCosKernel L161
• lemma hasDerivAt_quadPoly L170
• lemma hasDerivAt_numForm_zeroDot L182
• lemma hasDerivAt_near_slot L211
• lemma hasDerivAt_far_slot L238
• lemma near_path0_polys L265
• theorem hasDerivAt_near_slot0 L275
• lemma near_path1_polys L284
• theorem hasDerivAt_near_slot1 L294
• lemma near_path2_polys L303
• theorem hasDerivAt_near_slot2 L313
• lemma near_path3_polys L322
• theorem hasDerivAt_near_slot3 L332
• lemma near_path4_polys L341
• theorem hasDerivAt_near_slot4 L351
• lemma near_path5_polys L360
• theorem hasDerivAt_near_slot5 L370
• lemma near_path6_polys L379
• theorem hasDerivAt_near_slot6 L389
• lemma near_path7_polys L398
• theorem hasDerivAt_near_slot7 L408
• lemma near_path8_polys L417
• theorem hasDerivAt_near_slot8 L427
• lemma near_path9_polys L436
• theorem hasDerivAt_near_slot9 L446
• theorem hasDerivAt_near_coord L455
• lemma far_path0_polys L470
• theorem hasDerivAt_far_slot0 L480
• lemma far_path1_polys L489
• theorem hasDerivAt_far_slot1 L499
• lemma far_path2_polys L508
• theorem hasDerivAt_far_slot2 L518
• lemma far_path3_polys L527
• theorem hasDerivAt_far_slot3 L537
• lemma far_path4_polys L546
• theorem hasDerivAt_far_slot4 L556
• lemma far_path5_polys L565
• theorem hasDerivAt_far_slot5 L575
• lemma far_path6_polys L584
• theorem hasDerivAt_far_slot6 L594
• lemma far_path7_polys L603
• theorem hasDerivAt_far_slot7 L613
• lemma far_path8_polys L622
• theorem hasDerivAt_far_slot8 L632
• lemma far_path9_polys L641
• theorem hasDerivAt_far_slot9 L651
• theorem hasDerivAt_far_coord L660
• def chainRight L677
• def nearDeficitKernel L678
• def farDeficitKernel L679
• theorem nearDeficitKernel_eq_chain L681

… and 29 more