step_sum_eq

formal source

  47
  48def step_sum : ℕ := 13 + 11 + 6 + 8
  49
  50theorem step_sum_eq : step_sum = 38 := by native_decide
  51
  52/-- The partition sum for three overlapping consecutive pairs from (a,b,c,d)
  53    is a + 2b + 2c + d. -/
  54def partition_sum (a b c d : ℕ) : ℕ := a + 2*b + 2*c + d
  55
  56/-- Partition sum equals element sum plus middle pair sum. -/
  57theorem partition_sum_decomp (a b c d : ℕ) :
  58    partition_sum a b c d = (a + b + c + d) + (b + c) := by
  59  unfold partition_sum; omega
  60
  61/-- If the partition sum must equal 55 and element sum is 38,
  62    the middle pair must sum to 17 = W. -/
  63theorem middle_pair_sum_forced (a b c d : ℕ)
  64    (hsum : a + b + c + d = 38)
  65    (hpart : partition_sum a b c d = 55) :
  66    b + c = 17 := by
  67  have := partition_sum_decomp a b c d
  68  omega
  69
  70/-! ## Step 2: Uniqueness — Only {11, 6} sums to 17
  71
  72Among the four values {13, 11, 6, 8}, the only pair summing to 17
  73is {11, 6} = {E_pass, F}. -/
  74
  75/-- Exhaustive check: no other pair from {13, 11, 6, 8} sums to 17. -/
  76theorem only_11_6_sum_to_17 :
  77    (13 + 11 ≠ 17) ∧ (13 + 6 ≠ 17) ∧ (13 + 8 ≠ 17) ∧
  78    (11 + 8 ≠ 17) ∧ (6 + 8 ≠ 17) ∧
  79    (11 + 6 = 17) := by
  80  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> omega