Exact incidence counts of the positive drawing compiler

Positions and routes are counted on the emitted lists. In particular, source placeholders are absent from the actual vertex list, and splicing never introduces an additional graph edge.

Main results

• positiveDrawing_vertexCount: the exact actual incidence-graph vertex count.
• positiveDrawing_edgeCount: one actual route for each actual output literal occurrence.

References

The finite-profile counting and incidence-indexing proofs are original.

theorem Cslib.Complexity.SAT.ExactOne.clauseGeometry_incidence_count (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) (j : Fin 22) : (List.filter (fun (e : LocalIncidence) => e.clauseIndex == ↑j) (clauseGeometry φ d i c).incidenceRoutes).length = List.length (List.getD (profileFormula (clauseProfile c)) ↑j [])

Collars and source-boundary extensions preserve every local incidence's clause index.

theorem Cslib.Complexity.SAT.ExactOne.positiveClauseBlock_route_count (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) (i : ℕ) (c : Logic.PL.Clause ℕ) {pc : PositivePlacedClause} (hpc : pc ∈ positiveClauseBlock φ d i c) : pc.routes.length = List.length pc.clause

Every placed actual clause has exactly one route per literal position.

theorem Cslib.Complexity.SAT.ExactOne.positivePlacedClauses_route_count (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) {pc : PositivePlacedClause} (hpc : pc ∈ positivePlacedClauses φ d) : pc.routes.length = List.length pc.clause

Every actual emitted clause has exactly one actual incidence route per literal.

theorem Cslib.Complexity.SAT.ExactOne.positiveDrawing_vertexCount (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : (positiveDrawing φ d).1.length = (incidenceGraph (Logic.PL.CNF.PositiveExactOneCompile.formula φ)).vertices.length

The actual output drawing has exactly one position per actual output graph vertex.

theorem Cslib.Complexity.SAT.ExactOne.positiveDrawing_edgeCount (φ : Logic.PL.CNF ℕ) (d : Graph.OrthogonalDrawing) : (positiveDrawing φ d).2.length = (incidenceGraph (Logic.PL.CNF.PositiveExactOneCompile.formula φ)).edges.length

Splicing preserves one route per actual literal occurrence, in the emitted finite lists.