2.24. Native Fresh Forest Search🔗

Import CslibFrontier.Computability.PolyTime.CSP.Edge.Forest.Spec for the complete fresh-search entry point. Its input is an explicit-table CSP with binary original names and one finite occurrence-bit buffer. Table arities and output indices are binary, while internal constraint/scope positions are unary. All clocks are funded by actual lists, including on malformed input:

open Cslib.Complexity.CSP.EdgeForest Turing.MultiTapeTM in
example : ComputableInPolyTime run encInput (encOption encResultCode) := by⊢ ComputableInPolyTime run encInput (encOption encResultCode)
  fun_propAll goals completed! 🐙

Correct buffer width alone gives exact agreement and decoding, without semantic or forest-invariant hypotheses:

open Cslib.Logic.PL.CSP Cslib.Complexity.CSP Cslib.Complexity.CSP.EdgeForest in
example (input : Input)
    (hw : input.labels.length = (incidenceList input.body).length) :
    (run input).bind (decode input.body) =
      some (Forest.search Table.sem
        (EdgeAugmenting.labeling input.body input.labels)) :=
  decode_run input hw

Cslib.Complexity.CSP.EdgeForest.run_eq_none_iff proves that none means width mismatch. A correctly sized buffer never exhausts the clock. Logs, roots, partial current copies and timestamps are retained; decoding external codes rejects invalid indices. This establishes no semantic correctness for an event on invalid input. With the model hypotheses, the composed specification applies to the actual decoded result:

open Cslib.Logic.PL.CSP Cslib.Complexity.CSP Cslib.Complexity.CSP.EdgeForest in
example (input : Input)
    (hw : input.labels.length = (incidenceList input.body).length)
    (hF : EdgeInstance input.body)
    (hf : ValidLabeling Table.sem
      (EdgeAugmenting.labeling input.body input.labels))
    (hM : EdgeInstance.EvenConstraints Table.sem input.body)
    {m : Forest.Meeting input.body}
    (hr : (run input).bind (decode input.body) = some (.augment m)) :
    m.walk.IsAugmenting Table.sem
      (EdgeAugmenting.labeling input.body input.labels) := byinput:Inputhw:input.labels.length = input.body.incidenceList.lengthhF:input.body.EdgeInstancehf:ValidLabeling Table.sem (EdgeAugmenting.labeling input.body input.labels)hM:EdgeInstance.EvenConstraints Table.sem input.bodym:Forest.Meeting input.bodyhr:(run input).bind (decode input.body) = some (Forest.Result.augment m)⊢ Walk.IsAugmenting Table.sem (EdgeAugmenting.labeling input.body input.labels) m.walk
  have hs := run_spec input hw hF hf hMinput:Inputhw:input.labels.length = input.body.incidenceList.lengthhF:input.body.EdgeInstancehf:ValidLabeling Table.sem (EdgeAugmenting.labeling input.body input.labels)hM:EdgeInstance.EvenConstraints Table.sem input.bodym:Forest.Meeting input.bodyhr:(run input).bind (decode input.body) = some (Forest.Result.augment m)hs:have f := EdgeAugmenting.labeling input.body input.labels;
match (run input).bind (decode input.body) with
| none => False
| some (Forest.Result.exhausted log) => IsOptimalLabeling Table.sem f
| some (Forest.Result.augment m) =>
  Walk.IsAugmenting Table.sem f m.walk ∧
    ValidLabeling Table.sem (m.walk.flip f) ∧ (defects (m.walk.flip f)).card + 2 = (defects f).card
| some (Forest.Result.blossom m) =>
  ∃ b,
    m.blossomData = some b ∧
      Walk.IsBlossom Table.sem (b.prepare.flip f) b.cycle ∧
        ValidLabeling Table.sem (b.prepare.flip f) ∧ (defects (b.prepare.flip f)).card = (defects f).card⊢ Walk.IsAugmenting Table.sem (EdgeAugmenting.labeling input.body input.labels) m.walk
  rw [hrinput:Inputhw:input.labels.length = input.body.incidenceList.lengthhF:input.body.EdgeInstancehf:ValidLabeling Table.sem (EdgeAugmenting.labeling input.body input.labels)hM:EdgeInstance.EvenConstraints Table.sem input.bodym:Forest.Meeting input.bodyhr:(run input).bind (decode input.body) = some (Forest.Result.augment m)hs:have f := EdgeAugmenting.labeling input.body input.labels;
match some (Forest.Result.augment m) with
| none => False
| some (Forest.Result.exhausted log) => IsOptimalLabeling Table.sem f
| some (Forest.Result.augment m) =>
  Walk.IsAugmenting Table.sem f m.walk ∧
    ValidLabeling Table.sem (m.walk.flip f) ∧ (defects (m.walk.flip f)).card + 2 = (defects f).card
| some (Forest.Result.blossom m) =>
  ∃ b,
    m.blossomData = some b ∧
      Walk.IsBlossom Table.sem (b.prepare.flip f) b.cycle ∧
        ValidLabeling Table.sem (b.prepare.flip f) ∧ (defects (b.prepare.flip f)).card = (defects f).card⊢ Walk.IsAugmenting Table.sem (EdgeAugmenting.labeling input.body input.labels) m.walk] at hsinput:Inputhw:input.labels.length = input.body.incidenceList.lengthhF:input.body.EdgeInstancehf:ValidLabeling Table.sem (EdgeAugmenting.labeling input.body input.labels)hM:EdgeInstance.EvenConstraints Table.sem input.bodym:Forest.Meeting input.bodyhr:(run input).bind (decode input.body) = some (Forest.Result.augment m)hs:have f := EdgeAugmenting.labeling input.body input.labels;
match some (Forest.Result.augment m) with
| none => False
| some (Forest.Result.exhausted log) => IsOptimalLabeling Table.sem f
| some (Forest.Result.augment m) =>
  Walk.IsAugmenting Table.sem f m.walk ∧
    ValidLabeling Table.sem (m.walk.flip f) ∧ (defects (m.walk.flip f)).card + 2 = (defects f).card
| some (Forest.Result.blossom m) =>
  ∃ b,
    m.blossomData = some b ∧
      Walk.IsBlossom Table.sem (b.prepare.flip f) b.cycle ∧
        ValidLabeling Table.sem (b.prepare.flip f) ∧ (defects (b.prepare.flip f)).card = (defects f).card⊢ Walk.IsAugmenting Table.sem (EdgeAugmenting.labeling input.body input.labels) m.walk
  exact hs.1All goals completed! 🐙

The same specification supplies optimality for exhaustion and valid count-preserving preparation for a blossom. This is a native fresh-search routine, without an improving comparison input. The existing augmentation API is preserved through the shared buffer module. CslibFrontierTests/EdgeCSPForestNative.lean checks actual executions, including an end-to-end valid augmentation to zero defects. The next entries supply whole-blossom contraction/lifting and the complete native edge solver. Geometric recognition and the full planar dichotomy remain open.