Constructing an augmenting walk from an improving labeling

The two phases of Lemma 31 in [KKR18], arXiv v6, Section 6.1, printed p. 15, use deterministic scans of the actual positional incidence records. The first phase repairs defects of the comparison labeling outside the original defect set; the second phase follows remaining disagreements. Each exchange removes exactly two disagreements. The clock counts exchanges, not native-machine steps; native encoding and runtime certification belong to the solver integration. An improving valid comparison labeling is an input, not an assumed solver result. The construction works for any specified excluded start, strengthening the source's hypothesis that this variable is inconsistent; it may be the terminal variable.

Main definitions

• EdgeInstance.repair, EdgeInstance.buildWalk: the two clocked exchange phases.
• EdgeInstance.augmentingWalk: their total, choice-free composition.

Main results

• EdgeInstance.repair_spec, EdgeInstance.buildWalk_spec: phase invariants and exact progress.
• EdgeInstance.augmentingWalk_spec: Lemma 31 with a bound on the combined exchange count.
• EdgeInstance.isOptimalLabeling_iff_no_augmentingWalk: the augmenting-walk characterization.

def Cslib.Logic.PL.CSP.EdgeInstance.findPair {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) (P : F.Occurrence × F.Occurrence → Prop) [DecidablePred P] : Option (F.Occurrence × F.Occurrence)

First satisfying incidence pair in positional order. This scan examines pairs, not trails.

