Exact graph edge incidences

Every normalized graph edge occurs once at each of its two distinct declared endpoints. The resulting positional CSP satisfies the existing edge-instance condition without any canonicality assumption on the raw graph.

theorem Cslib.Complexity.Graph.count_vars_perfectMatchingInstance_eq_two (G : Graph) {x : ℕ} (hx : x < G.edgeList.length) : List.count x G.perfectMatchingInstance.vars = 2

Every actual edge position occurs exactly twice in the perfect-matching instance.

theorem Cslib.Complexity.Graph.edgeInstance_perfectMatchingInstance (G : Graph) : G.perfectMatchingInstance.EdgeInstance

The generated perfect-matching instance is an actual positional edge instance.