Finite size accounting for edge CSPs

Every edge variable has two positional occurrences. Positive-scope constraints are therefore bounded by twice the number of occurring variables. Nullary constraints are retained in the instance but excluded from this count, as required for the recursion argument in Corollary 27 of [KKR18], arXiv:1602.03124v6, printed p. 13.

def Cslib.Logic.PL.CSP.positiveCount {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : ℕ

Constraints with positive scope, retaining positional multiplicity.

theorem Cslib.Logic.PL.CSP.card_occurrence {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : Fintype.card F.Occurrence = F.vars.length

The number of positions is the cardinality of the original dependent occurrence type.

theorem Cslib.Logic.PL.CSP.card_occurrences_var {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) (v : V) : {o : F.Occurrence | o.var = v}.card = List.count v F.vars

Counting a variable in the occurrence list counts its actual positional fiber.

theorem Cslib.Logic.PL.CSP.EdgeInstance.card_occurrences_var {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {F : CSP Rel V} (hF : F.EdgeInstance) (v : V) (hv : v ∈ F.vars.toFinset) : {o : F.Occurrence | o.var = v}.card = 2

The two endpoints are exactly the finite fiber over an occurring edge variable.

theorem Cslib.Logic.PL.CSP.EdgeInstance.count_vars {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {F : CSP Rel V} (hF : F.EdgeInstance) {v : V} (hv : v ∈ F.vars) : List.count v F.vars = 2

Every occurring edge variable appears exactly twice in the original occurrence list.

theorem Cslib.Logic.PL.CSP.EdgeInstance.scope_nodup {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (hF : F.EdgeInstance) (i : Fin (List.length F)) : F[↑i].2.Nodup

Every actual scope of an edge instance has distinct variable names.

theorem Cslib.Logic.PL.CSP.edgeInstance_of_count_vars {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {F : CSP Rel V} (hs : ∀ (i : Fin (List.length F)), F[↑i].2.Nodup) (hc : ∀ v ∈ F.vars, List.count v F.vars = 2) : F.EdgeInstance

Distinct scope names and exactly two occurrences characterize an edge instance. The count ranges over the actual finite occurrence list, not a declared variable universe.

theorem Cslib.Logic.PL.CSP.EdgeInstance.length_vars_eq_two_mul_numVars {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {F : CSP Rel V} (hF : F.EdgeInstance) : F.vars.length = 2 * F.numVars

Exactly two occurrences per occurring variable, without a finite ambient universe.

theorem Cslib.Logic.PL.CSP.positiveCount_le_length_vars {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : F.positiveCount ≤ F.vars.length

Every positive-scope constraint spends at least one actual positional occurrence.

theorem Cslib.Logic.PL.CSP.EdgeInstance.positiveCount_le {Rel : Type u_1} {V : Type u_2} [DecidableEq V] {F : CSP Rel V} (hF : F.EdgeInstance) : F.positiveCount ≤ 2 * F.numVars

The positive constraint count is bounded even when nullary constraints are present.

def Cslib.Logic.PL.CSP.contractionMeasure {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (F : CSP Rel V) : ℕ

The finite recursion resource counts occurring variables and positive-scope constraints.