2.23. Fresh Forest Search🔗

Cslib.Logic.PL.CSP.Forest.search starts from the actual defective variables, without an improving comparison. Its positional log keeps copied constraints and zero-based timestamps. It stops at exhaustion, an augmentation or a blossom. Cslib.Logic.PL.CSP.Forest.search_terminal_isFDAG proves both terminal DAG invariants from the edge-instance condition and base validity, without evenness.

The three outcome theorems add even delta-matroid constraints, permitting odd local common parity. Exhaustion certifies genuine optimality:

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

An actual returned augmentation is prefix-valid, its flip is valid, and it removes exactly two defects:

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Logic.PL.CSP.Forest in
example {Rel V : Type} [DecidableEq V] {F : CSP Rel V}
    (sem : Rel → List Bool → Bool) (f : OccurrenceLabeling F Bool)
    (hF : EdgeInstance F) (hf : ValidLabeling sem f)
    (hM : EdgeInstance.EvenConstraints sem F) {m : Meeting F}
    (hr : search sem f = .augment m) :
    m.walk.IsAugmenting sem f ∧ ValidLabeling sem (m.walk.flip f) ∧
      (defects (m.walk.flip f)).card + 2 = (defects f).card :=
  search_augment_correct sem f hF hf hM hr

A blossom result certifies the data actually computed by the extractor. Preparation preserves validity and defect count. Its cycle has distinct copied steps, and the actual timestamps are distinct:

