IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22

declarations in this module (76)

• def absHingeMasks L62
• abbrev CubeCorner L66
• def cornerContainsMask L71
• def cornerContainsHinge L74
• def localMask L79
• def localHingeMasks L81
• def containsHinge L84
• structure StarMember L88
• def starMembers L93
• theorem starMembers_length L96
• theorem starMembers_complete L98
• theorem star_cardinality L103
• theorem only_origin_corner_contains_hinge L108
• def t22FlatSqEdges L117
• theorem hingeGramDet_t22 L121
• theorem apexDotNum_t22 L123
• theorem apex3NormSqNum_t22 L125
• theorem apex4NormSqNum_t22 L127
• theorem cosDihedral_t22_flat L130
• def flatAngleT22 L137
• theorem flatAngleT22_eq L139
• def starFlatAngleSum L141
• theorem star_flat_angle_sum_two_pi L143
• def starFlatCosines L147
• theorem starFlatCosines_match_orbit L149
• def t22CoordPath L155
• def t22CosKernel L158
• lemma hasDerivAt_quadPoly L170
• lemma hasDerivAt_numForm_t22 L184
• lemma hasDerivAt_t22_slot L210
• lemma t22_path0_polys L237
• lemma t22_path1_polys L247
• lemma t22_path2_polys L257
• lemma t22_path3_polys L267
• lemma t22_path4_polys L277
• lemma t22_path5_polys L287
• lemma t22_path6_polys L297
• lemma t22_path7_polys L307
• lemma t22_path8_polys L317
• lemma t22_path9_polys L327
• theorem hasDerivAt_t22_slot0 L337
• theorem hasDerivAt_t22_slot1 L345
• theorem hasDerivAt_t22_slot2 L353
• theorem hasDerivAt_t22_slot3 L361
• theorem hasDerivAt_t22_slot4 L369
• theorem hasDerivAt_t22_slot5 L377
• theorem hasDerivAt_t22_slot6 L385
• theorem hasDerivAt_t22_slot7 L393
• theorem hasDerivAt_t22_slot8 L401
• theorem hasDerivAt_t22_slot9 L409
• theorem hasDerivAt_t22_coord L417
• def chainT22 L435
• def t22DeficitKernel L438
• theorem t22DeficitKernel_eq_chain L440
• def starSlotClass L446
• def assembleStarMember L456
• def fullStarClassKernelAssembled L460
• def fullStarClassKernel L463
• lemma sum_fin10 L480
• lemma member_eval L491
• lemma sum4 L506
• theorem fullStarClassKernel_eq L514
• theorem fullStarClassKernel_values L522
• def swap01Mask L542
• theorem swap01Mask_bounds L548
• def swap01Class L552
• theorem fullStarClassKernel_nonvacuous L557
• theorem fullStarClassKernel_swap01 L560
• theorem fullStarClassKernel_swap23 L564
• def fullStarDirectional L568
• lemma sum15_all L571
• theorem fullStar_uniformScale_decoy L585
• theorem fullStar_homothety_stationary L591
• structure Hinge4DStarKernel22Status L616
• def hinge4DStarKernel22Status L625
• theorem hinge4DStarKernel22Status_flags L634