Internal ports of a closed edge-instance trail

Both occurrences of every blossom variable are used by the trail. Consequently the whole-instance constructor gathers exactly the used ports, and every touched original constraint supplies at least two internal coordinates, even when its copied node is visited repeatedly. The proof using a constant labeling and the exact trail defect equation is an original bookkeeping argument, independent of the delta-matroid axioms.

theorem Cslib.Logic.PL.CSP.Blossom.partner_mem_edges {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) (hw : w.IsWalk) (hc : w.finish = w.start) {o : F.Occurrence} (ho : o ∈ w.edges) : hF.partner o ∈ w.edges

A closed incidence trail uses both ports of each variable it visits.

theorem Cslib.Logic.PL.CSP.Blossom.var_mem_internal_iff {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) (hw : w.IsWalk) (hc : w.finish = w.start) (o : F.Occurrence) : o.var ∈ internal w ↔ o ∈ w.edges

For a closed edge-instance trail, gathering by variable name includes exactly the used original occurrences; it cannot accidentally include an unused port at a repeated constraint.

theorem Cslib.Logic.PL.CSP.Blossom.mem_positions {F : CSP Table ℕ} (vs : List ℕ) (i : Fin (List.length F)) (j : Fin F[↑i].2.length) : ↑j ∈ positions vs F[↑i].2 ↔ Occurrence.var ⟨i, j⟩ ∈ vs

Membership in a selected position list is precisely occurrence-variable membership.

theorem Cslib.Logic.PL.CSP.Blossom.touched_has_step {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) (hw : w.IsWalk) (hc : w.finish = w.start) {i : Fin (List.length F)} (hi : i ∈ touched F (internal w)) : ∃ s ∈ w.steps, match s with | (input, snd) => input.fst = i

Each touched constraint contains a whole cycle step, not a single dangling blossom port.

theorem Cslib.Logic.PL.CSP.Blossom.two_le_positions {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) (hw : w.IsWalk) (hc : w.finish = w.start) {i : Fin (List.length F)} (hi : i ∈ touched F (internal w)) : 2 ≤ (positions (internal w) F[↑i].2).length

At least two distinct internal positions are gathered at every touched original constraint. Repeated visits can increase this number; they never create duplicate connectors.

theorem Cslib.Logic.PL.CSP.Blossom.defects_inter_internal {F : CSP Table ℕ} {w : F.Walk} {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) : defects f ∩ (internal w).toFinset = {w.start}

A genuine prepared blossom has exactly one internal defective variable: its base.