Restoring surviving original incidences

Finite lookup in the actual original port list inverts whole-instance contraction away from fresh connectors. The walk map retains original constraint positions and binary variable names. The fallback is used only to make lookup total; the proved domain never reaches it.

theorem Cslib.Logic.PL.CSP.Blossom.exists_oldPort {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (o : (contract f vs).Occurrence) (ho : o.var ∉ connectors F vs) : ∃ (p : F.Occurrence) (hp : p.var ∉ vs), oldPort f vs p hp = o

Every nonconnector port of the actual contracted edge instance is a surviving old port.

theorem Cslib.Logic.PL.CSP.Blossom.exists_connectorPort {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (o : (contract f vs).Occurrence) (ho : o.var ∈ connectors F vs) (hindex : ↑o.fst < List.length F) : ∃ (i : Fin (List.length F)) (hi : i ∈ touched F vs), connectorPort f vs i hi = o

A connector port at an old constraint is exactly that constraint's terminal fresh port. The central alternative is excluded by its appended constraint index.

def Cslib.Logic.PL.CSP.Blossom.restorePort {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (o : (contract f vs).Occurrence) : Option F.Occurrence

Find an original outside port by scanning actual original incidences.

theorem Cslib.Logic.PL.CSP.Blossom.restorePort_spec {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (o : (contract f vs).Occurrence) (ho : o.var ∉ connectors F vs) : ∃ (p : F.Occurrence), restorePort f vs o = some p ∧ ∃ (hp : p.var ∉ vs), oldPort f vs p hp = o

Nonconnector lookup returns an actual surviving port with exactly the requested image.

def Cslib.Logic.PL.CSP.Blossom.restorePortOr {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback : F.Occurrence) (o : (contract f vs).Occurrence) : F.Occurrence

Total original-port lookup, with an explicit actual fallback for malformed requests.

theorem Cslib.Logic.PL.CSP.Blossom.restorePortOr_spec {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback : F.Occurrence) (o : (contract f vs).Occurrence) (ho : o.var ∉ connectors F vs) : ∃ (hp : (restorePortOr f vs fallback o).var ∉ vs), oldPort f vs (restorePortOr f vs fallback o) hp = o

On the certified domain the fallback is irrelevant and lookup is the actual inverse.

theorem Cslib.Logic.PL.CSP.Blossom.restorePortOr_var {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback : F.Occurrence) (o : (contract f vs).Occurrence) (ho : o.var ∉ connectors F vs) : (restorePortOr f vs fallback o).var = o.var

Successful restoration retains the original binary variable name.

theorem Cslib.Logic.PL.CSP.Blossom.restorePortOr_constraint {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback : F.Occurrence) (o : (contract f vs).Occurrence) (ho : o.var ∉ connectors F vs) : ↑(restorePortOr f vs fallback o).fst = ↑o.fst

Successful restoration retains the actual original constraint position.

theorem Cslib.Logic.PL.CSP.Blossom.oldPort_injective {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) {o p : F.Occurrence} (ho : o.var ∉ vs) (hp : p.var ∉ vs) (he : oldPort f vs o ho = oldPort f vs p hp) : o = p

Surviving original ports are embedded injectively in the actual output occurrence type.

theorem Cslib.Logic.PL.CSP.Blossom.restorePortOr_oldPort {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback o : F.Occurrence) (ho : o.var ∉ vs) : restorePortOr f vs fallback (oldPort f vs o ho) = o

Restoring an actual outside original port cancels the positional embedding.

def Cslib.Logic.PL.CSP.Blossom.restoreWalk {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback : F.Occurrence) (p : (contract f vs).Walk) : F.Walk

Restore each actual port of a contracted walk by the finite original-port lookup.

theorem Cslib.Logic.PL.CSP.Blossom.restoreWalk_spec {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback : F.Occurrence) {p : (contract f vs).Walk} (hp : p.IsWalk) (hno : ∀ o ∈ p.edges, o.var ∉ connectors F vs) : (restoreWalk f vs fallback p).IsWalk ∧ (restoreWalk f vs fallback p).finish = p.finish ∧ ∀ o ∈ (restoreWalk f vs fallback p).edges, o.var ∉ vs

A contracted trail avoiding connectors restores to an actual outside original trail with the same variable endpoints. Repeated original constraints remain positional.

theorem Cslib.Logic.PL.CSP.Blossom.mem_restoreWalk_edges {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback : F.Occurrence) (p : (contract f vs).Walk) (hno : ∀ o ∈ p.edges, o.var ∉ connectors F vs) (o : F.Occurrence) (ho : o.var ∉ vs) : o ∈ (restoreWalk f vs fallback p).edges ↔ oldPort f vs o ho ∈ p.edges

Membership in a restored outside trail is the exact inverse of surviving-port transport.

theorem Cslib.Logic.PL.CSP.Blossom.restoreWalk_flip {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (fallback : F.Occurrence) (p : (contract f vs).Walk) (hno : ∀ o ∈ p.edges, o.var ∉ connectors F vs) : (restoreWalk f vs fallback p).flip f = expandZero f vs (p.flip (reference f vs))

Flipping a restored outside walk is exactly zero-expansion of the actual contracted flip.

theorem Cslib.Logic.PL.CSP.Blossom.flip_reference_connectors {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (p : (contract f vs).Walk) (hno : ∀ o ∈ p.edges, o.var ∉ connectors F vs) : (∀ (i : Fin (List.length F)) (hi : i ∈ touched F vs), p.flip (reference f vs) (connectorPort f vs i hi) = false) ∧ ∀ (k : Fin (connectors F vs).length), p.flip (reference f vs) (centralPort f vs k) = (BitString.listSingle (connectors F vs).length 0).getD (↑k) false

Avoiding connector variables leaves both endpoint values of every fresh connector at the actual reference values, including the honest central one-hot row.

theorem Cslib.Logic.PL.CSP.Blossom.restoreWalk_isFPrefix {F : CSP Table ℕ} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (vs : List ℕ) (fallback : F.Occurrence) {p : (contract f vs).Walk} (hp : Walk.IsFPrefix Table.sem (reference f vs) p) (hno : ∀ o ∈ p.edges, o.var ∉ connectors F vs) : Walk.IsFPrefix Table.sem f (restoreWalk f vs fallback p)

Every connector-free contracted f-prefix restores to an original f-prefix. Each actual intermediate row is reflected through connector zero, so arbitrary outside changes are allowed.

theorem Cslib.Logic.PL.CSP.Blossom.restoreWalk_isFWalk {F : CSP Table ℕ} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling Table.sem f) (vs : List ℕ) (fallback : F.Occurrence) {p : (contract f vs).Walk} (hp : Walk.IsFWalk Table.sem (reference f vs) p) (hno : ∀ o ∈ p.edges, o.var ∉ connectors F vs) : Walk.IsFWalk Table.sem f (restoreWalk f vs fallback p)

Distinct endpoints are retained when restoring a contracted f-walk avoiding connectors.

theorem Cslib.Logic.PL.CSP.Blossom.restore_augmentation {F : CSP Table ℕ} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} {w : F.Walk} (hb : Walk.IsBlossom Table.sem f w) (hf : ValidLabeling Table.sem f) (fallback : F.Occurrence) {p : (contract f (internal w)).Walk} (hp : Walk.IsAugmenting Table.sem (reference f (internal w)) p) (hno : ∀ o ∈ p.edges, o.var ∉ connectors F (internal w)) : ValidLabeling Table.sem ((restoreWalk f (internal w) fallback p).flip f) ∧ (defects ((restoreWalk f (internal w) fallback p).flip f)).card + 2 = (defects f).card

The connector-free case of Lemma 44 returns the actual restored finite walk flip and removes exactly two original defects, with no condition on changed outside comparison values.