Correctness of native fresh forest search

The native certificate and exact representation bridge compose with the three mathematical fresh-search outcomes. Semantic correctness requires an edge instance, a valid initial labeling and even delta-matroid constraints; the runtime certificate and width-only agreement do not. This routine stops at its first event and does not implement contraction or recursive solving.

theorem Cslib.Complexity.CSP.EdgeForest.run_spec (input : Input) (hw : input.labels.length = input.body.incidenceList.length) (hF : input.body.EdgeInstance) (hf : Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem (EdgeAugmenting.labeling input.body input.labels)) (hM : Logic.PL.CSP.EdgeInstance.EvenConstraints Logic.PL.CSP.Table.sem input.body) : have f := EdgeAugmenting.labeling input.body input.labels; match (run input).bind (decode input.body) with | none => False | some (Logic.PL.CSP.Forest.Result.exhausted log) => Logic.PL.CSP.IsOptimalLabeling Logic.PL.CSP.Table.sem f | some (Logic.PL.CSP.Forest.Result.augment m) => Logic.PL.CSP.Walk.IsAugmenting Logic.PL.CSP.Table.sem f m.walk ∧ Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem (m.walk.flip f) ∧ (Logic.PL.CSP.defects (m.walk.flip f)).card + 2 = (Logic.PL.CSP.defects f).card | some (Logic.PL.CSP.Forest.Result.blossom m) => ∃ (b : Logic.PL.CSP.Forest.BlossomData input.body), m.blossomData = some b ∧ Logic.PL.CSP.Walk.IsBlossom Logic.PL.CSP.Table.sem (b.prepare.flip f) b.cycle ∧ Logic.PL.CSP.ValidLabeling Logic.PL.CSP.Table.sem (b.prepare.flip f) ∧ (Logic.PL.CSP.defects (b.prepare.flip f)).card = (Logic.PL.CSP.defects f).card

A decoded native result has the corresponding fresh-search guarantee. Exhaustion means optimality, augmentation removes two defects, and a blossom has valid count-preserving preparation. The semantic hypotheses are additional to the exact-width representation guard.