IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel13

declarations in this module (90)

• abbrev CubeOffset L68
• def offsetAxis L70
• def absHingeCoord L77
• def axisFits L83
• def vertexInCube L86
• def cubeContainsHinge L89
• def originOffset L92
• theorem cubeContainsHinge_origin L95
• theorem star_cube_cardinality L98
• theorem only_origin_contains_hinge L103
• def localHingeMasks L109
• def containsHinge L112
• def starMembers L115
• theorem starMembers_length L117
• theorem starMembers_complete L119
• theorem star_cardinality L123
• def t13FlatSqEdges L133
• theorem hingeGramDet_t13 L137
• theorem apexDotNum_t13 L139
• theorem apex3NormSqNum_t13 L141
• theorem apex4NormSqNum_t13 L143
• theorem cosDihedral_t13_flat L146
• theorem arccos_one_half L158
• def flatAngleT13 L164
• theorem flatAngleT13_eq L166
• def starFlatAngleSum L168
• theorem star_flat_angle_sum_two_pi L170
• def starFlatCosines L174
• theorem starFlatCosines_match L176
• def t13CoordPath L183
• def t13CosKernel L186
• lemma hasDerivAt_quadPoly L193
• lemma hasDerivAt_numForm_t13 L206
• lemma hasDerivAt_t13_slot L232
• lemma t13_path0_polys L260
• lemma t13_path1_polys L270
• lemma t13_path2_polys L280
• lemma t13_path3_polys L290
• lemma t13_path4_polys L300
• lemma t13_path5_polys L310
• lemma t13_path6_polys L320
• lemma t13_path7_polys L330
• lemma t13_path8_polys L340
• lemma t13_path9_polys L350
• theorem hasDerivAt_t13_slot0 L360
• theorem hasDerivAt_t13_slot1 L368
• theorem hasDerivAt_t13_slot2 L376
• theorem hasDerivAt_t13_slot3 L384
• theorem hasDerivAt_t13_slot4 L392
• theorem hasDerivAt_t13_slot5 L401
• theorem hasDerivAt_t13_slot6 L409
• theorem hasDerivAt_t13_slot7 L418
• theorem hasDerivAt_t13_slot8 L427
• theorem hasDerivAt_t13_slot9 L435
• theorem hasDerivAt_t13_coord L444
• def chainT13 L462
• theorem chainT13_eq L464
• def t13DeficitKernel L470
• theorem t13DeficitKernel_eq_chain L477
• def starSlotClass L491
• def assembleStarMember L505
• def fullStarClassKernelAssembled L509
• def fullStarClassKernel L512
• lemma sum_support4_4679 L522
• lemma deficit_zero_off L536
• lemma member_eval L541
• lemma sum6 L552
• lemma member0_closed L561
• lemma member1_closed L571
• lemma member2_closed L581
• lemma member3_closed L591
• lemma member4_closed L601
• lemma member5_closed L611
• theorem fullStarClassKernel_eq L621
• theorem fullStarClassKernel_values L629
• theorem fullStarClassKernel_zero_off L639
• theorem fullStarClassKernel_nonvacuous L647
• def swap12Mask L653
• theorem swap12Mask_bounds L659
• def swap12Class L663

… and 10 more