current_chain_middle

formal source

 133    13 + 2*11 + 2*6 + 8 = 55 := by norm_num
 134
 135/-- The current chain has middle pair summing to W. -/
 136theorem current_chain_middle : 11 + 6 = 17 := by norm_num
 137
 138/-- The current chain has endpoint sum = 21. -/
 139theorem current_chain_endpoints : 13 + 8 = 21 := by norm_num
 140
 141/-- All four values of the current chain are distinct. -/
 142theorem current_chain_distinct : (13 : ℕ) ≠ 11 ∧ 11 ≠ 6 ∧ 6 ≠ 8 ∧ 13 ≠ 6 ∧ 13 ≠ 8 ∧ 11 ≠ 8 := by
 143  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> norm_num
 144
 145/-! ## Constraint 4: The Unique Fully-Integer-Chain Containing E±1
 146
 147One natural structural filter: the chain should contain both "edge plus one"
 148(E+1 = 13) and "edge minus one" (E-1 = 11). These are the simplest
 149symmetric deformations of the edge count E = 12.
 150
 151Under this filter, the remaining two values must sum to 21 - 13 - 11 = ...
 152wait, that over-constrains. Let me redo:
 153
 154If two of the four values are E±1, and the cyclic chain structure is
 155(E+1, E-1, ?, ?) ending back at E+1, then the middle pair is (E-1, ?) with
 156sum 17, forcing ? = 17 - 11 = 6 = F. Then the fourth value must satisfy
 1576 + d = span_down, with span_down = 55 - 24 - 17 = 14, so d = 8 = V.
 158
 159Under this filter, the chain (E+1, E-1, F, V) = (13, 11, 6, 8) is unique.
 160-/
 161
 162/-- If the chain contains both E+1 and E-1 as adjacent values, the chain is
 163    uniquely determined. -/
 164theorem chain_unique_given_edge_pair
 165    (a b c d : ℕ)
 166    (h_chain_partition : a + 2*b + 2*c + d = 55)