refactor(planar-SAT): extract shared path certificates

Complexity.lean

@@ -815,6 +815,11 @@ public import Complexity.Computability.Complexity.Problems.SAT.Planar.OrdinaryRi
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayout
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutChecks
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutData
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathBounds
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathData
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathGeometry
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathPolyTime
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths.Occupancy
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PolyTime

Complexity/Computability/Complexity/Problems/SAT/Planar/Bounds.lean

@@ -7,6 +7,7 @@ Authors: Erik Demaine
 module
 -- upstream: candidate
 
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathBounds
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile
 public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalDrawing
 import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry
@@ -50,12 +51,6 @@ These bounds concern the original finite compiler in `Compile` and its 240-squar
 namespace Cslib.Complexity.SAT.PlanarCompile
 open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal
 
-/-- Horizontal side of the actual tiled drawing, including its last square. -/
-def gridWidth (φ : CNF ℕ) : ℕ := 240 * (8 * (SAT.incidenceGraph φ).1.length + 1)
-/-- Vertical side of the actual tiled drawing, including its last square. -/
-def gridHeight (φ : CNF ℕ) : ℕ :=
-  240 * (8 * (SAT.incidenceGraph φ).1.length + 2 * (SAT.incidenceGraph φ).2.length + 1)
-
 private def CellBound (φ : CNF ℕ) (p : Point) : Prop :=
   0 ≤ p.1 ∧ p.1 ≤ 8 * ((SAT.incidenceGraph φ).1.length : ℤ) ∧
     0 ≤ p.2 ∧ p.2 ≤ 8 * ((SAT.incidenceGraph φ).1.length : ℤ) +
@@ -279,20 +274,6 @@ theorem drawing_fits (φ : CNF ℕ) :
     obtain ⟨pc, hpc, hr⟩ := List.mem_flatMap.mp hr
     exact (placedClauses_bounds φ pc hpc).2.2 r hr p hp
 
-/-- The horizontal grid side is at most 1920 times the source incidence size plus one. -/
-theorem gridWidth_le (φ : CNF ℕ) :
-    gridWidth φ ≤ 1920 * (φ.numVars + φ.length + φ.vars.length + 1) := by
-  unfold gridWidth
-  rw [SAT.length_vertices_incidenceGraph]
-  nlinarith
-
-/-- The vertical grid side is at most 1920 times the source incidence size plus one. -/
-theorem gridHeight_le (φ : CNF ℕ) :
-    gridHeight φ ≤ 1920 * (φ.numVars + φ.length + φ.vars.length + 1) := by
-  unfold gridHeight
-  rw [SAT.length_vertices_incidenceGraph, SAT.length_edges_incidenceGraph]
-  nlinarith
-
 private theorem access_cost (sites : List Point) (p q : Point) :
     wireLength (access sites p q) ≤ 240 ∧
       (access sites p q).consecutivePairs.length ≤ 19 := by

Complexity/Computability/Complexity/Problems/SAT/Planar/Compile.lean

@@ -7,6 +7,8 @@ Authors: Erik Demaine
 module
 -- upstream: candidate
 
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathData
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments
 public import Complexity.Computability.Complexity.Problems.SAT.Incidence
 public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalLayout
 public import Complexity.Foundations.Geometry.Orthogonal.Subdivision
@@ -44,57 +46,9 @@ namespace Cslib.Complexity.SAT.PlanarCompile
 
 open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal
 
-/-- A cell's ordinary signal, or a local variable of its crossover. -/
-abbrev Variable := Point × Option Crossover.SplitVariable
-
 /-- A clause, its position, and one route per literal in literal order. -/
 abbrev PlacedClause := Clause Variable × Point × List Route
 
-/-- The explicit linear per-route expansion budget. -/
-def budget (φ : CNF ℕ) : ℕ :=
-  80 * (SAT.incidenceGraph φ).1.length + 10 * (SAT.incidenceGraph φ).2.length
-
-/-- Unit paths in the order of the original literal occurrences. -/
-def paths (φ : CNF ℕ) : List Route :=
-  let G := SAT.incidenceGraph φ
-  (G.orthogonalRoutes G.canonicalPorts).map (subdivideWithin (budget φ))
-
-/-- The path of a particular original literal occurrence. -/
-def occurrencePath (φ : CNF ℕ) (o : Occurrence ℕ) : Route :=
-  (paths φ).getD ((Cslib.Logic.PL.occurrences φ).idxOf o) []
-
-/-- Actual occupied crossing candidates, excluding every declared graph vertex center.
-First-occurrence selection ensures exactly one local gadget per selected square. -/
-def crossingSites (φ : CNF ℕ) : List Point :=
-  let G := SAT.incidenceGraph φ
-  let occupied := (G.crossingCandidates G.canonicalPorts).filter fun p =>
-    !(G.orthogonalPositions.contains p) &&
-      decide (2 ≤ ((paths φ).filter fun r => r.contains p).length)
-  Cslib.Complexity.selectDistinct occupied (List.replicate occupied.length true)
-
-/-- The selected cells are exactly occupied nonvertex candidates. -/
-theorem mem_crossingSites (φ : CNF ℕ) (p : Point) :
-    p ∈ crossingSites φ ↔
-      p ∈ (SAT.incidenceGraph φ).crossingCandidates (SAT.incidenceGraph φ).canonicalPorts ∧
-        p ∉ (SAT.incidenceGraph φ).orthogonalPositions ∧
-          2 ≤ ((paths φ).filter fun r => r.contains p).length := by
-  simp [crossingSites, mem_selectDistinct_replicate, Bool.and_eq_true]
-
-/-- Every selected square receives exactly one template. -/
-theorem crossingSites_nodup (φ : CNF ℕ) : (crossingSites φ).Nodup := nodup_selectDistinct _ _
-
-/-- Side facing a neighboring square, in left/right/bottom/top order.
-Only unit neighbors are used by the correctness theorem. -/
-def side (p q : Point) : Fin 4 :=
-  if q.1 < p.1 then 0 else if p.1 < q.1 then 1 else if q.2 < p.2 then 2 else 3
-
-/-- The center of a square of side 240 indexed by an integer grid point. -/
-def center (p : Point) : Point := cellOrigin 120 p + (120, 120)
-
-/-- The signal presented by a cell toward a neighboring cell. -/
-def signal (sites : List Point) (p q : Point) : Variable :=
-  (p, if p ∈ sites then some (Crossover.splitTerminal (side p q)) else none)
-
 /-- Geometric position of a structured output variable. -/
 def variablePosition (v : Variable) : Point :=
   cellOrigin 120 v.1 + v.2.elim (120, 120) Crossover.variablePosition
@@ -104,12 +58,6 @@ def access (sites : List Point) (p q : Point) : Route :=
   if p ∈ sites then translate (cellOrigin 120 p) (Crossover.accessRoute (side p q))
   else [cellPort 120 p (side p q), center p]
 
-/-- Every cell before the original clause vertex contributes an entry/exit signal pair.
-At the source endpoint the unused entry defaults to the source's own ordinary signal. -/
-def wire (sites : List Point) (r : Route) : List (Variable × Variable) :=
-  r.dropLast.zipIdx.map fun (p, i) =>
-    (signal sites p (r.getD (i - 1) p), signal sites p (r.getD (i + 1) p))
-
 /-- One implication at the common side midpoint of adjacent occupied cells.
 Positive literals propagate toward the source, negative literals toward the clause. -/
 def link (sites : List Point) (positive : Bool) (p q : Point) : PlacedClause :=