Ordered scope and port accounting for whole-instance contraction

The actual index projection equals deletion of all internal variables in scope order. The fresh connector is appended once per touched original constraint.

theorem Cslib.Logic.PL.CSP.Blossom.outsideScope_eq_filter (vs scope : List ℕ) : List.map (fun (j : ℕ) => scope.getD j 0) (Table.outsidePositions scope.length (positions vs scope)) = List.filter (fun (v : ℕ) => !vs.contains v) scope

The outside index projection is precisely the original scope with internal names deleted.

theorem Cslib.Logic.PL.CSP.Blossom.filter_eq_self_of_positions_empty {vs scope : List ℕ} (hp : positions vs scope = []) : List.filter (fun (v : ℕ) => !vs.contains v) scope = scope

No selected coordinate means that deletion leaves the whole ordered scope unchanged.

theorem Cslib.Logic.PL.CSP.Blossom.scope_ne_nil_of_positions_ne_nil {vs scope : List ℕ} (hp : positions vs scope ≠ []) : scope ≠ []

A touched original scope is nonempty, even before imposing the two-port blossom condition.

theorem Cslib.Logic.PL.CSP.Blossom.scope_constraint {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) : (constraint f vs i).2 = List.filter (fun (v : ℕ) => !vs.contains v) F[↑i].2 ++ if (positions vs F[↑i].2).isEmpty = true then [] else [connector F i]

The scope at an old constraint deletes all internal variables and appends its own fresh connector exactly when touched. Outside order and original constraint multiplicity are retained.

theorem Cslib.Logic.PL.CSP.Blossom.positive_constraint {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (i : Fin (List.length F)) : (!(constraint f vs i).2.isEmpty) = !F[↑i].2.isEmpty

Positivity at every retained old constraint is unchanged by actual contraction.

theorem Cslib.Logic.PL.CSP.Blossom.positiveCount_contract {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (hne : touched F vs ≠ []) : (contract f vs).positiveCount = F.positiveCount + 1

Adding the central nonempty exactly-one scope increases the positive count by exactly one. Nullary original constraints are preserved and are not charged to this measure.

theorem Cslib.Logic.PL.CSP.Blossom.mem_touched {F : CSP Table ℕ} (vs : List ℕ) (i : Fin (List.length F)) : i ∈ touched F vs ↔ positions vs F[↑i].2 ≠ []

Touching is determined by the gathered ports, not by the number of cycle visits.

theorem Cslib.Logic.PL.CSP.Blossom.touched_ne_nil {F : CSP Table ℕ} (w : F.Walk) (hne : w.steps ≠ []) : touched F (internal w) ≠ []

Any nonempty incidence sequence touches an actual original constraint.

theorem Cslib.Logic.PL.CSP.Blossom.vars_contract {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : (contract f vs).vars.toFinset = F.vars.toFinset \ vs.toFinset ∪ (connectors F vs).toFinset

The actual output variable set consists of surviving old names and the fresh connectors.

theorem Cslib.Logic.PL.CSP.Blossom.numVars_contract {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : (contract f vs).numVars = (F.vars.toFinset \ vs.toFinset).card + (touched F vs).length

Freshness makes the output variable count an exact deletion-plus-connectors formula.

theorem Cslib.Logic.PL.CSP.Blossom.numVars_contract_add {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (hv : vs.toFinset ⊆ F.vars.toFinset) : (contract f vs).numVars + vs.toFinset.card = F.numVars + (touched F vs).length

Exact finite accounting when all deleted variables actually occurred in the old instance.

theorem Cslib.Logic.PL.CSP.Blossom.flatMap_connectors (F : CSP Table ℕ) (vs : List ℕ) : List.flatMap (fun (i : Fin (List.length F)) => if (positions vs F[↑i].2).isEmpty = true then [] else [connector F i]) (List.finRange (List.length F)) = connectors F vs

Collecting the new port of each touched constraint gives precisely the central scope.

theorem Cslib.Logic.PL.CSP.Blossom.vars_contract_perm {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : (contract f vs).vars.Perm (List.filter (fun (v : ℕ) => !vs.contains v) F.vars ++ connectors F vs ++ connectors F vs)

Occurrence multiplicities are exactly old outside occurrences plus two copies of the connector scope. This permutation does not reorder the constructed CSP itself.

theorem Cslib.Logic.PL.CSP.Blossom.count_vars_contract {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) (v : ℕ) : List.count v (contract f vs).vars = (if v ∈ vs then 0 else List.count v F.vars) + 2 * List.count v (connectors F vs)

Each output name retains its two old outside occurrences, or is a fresh connector with one old-constraint port and one central port. No enumeration below a binary name is involved.

theorem Cslib.Logic.PL.CSP.Blossom.edge_contract {F : CSP Table ℕ} (hF : F.EdgeInstance) (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : (contract f vs).EdgeInstance

Actual contraction preserves the edge-instance model at arbitrary finite table arities.