Counted criterion for edge instances

A duplicate-free scope and exactly two global occurrences per occurring variable imply the existing positional EdgeInstance condition. Constraint records may repeat: constraint indices, rather than record equality, distinguish their two endpoints.

theorem Cslib.Logic.PL.CSP.Occurrence.eq_of_scope_nodup {Rel V : Type} {F : CSP Rel V} (hscope : ∀ c ∈ F, c.2.Nodup) {o p : F.Occurrence} (hi : o.fst = p.fst) (hv : o.var = p.var) : o = p

A duplicate-free scope identifies an occurrence from its constraint and variable.

theorem Cslib.Logic.PL.CSP.edgeInstance_of_count_eq_two {Rel V : Type} [DecidableEq V] {F : CSP Rel V} (hscope : ∀ c ∈ F, c.2.Nodup) (hcount : ∀ v ∈ F.vars, List.count v F.vars = 2) : F.EdgeInstance

Two total occurrences, with no repetition inside a scope, are exactly an edge's endpoints. Only the actual variable list is counted; no finite universe or maximum name is required.