Words / CONCEPT

AdaptiveMergeSignedFork

Fix distinct nonzero a,b in a finite alphabet A and a Good compressed word L,(a+b),R. Assume L and R have distinct labels in A minus {a,b} and are disjoint. If both adjacent expansions fail, then M(a,b), M(b,a), E(a,b) or E(b,a) holds. M(x,y) quantifies disjoint nonempty Finsets U,V contained in A minus {x}, with y in V, sum U = -x and sum V = x. E(x,y) quantifies disjoint nonempty Finsets avoiding both x and y, each with sum -x. ForkEdge is exactly the disjunction of these four predicates, independent of any word. Same-side collision suffixes are nested; their difference together with the other merge label supplies M. Opposite-side suffix and prefix are disjoint and supply E. Right/right collisions reduce by reversal. List certificates are converted using nodup and List.sum_toFinset, preserving each original label with coefficient one. The original fixed C2 x C4 chosen-pair refutation calibrates the quantifier boundary and is not copied or generalized here.