IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification

declarations in this module (58)

• def triangleIndexTriple L69
• def maskPop L83
• def triangleVertexMasks L90
• def diffMaskA L95
• def diffMaskB L100
• def hingeTypePop L105
• inductive HingeOrbitType L109
• def popToOrbitType L126
• theorem hingeTypePop_is_orbitType L136
• def hingeOrbitType L141
• theorem hingeOrbitType_toPop L144
• theorem triangle_diff_masks_ok L150
• def triangleTypeNat L159
• def cellTriangleCount L163
• theorem cellTriangleCount_t11 L166
• theorem cellTriangleCount_t12 L169
• theorem cellTriangleCount_t21 L172
• theorem cellTriangleCount_t13 L175
• theorem cellTriangleCount_t31 L178
• theorem cellTriangleCount_t22 L181
• theorem cellTriangleCount_values L185
• theorem cellTriangleCount_sum L196
• theorem oriented_slot_total L204
• def isRealizableDiffPair L211
• def isDisjointDiffPair L216
• theorem disjoint_implies_realizable L220
• theorem decoy_overlapping_not_realizable L227
• theorem decoy_overlapping_is_not_disjoint L231
• theorem seed_slot_masks L236
• theorem seed_hinge_type_t11 L241
• def permMask L248
• def coordPermOf L256
• def permDiffPair L264
• theorem coordPerm_preserves_pop L269
• theorem coordPerm_preserves_type L275
• def orbitRep L282
• theorem orbitRep_realizable L290
• theorem orbitRep_type L294
• def inOrbitOfRep L299
• theorem realizable_in_type_orbit L306
• theorem realizable_matches_rep_orbit L317
• def complementMask L325
• theorem complement_preserves_kuhn L329
• theorem complement_swaps_diff_pair L336
• theorem complement_swaps_type L343
• inductive HingeOrbitTypeModComplement L350
• theorem orbit_count_S4 L363
• theorem orbit_count_S4_complement L366
• def absoluteTriple L373
• def permTriple L377
• theorem absolute_t11_not_S4_transitive L386
• structure OrbitLocalSq L398
• def localSqOfDiff L404
• def orbitLocalSq L407
• theorem orbitLocalSq_values L410
• theorem slot_localSq L421
• def hinge4DOrbitClassificationStatus L428
• theorem hinge4DOrbitClassificationStatus_flags L436