IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureDerivationHostileProbe

declarations in this module (13)

• theorem gcp_closing_is_blocker_gcp L36
• theorem gibbsWeight_def_no_aut L50
• theorem classMass_gibbs_eq_mu_is_not_rfl L56
• theorem classMass_one_eq_orbit L61
• theorem twoPoint_orbitCard L66
• theorem wrong_labeled_weight_fails_gaugeCounting L75
• theorem only_gibbs_among_invariant L89
• theorem closing_has_no_premises_arg L111
• theorem composition_load_bearing_shape L117
• theorem closing_via_blocker_iff L129
• theorem closing_lands_on_mu L137
• theorem blocker_certificate_available L142
• theorem flag_moved L158