IndisputableMonolith.Foundation.GaugeFromCube

declarations in this module (43)

• def CubeVertex L93
• theorem cube_vertex_count L101
• theorem cube3_vertex_count L105
• def cube_edge_count L109
• theorem cube3_edge_count L112
• def cube_face_count L117
• theorem cube3_face_count L120
• structure SignedPerm L131
• theorem signed_perm_card L144
• theorem cube_aut_order L153
• def IsAxisPermutation L162
• def axis_perm_count L166
• theorem axis_perm_count_D3 L168
• def IsSignFlip L173
• def sign_flip_count L177
• theorem sign_flip_count_D3 L179
• def IsEvenSignFlip L187
• def sign_parity L191
• def even_sign_flip_count L195
• theorem even_sign_flip_count_D3 L198
• def parity_quotient_order L206
• theorem three_layer_factorization L216
• theorem sm_factorization L223
• structure GaugeLayer L238
• def color_layer L244
• def weak_layer L249
• def hypercharge_layer L254
• theorem gauge_rank_match L262
• theorem dimension_sum L275
• theorem dimension_sum_triangular L283
• theorem s3_is_weyl_of_su3 L298
• theorem color_from_axis_permutations L304
• theorem even_flips_give_weak_structure L318
• theorem parity_gives_hypercharge L327
• theorem unique_gauge_factorization L338
• theorem no_alternative_321 L362
• def sm_gauge_ranks L371
• def cube_gauge_ranks L374
• theorem cube_matches_sm L378
• theorem total_gauge_dim L383
• theorem gauge_order_product L388
• theorem gauge_generation_unification L406
• theorem gauge_group_certificate L432