IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel

declarations in this module (48)

• def permAxes L70
• def permOf L98
• def axisMask L106
• def vertexMask L110
• theorem vertexMask_start L118
• theorem vertexMask_end L120
• def localEdgePair L123
• def localEdgeMask L137
• theorem localEdgeMask_bounds L141
• def localEdgeClass L146
• theorem localEdgeClass_mask L151
• def simplexHasClass L158
• theorem permOf_eq_of_eq L161
• def containsSeedHinge L170
• theorem containsSeedHinge_iff L176
• theorem seedHinge_simplex_count L182
• theorem seedHinge_simplices L188
• def simplex0Classes L196
• def simplex1Classes L200
• theorem simplex0Classes_correct L204
• theorem simplex1Classes_correct L209
• theorem simplex0Classes_complete L214
• theorem simplex1Classes_complete L220
• def seedHingeIncidenceNat L226
• theorem seedHingeIncidenceNat_values L231
• theorem sum_seedHingeIncidenceNat L250
• theorem seedHingeIncidence_nonvacuous L259
• def swap23Mask L265
• theorem swap23Mask_bounds L271
• def swap23Class L276
• theorem seedHingeIncidence_swap23 L283
• def decoyClass4 L288
• def decoyClass8 L289
• def decoyClass12 L290
• theorem seedHingeIncidence_decoy_zero L294
• def hingeBoundaryClass L301
• theorem hingeBoundary_incidence_pos L307
• def classInSimplexNat L314
• theorem simplex_class_count L318
• theorem cell_covers_all_classes L323
• def flatHessianOrbitForm L336
• def seedOrbitAssembly L344
• theorem seedOrbitAssembly_decoy_area L357
• def supportProject L376
• theorem seedOrbitAssembly_support_projection L381
• structure Hinge4DFlatKernelStatus L397
• def hinge4DFlatKernelStatus L404
• theorem hinge4DFlatKernelStatus_flags L411