IndisputableMonolith.Masses.SDGTForcing

declarations in this module (22)

• def step_sum L48
• theorem step_sum_eq L50
• def partition_sum L54
• theorem partition_sum_decomp L57
• theorem middle_pair_sum_forced L63
• theorem only_11_6_sum_to_17 L76
• theorem middle_pair_is_11_6 L83
• def ordering_A_spans L98
• def ordering_B_spans L99
• theorem ordering_A_unequal L101
• theorem ordering_B_equal L102
• theorem ordering_A_distinct_ends L105
• theorem ordering_B_equal_ends L109
• def Q_tilde_up L121
• def Q_tilde_down L122
• theorem charges_distinct L124
• theorem larger_charge_larger_span L128
• theorem sdgt_assignment_forced L138
• theorem span_up_eq_2E L155
• theorem span_lepton_eq_W L156
• theorem span_down_eq_VF L159
• theorem spans_partition_N3 L160