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. -/
depends on (33)
Lean names referenced from this declaration's body.