Optimality of a fresh exhausted forest search

search_exhausted_isOptimalLabeling proves the conclusion of Lemma 45 of [KKR18], arXiv:1602.03124v6, printed pp. 0:22–23: when the fresh forest search exhausts its frontier before augmentation or a blossom, its valid base labeling has the fewest defects among all valid labelings. Constraints are nonempty even delta-matroids on their actual argument positions; their common parities may be odd. Variables need only decidable equality, since all counts range over occurring variables and positional ports.

This is an alternative counting reconstruction, rather than the paper's shortest-bad-walk proof. Saturation gives a local disagreement bound by one-sided exchange. Fresh roots and unique children give the opposite global bound on changes at incoming and outgoing ports. No terminal-event correctness, blossom contraction, native runtime or full solver is claimed.

Main results

• search_exhausted_isOptimalLabeling: actual fresh exhaustion implies optimality.

theorem Cslib.Logic.PL.CSP.Forest.search_exhausted_isOptimalLabeling {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (hF : F.EdgeInstance) (hf : ValidLabeling sem f) (hM : EdgeInstance.EvenConstraints sem F) {es : Log F} (hs : search sem f = Result.exhausted es) : IsOptimalLabeling sem f

Lemma 45 of [KKR18], printed pp. 0:22–23, by an alternative counting proof. A fresh executable search returning exhaustion certifies that its valid base labeling minimizes defects among all valid labelings. No finite universe of variable names, comparison labeling, supplied forest invariant or terminal-event theorem is required.