diff --git a/Complexity.lean b/Complexity.lean
index 322cfd3ae..276b335da 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -809,6 +809,7 @@ public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverL
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverLayoutData
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.Occurrence
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.OrdinaryRing
 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
@@ -1958,6 +1959,9 @@ public import Complexity.Foundations.Geometry.Orthogonal.Endpoint
 public import Complexity.Foundations.Geometry.Orthogonal.Layout
 public import Complexity.Foundations.Geometry.Orthogonal.Macrocell
 public import Complexity.Foundations.Geometry.Orthogonal.Neighborhood
+public import Complexity.Foundations.Geometry.Orthogonal.PairedBoundary
+public import Complexity.Foundations.Geometry.Orthogonal.PairedPorts
+public import Complexity.Foundations.Geometry.Orthogonal.PairedSpokes
 public import Complexity.Foundations.Geometry.Orthogonal.Separation
 public import Complexity.Foundations.Geometry.Orthogonal.Simple
 public import Complexity.Foundations.Geometry.Orthogonal.Subdivision
@@ -2103,8 +2107,11 @@ public import Complexity.Logics.Propositional.CNF.ModelCount
 public import Complexity.Logics.Propositional.CNF.Occurrence
 public import Complexity.Logics.Propositional.CNF.Parity
 public import Complexity.Logics.Propositional.CNF.Planar.Crossover
+public import Complexity.Logics.Propositional.CNF.Planar.CrossoverCounting
 public import Complexity.Logics.Propositional.CNF.Planar.CrossoverSplit
 public import Complexity.Logics.Propositional.CNF.Planar.DirectedWire
