IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasureHostileProbe

declarations in this module (30)

• theorem g1_hyp_defs_avoid_aut L30
• theorem push_preserves_ordered_incidence L42
• theorem relabel_edge_comm_is_ordered L48
• theorem classMass_def_is_fibre_sum L56
• theorem orbit_stabilizer_is_proved L64
• theorem corollary_factor_explicit L69
• def pathPlusIsolated L83
• theorem pathPlusIsolated_counts L93
• theorem twoEdgeComplex_counts L97
• def edgeCommOK L101
• def twoEdgeEV L105
• def pathPlusEV L108
• def twoEdgeAutCount L111
• def pathPlusAutCount L115
• theorem twoEdge_autCount_eq_two L120
• theorem pathPlus_autCount_eq_one L123
• def twoEdgeSwapV L126
• theorem twoEdge_component_swap_ok L129
• theorem twoEdge_id_ok L134
• theorem twoEdge_edge_flip_fails_comm L139
• theorem enumerated_mu_ratio_is_half L144
• theorem dust_aut_arithmetic L149
• theorem pathPlus_aut_inhabited L156
• theorem locallyAdditive_is_explicit L161
• theorem uniform_quantifies_all_Q L165
• theorem relabelInvariant_inhabited_constant L176
• theorem relabelInvariant_inhabited_equivariant_numerator L180
• theorem dust_twin_admissible_real L185
• theorem wreath_proved_not_assumed L190
• theorem flag_still_false L195