refactor(planar-SAT): share orthogonal route decidability

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

@@ -94,9 +94,6 @@ def commonEndpoints (e f : ℕ × SplitVariable × Route) : List Point :=
 def consecutiveContact (a b : Point × Point) : List Point :=
   if a.2 = b.1 then [a.2] else if b.2 = a.1 then [a.1] else []
 
-private instance (r : Route) : Decidable (IsOrthogonal r) :=
-  inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2))
-
 private def LocalSpec (e : ℕ × SplitVariable × Route) : Prop :=
   (e.1 < 74 ∧ e.2.2.head? = some (clausePosition e.1) ∧
     e.2.2.getLast? = some (variablePosition e.2.1)) ∧

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

@@ -114,9 +114,6 @@ theorem formula_sizes : formula.length = 8 ∧ ∀ c ∈ formula, c.length = 2 :
 /-- Every variable is actually used, including variables with no external access in a client. -/
 theorem variables_used : ∀ v : Variable, v ∈ formula.vars := by decide +kernel
 
-private instance (r : Route) : Decidable (IsOrthogonal r) :=
-  inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2))
-
 /-- All literal incidences occur exactly once, in formula order. -/
 theorem incidenceRoutes_cover :
     incidenceRoutes.map (fun e => (e.1, e.2.1)) =

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

@@ -90,9 +90,6 @@ def commonEndpoints (e f : ℕ × Variable × Route) : List Point :=
 def consecutiveContact (a b : Point × Point) : List Point :=
   if a.2 = b.1 then [a.2] else if b.2 = a.1 then [a.1] else []
 
-private instance (r : Route) : Decidable (IsOrthogonal r) :=
-  inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2))
-
 private def LocalSpec (e : ℕ × Variable × Route) : Prop :=
   (e.1 < 78 ∧ e.2.2.head? = some (clausePosition e.1) ∧
     e.2.2.getLast? = some (variablePosition e.2.1)) ∧

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

@@ -32,7 +32,6 @@ All geometric assertions concern entire real supports.
 
 ## Main results
 
-* `boundary_eq_cases`: matching boundaries identify opposite adjacent sides and the lane.
 * `access_eq_translate`: every actual access uses the common fixed paired-port interface.
 * `route_contacts`, `routes_contacts`: continuous endpoint-only contacts of the actual routes.
 * `isPlanarOrthogonalDrawing`: the actual compact formula's continuous drawing certificate.
@@ -48,12 +47,6 @@ namespace Cslib.Complexity.SAT.ParsimoniousPlanar
 
 open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal
 
-/-- Equal paired boundary points in different cells identify both the side and the lane. -/
-theorem boundary_eq_cases {c d : Point} {s t : Fin 4} {l k : Fin 2}
-    (hcd : c ≠ d) (h : boundary c s l = boundary d t k) :
-    l = k ∧ d = c + PairedPorts.neighbor s ∧ t = PairedPorts.oppositeSide s :=
-  PairedPorts.boundary_eq_cases hcd h
-
 /-- Within one cell, boundary positions identify both the side and the lane. -/
 theorem boundary_injective (c : Point) :
     Function.Injective (fun p : PairedPorts.Port => boundary c p.1 p.2) := by
@@ -248,9 +241,6 @@ theorem clause_cell_not_ordinary {φ : CNF ℕ} {i : ℕ} (hi : i < φ.length) :
   obtain ⟨o, ho, rfl⟩ := List.mem_map.mp hr
   exact PlanarCompile.clause_cell_not_mem_path_dropLast ho hi hp
 
-private instance (r : Route) : Decidable (IsOrthogonal r) :=
-  inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2))
-
 private def finalLocalRoute (s : Fin 4) : Route :=
   [(120, 120), PairedPorts.spokeElbow s, PairedPorts.boundaryPort s (PairedPorts.spokeLane s),
     cellOrigin 120 (PairedPorts.neighbor s) +

Complexity/Foundations/Geometry/Orthogonal.lean

@@ -81,6 +81,10 @@ instance (a b : Point) : Decidable (AxisAligned a b) := inferInstanceAs (Decidab
 /-- Every consecutive segment is proper and axis aligned. -/
 def IsOrthogonal (r : Route) : Prop := ∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2
 
+/-- Orthogonality is decidable by checking the finitely many consecutive segments. -/
+instance : DecidablePred IsOrthogonal :=
+  fun r => inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2))
+
 /-- Removing the initial listed point preserves proper orthogonality. -/
 theorem IsOrthogonal.of_cons {a : Point} {r : Route} (h : IsOrthogonal (a :: r)) :
     IsOrthogonal r := by

Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean

@@ -94,9 +94,6 @@ theorem variable_bounds : ∀ s l,
     20 ≤ (variablePosition s l).1 ∧ (variablePosition s l).1 ≤ 220 ∧
       20 ≤ (variablePosition s l).2 ∧ (variablePosition s l).2 ≤ 220 := by decide +kernel
 
-private instance (r : Route) : Decidable (IsOrthogonal r) :=
-  inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2))
-
 /-- Every access is orthogonal, with its prescribed boundary and inner endpoints. -/
 theorem access_endpoints : ∀ s l, IsOrthogonal (accessRoute s l) ∧
     (accessRoute s l).head? = some (boundaryPort s l) ∧

Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean

@@ -50,9 +50,6 @@ def spokeElbow (s : Fin 4) : Point :=
 def spokeRoute (s : Fin 4) : Route :=
   [(120, 120), spokeElbow s, boundaryPort s (spokeLane s)]
 
-private instance (r : Route) : Decidable (IsOrthogonal r) :=
-  inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2))
-
 /-- Every spoke is proper and orthogonal with its prescribed endpoints. -/
 theorem spoke_endpoints : ∀ s, IsOrthogonal (spokeRoute s) ∧
     (spokeRoute s).head? = some (120, 120) ∧

Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean

@@ -29,6 +29,9 @@ rings. Construction and source credit are documented in `Crossover` and `Crossov
 ## References
 
 The construction adapts [Lichtenstein1982, Figs. 4–5] and [Tromino2025, Fig. 8(b)].
+Unique extension is the parsimony condition of
+[HuntMaratheRadhakrishnanStearns1998, Definition 3.1]. Their Theorem 3.2 proves that property for
+Lichtenstein's crossover; kernel evaluation checks the adapted 13-variable table here.
 -/
 
 @[expose] public section

Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean

@@ -26,6 +26,8 @@ Lichtenstein's crossover [Lichtenstein1982, Figs. 4–5], as drawn in [Tromino20
 
 ## Main results
 
+* `PairedCrossover.existsUnique_holds`: a unique full satisfying assignment for each input pair.
+* `PairedCrossover.eval_formula_iff`: split-formula semantics with paired-terminal agreement.
 * `PairedCrossover.eq_canonicalExtension_of_holds`: uniqueness of the full extension.
 * `PairedCrossover.terminal_occurrences`: two internal incidences at each of the eight ports.