Exact black-side occurrence accounting

Black scopes partition original argument positions once, retaining the original constraint positions and cyclic argument order. No source well-formedness premise is needed for this fact.

theorem Cslib.Complexity.CSP.CyclicCompiler.mem_vars_blackConstraints {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (F : Logic.PL.CSP Rel ℕ) (v : ℕ) : v ∈ (blackConstraints arity sem F).vars ↔ v < F.occurrences.length

Every original edge position occurs on the black side and no other name is introduced.

theorem Cslib.Complexity.CSP.CyclicCompiler.blackConstraints_scopes_nodup {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (F : Logic.PL.CSP Rel ℕ) (constraint : Logic.PL.Constraint Logic.PL.CSP.Table ℕ) (hc : constraint ∈ blackConstraints arity sem F) : constraint.2.Nodup

Each actual black constraint has a duplicate-free scope.

theorem Cslib.Complexity.CSP.CyclicCompiler.nodup_vars_blackConstraints {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (F : Logic.PL.CSP Rel ℕ) : (blackConstraints arity sem F).vars.Nodup

Different original constraint positions have disjoint black scopes.

theorem Cslib.Complexity.CSP.CyclicCompiler.count_vars_blackConstraints {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (F : Logic.PL.CSP Rel ℕ) (v : ℕ) : List.count v (blackConstraints arity sem F).vars = if v < F.occurrences.length then 1 else 0

Each old edge position occurs exactly once on the black side, including malformed sources.