theorem
proved
term proof
sdgt_assignment_forced
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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