open Cslib.Logic.PL Cslib.Logic.PL.CSP Cslib.Logic.PL.CSP.Forest in
example {Rel V : Type} [DecidableEq V] {F : CSP Rel V}
    (sem : Rel → List Bool → Bool) (f : OccurrenceLabeling F Bool)
    (hF : EdgeInstance F) (hf : ValidLabeling sem f)
    (hM : EdgeInstance.EvenConstraints sem F) {m : Meeting F}
    (hr : search sem f = .blossom m) :
    ∃ b, m.blossomData = some b ∧ b.cycle.IsBlossom sem (b.prepare.flip f) ∧
      b.times.Nodup ∧ ValidLabeling sem (b.prepare.flip f) ∧
      (defects (b.prepare.flip f)).card = (defects f).card := byRel:TypeV:Typeinst✝:DecidableEq VF:CSP Rel Vsem:Rel → List Bool → Boolf:F.OccurrenceLabeling BoolhF:F.EdgeInstancehf:ValidLabeling sem fhM:EdgeInstance.EvenConstraints sem Fm:Meeting Fhr:search sem f = Result.blossom m⊢ ∃ b,
  m.blossomData = some b ∧
    Walk.IsBlossom sem (b.prepare.flip f) b.cycle ∧
      b.times.Nodup ∧ ValidLabeling sem (b.prepare.flip f) ∧ (defects (b.prepare.flip f)).card = (defects f).card
  obtain ⟨b, hb, hbl, hv, hd⟩ := search_blossom_correct sem f hF hf hM hrRel:TypeV:Typeinst✝:DecidableEq VF:CSP Rel Vsem:Rel → List Bool → Boolf:F.OccurrenceLabeling BoolhF:F.EdgeInstancehf:ValidLabeling sem fhM:EdgeInstance.EvenConstraints sem Fm:Meeting Fhr:search sem f = Result.blossom mb:BlossomData Fhb:m.blossomData = some bhbl:Walk.IsBlossom sem (b.prepare.flip f) b.cyclehv:ValidLabeling sem (b.prepare.flip f)hd:(defects (b.prepare.flip f)).card = (defects f).card⊢ ∃ b,
  m.blossomData = some b ∧
    Walk.IsBlossom sem (b.prepare.flip f) b.cycle ∧
      b.times.Nodup ∧ ValidLabeling sem (b.prepare.flip f) ∧ (defects (b.prepare.flip f)).card = (defects f).card
  have ht := search_trace sem f hFRel:TypeV:Typeinst✝:DecidableEq VF:CSP Rel Vsem:Rel → List Bool → Boolf:F.OccurrenceLabeling BoolhF:F.EdgeInstancehf:ValidLabeling sem fhM:EdgeInstance.EvenConstraints sem Fm:Meeting Fhr:search sem f = Result.blossom mb:BlossomData Fhb:m.blossomData = some bhbl:Walk.IsBlossom sem (b.prepare.flip f) b.cyclehv:ValidLabeling sem (b.prepare.flip f)hd:(defects (b.prepare.flip f)).card = (defects f).cardht:Result.Events (Meeting.Trace sem f) (search sem f)⊢ ∃ b,
  m.blossomData = some b ∧
    Walk.IsBlossom sem (b.prepare.flip f) b.cycle ∧
      b.times.Nodup ∧ ValidLabeling sem (b.prepare.flip f) ∧ (defects (b.prepare.flip f)).card = (defects f).card
  rw [hrRel:TypeV:Typeinst✝:DecidableEq VF:CSP Rel Vsem:Rel → List Bool → Boolf:F.OccurrenceLabeling BoolhF:F.EdgeInstancehf:ValidLabeling sem fhM:EdgeInstance.EvenConstraints sem Fm:Meeting Fhr:search sem f = Result.blossom mb:BlossomData Fhb:m.blossomData = some bhbl:Walk.IsBlossom sem (b.prepare.flip f) b.cyclehv:ValidLabeling sem (b.prepare.flip f)hd:(defects (b.prepare.flip f)).card = (defects f).cardht:Result.Events (Meeting.Trace sem f) (Result.blossom m)⊢ ∃ b,
  m.blossomData = some b ∧
    Walk.IsBlossom sem (b.prepare.flip f) b.cycle ∧
      b.times.Nodup ∧ ValidLabeling sem (b.prepare.flip f) ∧ (defects (b.prepare.flip f)).card = (defects f).card] at htRel:TypeV:Typeinst✝:DecidableEq VF:CSP Rel Vsem:Rel → List Bool → Boolf:F.OccurrenceLabeling BoolhF:F.EdgeInstancehf:ValidLabeling sem fhM:EdgeInstance.EvenConstraints sem Fm:Meeting Fhr:search sem f = Result.blossom mb:BlossomData Fhb:m.blossomData = some bhbl:Walk.IsBlossom sem (b.prepare.flip f) b.cyclehv:ValidLabeling sem (b.prepare.flip f)hd:(defects (b.prepare.flip f)).card = (defects f).cardht:Result.Events (Meeting.Trace sem f) (Result.blossom m)⊢ ∃ b,
  m.blossomData = some b ∧
    Walk.IsBlossom sem (b.prepare.flip f) b.cycle ∧
      b.times.Nodup ∧ ValidLabeling sem (b.prepare.flip f) ∧ (defects (b.prepare.flip f)).card = (defects f).card
  exact ⟨b, hb, hbl, ht.blossom_times_nodup hb, hv, hd⟩All goals completed! 🐙

No supplied forest/event invariant or finite universe of variable names is needed. Both variable and constraint least-common-ancestor cases are proved. Cslib.Logic.PL.CSP.Walk.DistinctCopies forbids sharing a copied node between cycle steps; original constraints may recur at different timestamps. The graph union alone admits an invalid-prefix counterexample, checked in CslibFrontierTests/EdgeCSPBlossomCopies.lean. The cycle certificate also retains the pivot, feasibility and no shortcuts; its validity does not follow from reversing an arbitrary f-walk. Exhaustion uses an alternative exchange-counting proof of KKR Lemma 45. The preparation proof uses chronological prefix transfer and Lemma 37 rerooting.

Complete actual-run clients are in CslibFrontierTests/EdgeCSPForestEvents.lean, CslibFrontierTests/EdgeCSPForestTerminal.lean and CslibFrontierTests/EdgeCSPForestOptimality.lean. They include nonempty preparation, repeated original constraints, timestamp zero, odd parity and sparse labels. These mathematical endpoints compose with the native compiler and whole-instance contraction/lifting and complete native edge solver below. The full planar dichotomy remains open.