Incidence-order assembly of clause-replacement drawings

The drawing lists follow the actual formula: variables use first-occurrence order, clauses use list order, and routes use literal-occurrence order. This interface bridges local replacement geometry to Graph.IsPlanarOrthogonalDrawing without changing the output incidence graph.

Main definitions

• FormulaDrawing: variable positions, clause positions, and occurrence-indexed routes.
• FormulaDrawing.drawing: the finite lists of the actual incidence drawing.
• FormulaDrawing.Valid: continuous geometric conditions on those data.

Main results

• FormulaDrawing.isPlanarOrthogonalDrawing: the assembled drawing has the actual incidence graph.
• FormulaDrawing.isPlanarOrthogonalDrawing_compact: compact numbering preserves that graph.

References

The finite assembly and its indexing proofs are original.

structure Cslib.Complexity.SAT.ExactOne.FormulaDrawing {V : Type} (φ : Logic.PL.CNF V) : Type

Geometric data indexed by the variables, clauses, and literal positions of a fixed formula.

• variablePoint : V → Orthogonal.Point

  The displayed position of each occurring variable. Values outside the support are ignored.

• clausePoints : List Orthogonal.Point

  Clause positions, in formula-list order.

• incidenceRoute : Logic.PL.Occurrence V → Orthogonal.Route

  A clause-to-variable route for every actual literal occurrence.

def Cslib.Complexity.SAT.ExactOne.FormulaDrawing.positions {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} (a : FormulaDrawing φ) : List Orthogonal.Point

Variable vertices precede clause vertices in the actual incidence graph.

def Cslib.Complexity.SAT.ExactOne.FormulaDrawing.routes {V : Type} {φ : Logic.PL.CNF V} (a : FormulaDrawing φ) : List Orthogonal.Route

Routes retain the actual formula's literal-occurrence order.

def Cslib.Complexity.SAT.ExactOne.FormulaDrawing.drawing {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} (a : FormulaDrawing φ) : Graph.OrthogonalDrawing

Finite drawing data for the actual listed incidence graph.

structure Cslib.Complexity.SAT.ExactOne.FormulaDrawing.Valid {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} (a : FormulaDrawing φ) : Prop

Geometric replacement certificates are stated on actual literal occurrences, including repeated literals and repeated clause records. All intersections concern full real supports.

• clauseCount : a.clausePoints.length = List.length φ

  There is exactly one displayed clause vertex per clause position.

• positionsNodup : a.positions.Nodup

  No distinct formula vertices share their displayed positions.

• endpoints (o : Logic.PL.Occurrence V) : o ∈ Logic.PL.occurrences φ → List.head? (a.incidenceRoute o) = some (a.clausePoints.getD o.1 (0, 0)) ∧ List.getLast? (a.incidenceRoute o) = some (a.variablePoint o.2.2.1)

  Every route has the actual clause and variable endpoints.

• orthogonal (o : Logic.PL.Occurrence V) : o ∈ Logic.PL.occurrences φ → Orthogonal.IsOrthogonal (a.incidenceRoute o)

  Routes are proper and orthogonal.

• simple (o : Logic.PL.Occurrence V) : o ∈ Logic.PL.occurrences φ → Orthogonal.IsSimple (a.incidenceRoute o)

  Routes have no self-crossings or retracing.

• avoidsVariables (o : Logic.PL.Occurrence V) : o ∈ Logic.PL.occurrences φ → ∀ v ∈ φ.vars, Orthogonal.realPoint (a.variablePoint v) ∈ Orthogonal.support (a.incidenceRoute o) → v = o.2.2.1

  Only the incident variable vertex can lie on a route.

• avoidsClauses (o : Logic.PL.Occurrence V) : o ∈ Logic.PL.occurrences φ → ∀ i < List.length φ, Orthogonal.realPoint (a.clausePoints.getD i (0, 0)) ∈ Orthogonal.support (a.incidenceRoute o) → i = o.1

  Only the incident clause vertex can lie on a route.

• contacts (o : Logic.PL.Occurrence V) : o ∈ Logic.PL.occurrences φ → ∀ t ∈ Logic.PL.occurrences φ, o ≠ t → ∀ p ∈ Orthogonal.support (a.incidenceRoute o), p ∈ Orthogonal.support (a.incidenceRoute t) → o.2.2.1 = t.2.2.1 ∧ p = Orthogonal.realPoint (a.variablePoint o.2.2.1) ∨ o.1 = t.1 ∧ p = Orthogonal.realPoint (a.clausePoints.getD o.1 (0, 0))

  Different occurrence routes meet only at their shared actual variable or clause vertex.

theorem Cslib.Complexity.SAT.ExactOne.FormulaDrawing.drawingPosition_variable {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} (a : FormulaDrawing φ) {v : V} (hv : v ∈ φ.vars) : (incidenceGraph φ).drawingPosition a.drawing (List.idxOf v φ.distinctVars) = a.variablePoint v

An occurring variable resolves to its supplied position in the actual graph.

theorem Cslib.Complexity.SAT.ExactOne.FormulaDrawing.drawingPosition_clause {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} (a : FormulaDrawing φ) (_ha : a.Valid) {i : ℕ} (hi : i < List.length φ) : (incidenceGraph φ).drawingPosition a.drawing (φ.distinctVars.length + i) = a.clausePoints.getD i (0, 0)

A clause index resolves to its supplied position in the actual graph.

theorem Cslib.Complexity.SAT.ExactOne.FormulaDrawing.indexed_route {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} (a : FormulaDrawing φ) {i : ℕ} (hi : i < (incidenceGraph φ).2.length) : a.routes.getD i [] = a.incidenceRoute (Logic.PL.occurrences φ)[i]

The occurrence at an edge-list index is the same occurrence used to build its route.

theorem Cslib.Complexity.SAT.ExactOne.FormulaDrawing.isPlanarOrthogonalDrawing {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} (a : FormulaDrawing φ) (ha : a.Valid) : (incidenceGraph φ).IsPlanarOrthogonalDrawing a.drawing

Local occurrence-indexed certificates give a drawing of the actual formula incidence graph.

theorem Cslib.Complexity.SAT.ExactOne.FormulaDrawing.isPlanarOrthogonalDrawing_compact {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} (a : FormulaDrawing φ) (ha : a.Valid) : (incidenceGraph φ.compact).IsPlanarOrthogonalDrawing a.drawing

The same actual drawing certifies compact output labels, with no change in any graph record.