theorem Cslib.Logic.PL.CSP.EdgeInstance.findPair_spec {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {P : F.Occurrence × F.Occurrence → Prop} [DecidablePred P] {a : F.Occurrence × F.Occurrence} (ha : findPair F P = some a) : P a

A returned scan pair satisfies the predicate.

theorem Cslib.Logic.PL.CSP.EdgeInstance.findPair_none {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {P : F.Occurrence × F.Occurrence → Prop} [DecidablePred P] (hn : findPair F P = none) (o p : F.Occurrence) : ¬P (o, p)

A failed scan rules out every pair, since all incidences are enumerated.

def Cslib.Logic.PL.CSP.EdgeInstance.RepairMove {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (sem : Rel → List Bool → Bool) (f g : F.OccurrenceLabeling Bool) (a : F.Occurrence × F.Occurrence) : Prop

A first-phase exchange repairs an f-consistent variable at which g has a new defect.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.EdgeInstance.instDecidableRepairMove {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f g : F.OccurrenceLabeling Bool) (a : F.Occurrence × F.Occurrence) : Decidable (RepairMove sem f g a)

def Cslib.Logic.PL.CSP.EdgeInstance.repair {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) : ℕ → F.OccurrenceLabeling Bool → F.OccurrenceLabeling Bool × ℕ

Clocked first phase. The second output counts exchanges. No choice or partner operation occurs in this routine; an exhausted clock returns its current labeling.

theorem Cslib.Logic.PL.CSP.EdgeInstance.exists_repairMove {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) (hg : ValidLabeling sem g) {v : V} (hvf : ¬Inconsistent f v) (hvg : Inconsistent g v) : ∃ (a : F.Occurrence × F.Occurrence), RepairMove sem f g a

A new defect provides a first-phase exchange using the local even delta-matroid axiom.

theorem Cslib.Logic.PL.CSP.EdgeInstance.repair_spec {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) (hg : ValidLabeling sem g) (fuel : ℕ) : match repair sem f fuel g with | (g', k) => ValidLabeling sem g' ∧ (defects g').card ≤ (defects g).card ∧ hammingDist f g' + 2 * k = hammingDist f g ∧ k ≤ fuel ∧ (hammingDist f g ≤ fuel → defects g' ⊆ defects f)

The clocked repair preserves validity and never increases defects. It removes two occurrence disagreements per exchange, and a clock at least the initial Hamming distance suffices to leave no new defects.

theorem Cslib.Logic.PL.CSP.EdgeInstance.exists_start_ne {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) (hg : ValidLabeling sem g) (hlt : (defects g).card < (defects f).card) (x : V) : ∃ (r : V), r ≠ x ∧ Inconsistent f r ∧ ¬Inconsistent g r

Two fewer defects and containment provide a starting defect different from any specified variable. Only the start is excluded; the walk may end at that variable.

def Cslib.Logic.PL.CSP.EdgeInstance.WalkMove {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (sem : Rel → List Bool → Bool) (g current : F.OccurrenceLabeling Bool) (v : V) (a : F.Occurrence × F.Occurrence) : Prop

A second-phase move follows an incidence disagreement at the current endpoint.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.EdgeInstance.instDecidableWalkMove {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (g current : F.OccurrenceLabeling Bool) (v : V) (a : F.Occurrence × F.Occurrence) : Decidable (WalkMove sem g current v a)

def Cslib.Logic.PL.CSP.EdgeInstance.buildWalk {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f g : F.OccurrenceLabeling Bool) : ℕ → F.Walk → Option F.Walk

Clocked second phase. It extends the current trail by one local exchange and stops on the first original defect reached. The scan and recursion contain no noncomputable choice.

theorem Cslib.Logic.PL.CSP.EdgeInstance.exists_walkMove {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {g current : F.OccurrenceLabeling Bool} (hg : ValidLabeling sem g) (hc : ValidLabeling sem current) {v : V} (hcv : Inconsistent current v) (hgv : ¬Inconsistent g v) : ∃ (a : F.Occurrence × F.Occurrence), WalkMove sem g current v a

A defective current endpoint, consistent in the target, always admits an exchange.

structure Cslib.Logic.PL.CSP.EdgeInstance.WalkState {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (sem : Rel → List Bool → Bool) (f g : F.OccurrenceLabeling Bool) (w : F.Walk) : Prop

The second-phase invariant. Already-used incidences agree with the target, so scans of remaining disagreements cannot reuse them. Once the first step is taken, every incidence of the starting variable agrees with the target, preventing a return to that start.

• prefix_valid : Walk.IsFPrefix sem f w
• endpoint_defect : Inconsistent (w.flip f) w.finish
• target_endpoint : ¬Inconsistent g w.finish
• internal_endpoint : w.steps = [] ∨ ¬Inconsistent f w.finish
• start_defect : Inconsistent f w.start
• target_start : ¬Inconsistent g w.start
• used_agrees (a : F.Occurrence) : a ∈ w.edges → w.flip f a = g a
• start_cleared : w.steps ≠ [] → ∀ (a : F.Occurrence), a.var = w.start → w.flip f a = g a

theorem Cslib.Logic.PL.CSP.EdgeInstance.buildWalk_spec {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f g : F.OccurrenceLabeling Bool} (hg : ValidLabeling sem g) (hsub : defects g ⊆ defects f) (fuel : ℕ) {w : F.Walk} (hw : WalkState sem f g w) (hclock : hammingDist (w.flip f) g ≤ fuel) : ∃ (w' : F.Walk) (k : ℕ), buildWalk sem f g fuel w = some w' ∧ Walk.IsAugmenting sem f w' ∧ w'.start = w.start ∧ w'.steps.length = w.steps.length + k ∧ hammingDist (w'.flip f) g + 2 * k = hammingDist (w.flip f) g ∧ k ≤ fuel

The second phase returns an augmenting prefix-valid incidence trail. Its clock counts exchanges, and each appended step removes exactly two remaining occurrence disagreements.

theorem Cslib.Logic.PL.CSP.EdgeInstance.buildWalk_from_start {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) (hg : ValidLabeling sem g) (hsub : defects g ⊆ defects f) (r : V) (hrf : Inconsistent f r) (hrg : ¬Inconsistent g r) : ∃ (w : F.Walk) (k : ℕ), buildWalk sem f g (hammingDist f g) { start := r, steps := [] } = some w ∧ Walk.IsAugmenting sem f w ∧ w.start = r ∧ w.steps.length = k ∧ hammingDist (w.flip f) g + 2 * k = hammingDist f g ∧ k ≤ hammingDist f g

Start the second phase at a chosen original defect absent from the comparison labeling.

theorem Cslib.Logic.PL.CSP.EdgeInstance.exists_augmentingWalk_start_ne {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) (hg : ValidLabeling sem g) (hlt : (defects g).card < (defects f).card) (x : V) : ∃ (w : F.Walk), Walk.IsAugmenting sem f w ∧ w.start ≠ x ∧ 2 * w.steps.length ≤ hammingDist f g

Full Lemma 31 existence conclusion, obtained by the actual two phases. The specified variable is excluded only as the start. No solver or augmenting-walk assumption is used.

def Cslib.Logic.PL.CSP.EdgeInstance.findStart {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) (f g : F.OccurrenceLabeling Bool) (x : V) : Option F.Occurrence

First original defect absent from the comparison labeling, excluding the specified start. Incidences are scanned in positional order; no arbitrary occurrence is chosen.

def Cslib.Logic.PL.CSP.EdgeInstance.augmentingWalk {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f g : F.OccurrenceLabeling Bool) (x : V) : Option F.Walk

The full two-phase construction of Lemma 31. The clocks are occurrence Hamming distances; failed or insufficient inputs return none. Correctness under the mathematical hypotheses is augmentingWalk_spec. The routine does not solve for the improving comparison labeling.

theorem Cslib.Logic.PL.CSP.EdgeInstance.augmentingWalk_spec {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f g : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) (hg : ValidLabeling sem g) (hlt : (defects g).card < (defects f).card) (x : V) : ∃ (w : F.Walk), augmentingWalk sem f g x = some w ∧ Walk.IsAugmenting sem f w ∧ w.start ≠ x ∧ 2 * ((repair sem f (hammingDist f g) g).2 + w.steps.length) ≤ hammingDist f g

Lemma 31 with a concrete total routine: given an improving valid comparison labeling, augmentingWalk returns an augmenting f-walk starting away from the specified variable. Both phases together perform at most half the original occurrence disagreements in exchanges. This bounds local exchanges; no native-machine runtime bound is asserted.

theorem Cslib.Logic.PL.CSP.EdgeInstance.exists_improvement_iff_exists_augmentingWalk {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) : (∃ (g : F.OccurrenceLabeling Bool), ValidLabeling sem g ∧ (defects g).card < (defects f).card) ↔ ∃ (w : F.Walk), Walk.IsAugmenting sem f w

Nonoptimality is equivalent to existence of an augmenting walk, without assuming a solver.

theorem Cslib.Logic.PL.CSP.EdgeInstance.isOptimalLabeling_iff_no_augmentingWalk {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (h : F.EdgeInstance) {sem : Rel → List Bool → Bool} (hM : EvenConstraints sem F) {f : F.OccurrenceLabeling Bool} : IsOptimalLabeling sem f ↔ ValidLabeling sem f ∧ ¬∃ (w : F.Walk), Walk.IsAugmenting sem f w

An optimal valid labeling has no augmenting walk, and conversely.