Concrete size decrease of whole-instance blossom contraction

For b distinct blossom variables and r distinct touched original constraints, the constructor has old.numVars - b + r occurring variables and one additional positive-scope constraint. Every touched constraint has at least two internal positions, so r ≤ b. The natural resource 2 * numVars - positiveCount strictly decreases even when r = b. Nullary constraints are preserved but do not contribute to the positive count.

This is the finite accounting behind Observation 26 and Corollary 27 of [KKR18], arXiv:1602.03124v6, printed p. 13. No native time bound is claimed.

theorem Cslib.Logic.PL.CSP.Blossom.length_positions (vs scope : List ℕ) : (positions vs scope).length = (List.filter (fun (v : ℕ) => vs.contains v) scope).length

Gathering positions counts actual internal occurrences in the original scope.

theorem Cslib.Logic.PL.CSP.Blossom.internal_subset_vars {F : CSP Table ℕ} (w : F.Walk) : (internal w).toFinset ⊆ F.vars.toFinset

Every deleted name in the actual trail was an occurring original variable.

theorem Cslib.Logic.PL.CSP.Blossom.sum_length_positions {F : CSP Table ℕ} (vs : List ℕ) : ∑ i : Fin (List.length F), (positions vs F[↑i].2).length = (List.filter (fun (v : ℕ) => vs.contains v) F.vars).length

Summed internal position counts are funded by the original finite occurrence list.

theorem Cslib.Logic.PL.CSP.Blossom.length_internal_occurrences {F : CSP Table ℕ} (hF : F.EdgeInstance) (vs : List ℕ) (hv : vs.toFinset ⊆ F.vars.toFinset) : (List.filter (fun (v : ℕ) => vs.contains v) F.vars).length = 2 * vs.toFinset.card

An edge instance spends precisely two old ports per selected occurring variable.

theorem Cslib.Logic.PL.CSP.Blossom.length_touched_le_internal {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) (hw : w.IsWalk) (hc : w.finish = w.start) : (touched F (internal w)).length ≤ (internal w).toFinset.card

Two internal ports at every touched original constraint imply r ≤ b, even when copied nodes of a repeated original constraint occur several times in the blossom.

theorem Cslib.Logic.PL.CSP.Blossom.numVars_contract_le {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) (hw : w.IsWalk) (hc : w.finish = w.start) (f : F.OccurrenceLabeling Bool) : (contract f (internal w)).numVars ≤ F.numVars

The exact constructor cannot increase the number of occurring variables.

theorem Cslib.Logic.PL.CSP.Blossom.contractionMeasure_contract_lt {F : CSP Table ℕ} {w : F.Walk} (hF : F.EdgeInstance) {f : F.OccurrenceLabeling Bool} (hb : Walk.IsBlossom Table.sem f w) : (contract f (internal w)).contractionMeasure < F.contractionMeasure

The actual finite contraction strictly decreases the recursion resource, including the case where the variable count is unchanged. Every hypothesis comes from the actual blossom.

theorem Cslib.Logic.PL.CSP.Blossom.totalRows_contract_le {F : CSP Table ℕ} (f : F.OccurrenceLabeling Bool) (vs : List ℕ) : (List.map (fun (c : Constraint Table ℕ) => c.1.rows.length) (contract f vs)).sum ≤ (List.map (fun (c : Constraint Table ℕ) => c.1.rows.length) F).sum + (touched F vs).length

The actual number of stored table rows grows by at most r. The central table has r rows of width r; thus its new Boolean row data is quadratic in r, not linear in r. Every old table retains at most its original number of rows, with original outside order.