sdgt_assignment_forced

formal source

 135
 136/-- The complete forcing result: given the four step values and the
 137    partition + charge constraints, the SDGT assignment is unique. -/
 138theorem sdgt_assignment_forced :
 139    -- The partition constraint forces middle pair to sum to W
 140    (∀ a b c d : ℕ, a + b + c + d = 38 → partition_sum a b c d = 55 → b + c = 17) ∧
 141    -- Only {11, 6} sums to 17
 142    (11 + 6 = 17) ∧
 143    -- Ordering A has unequal end spans (forced by charge asymmetry)
 144    ((13 + 11 : ℕ) ≠ 6 + 8) ∧
 145    -- The spans are 24, 17, 14
 146    (13 + 11 = 24) ∧ (11 + 6 = 17) ∧ (6 + 8 = 14) ∧
 147    -- They partition 55
 148    (24 + 17 + 14 = 55) := by
 149  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
 150  · intro a b c d hsum hpart; exact middle_pair_sum_forced a b c d hsum hpart
 151  all_goals omega
 152
 153/-! ## Corollary: The spans are cube-geometric -/
 154
 155theorem span_up_eq_2E : (13 + 11 : ℕ) = 2 * cube_edges' 3 := by native_decide
 156theorem span_lepton_eq_W : (11 + 6 : ℕ) = Constants.AlphaDerivation.wallpaper_groups := by
 157  unfold Constants.AlphaDerivation.wallpaper_groups
 158  native_decide
 159theorem span_down_eq_VF : (6 + 8 : ℕ) = cube_vertices' 3 + cube_faces' 3 := by native_decide
 160theorem spans_partition_N3 : (24 + 17 + 14 : ℕ) = N3' 3 := by native_decide
 161
 162end SDGTForcing
 163end Masses
 164end IndisputableMonolith