Proximity with Six Forbidden Basis Sums in Binary Matroids

Let the elements of a finite matroid be labeled by an arbitrary abelian group, and forbid a finite set F of possible basis sums. We give a computer-assisted proof that, in a binary matroid, if an avoiding basis exists, then every basis is within |F| exchanges of an avoiding basis whenever |F|≤6. The same conclusion holds after relaxing any collection of circuit-hyperplanes of a binary matroid. The proof reduces to two finite binary matrix qualifications at ranks six and seven. Most pairs have interval-exchange orderings; the remaining pairs have explicit additive conflict graphs with certified chromatic obstructions. Orbit accounting and positive certificates provide a verification route independent of the discovery search. Consequently the unrestricted single-label proximity conjecture holds in these classes when the rank or corank is at most seven.