+public import Complexity.Logics.Propositional.CNF.Planar.PairedCrossover
+public import Complexity.Logics.Propositional.CNF.Planar.PairedWire
 public import Complexity.Logics.Propositional.CNF.PolyTime
 public import Complexity.Logics.Propositional.CNF.ThreeCNF
 public import Complexity.Logics.Propositional.CNF.ThreeCNF.PolyTime
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean
new file mode 100644
index 000000000..7a496be62
--- /dev/null
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean
@@ -0,0 +1,269 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Geometry.Orthogonal.PairedPorts
+public import Complexity.Logics.Propositional.CNF.ImplicationCycle
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.SplitIfs
+
+/-!
+# An eight-port ordinary signal ring
+
+Eight binary implications follow the perimeter of `[20,220]²`, forcing all eight
+variables to agree. Every variable has two internal literal occurrences, leaving
+one external occurrence for its paired access. Unused accesses introduce no freedom.
+The sixteen incidence routes are straight and have total Manhattan length 800.
+
+## Main definitions
+
+* `Variable`, `cyclicOrder`, `formula`: the fixed implication ring.
+* `variablePosition`, `clausePositions`, `incidenceRoutes`: its explicit drawing.
+
+## Main results
+
+* `eval_formula_iff`, `eval_constant`: all ports carry one freely chosen bit.
+* `internal_occurrences`: exactly two internal literal occurrences per port.
+
+## References
+
+This fixed template is original and reuses `CNF.implicationCycle`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Complexity.SAT.OrdinaryRing
+
+open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal
+
+/-- One variable for each side and lane of the common paired-port interface. -/
+abbrev Variable := Fin 4 × Fin 2
+
+/-- Cyclic geometric order, traversing the inner square clockwise. -/
+def cyclicOrder : List Variable :=
+  [(0, 0), (0, 1), (3, 0), (3, 1), (1, 1), (1, 0), (2, 1), (2, 0)]
+
+/-- The eight directed implications closing the signal ring. -/
+def formula : CNF Variable := implicationCycle cyclicOrder
+
+/-- The eight common inner access positions. -/
+def variablePosition (v : Variable) : Point := PairedPorts.variablePosition v.1 v.2
+
+/-- Clause positions in precisely the order of the eight implications. -/
+def clausePositions : List Point :=
+  [(20, 120), (20, 220), (120, 220), (220, 220),
+    (220, 120), (220, 20), (120, 20), (20, 20)]
+
+/-- Indexed clause position, with an irrelevant out-of-range default. -/
+def clausePosition (i : ℕ) : Point := clausePositions.getD i (0, 0)
+
+/-- The sixteen clause-to-variable incidences, in clause and literal order. -/
+def incidenceRoutes : List (ℕ × Variable × Route) :=
+  [(0, (0, 0), [(20, 120), (20, 110)]),
+    (0, (0, 1), [(20, 120), (20, 130)]),
+    (1, (0, 1), [(20, 220), (20, 130)]),
+    (1, (3, 0), [(20, 220), (110, 220)]),
+    (2, (3, 0), [(120, 220), (110, 220)]),
+    (2, (3, 1), [(120, 220), (130, 220)]),
+    (3, (3, 1), [(220, 220), (130, 220)]),
+    (3, (1, 1), [(220, 220), (220, 130)]),
+    (4, (1, 1), [(220, 120), (220, 130)]),
+    (4, (1, 0), [(220, 120), (220, 110)]),
+    (5, (1, 0), [(220, 20), (220, 110)]),
+    (5, (2, 1), [(220, 20), (130, 20)]),
+    (6, (2, 1), [(120, 20), (130, 20)]),
+    (6, (2, 0), [(120, 20), (110, 20)]),
+    (7, (2, 0), [(20, 20), (110, 20)]),
+    (7, (0, 0), [(20, 20), (20, 110)])]
+
+/-- Common graph endpoints are the only permitted contacts between distinct incidences. -/
+def commonEndpoints (e f : ℕ × Variable × Route) : List Point :=
+  (if e.1 = f.1 then [clausePosition e.1] else []) ++
+    (if e.2.1 = f.2.1 then [variablePosition e.2.1] else [])
+
+/-- All eight port variables occur in the cycle. -/
+theorem mem_cyclicOrder : ∀ v : Variable, v ∈ cyclicOrder := by decide +kernel
+
+/-- The ring holds exactly when every port carries the value of the first port. -/
+theorem eval_formula_iff (σ : Variable → Bool) :
+    formula.eval σ = true ↔ ∀ v, σ v = σ (0, 0) := by
+  rw [formula, eval_implicationCycle]
+  constructor
+  · intro h v
+    exact h v (mem_cyclicOrder v) (0, 0) (mem_cyclicOrder (0, 0))
+  · intro h x _ y _
+    exact (h x).trans (h y).symm
+
+/-- Either constant assignment satisfies the ring. -/
+theorem eval_constant (b : Bool) : formula.eval (fun _ => b) = true :=
+  (eval_formula_iff _).2 fun _ => rfl
+
+/-- Every port has exactly two internal literal occurrences. -/
+theorem internal_occurrences : ∀ v : Variable, formula.vars.count v = 2 := by decide +kernel
+
+/-- The formula has eight clauses, each of width two. -/
+theorem formula_sizes : formula.length = 8 ∧ ∀ c ∈ formula, c.length = 2 := by decide +kernel
+
+/-- 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)) =
+      formula.zipIdx.flatMap (fun ci => ci.1.map fun l => (ci.2, l.1)) := by decide +kernel
+
+/-- There are eight clause positions and sixteen incidence routes. -/
+theorem drawing_sizes : clausePositions.length = 8 ∧ incidenceRoutes.length = 16 := by
+  decide +kernel
+
+/-- Inner positions identify the eight variables. -/
+theorem variablePosition_injective : Function.Injective variablePosition :=
+  PairedPorts.variablePosition_injective
+
+/-- Clause positions are distinct. -/
+theorem clausePositions_nodup : clausePositions.Nodup := by decide +kernel
+
+/-- Variables and clauses have different positions. -/
+theorem variablePosition_not_mem_clauses :
+    ∀ v : Variable, variablePosition v ∉ clausePositions := by decide +kernel
+
+/-- The sixteen labeled incidences are distinct. -/
+theorem incidenceEndpoints_nodup :
+    (incidenceRoutes.map fun e => (e.1, e.2.1)).Nodup := by decide +kernel
+
+/-- Every incidence has its prescribed clause and variable endpoints. -/
+theorem incidence_endpoints : ∀ e ∈ incidenceRoutes,
+    e.1 < 8 ∧ e.2.2.head? = some (clausePosition e.1) ∧
+      e.2.2.getLast? = some (variablePosition e.2.1) := by decide +kernel
+
+/-- All sixteen incidence routes are straight segments. -/
+theorem incidence_pair : ∀ e ∈ incidenceRoutes,
+    e.2.2 = [clausePosition e.1, variablePosition e.2.1] := by decide +kernel
+
+/-- Every incidence is properly orthogonal. -/
+theorem incidence_orthogonal : ∀ e ∈ incidenceRoutes, IsOrthogonal e.2.2 := by decide +kernel
+
+/-- Listed incidence vertices are distinct within each route. -/
+theorem incidence_points_nodup : ∀ e ∈ incidenceRoutes, e.2.2.Nodup := by decide +kernel
+
+/-- Every incidence is continuously simple. -/
+theorem incidence_isSimple {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes) :
+    IsSimple e.2.2 := by
+  refine ⟨incidence_points_nodup e he, ?_⟩
+  intro a ha b hb hne
+  rw [incidence_pair e he] at ha hb
+  have ha' : a = (clausePosition e.1, variablePosition e.2.1) := by
+    simpa only [List.consecutivePairs, List.tail_cons, List.tail_nil, List.zip_cons_cons,
+      List.zip_nil_right, List.mem_singleton] using ha
+  have hb' : b = (clausePosition e.1, variablePosition e.2.1) := by
+    simpa only [List.consecutivePairs, List.tail_cons, List.tail_nil, List.zip_cons_cons,
+      List.zip_nil_right, List.mem_singleton] using hb
+  exact False.elim (hne (ha'.trans hb'.symm))
+
+/-- All listed core points lie in `[20,220]²`. -/
+theorem core_bounds : ∀ e ∈ incidenceRoutes, ∀ p ∈ e.2.2,
+    20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by decide +kernel
+
+/-- Every variable lies in the inner core square. -/
+theorem variable_bounds : ∀ v : Variable,
+    20 ≤ (variablePosition v).1 ∧ (variablePosition v).1 ≤ 220 ∧
+      20 ≤ (variablePosition v).2 ∧ (variablePosition v).2 ≤ 220 := by decide +kernel
+
+/-- Every clause lies in the inner core square. -/
+theorem clause_bounds : ∀ p ∈ clausePositions,
+    20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by decide +kernel
+
+/-- The full continuous core support lies strictly inside the outer cell. -/
+theorem core_support_interior {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes)
+    {p : ℝ × ℝ} (hp : p ∈ support e.2.2) :
+    0 < p.1 ∧ p.1 < 240 ∧ 0 < p.2 ∧ p.2 < 240 := by
+  have hsub : support e.2.2 ⊆ openCell 120 (0, 0) := by
+    apply support_subset_openCell
+    intro q hq
+    have hb := core_bounds e he q hq
+    have hq' : 0 < q.1 ∧ q.1 < 240 ∧ 0 < q.2 ∧ q.2 < 240 := by omega
+    have hreal : (0 : ℝ) < q.1 ∧ (q.1 : ℝ) < 240 ∧
+        (0 : ℝ) < q.2 ∧ (q.2 : ℝ) < 240 := by exact_mod_cast hq'
+    simpa [openCell, realPoint] using hreal
+  simpa [openCell] using hsub hp
+
+/-- Finite certificate of all permitted contacts between distinct incidences. -/
+theorem routes_contact_check : ∀ e ∈ incidenceRoutes, ∀ f ∈ incidenceRoutes, e ≠ f →
+    routeContactCheck (commonEndpoints e f) e.2.2 f.2.2 = true := by decide +kernel
+
+/-- Continuous contacts between distinct incidences are shared graph endpoints. -/
+theorem routes_contact {e f : ℕ × Variable × Route}
+    (he : e ∈ incidenceRoutes) (hf : f ∈ incidenceRoutes) (hne : e ≠ f)
+    {p : ℝ × ℝ} (hp : p ∈ support e.2.2) (hq : p ∈ support f.2.2) :
+    ∃ q ∈ commonEndpoints e f, p = realPoint q :=
+  routeContactCheck_sound (routes_contact_check e he f hf hne) hp hq
+
+/-- Finite certificate excluding nonincident variable vertices. -/
+theorem variable_avoidance_check : ∀ e ∈ incidenceRoutes, ∀ v : Variable, v ≠ e.2.1 →
+    routeContactCheck [] e.2.2 [variablePosition v] = true := by decide +kernel
+
+/-- Finite certificate excluding nonincident clause vertices. -/
+theorem clause_avoidance_check : ∀ e ∈ incidenceRoutes, ∀ i : Fin 8, i.val ≠ e.1 →
+    routeContactCheck [] e.2.2 [clausePosition i] = true := by decide +kernel
+
+/-- Incidences avoid every nonincident variable over their full real support. -/
+theorem variable_not_mem_support {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes)
+    {v : Variable} (hv : v ≠ e.2.1) : realPoint (variablePosition v) ∉ support e.2.2 :=
+  not_mem_support_of_routeContactCheck (variable_avoidance_check e he v hv)
+
+/-- Incidences avoid every nonincident clause over their full real support. -/
+theorem clause_not_mem_support {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes)
+    {i : Fin 8} (hi : i.val ≠ e.1) : realPoint (clausePosition i) ∉ support e.2.2 :=
+  not_mem_support_of_routeContactCheck (clause_avoidance_check e he i hi)
+
+/-- Finite certificate that access touches the core only at its own variable. -/
+theorem access_contact_check : ∀ s l, ∀ e ∈ incidenceRoutes,
+    routeContactCheck (if e.2.1 = (s, l) then [variablePosition (s, l)] else [])
+      (PairedPorts.accessRoute s l) e.2.2 = true := by decide +kernel
+
+/-- Every access/core contact is its designated variable endpoint. -/
+theorem access_contact {s : Fin 4} {l : Fin 2} {e : ℕ × Variable × Route}
+    (he : e ∈ incidenceRoutes) {p : ℝ × ℝ}
+    (hp : p ∈ support (PairedPorts.accessRoute s l)) (hq : p ∈ support e.2.2) :
+    e.2.1 = (s, l) ∧ p = realPoint (variablePosition (s, l)) := by
+  obtain ⟨q, hq, hpq⟩ := routeContactCheck_sound (access_contact_check s l e he) hp hq
+  split_ifs at hq with h
+  · have hq' : q = variablePosition (s, l) := List.mem_singleton.mp hq
+    exact ⟨h, hq' ▸ hpq⟩
+  · exact False.elim (List.not_mem_nil hq)
+
+/-- Finite certificate excluding every other variable from an access. -/
+theorem access_variable_avoidance_check : ∀ s l, ∀ v : Variable, v ≠ (s, l) →
+    routeContactCheck [] (PairedPorts.accessRoute s l) [variablePosition v] = true := by
+  decide +kernel
+
+/-- Finite certificate excluding every clause from every access. -/
+theorem access_clause_avoidance_check : ∀ s l, ∀ p ∈ clausePositions,
+    routeContactCheck [] (PairedPorts.accessRoute s l) [p] = true := by decide +kernel
+
+/-- Access avoids every other variable over its full real support. -/
+theorem access_variable_not_mem {s : Fin 4} {l : Fin 2} {v : Variable} (hv : v ≠ (s, l)) :
+    realPoint (variablePosition v) ∉ support (PairedPorts.accessRoute s l) :=
+  not_mem_support_of_routeContactCheck (access_variable_avoidance_check s l v hv)
+
+/-- Access avoids every clause over its full real support. -/
+theorem access_clause_not_mem {s : Fin 4} {l : Fin 2} {p : Point} (hp : p ∈ clausePositions) :
+    realPoint p ∉ support (PairedPorts.accessRoute s l) :=
+  not_mem_support_of_routeContactCheck (access_clause_avoidance_check s l p hp)
+
+/-- The sixteen incidence segments have total Manhattan length 800. -/
+theorem route_sizes :
+    (incidenceRoutes.map fun e => e.2.2.consecutivePairs.length).sum = 16 ∧
+      (incidenceRoutes.map fun e => wireLength e.2.2).sum = 800 := by decide +kernel
+
+end Cslib.Complexity.SAT.OrdinaryRing
diff --git a/Complexity/Foundations/Geometry/Orthogonal/PairedBoundary.lean b/Complexity/Foundations/Geometry/Orthogonal/PairedBoundary.lean
new file mode 100644
index 000000000..35b761b72
--- /dev/null
+++ b/Complexity/Foundations/Geometry/Orthogonal/PairedBoundary.lean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Geometry.Orthogonal.PairedPorts
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum
+
+/-!
+# Matching paired boundaries of grid cells
+
+## Main results
+
+* `boundary_eq_cases`: equal boundary points in distinct cells determine adjacent opposite
+  sides and the same lane.
+* `boundary_not_mem_openCell`: a paired boundary belongs to no open grid cell.
+
+## References
+
+These are original integer-coordinate facts about the fixed paired-port interface.
+-/
+
+@[expose] public section
+
+namespace Cslib.Orthogonal.PairedPorts
+
+/-- Equal boundary points in distinct cells identify the lane and opposite adjacent sides. -/
+theorem boundary_eq_cases {c d : Point} {s t : Fin 4} {l k : Fin 2}
+    (hcd : c ≠ d)
+    (h : cellOrigin 120 c + boundaryPort s l = cellOrigin 120 d + boundaryPort t k) :
+    l = k ∧ d = c + neighbor s ∧ t = oppositeSide s := by
+  rcases c with ⟨cx, cy⟩
+  rcases d with ⟨dx, dy⟩
+  have hcd' : ¬ (cx = dx ∧ cy = dy) := fun h => hcd (Prod.ext h.1 h.2)
+  fin_cases s <;> fin_cases t <;> fin_cases l <;> fin_cases k <;>
+    norm_num [cellOrigin, boundaryPort, offset, neighbor, oppositeSide, Prod.ext_iff] at h ⊢ <;>
+    omega
+
+/-- Each translated paired boundary belongs to its own closed cell. -/
+theorem boundary_mem_closedCell (c : Point) (s : Fin 4) (l : Fin 2) :
+    realPoint (cellOrigin 120 c + boundaryPort s l) ∈ closedCell 120 c := by
+  rw [realPoint_add, add_comm, mem_closedCell_add_origin_iff]
+  fin_cases s <;> fin_cases l <;> norm_num [boundaryPort, offset, realPoint]
+
+/-- A translated paired boundary lies outside every open grid cell. -/
+theorem boundary_not_mem_openCell (c d : Point) (s : Fin 4) (l : Fin 2) :
+    realPoint (cellOrigin 120 c + boundaryPort s l) ∉ openCell 120 d := by
+  intro hp
+  have hdc := cell_eq_of_mem_open_closed (by decide) hp (boundary_mem_closedCell c s l)
+  subst d
+  rw [realPoint_add, add_comm, mem_openCell_add_origin_iff] at hp
+  fin_cases s <;> fin_cases l <;> norm_num [boundaryPort, offset, realPoint] at hp
+
+end Cslib.Orthogonal.PairedPorts
diff --git a/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean b/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean
new file mode 100644
index 000000000..b311f95a1
--- /dev/null
+++ b/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean
@@ -0,0 +1,153 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Geometry.Orthogonal.Macrocell
+public import Complexity.Foundations.Geometry.Orthogonal.Separation
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
+
+/-!
+# Paired ports of a fixed square cell
+
+Each side of `[0,240]²` has two ports, at offsets 110 and 130. Sides are ordered
+left, right, bottom, top. Lane zero always has the smaller coordinate; translation
+to an adjacent cell preserves the lane. Straight access routes end 20 units inside.
+
+## Main definitions
+
+* `boundaryPort`, `variablePosition`, `accessRoute`: the eight paired accesses.
+* `oppositeSide`, `neighbor`: matching sides and adjacent cell displacements.
+
+## Main results
+
+* `boundaryPort_shared`: adjacent cells share the same port in the same lane.
+* `access_disjoint`, `access_boundary_isolation`: continuous access separation.
+
+## References
+
+This fixed geometric interface is original.
+-/
+
+@[expose] public section
+
+namespace Cslib.Orthogonal.PairedPorts
+
+/-- A side and its lower- or higher-coordinate lane. -/
+abbrev Port := Fin 4 × Fin 2
+
+/-- The two lane coordinates. -/
+def offset (l : Fin 2) : ℤ := 110 + 20 * (l : ℕ)
+
+/-- Paired boundary ports, in left/right/bottom/top side order. -/
+def boundaryPort (s : Fin 4) (l : Fin 2) : Point :=
+  if s = 0 then (0, offset l) else if s = 1 then (240, offset l)
+    else if s = 2 then (offset l, 0) else (offset l, 240)
+
+/-- The corresponding inner positions on the perimeter of `[20,220]²`. -/
+def variablePosition (s : Fin 4) (l : Fin 2) : Point :=
+  if s = 0 then (20, offset l) else if s = 1 then (220, offset l)
+    else if s = 2 then (offset l, 20) else (offset l, 220)
+
+/-- Straight access from one boundary port to its corresponding inner position. -/
+def accessRoute (s : Fin 4) (l : Fin 2) : Route :=
+  [boundaryPort s l, variablePosition s l]
+
+/-- Opposite sides of neighboring cells. -/
+def oppositeSide (s : Fin 4) : Fin 4 :=
+  if s = 0 then 1 else if s = 1 then 0 else if s = 2 then 3 else 2
+
+/-- Displacement to the neighboring cell on the indicated side. -/
+def neighbor (s : Fin 4) : Point :=
+  if s = 0 then (-1, 0) else if s = 1 then (1, 0)
+    else if s = 2 then (0, -1) else (0, 1)
+
+/-- Taking the opposite side twice recovers the original side. -/
+theorem oppositeSide_involutive : Function.Involutive oppositeSide := by
+  change ∀ s, oppositeSide (oppositeSide s) = s
+  decide +kernel
+
+/-- Adjacent cells match ports without reversing the lane. -/
+theorem boundaryPort_shared (p : Point) (s : Fin 4) (l : Fin 2) :
+    cellOrigin 120 p + boundaryPort s l =
+      cellOrigin 120 (p + neighbor s) + boundaryPort (oppositeSide s) l := by
+  fin_cases s <;> fin_cases l <;> ext <;>
+    simp [cellOrigin, boundaryPort, oppositeSide, neighbor, offset] <;> ring
+
+/-- All eight boundary positions are distinct. -/
+theorem boundaryPort_injective : Function.Injective (fun p : Port => boundaryPort p.1 p.2) := by
+  decide +kernel
+
+/-- All eight inner positions are distinct. -/
+theorem variablePosition_injective :
+    Function.Injective (fun p : Port => variablePosition p.1 p.2) := by decide +kernel
+
+/-- Every inner position lies in the smaller core square. -/
+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) ∧
+      (accessRoute s l).getLast? = some (variablePosition s l) := by decide +kernel
+
+/-- Every access is simple over its full real support. -/
+theorem access_isSimple (s : Fin 4) (l : Fin 2) : IsSimple (accessRoute s l) := by
+  constructor
+  · fin_cases s <;> fin_cases l <;> decide
+  · intro a ha b hb hne
+    have ht : (accessRoute s l).consecutivePairs =
+        [(boundaryPort s l, variablePosition s l)] := rfl
+    rw [ht, List.mem_singleton] at ha hb
+    exact False.elim (hne (ha.trans hb.symm))
+
+/-- Each access has one segment and 20 units of Manhattan length. -/
+theorem access_route_sizes : ∀ s l, (accessRoute s l).consecutivePairs.length = 1 ∧
+    wireLength (accessRoute s l) = 20 := by decide +kernel
+
+/-- Finite certificate separating every pair of distinct accesses. -/
+theorem access_disjoint_check : ∀ p q : Port, p ≠ q →
+    routeContactCheck [] (accessRoute p.1 p.2) (accessRoute q.1 q.2) = true := by decide +kernel
+
+/-- Distinct accesses have disjoint full real supports. -/
+theorem access_disjoint {p q : Port} (h : p ≠ q) :
+    Disjoint (support (accessRoute p.1 p.2)) (support (accessRoute q.1 q.2)) :=
+  disjoint_support_of_routeContactCheck (access_disjoint_check p q h)
+
+private theorem mem_support_pair {a b : Point} {p : ℝ × ℝ} :
+    p ∈ support [a, b] ↔ p ∈ segment a b := by
+  rw [support_cons_cons]
+  change (p ∈ segment a b ∨ p ∈ support [b]) ↔ _
+  have hright : realPoint b ∈ segment a b := _root_.right_mem_segment ℝ _ _
+  have hs : p ∈ support [b] ↔ p = realPoint b := by simp [support, List.consecutivePairs]
+  rw [hs]
+  exact ⟨fun h => h.elim id (fun h => h ▸ hright), Or.inl⟩
+
+/-- An access stays in the cell and touches its boundary only at the designated port. -/
+theorem access_boundary_isolation {s : Fin 4} {l : Fin 2} {p : ℝ × ℝ}
+    (hp : p ∈ support (accessRoute s l)) :
+    0 ≤ p.1 ∧ p.1 ≤ 240 ∧ 0 ≤ p.2 ∧ p.2 ≤ 240 ∧
+      (p.1 = 0 ∨ p.1 = 240 ∨ p.2 = 0 ∨ p.2 = 240 → p = realPoint (boundaryPort s l)) := by
+  unfold accessRoute at hp
+  rw [mem_support_pair] at hp
+  fin_cases s <;> fin_cases l <;>
+    simp only [boundaryPort, variablePosition, offset, Orthogonal.segment, realPoint] at hp ⊢
+  all_goals
+    norm_num [mem_horizontal, mem_vertical, Set.mem_uIcc] at hp ⊢
+    rcases hp with ⟨heq, hlo, hhi⟩
+    refine ⟨by linarith, by linarith, by linarith, by linarith, ?_⟩
+    intro h
+    rcases h with h | h | h | h <;> apply Prod.ext <;> norm_num <;> linarith
+
+end Cslib.Orthogonal.PairedPorts
diff --git a/Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean b/Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean
new file mode 100644
index 000000000..f80b2dc0f
--- /dev/null
+++ b/Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean
@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Geometry.Orthogonal.PairedPorts
+import Mathlib.Tactic.FinCases
+
+/-!
+# Four disjoint offset spokes
+
+A rotational choice of one of the paired ports on each side gives four proper orthogonal
+spokes from the center of the square. Distinct spokes meet only at that center. These are
+finite certificates about entire real route supports.
+
+## Main definitions
+
+* `Cslib.Orthogonal.PairedPorts.spokeLane`, `.spokeRoute`: selected ports and two-segment spokes.
+
+## Main results
+
+* `Cslib.Orthogonal.PairedPorts.spoke_isSimple`, `.spokes_contact`: simplicity and center-only
+  contacts.
+
+## References
+
+The finite offset star is original.
+-/
+
+@[expose] public section
+
+namespace Cslib.Orthogonal.PairedPorts
+
+/-- One selected lane on each side, in rotational order around the center. -/
+def spokeLane (s : Fin 4) : Fin 2 := if s = 1 ∨ s = 2 then 1 else 0
+
+/-- A spoke first travels toward its bend and then toward its selected boundary point. -/
+def spokeElbow (s : Fin 4) : Point :=
+  match s with
+  | 0 => (120, 110)
+  | 1 => (120, 130)
+  | 2 => (130, 120)
+  | _ => (110, 120)
+
+/-- A two-segment route from the center to the selected side port. -/
+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) ∧
+      (spokeRoute s).getLast? = some (boundaryPort s (spokeLane s)) := by decide +kernel
+
+/-- The two segments of a spoke meet only at their shared bend. -/
+theorem spoke_bend_check : ∀ s,
+    segmentContactCheck [spokeElbow s] (120, 120) (spokeElbow s)
+      (spokeElbow s) (boundaryPort s (spokeLane s)) = true := by decide +kernel
+
+/-- Each spoke is simple over its full real support. -/
+theorem spoke_isSimple (s : Fin 4) : IsSimple (spokeRoute s) := by
+  have hcontact : EndpointContacts (120, 120) (spokeElbow s) (spokeElbow s)
+      (boundaryPort s (spokeLane s)) := by
+    intro p hp hq
+    obtain ⟨q, hq, heq⟩ := segmentContactCheck_sound (spoke_bend_check s) hp hq
+    have hqb := List.mem_singleton.mp hq
+    exact ⟨Or.inr (hqb ▸ heq), Or.inl (hqb ▸ heq)⟩
+  refine ⟨?_, ?_⟩
+  · fin_cases s <;> decide
+  · intro e he f hf hne
+    simp only [spokeRoute, List.consecutivePairs, List.tail_cons, List.zip_cons_cons,
+      List.zip_nil_right, List.mem_cons, List.not_mem_nil, or_false] at he hf
+    rcases he with rfl | rfl <;> rcases hf with rfl | rfl
+    · exact False.elim (hne rfl)
+    · exact hcontact
+    · exact hcontact.symm
+    · exact False.elim (hne rfl)
+
+/-- Distinct spokes have only the center as an allowed continuous contact. -/
+theorem spokes_contact_check : ∀ s t : Fin 4, s ≠ t →
+    routeContactCheck [(120, 120)] (spokeRoute s) (spokeRoute t) = true := by decide +kernel
+
+/-- Every real intersection of distinct spokes is their common center. -/
+theorem spokes_contact {s t : Fin 4} (hst : s ≠ t) {p : ℝ × ℝ}
+    (hp : p ∈ support (spokeRoute s)) (hq : p ∈ support (spokeRoute t)) :
+    p = realPoint (120, 120) := by
+  obtain ⟨q, hq, hpq⟩ := routeContactCheck_sound (spokes_contact_check s t hst) hp hq
+  exact (List.mem_singleton.mp hq) ▸ hpq
+
+end Cslib.Orthogonal.PairedPorts
diff --git a/Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean b/Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean
new file mode 100644
index 000000000..b0371b7ae
--- /dev/null
+++ b/Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean
@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Logics.Propositional.CNF.Planar.CrossoverSplit
+
+/-!
+# Unique extensions through the fixed crossover
+
+The fixed clause tables have exactly one satisfying full assignment for each pair of incoming
+bits. The explicit Boolean extension and its uniqueness are preserved by the internal splitting
+rings. Construction and source credit are documented in `Crossover` and `CrossoverSplit`.
+
+## Main definitions
+
+* `Cslib.Logic.PL.CNF.Crossover.canonicalExtension`: the original full assignment from two bits.
+* `Cslib.Logic.PL.CNF.Crossover.canonicalSplitExtension`: its lift to all internal copies.
+
+## Main results
+
+* `Cslib.Logic.PL.CNF.Crossover.existsUnique_holds`: uniqueness before splitting.
+* `Cslib.Logic.PL.CNF.Crossover.existsUnique_split_holds`: uniqueness after splitting.
+
+## References
+
+The construction adapts [Lichtenstein1982, Figs. 4–5] and [Tromino2025, Fig. 8(b)].
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.CNF.Crossover
+
+/-- The full satisfying assignment determined by the left and top input values.
+The explicit Boolean expressions describe all nine internal values as well as the outputs. -/
+def canonicalExtension (a b : Bool) : Variable → Bool :=
+  assignment a a b b a (!a || b) (!a || !b) b a b (a || b) (a || !b) a
+
+/-- The explicit extension satisfies all 26 clauses for every pair of inputs. -/
+theorem eval_canonicalExtension (a b : Bool) :
+    formula.eval (canonicalExtension a b) = true := by
+  cases a <;> cases b <;> decide +kernel
+
+-- Only the nine internal values are enumerated after the two inputs are fixed; the existing
+-- boundary theorem has already identified the outputs with those inputs.
+private theorem assignment_eq_canonicalExtension (a b : Bool) :
+    ∀ aInnerLeft upperLeft lowerLeft bInnerTop center bInnerBottom
+        upperRight lowerRight aInnerRight : Bool,
+      formula.eval (assignment a a b b aInnerLeft upperLeft lowerLeft bInnerTop center
+        bInnerBottom upperRight lowerRight aInnerRight) = true →
+      ∀ v, assignment a a b b aInnerLeft upperLeft lowerLeft bInnerTop center
+        bInnerBottom upperRight lowerRight aInnerRight v = canonicalExtension a b v := by
+  cases a <;> cases b <;> decide +kernel
+
+/-- Every satisfying full assignment is the explicit extension of its two incoming values. -/
+theorem eq_canonicalExtension_of_holds {σ : Variable → Bool}
+    (h : formula.eval σ = true) :
+    σ = canonicalExtension (σ .aLeft) (σ .bTop) := by
+  obtain ⟨horizontal, vertical⟩ := boundary_eq_of_holds h
+  have heq : assignment (σ .aLeft) (σ .aLeft) (σ .bTop) (σ .bTop)
+      (σ .aInnerLeft) (σ .upperLeft) (σ .lowerLeft) (σ .bInnerTop) (σ .center)
+      (σ .bInnerBottom) (σ .upperRight) (σ .lowerRight) (σ .aInnerRight) = σ := by
+    funext v
+    cases v <;> first | rfl | exact horizontal | exact vertical
+  have hfull := assignment_eq_canonicalExtension (σ .aLeft) (σ .bTop)
+    (σ .aInnerLeft) (σ .upperLeft) (σ .lowerLeft) (σ .bInnerTop) (σ .center)
+    (σ .bInnerBottom) (σ .upperRight) (σ .lowerRight) (σ .aInnerRight)
+  rw [heq] at hfull
+  exact funext (hfull h)
+
+/-- Satisfying assignments agreeing on the incoming ports agree on every variable. -/
+theorem ext_of_holds {σ τ : Variable → Bool}
+    (hσ : formula.eval σ = true) (hτ : formula.eval τ = true)
+    (ha : σ .aLeft = τ .aLeft) (hb : σ .bTop = τ .bTop) : σ = τ := by
+  rw [eq_canonicalExtension_of_holds hσ, eq_canonicalExtension_of_holds hτ, ha, hb]
+
+/-- Each pair of incoming values extends uniquely to a satisfying full assignment. -/
+theorem existsUnique_holds (a b : Bool) :
+    ∃! σ : Variable → Bool,
+      formula.eval σ = true ∧ σ .aLeft = a ∧ σ .bTop = b := by
+  refine ⟨canonicalExtension a b, ⟨eval_canonicalExtension a b, rfl, rfl⟩, ?_⟩
+  rintro σ ⟨hσ, ha, hb⟩
+  rw [eq_canonicalExtension_of_holds hσ, ha, hb]
+
+/-- The explicit full split assignment: every local copy receives its original variable's
+canonical value, determined by the left and top inputs. -/
+def canonicalSplitExtension (a b : Bool) : SplitVariable → Bool :=
+  canonicalExtension a b ∘ SplitVariable.origin
+
+/-- The canonical split extension satisfies all 74 clauses. -/
+theorem eval_canonicalSplitExtension (a b : Bool) :
+    splitFormula.eval (canonicalSplitExtension a b) = true :=
+  eval_splitFormula_lift _ (eval_canonicalExtension a b)
+
+/-- Every satisfying split assignment is the explicit extension of its incoming values.
+The implication rings identify the six copies before applying the original uniqueness result;
+no enumeration of assignments to the 53 split variables is needed. -/
+theorem eq_canonicalSplitExtension_of_holds {σ : SplitVariable → Bool}
+    (h : splitFormula.eval σ = true) :
+    σ = canonicalSplitExtension (σ .aLeft) (σ .bTop) := by
+  obtain ⟨hbase, hagree⟩ := (eval_splitFormula_iff σ).1 h
+  have heq := eq_canonicalExtension_of_holds hbase
+  funext v
+  have hv := congrFun heq v.origin
+  cases v with
+  | aLeft | aRight | bTop | bBottom | center => exact hv
+  | copy v i =>
+    have hzero : σ (.copy v 0) = canonicalSplitExtension (σ .aLeft) (σ .bTop)
+        (.copy v i) := by
+      cases v <;> exact hv
+    exact (hagree v i).trans hzero
+
+/-- Satisfying split assignments agreeing on the two incoming ports agree everywhere. -/
+theorem split_ext_of_holds {σ τ : SplitVariable → Bool}
+    (hσ : splitFormula.eval σ = true) (hτ : splitFormula.eval τ = true)
+    (ha : σ .aLeft = τ .aLeft) (hb : σ .bTop = τ .bTop) : σ = τ := by
+  rw [eq_canonicalSplitExtension_of_holds hσ, eq_canonicalSplitExtension_of_holds hτ, ha, hb]
+
+/-- Each pair of incoming values extends uniquely to a satisfying full split assignment. -/
+theorem existsUnique_split_holds (a b : Bool) :
+    ∃! σ : SplitVariable → Bool,
+      splitFormula.eval σ = true ∧ σ .aLeft = a ∧ σ .bTop = b := by
+  refine ⟨canonicalSplitExtension a b, ⟨eval_canonicalSplitExtension a b, rfl, rfl⟩, ?_⟩
+  rintro σ ⟨hσ, ha, hb⟩
+  rw [eq_canonicalSplitExtension_of_holds hσ, ha, hb]
+
+end Cslib.Logic.PL.CNF.Crossover
diff --git a/Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean b/Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean
new file mode 100644
index 000000000..05994f7e5
--- /dev/null
+++ b/Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean
@@ -0,0 +1,283 @@
+/-
+Copyright (c) 2026 lean-trominoes contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine, Stefan Langerman, GPT 5.6
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Logics.Propositional.CNF.Planar.CrossoverCounting
+import Mathlib.Tactic.FinCases
+
+/-!
+# A crossover with two attachment ports per side
+
+Each old terminal is replaced by two ports and one implication between them. Together with
+its two old incidences this forms an implication chain between two equal internal copies.
+Consequently both ports have the old terminal's uniquely determined value. Each port has two
+internal incidences and room for one external incidence. The unchanged internal core comes from
+Lichtenstein's crossover [Lichtenstein1982, Figs. 4–5], as drawn in [Tromino2025, Fig. 8(b)].
+
+## Main definitions
+
+* `PairedCrossover.formula`: the 57-variable, 78-clause paired-port template.
+* `PairedCrossover.canonicalExtension`: its full assignment from two input bits.
+
+## Main results
+
+* `PairedCrossover.eq_canonicalExtension_of_holds`: uniqueness of the full extension.
+* `PairedCrossover.terminal_occurrences`: two internal incidences at each of the eight ports.
+
+## References
+
+* David Lichtenstein, *Planar Formulae and Their Uses*, Figs. 4–5 [Lichtenstein1982].
+* MIT–ULB CompGeom Group, *Undecidability of Tiling with a Tromino*, Fig. 8(b) [Tromino2025].
+
+The paired-terminal replacement and its uniqueness proof are original.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.CNF.PairedCrossover
+
+/-- Eight boundary ports, the unsplit center, and the old 48 internal copies. -/
+inductive Variable
+  | port (side : Fin 4) (lane : Fin 2)
+  | center
+  | copy (v : Crossover.Internal) (i : Fin 6)
+  deriving DecidableEq, Repr
+
+instance : Fintype Variable where
+  elems := { .center } ∪
+    Finset.univ.biUnion (fun s => Finset.univ.image (Variable.port s)) ∪
+    Finset.univ.biUnion (fun v => Finset.univ.image (Variable.copy v))
+  complete v := by cases v <;> simp
+
+/-- The eight attachment ports in left/right/bottom/top geometric order, with two lanes per
+side. The source variables `.bTop` and `.bBottom` retain their historical names. -/
+def terminal : Fin 4 → Fin 2 → Variable := Variable.port
+
+/-- Forget the lane of a boundary port. -/
+def Variable.origin : Variable → Crossover.SplitVariable
+  | .port 0 _ => .aLeft
+  | .port 1 _ => .aRight
+  | .port 2 _ => .bTop
+  | .port 3 _ => .bBottom
+  | .center => .center
+  | .copy v i => .copy v i
+
+/-- Choose lane zero as the representative of each old terminal. -/
+def representative : Crossover.SplitVariable → Variable
+  | .aLeft => .port 0 0
+  | .aRight => .port 1 0
+  | .bTop => .port 2 0
+  | .bBottom => .port 3 0
+  | .center => .center
+  | .copy v i => .copy v i
+
+/-- Replace each old boundary literal by the port at that incidence's geometric lane. -/
+def mapLiteral : Literal Crossover.SplitVariable → Literal Variable
+  | (.aLeft, true) => (.port 0 0, true)
+  | (.aLeft, false) => (.port 0 1, false)
+  | (.aRight, false) => (.port 1 0, false)
+  | (.aRight, true) => (.port 1 1, true)
+  | (.bTop, false) => (.port 2 0, false)
+  | (.bTop, true) => (.port 2 1, true)
+  | (.bBottom, true) => (.port 3 0, true)
+  | (.bBottom, false) => (.port 3 1, false)
+  | (.center, b) => (.center, b)
+  | (.copy v i, b) => (.copy v i, b)
+
+/-- One directed implication joins the paired ports on each side. -/
+def bridges : CNF Variable :=
+  [[(.port 0 0, false), (.port 0 1, true)],
+   [(.port 1 1, false), (.port 1 0, true)],
+   [(.port 2 1, false), (.port 2 0, true)],
+   [(.port 3 0, false), (.port 3 1, true)]]
+
+/-- Preserve the old 74 clauses with their terminal incidences separated, then add four bridges. -/
+def formula : CNF Variable :=
+  Crossover.splitFormula.map (List.map mapLiteral) ++ bridges
+
+/-- The internal copy at the start of each terminal's implication chain. -/
+def chainStart : Fin 4 → Variable
+  | 0 => .copy .aInnerLeft 5
+  | 1 => .copy .aInnerRight 3
+  | 2 => .copy .bInnerTop 1
+  | 3 => .copy .bInnerBottom 4
+
+/-- The internal copy at the end of each terminal's implication chain. -/
+def chainEnd : Fin 4 → Variable
+  | 0 => .copy .aInnerLeft 4
+  | 1 => .copy .aInnerRight 2
+  | 2 => .copy .bInnerTop 0
+  | 3 => .copy .bInnerBottom 3
+
+/-- The first lane in each directed chain. -/
+def firstLane : Fin 4 → Fin 2
+  | 0 => 0
+  | 1 => 1
+  | 2 => 1
+  | 3 => 0
+
+/-- Three existing clauses form a chain between two equal internal copies. -/
+def chain : Fin 4 → CNF Variable
+  | 0 => [[(.port 0 0, true), (.copy .aInnerLeft 5, false)],
+      [(.port 0 0, false), (.port 0 1, true)],
+      [(.port 0 1, false), (.copy .aInnerLeft 4, true)]]
+  | 1 => [[(.copy .aInnerRight 3, false), (.port 1 1, true)],
+      [(.port 1 1, false), (.port 1 0, true)],
+      [(.copy .aInnerRight 2, true), (.port 1 0, false)]]
+  | 2 => [[(.port 2 1, true), (.copy .bInnerTop 1, false)],
+      [(.port 2 1, false), (.port 2 0, true)],
+      [(.port 2 0, false), (.copy .bInnerTop 0, true)]]
+  | 3 => [[(.copy .bInnerBottom 4, false), (.port 3 0, true)],
+      [(.port 3 0, false), (.port 3 1, true)],
+      [(.copy .bInnerBottom 3, true), (.port 3 1, false)]]
+
+private theorem chain_mem : ∀ s, ∀ c ∈ chain s, c ∈ formula := by decide +kernel
+
+private theorem ring_mem : ∀ v, ∀ c ∈ (Crossover.ring v).relabel representative,
+    c ∈ formula := by decide +kernel
+
+private theorem eval_chain {σ : Variable → Bool} {s : Fin 4}
+    (h : (chain s).eval σ = true) (heq : σ (chainStart s) = σ (chainEnd s)) :
+    σ (terminal s 0) = σ (chainStart s) ∧
+      σ (terminal s 1) = σ (chainStart s) := by
+  have cert : ∀ a p q : Bool,
+      ((!a || p) && (!p || q) && (!q || a)) = true → p = a ∧ q = a := by
+    decide +kernel
+  have h' : ((!σ (chainStart s) || σ (terminal s (firstLane s))) &&
+      (!σ (terminal s (firstLane s)) || σ (terminal s (1 - firstLane s))) &&
+      (!σ (terminal s (1 - firstLane s)) || σ (chainEnd s))) = true := by
+    fin_cases s <;>
+      simpa [chain, chainStart, chainEnd, terminal, firstLane, CNF.eval, Clause.eval,
+        Literal.eval, Bool.and_assoc, Bool.or_comm] using h
+  rw [← heq] at h'
+  have hp := cert _ _ _ h'
+  fin_cases s <;> simpa [firstLane, and_comm] using hp
+
+private theorem eval_mapped (σ : Variable → Bool)
+    (ha : ∀ s, σ (terminal s 0) = σ (terminal s 1)) :
+    CNF.eval σ (Crossover.splitFormula.map (List.map mapLiteral)) =
+      Crossover.splitFormula.eval (σ ∘ representative) := by
+  have hl : ∀ l, Literal.eval σ (mapLiteral l) = Literal.eval (σ ∘ representative) l := by
+    simp only [terminal] at ha
+    rintro ⟨v, b⟩
+    cases v <;> cases b <;>
+      simp [mapLiteral, Literal.eval, representative, ← ha]
+  simp only [CNF.eval, List.all_map, Function.comp_def, Clause.eval, List.any_map, hl]
+  rfl
+
+/-- Exact semantics: the old split formula together with agreement of each paired terminal. -/
+theorem eval_formula_iff (σ : Variable → Bool) :
+    formula.eval σ = true ↔
+      Crossover.splitFormula.eval (σ ∘ representative) = true ∧
+        ∀ s, σ (terminal s 0) = σ (terminal s 1) := by
+  constructor
+  · intro h
+    have hc := CNF.eval_eq_true_iff σ formula |>.1 h
+    have hr : ∀ v i, σ (.copy v i) = σ (.copy v 0) := by
+      intro v
+      apply (Crossover.eval_ring_iff (σ ∘ representative) v).1
+      rw [← CNF.eval_relabel]
+      exact (CNF.eval_eq_true_iff _ _).2 fun c hc' => hc c (ring_mem v c hc')
+    have hp : ∀ s, σ (terminal s 0) = σ (terminal s 1) := by
+      intro s
+      have hchain := (CNF.eval_eq_true_iff σ (chain s)).2 fun c hc' => hc c (chain_mem s c hc')
+      have heq : σ (chainStart s) = σ (chainEnd s) := by
+        fin_cases s <;> exact (hr _ _).trans (hr _ _).symm
+      exact (eval_chain hchain heq).1.trans (eval_chain hchain heq).2.symm
+    refine ⟨?_, hp⟩
+    rw [formula, CNF.eval_append, Bool.and_eq_true] at h
+    rw [eval_mapped σ hp] at h
+    exact h.1
+  · rintro ⟨h, hp⟩
+    rw [formula, CNF.eval_append, Bool.and_eq_true, eval_mapped σ hp]
+    refine ⟨h, ?_⟩
+    simp only [terminal] at hp
+    simp [bridges, CNF.eval, Clause.eval, Literal.eval, ← hp]
+
+/-- The explicit unique full assignment, including both lanes on every side. -/
+def canonicalExtension (a b : Bool) : Variable → Bool :=
+  Crossover.canonicalSplitExtension a b ∘ Variable.origin
+
+/-- The explicit full assignment satisfies the paired-port formula. -/
+theorem eval_canonicalExtension (a b : Bool) : formula.eval (canonicalExtension a b) = true := by
+  apply (eval_formula_iff _).2
+  constructor
+  · have heq : canonicalExtension a b ∘ representative = Crossover.canonicalSplitExtension a b := by
+      funext v
+      cases v <;> rfl
+    rw [heq]
+    exact Crossover.eval_canonicalSplitExtension a b
+  · intro s
+    fin_cases s <;> rfl
+
+/-- Both lanes on the left and right carry `a`; both lanes on the top and bottom carry `b`. -/
+theorem terminal_values_canonicalExtension (a b : Bool) :
+    ∀ s l, canonicalExtension a b (terminal s l) = if s.val < 2 then a else b := by
+  intro s l
+  fin_cases s <;> rfl
+
+/-- Every satisfying full assignment is determined by the left and top lane-zero inputs. -/
+theorem eq_canonicalExtension_of_holds {σ : Variable → Bool} (h : formula.eval σ = true) :
+    σ = canonicalExtension (σ (terminal 0 0)) (σ (terminal 2 0)) := by
+  obtain ⟨hb, hp⟩ := (eval_formula_iff σ).1 h
+  have heq := Crossover.eq_canonicalSplitExtension_of_holds hb
+  funext v
+  cases v with
+  | center => exact congrFun heq .center
+  | copy v i => exact congrFun heq (.copy v i)
+  | port s l =>
+    have hs : σ (terminal s 0) = canonicalExtension (σ (terminal 0 0))
+        (σ (terminal 2 0)) (terminal s l) := by
+      fin_cases s
+      · exact congrFun heq .aLeft
+      · exact congrFun heq .aRight
+      · exact congrFun heq .bTop
+      · exact congrFun heq .bBottom
+    fin_cases l
+    · exact hs
+    · exact (hp s).symm.trans hs
+
+/-- All satisfying terminal values are the horizontal or vertical input value. -/
+theorem terminal_value_of_holds {σ : Variable → Bool} (h : formula.eval σ = true)
+    (s : Fin 4) (l : Fin 2) :
+    σ (terminal s l) = if s.val < 2 then σ (terminal 0 0) else σ (terminal 2 0) :=
+  (congrFun (eq_canonicalExtension_of_holds h) (terminal s l)).trans
+    (terminal_values_canonicalExtension _ _ s l)
+
+/-- Projecting a satisfying paired assignment recovers a satisfying old split assignment. -/
+theorem eval_representative_of_holds {σ : Variable → Bool} (h : formula.eval σ = true) :
+    Crossover.splitFormula.eval (σ ∘ representative) = true :=
+  ((eval_formula_iff σ).1 h).1
+
+/-- Every two-bit input has exactly one satisfying full assignment. -/
+theorem existsUnique_holds (a b : Bool) :
+    ∃! σ : Variable → Bool,
+      formula.eval σ = true ∧ σ (terminal 0 0) = a ∧ σ (terminal 2 0) = b := by
+  refine ⟨canonicalExtension a b, ⟨eval_canonicalExtension a b, rfl, rfl⟩, ?_⟩
+  rintro σ ⟨h, ha, hb⟩
+  rw [eq_canonicalExtension_of_holds h, ha, hb]
+
+/-- The template uses exactly 57 variables. -/
+theorem card_variable : Fintype.card Variable = 57 := by decide +kernel
+
+/-- The template has exactly 78 clauses. -/
+theorem length_formula : formula.length = 78 := by decide +kernel
+
+/-- All clauses have width at most three. -/
+theorem width_formula : ∀ c ∈ formula, c.length ≤ 3 := by decide +kernel
+
+/-- No clause repeats a variable. -/
+theorem distinct_variables : ∀ c ∈ formula, (c.map Prod.fst).Nodup := by decide +kernel
+
+/-- Every variable has at most three internal incidences. -/
+theorem occurrences_le_three : ∀ v, formula.occurrences v ≤ 3 := by decide +kernel
+
+/-- Each of the eight ports has exactly two internal incidences. -/
+theorem terminal_occurrences : ∀ s l, formula.occurrences (terminal s l) = 2 := by decide +kernel
+
+end Cslib.Logic.PL.CNF.PairedCrossover
diff --git a/Complexity/Logics/Propositional/CNF/Planar/PairedWire.lean b/Complexity/Logics/Propositional/CNF/Planar/PairedWire.lean
new file mode 100644
index 000000000..022d1f5e8
--- /dev/null
+++ b/Complexity/Logics/Propositional/CNF/Planar/PairedWire.lean
@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Logics.Propositional.CNF
+public import Mathlib.Data.List.Defs
+import Mathlib.Data.List.Basic
+import Mathlib.Data.Bool.Basic
+
+/-!
+# Paired implication wires
+
+Each cell has two lanes, each with an entry and an exit. Local constraints must equate all
+four port values. Across a gap, lane zero implies the next entry from the previous exit;
+lane one implies the previous exit from the next entry. These implications use separate
+ports. Under the local equalities, they force the representative values of consecutive cells
+to agree. Thus every port of a nonempty wire has the value of its first lane-zero entry.
+
+This module uses ordinary CNF semantics. It supplies no local cell constraints or geometry.
+The two clauses and four literal positions per gap are counted with multiplicity, without
+distinctness assumptions on the port variables.
+
+## Main definitions
+
+* `Cell`, `Cell.Agree`: two entry/exit pairs and equality of all four values.
+* `gapClauses`, `links`: opposite implications across one gap and all consecutive gaps.
+
+## Main results
+
+* `eval_links_iff`: under local agreement, the links equate consecutive representatives.
+* `agree_head`, `agree_head_of_ne_nil`: every entry and exit has the first entry's value.
+* `eval_links_of_constant`: constant port values satisfy every link.
+* `length_links`, `length_vars_links`, `length_of_mem_links`: exact sizes and binary width.
+
+## References
+
+The paired-port composition and equality argument are original.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.CNF.PairedWire
+
+variable {V : Type*}
+
+/-- Two lanes of entry/exit variables. Lane zero's entry represents the cell's value. -/
+abbrev Cell (V : Type*) := Fin 2 → V × V
+
+/-- All four port values agree with the lane-zero entry. Local cell constraints must provide
+this property; the wire clauses alone do not impose it. -/
+def Cell.Agree (cell : Cell V) (σ : V → Bool) : Prop :=
+  ∀ lane, σ (cell lane).1 = σ (cell 0).1 ∧ σ (cell lane).2 = σ (cell 0).1
+
+/-- Across one gap, lane zero points forward and lane one points backward. -/
+def gapClauses (previous next : Cell V) : CNF V :=
+  [Clause.imp [(previous 0).2] (next 0).1,
+    Clause.imp [(next 1).1] (previous 1).2]
+
+/-- Two opposite implications across every consecutive pair of cells. -/
+def links (cells : List (Cell V)) : CNF V :=
+  cells.consecutivePairs.flatMap fun p => gapClauses p.1 p.2
+
+/-- With local agreement, the two implications equate the neighboring cell values. -/
+theorem eval_gapClauses_iff (σ : V → Bool) (previous next : Cell V)
+    (hp : previous.Agree σ) (hn : next.Agree σ) :
+    (gapClauses previous next).eval σ = true ↔ σ (previous 0).1 = σ (next 0).1 := by
+  simp only [gapClauses, eval_cons, eval_nil, Bool.and_true, Bool.and_eq_true,
+    Clause.eval_imp, List.forall_mem_singleton, (hp 0).2, (hp 1).2, (hn 1).1]
+  cases σ (previous 0).1 <;> cases σ (next 0).1 <;> simp
+
+/-- Under local agreement in every cell, the links hold exactly when consecutive lane-zero
+entries agree. -/
+theorem eval_links_iff (σ : V → Bool) (cells : List (Cell V))
+    (hcells : ∀ c ∈ cells, c.Agree σ) :
+    (links cells).eval σ = true ↔
+      ∀ p ∈ cells.consecutivePairs, σ (p.1 0).1 = σ (p.2 0).1 := by
+  rw [links, eval_flatMap_eq_true_iff]
+  apply forall₂_congr fun p hp => ?_
+  have hm := List.of_mem_zip hp
+  exact eval_gapClauses_iff σ p.1 p.2 (hcells _ hm.1)
+    (hcells _ (List.mem_of_mem_tail hm.2))
+
+/-- Empty wires have no gap clauses. -/
+@[simp] theorem links_nil : links ([] : List (Cell V)) = [] := rfl
+
+/-- A single cell has no gap clauses. -/
+@[simp] theorem links_singleton (cell : Cell V) : links [cell] = [] := rfl
+
+/-- Remove the first gap, leaving the links of the nonempty tail. -/
+theorem links_cons_cons (first next : Cell V) (rest : List (Cell V)) :
+    links (first :: next :: rest) = gapClauses first next ++ links (next :: rest) := rfl
+
+/-- Under local agreement and satisfied links, all entries and exits have the value of the
+first lane-zero entry, including for a singleton wire. -/
+theorem agree_head (σ : V → Bool) (first : Cell V) (rest : List (Cell V))
+    (hcells : ∀ c ∈ first :: rest, c.Agree σ)
+    (hlinks : (links (first :: rest)).eval σ = true) :
+    ∀ c ∈ first :: rest, ∀ lane,
+      σ (c lane).1 = σ (first 0).1 ∧ σ (c lane).2 = σ (first 0).1 := by
+  induction rest generalizing first with
+  | nil =>
+    intro c hc lane
+    rw [List.mem_singleton.1 hc]
+    exact hcells first List.mem_cons_self lane
+  | cons next rest ih =>
+    rw [links_cons_cons, eval_append, Bool.and_eq_true] at hlinks
+    have he := (eval_gapClauses_iff σ first next (hcells _ List.mem_cons_self)
+      (hcells _ (List.mem_cons_of_mem _ List.mem_cons_self))).1 hlinks.1
+    intro c hc lane
+    rcases List.mem_cons.1 hc with he | hc
+    · rw [he]
+      exact hcells first List.mem_cons_self lane
+    · have h := ih next (fun c hc => hcells c (List.mem_cons_of_mem _ hc)) hlinks.2 c hc lane
+      exact ⟨h.1.trans he.symm, h.2.trans he.symm⟩
+
+/-- The head-agreement rule for a list with an explicit nonemptiness hypothesis. The fallback
+only makes `headD` total and does not affect the result. -/
+theorem agree_head_of_ne_nil (σ : V → Bool) (fallback : Cell V) (cells : List (Cell V))
+    (hne : cells ≠ []) (hcells : ∀ c ∈ cells, c.Agree σ)
+    (hlinks : (links cells).eval σ = true) :
+    ∀ c ∈ cells, ∀ lane,
+      σ (c lane).1 = σ (cells.headD fallback 0).1 ∧
+        σ (c lane).2 = σ (cells.headD fallback 0).1 := by
+  cases cells with
+  | nil => exact False.elim (hne rfl)
+  | cons first rest => exact agree_head σ first rest hcells hlinks
+
+/-- A common value on every entry and exit satisfies all paired links. -/
+theorem eval_links_of_constant (σ : V → Bool) (value : Bool) (cells : List (Cell V))
+    (h : ∀ c ∈ cells, ∀ lane, σ (c lane).1 = value ∧ σ (c lane).2 = value) :
+    (links cells).eval σ = true := by
+  have hcells : ∀ c ∈ cells, c.Agree σ := fun c hc lane =>
+    ⟨(h c hc lane).1.trans (h c hc 0).1.symm, (h c hc lane).2.trans (h c hc 0).1.symm⟩
+  apply (eval_links_iff σ cells hcells).2
+  intro p hp
+  have hm := List.of_mem_zip hp
+  exact (h p.1 hm.1 0).1.trans (h p.2 (List.mem_of_mem_tail hm.2) 0).1.symm
+
+/-- There are exactly two clauses per gap. -/
+theorem length_gapClauses (previous next : Cell V) :
+    (gapClauses previous next).length = 2 := rfl
+
+/-- Each gap clause is binary, even if some port variables coincide. -/
+theorem length_of_mem_gapClauses (previous next : Cell V) {c : Clause V}
+    (hc : c ∈ gapClauses previous next) : c.length = 2 := by
+  simp only [gapClauses, List.mem_cons, List.not_mem_nil, or_false] at hc
+  rcases hc with rfl | rfl <;> rfl
+
+/-- A gap contributes four literal positions, counted with multiplicity. -/
+theorem length_vars_gapClauses (previous next : Cell V) :
+    (gapClauses previous next).vars.length = 4 := rfl
+
+/-- There are exactly two clauses for each consecutive pair of cells. -/
+theorem length_links_eq_gaps (cells : List (Cell V)) :
+    (links cells).length = 2 * cells.consecutivePairs.length := by
+  simp [links, List.length_flatMap, length_gapClauses, Nat.mul_comm]
+
+/-- A wire with `n` cells has `2 (n - 1)` clauses, with truncated subtraction for `n = 0`. -/
+theorem length_links (cells : List (Cell V)) :
+    (links cells).length = 2 * (cells.length - 1) := by
+  rw [length_links_eq_gaps]
+  simp [List.consecutivePairs]
+
+/-- Every clause of a paired wire has exactly two literal positions. -/
+theorem length_of_mem_links (cells : List (Cell V)) {c : Clause V}
+    (hc : c ∈ links cells) : c.length = 2 := by
+  obtain ⟨p, _, hc⟩ := List.mem_flatMap.1 hc
+  exact length_of_mem_gapClauses p.1 p.2 hc
+
+/-- Paired links have width at most two. -/
+theorem width_links (cells : List (Cell V)) : ∀ c ∈ links cells, c.length ≤ 2 :=
+  fun _ hc => Nat.le_of_eq (length_of_mem_links cells hc)
+
+/-- There are exactly four literal positions per gap. -/
+theorem length_vars_links (cells : List (Cell V)) :
+    (links cells).vars.length = 4 * (cells.length - 1) := by
+  have h : (links cells).map List.length = List.replicate (links cells).length 2 := by
+    apply List.map_eq_replicate_iff.2
+    exact fun c hc => length_of_mem_links cells hc
+  rw [CNF.length_vars, h]
+  simp [length_links, Nat.mul_right_comm]
+
+end Cslib.Logic.PL.CNF.PairedWire
diff --git a/ComplexityTests/PairedCrossover.lean b/ComplexityTests/PairedCrossover.lean
new file mode 100644
index 000000000..05277fd48
--- /dev/null
+++ b/ComplexityTests/PairedCrossover.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+import Complexity.Logics.Propositional.CNF.Planar.PairedCrossover
+import Mathlib.Data.Fintype.Pi
+import Mathlib.Data.Fintype.Prod
+
+/-! The paired template has exactly four full models, including every internal copy and all
+eight ports. Counting uses the canonical-extension bijection instead of enumerating 57 bits. -/
+
+open Cslib.Logic.PL Cslib.Logic.PL.CNF.PairedCrossover
+
+private def modelsEquivInputs :
+    {σ : Variable → Bool // formula.eval σ = true} ≃ Bool × Bool where
+  toFun σ := (σ.val (terminal 0 0), σ.val (terminal 2 0))
+  invFun ab := ⟨canonicalExtension ab.1 ab.2, eval_canonicalExtension ab.1 ab.2⟩
+  left_inv σ := Subtype.ext (eq_canonicalExtension_of_holds σ.property).symm
+  right_inv _ := rfl
+
+example : Fintype.card {σ : Variable → Bool // formula.eval σ = true} = 4 := by
+  rw [Fintype.card_congr modelsEquivInputs]
+  decide
+
+-- Incoming and outgoing values on distinct lanes still agree across the same wire.
+example {σ : Variable → Bool} (h : formula.eval σ = true) :
+    σ (terminal 0 1) = σ (terminal 1 0) ∧
+      σ (terminal 2 1) = σ (terminal 3 0) := by
+  constructor
+  · exact (terminal_value_of_holds h 0 1).trans (terminal_value_of_holds h 1 0).symm
+  · exact (terminal_value_of_holds h 2 1).trans (terminal_value_of_holds h 3 0).symm
+
+-- The two signals are independent, with all ports populated in this concrete model.
+example : formula.eval (canonicalExtension true false) = true ∧
+    canonicalExtension true false (terminal 1 1) = true ∧
+      canonicalExtension true false (terminal 3 1) = false :=
+  ⟨eval_canonicalExtension true false, rfl, rfl⟩
diff --git a/ComplexityTests/PairedWire.lean b/ComplexityTests/PairedWire.lean
new file mode 100644
index 000000000..b72c10171
--- /dev/null
+++ b/ComplexityTests/PairedWire.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+import Complexity.Logics.Propositional.CNF.Planar.PairedWire
+
+/-! # Paired-wire directions, propagation, and exact sizes -/
+
+open Cslib.Logic.PL Cslib.Logic.PL.CNF.PairedWire
+
+/-- Four distinct variables per cell, with two consecutive variables per lane. -/
+private def cell (index : ℕ) : Cell ℕ :=
+  fun lane => (4 * index + 2 * lane.val, 4 * index + 2 * lane.val + 1)
+
+/-- The opposite clauses use separate lanes, with the prescribed entry/exit directions. -/
+example : gapClauses (cell 0) (cell 1) =
+    [[(1, false), (4, true)], [(6, false), (3, true)]] := rfl
+
+example : (links ([] : List (Cell ℕ))).length = 0 ∧
+    (links ([] : List (Cell ℕ))).vars.length = 0 := by decide
+
+example : (links [cell 0]).length = 0 ∧ (links [cell 0]).vars.length = 0 := by decide
+
+example : (links [cell 0, cell 1, cell 2]).length = 4 ∧
+    (links [cell 0, cell 1, cell 2]).vars.length = 8 := by decide
+
+/-- Counts retain multiplicity even when all port variables coincide. -/
+example : (links [fun _ => (0, 0), fun _ => (0, 0)]).length = 2 ∧
+    (links [fun _ => (0, 0), fun _ => (0, 0)]).vars.length = 4 := by decide
+
+example (value : Bool) : (links [cell 0, cell 1, cell 2]).eval (fun _ => value) = true :=
+  eval_links_of_constant _ value _ (fun _ _ _ => ⟨rfl, rfl⟩)
+
+/-- Local agreement is satisfiable when the two cells have different representative values. -/
+example : ∀ c ∈ [cell 0, cell 1], c.Agree (fun v => decide (v < 4)) := by
+  intro c hc
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+  rcases hc with rfl | rfl <;> unfold Cell.Agree <;> decide
+
+/-- The forward implication excludes a drop from true to false between cells. -/
+example : (links [cell 0, cell 1]).eval (fun v => decide (v < 4)) = false := by decide
+
+/-- The backward implication excludes a rise from false to true between cells. -/
+example : (links [cell 0, cell 1]).eval (fun v => decide (4 ≤ v)) = false := by decide
+
+/-- Links alone allow different representatives when local agreement is absent. -/
+example : (links [cell 0, cell 1]).eval (fun v => v == 4) = true ∧
+    ((cell 0 0).1 == 4) ≠ ((cell 1 0).1 == 4) := by decide
+
+/-- A compiler can recover any terminal port from local cell guarantees and satisfied links. -/
+example (σ : ℕ → Bool) (hcells : ∀ c ∈ [cell 0, cell 1, cell 2], c.Agree σ)
+    (hlinks : (links [cell 0, cell 1, cell 2]).eval σ = true) :
+    σ (cell 2 1).2 = σ (cell 0 0).1 :=
+  (agree_head σ (cell 0) [cell 1, cell 2] hcells hlinks (cell 2) (by simp) 1).2
diff --git a/ComplexityTests/PlanarCrossoverCounting.lean b/ComplexityTests/PlanarCrossoverCounting.lean
new file mode 100644
index 000000000..17167cb9a
--- /dev/null
+++ b/ComplexityTests/PlanarCrossoverCounting.lean
@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+import Complexity.Logics.Propositional.CNF.Planar.CrossoverCounting
+import Mathlib.Data.Fintype.Pi
+import Mathlib.Data.Fintype.Prod
+
+/-! Full satisfying assignments correspond bijectively to the two incoming bits, including
+after splitting. The model counts below use these structural equivalences, not enumeration. -/
+
+open Cslib.Logic.PL Cslib.Logic.PL.CNF.Crossover
+
+private def modelsEquivInputs :
+    {σ : Variable → Bool // formula.eval σ = true} ≃ Bool × Bool where
+  toFun σ := (σ.val .aLeft, σ.val .bTop)
+  invFun ab := ⟨canonicalExtension ab.1 ab.2, eval_canonicalExtension ab.1 ab.2⟩
+  left_inv σ := Subtype.ext (eq_canonicalExtension_of_holds σ.property).symm
+  right_inv _ := rfl
+
+private def splitModelsEquivInputs :
+    {σ : SplitVariable → Bool // splitFormula.eval σ = true} ≃ Bool × Bool where
+  toFun σ := (σ.val .aLeft, σ.val .bTop)
+  invFun ab := ⟨canonicalSplitExtension ab.1 ab.2, eval_canonicalSplitExtension ab.1 ab.2⟩
+  left_inv σ := Subtype.ext (eq_canonicalSplitExtension_of_holds σ.property).symm
+  right_inv _ := rfl
+
+example : Fintype.card {σ : Variable → Bool // formula.eval σ = true} = 4 := by
+  rw [Fintype.card_congr modelsEquivInputs]
+  decide
+
+example : Fintype.card {σ : SplitVariable → Bool // splitFormula.eval σ = true} = 4 := by
+  rw [Fintype.card_congr splitModelsEquivInputs]
+  decide
+
+-- The mixed input has a concrete internal value, common to all six copies.
+example (i : Fin 6) : canonicalSplitExtension false true (.copy .upperLeft i) = true := rfl
+
+-- Changing a free-looking internal value cannot produce another satisfying full assignment.
+example : splitFormula.eval (Function.update (canonicalSplitExtension false true) .center true) =
+    false := by
+  cases h : splitFormula.eval
+      (Function.update (canonicalSplitExtension false true) .center true) with
+  | false => rfl
+  | true =>
+    have heq := eq_canonicalSplitExtension_of_holds h
+    have hcenter := congrFun heq .center
+    simp [canonicalSplitExtension, canonicalExtension, assignment, SplitVariable.origin] at hcenter
diff --git a/references.bib b/references.bib
index 440dac03d..6b32ca500 100644
--- a/references.bib
+++ b/references.bib
@@ -2029,6 +2029,17 @@ @article{Huang2019
   doi       = {10.4007/annals.2019.190.3.6}
 }
 
+@article{HuntMaratheRadhakrishnanStearns1998,
+  author    = {Hunt III, Harry B. and Marathe, Madhav V. and Radhakrishnan, Venkatesh and Stearns, Richard E.},
+  title     = {The Complexity of Planar Counting Problems},
+  journal   = {SIAM Journal on Computing},
+  volume    = {27},
+  number    = {4},
+  pages     = {1142--1167},
+  year      = {1998},
+  doi       = {10.1137/S0097539793304601}
+}
+
 @inproceedings{Ilango2020,
   author    = {Ilango, Rahul},
   title     = {Approaching {MCSP} from Above and Below: Hardness for a Conditional Variant and {$\mathsf{AC}^0[p]$}},