IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel

declarations in this module (114)

• inductive CubeTranslate L56
• def localHingeMasks L63
• def containsHinge L69
• structure StarMember L72
• def starMembers L77
• theorem starMembers_length L82
• theorem starMembers_complete L84
• theorem star_cardinality L88
• def oppFlatSqEdges L95
• def orthFlatSqEdges L99
• theorem hingeGramDet_opp L103
• theorem apexDotNum_opp L105
• theorem apex3NormSqNum_opp L107
• theorem apex4NormSqNum_opp L109
• theorem hingeGramDet_orth L112
• theorem apexDotNum_orth L114
• theorem apex3NormSqNum_orth L116
• theorem apex4NormSqNum_orth L118
• theorem cosDihedral_opp_flat L121
• theorem cosDihedral_orth_flat L133
• theorem arccos_one_div_sqrt_two L140
• def flatAngleSeedOpp L151
• def flatAngleOrth L152
• theorem flatAngleSeedOpp_eq L154
• theorem flatAngleOrth_eq L156
• def starFlatAngleSum L158
• theorem star_flat_angle_sum_two_pi L160
• def starFlatCosines L164
• theorem starFlatCosines_match_orbits L169
• def oppCoordPath L178
• def oppCosKernel L181
• lemma hasDerivAt_quadPoly L186
• lemma hasDerivAt_numForm_opp L198
• lemma hasDerivAt_opp_slot L249
• lemma opp_path0_polys L277
• lemma opp_path1_polys L287
• lemma opp_path2_polys L297
• lemma opp_path3_polys L307
• lemma opp_path4_polys L317
• lemma opp_path5_polys L327
• lemma opp_path6_polys L337
• lemma opp_path7_polys L347
• lemma opp_path8_polys L357
• lemma opp_path9_polys L367
• theorem hasDerivAt_opp_slot0 L377
• theorem hasDerivAt_opp_slot1 L386
• theorem hasDerivAt_opp_slot2 L395
• theorem hasDerivAt_opp_slot3 L404
• theorem hasDerivAt_opp_slot4 L413
• theorem hasDerivAt_opp_slot5 L422
• theorem hasDerivAt_opp_slot6 L431
• theorem hasDerivAt_opp_slot7 L440
• theorem hasDerivAt_opp_slot8 L449
• theorem hasDerivAt_opp_slot9 L458
• theorem hasDerivAt_opp_coord L468
• def orthCoordPath L485
• def orthCosKernel L488
• lemma hasDerivAt_numForm_orth L495
• lemma hasDerivAt_orth_slot L521
• lemma orth_path0_polys L548
• lemma orth_path1_polys L558
• lemma orth_path2_polys L568
• lemma orth_path3_polys L578
• lemma orth_path4_polys L588
• lemma orth_path5_polys L598
• lemma orth_path6_polys L608
• lemma orth_path7_polys L618
• lemma orth_path8_polys L628
• lemma orth_path9_polys L638
• theorem hasDerivAt_orth_slot0 L648
• theorem hasDerivAt_orth_slot1 L657
• theorem hasDerivAt_orth_slot2 L666
• theorem hasDerivAt_orth_slot3 L675
• theorem hasDerivAt_orth_slot4 L684
• theorem hasDerivAt_orth_slot5 L693
• theorem hasDerivAt_orth_slot6 L702
• theorem hasDerivAt_orth_slot7 L711
• theorem hasDerivAt_orth_slot8 L720
• theorem hasDerivAt_orth_slot9 L729
• theorem hasDerivAt_orth_coord L739

… and 34 more