current_chain_distinct

formal source

 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)
 167    (h_middle : b + c = 17)
 168    (h_a_eq : a = 13)  -- E+1
 169    (h_b_eq : b = 11)  -- E-1
 170    :
 171    a = 13 ∧ b = 11 ∧ c = 6 ∧ d = 8 := by
 172  subst h_a_eq h_b_eq