diff --git a/Complexity.lean b/Complexity.lean
index 80ab96083a..538c50259a 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -812,6 +812,9 @@ public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverL
 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.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.Paths
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths.Occupancy
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PolyTime
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean
new file mode 100644
index 0000000000..2b111bc70d
--- /dev/null
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean
@@ -0,0 +1,203 @@
+/-
+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.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutChecks
+public import Complexity.Foundations.Geometry.Orthogonal.Simple
+import Mathlib.Data.List.Zip
+import Mathlib.Tactic.Linarith
+
+/-!
+# Certified continuous orthogonal paired-port crossover
+
+The finite checks for the fixed degree-three CNF template certify entire real supports.
+Its 57 variable vertices and 78 clause vertices are distinct. Its 162 incidence routes are simple,
+orthogonal, avoid nonincident vertices, and meet only at common graph endpoints. Their total
+wire length is 2192. Eight mutually disjoint access routes connect degree-two terminals to the
+boundary of `[0,240]²`, and meet the core only at the corresponding terminal. Each terminal
+therefore accommodates exactly one external clause occurrence.
+
+## Main definitions
+
+This module uses the fixed table from `PairedCrossoverLayoutData` and the shared `Orthogonal` route
+and continuous support semantics.
+
+## Main results
+
+* `Cslib.Logic.PL.CNF.PairedCrossover.incidence_simple`: continuous segment simplicity.
+* `Cslib.Logic.PL.CNF.PairedCrossover.routes_contact`: intersections are common endpoints.
+* `Cslib.Logic.PL.CNF.PairedCrossover.access_contact`: access meets the core only at its terminal.
+* `Cslib.Logic.PL.CNF.PairedCrossover.access_boundary_isolation`: only ports touch the boundary.
+
+## 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 modification and its continuous orthogonal certificates are original.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.CNF.PairedCrossover
+
+open Orthogonal
+
+private theorem support_bounds_of_points {r : Route}
+    (h : ∀ q ∈ r, 20 ≤ q.1 ∧ q.1 ≤ 220 ∧ 20 ≤ q.2 ∧ q.2 ≤ 220)
+    {p : ℝ × ℝ} (hp : p ∈ support r) :
+    20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by
+  have cast_bounds (q : Point) (hq : q ∈ r) :
+      (20 : ℝ) ≤ q.1 ∧ (q.1 : ℝ) ≤ 220 ∧ 20 ≤ (q.2 : ℝ) ∧ (q.2 : ℝ) ≤ 220 := by
+    exact_mod_cast h q hq
+  rcases hp with ⟨q, hq, rfl⟩ | ⟨e, he, hp⟩
+  · exact cast_bounds q hq
+  · have he' := List.of_mem_zip he
+    have ha := cast_bounds e.1 he'.1
+    have hb := cast_bounds e.2 (List.mem_of_mem_tail he'.2)
+    obtain ⟨hx, hy⟩ := mem_segment_bounds hp
+    rw [Set.mem_uIcc] at hx hy
+    have hx' : 20 ≤ p.1 ∧ p.1 ≤ 220 := by
+      rcases hx with hx | hx <;> constructor <;> linarith [ha.1, ha.2.1, hb.1, hb.2.1]
+    have hy' : 20 ≤ p.2 ∧ p.2 ≤ 220 := by
+      rcases hy with hy | hy <;> constructor <;>
+        linarith [ha.2.2.1, ha.2.2.2, hb.2.2.1, hb.2.2.2]
+    exact ⟨hx'.1, hx'.2, hy'.1, hy'.2⟩
+
+/-- Every real point of the core drawing is strictly inside the outer 240-by-240 box. -/
+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 h := support_bounds_of_points (core_bounds e he) hp
+  constructor
+  · linarith [h.1]
+  constructor
+  · linarith [h.2.1]
+  constructor <;> linarith [h.2.2.1, h.2.2.2]
+
+/-- Distinct segments of a route intersect only at their consecutive shared bend. -/
+theorem incidence_simple {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes)
+    {a b : Point × Point} (ha : a ∈ e.2.2.consecutivePairs)
+    (hb : b ∈ e.2.2.consecutivePairs) (hne : a ≠ b)
+    {p : ℝ × ℝ} (hp : p ∈ segment a.1 a.2) (hq : p ∈ segment b.1 b.2) :
+    ∃ q ∈ consecutiveContact a b, p = realPoint q :=
+  segmentContactCheck_sound (incidence_simple_check e he a ha b hb hne) hp hq
+
+/-- Every incidence route is simple in the shared continuous polygonal-route semantics. -/
+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 p hp hq
+  obtain ⟨q, hq, hpq⟩ := incidence_simple he ha hb hne hp hq
+  unfold consecutiveContact at hq
+  split_ifs at hq with h h'
+  · have hqa : q = a.2 := List.mem_singleton.mp hq
+    subst q
+    exact ⟨Or.inr hpq, Or.inl (hpq.trans (congrArg realPoint h))⟩
+  · have hqa : q = a.1 := List.mem_singleton.mp hq
+    subst q
+    exact ⟨Or.inl hpq, Or.inr (hpq.trans (congrArg realPoint h'.symm))⟩
+  · exact False.elim (List.not_mem_nil hq)
+
+/-- Every continuous intersection of distinct incidence routes is a shared graph endpoint. -/
+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
+
+/-- Continuous incidence routes avoid every nonincident variable vertex. -/
+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)
+
+/-- Continuous incidence routes avoid every nonincident clause vertex. -/
+theorem clause_not_mem_support {e : ℕ × Variable × Route}
+    (he : e ∈ incidenceRoutes) {i : Fin 78} (hi : i.val ≠ e.1) :
+    realPoint (clausePosition i) ∉ support e.2.2 :=
+  not_mem_support_of_routeContactCheck (clause_avoidance_check e he i hi)
+
+/-- Every literal incidence appears exactly once in the route list. -/
+theorem incidenceEndpoints_nodup :
+    (incidenceRoutes.map fun e => (e.1, e.2.1)).Nodup := by decide +kernel
+
+/-- Every variable vertex lies in the core rectangle. -/
+theorem variable_bounds : ∀ v, 20 ≤ (variablePosition v).1 ∧ (variablePosition v).1 ≤ 220 ∧
+    20 ≤ (variablePosition v).2 ∧ (variablePosition v).2 ≤ 220 := by decide +kernel
+
+/-- Every clause vertex lies in the core rectangle. -/
+theorem clause_bounds : ∀ p ∈ clausePositions,
+    20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by decide +kernel
+
+/-- Each of the 57 variable names is genuinely used by the fixed formula. -/
+theorem variables_used : ∀ v, v ∈ formula.vars := by decide +kernel
+
+/-- No access route visits any other variable vertex. -/
+theorem access_variable_avoidance_check : ∀ s l v, v ≠ terminal s l →
+    routeContactCheck [] (accessRoute s l) [variablePosition v] = true := by decide +kernel
+
+/-- No access route visits a clause vertex. -/
+theorem access_clause_avoidance_check : ∀ s l, ∀ p ∈ clausePositions,
+    routeContactCheck [] (accessRoute s l) [p] = true := by decide +kernel
+
+/-- The full real access route avoids every other variable vertex. -/
+theorem access_variable_not_mem {s : Fin 4} {l : Fin 2} {v : Variable}
+    (hv : v ≠ terminal s l) :
+    realPoint (variablePosition v) ∉ support (accessRoute s l) :=
+  not_mem_support_of_routeContactCheck (access_variable_avoidance_check s l v hv)
+
+/-- The full real access route avoids every clause vertex. -/
+theorem access_clause_not_mem {s : Fin 4} {l : Fin 2} {p : Point}
+    (hp : p ∈ clausePositions) :
+    realPoint p ∉ support (accessRoute s l) :=
+  not_mem_support_of_routeContactCheck (access_clause_avoidance_check s l p hp)
+
+/-- Each access route has one segment and 20 units of wire length. -/
+theorem access_route_sizes : ∀ s l, (accessRoute s l).consecutivePairs.length = 1 ∧
+    wireLength (accessRoute s l) = 20 := PairedPorts.access_route_sizes
+
+/-- Including all eight accesses gives 415 segments and total wire length 2352. -/
+theorem full_route_sizes :
+    (incidenceRoutes.map fun e => e.2.2.consecutivePairs.length).sum +
+      ((List.finRange 4).flatMap fun s => (List.finRange 2).map fun l =>
+        (accessRoute s l).consecutivePairs.length).sum = 415 ∧
+    (incidenceRoutes.map fun e => wireLength e.2.2).sum +
+      ((List.finRange 4).flatMap fun s => (List.finRange 2).map fun l =>
+        wireLength (accessRoute s l)).sum = 2352 := by
+  rw [route_sizes.1, route_sizes.2]
+  decide +kernel
+
+/-- Each straight access is simple over its full real support. -/
+theorem access_isSimple (s : Fin 4) (l : Fin 2) : IsSimple (accessRoute s l) :=
+  PairedPorts.access_isSimple s l
+
+/-- Distinct accesses have disjoint full real support. -/
+theorem access_disjoint {p q : PairedPorts.Port} (h : p ≠ q) :
+    Disjoint (support (accessRoute p.1 p.2)) (support (accessRoute q.1 q.2)) :=
+  PairedPorts.access_disjoint h
+
+/-- Every continuous contact between an access and the core is its associated port. -/
+theorem access_contact {s : Fin 4} {l : Fin 2} {e : ℕ × Variable × Route}
+    (he : e ∈ incidenceRoutes) {p : ℝ × ℝ}
+    (hp : p ∈ support (accessRoute s l)) (hq : p ∈ support e.2.2) :
+    e.2.1 = terminal s l ∧ p = realPoint (variablePosition (terminal 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 (terminal s l) := List.mem_singleton.mp hq
+    exact ⟨h, hq' ▸ hpq⟩
+  · exact False.elim (List.not_mem_nil hq)
+
+/-- Only the designated boundary point of an access lies on the outer box boundary. -/
+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)) :=
+  PairedPorts.access_boundary_isolation hp
+
+end Cslib.Logic.PL.CNF.PairedCrossover
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean
new file mode 100644
index 0000000000..1f584ab938
--- /dev/null
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean
@@ -0,0 +1,841 @@
+/-
+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.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutData
+public import Complexity.Foundations.Geometry.Orthogonal.Separation
+import Mathlib.Data.List.GetD
+import Mathlib.Data.List.Nodup
+import Mathlib.Data.List.Zip
+import Mathlib.Tactic.FinCases
+
+/-!
+# Finite certificates for the paired-port orthogonal crossover
+
+Finite arithmetic certificates control the full real support of every route. The core has
+57 variable vertices, 78 clause vertices and 162 incidences. Eight mutually disjoint access routes
+connect the signal terminals to the boundary of `[0,240]²`; only the associated terminal may meet
+an access route. An external clause uses this access and the terminal's remaining occurrence.
+
+## Main definitions
+
+* `Cslib.Logic.PL.CNF.PairedCrossover.clausePosition`: indexed positions of clause vertices.
+* `Cslib.Logic.PL.CNF.PairedCrossover.commonEndpoints`: permitted contacts of incidence routes.
+
+## Main results
+
+* `Cslib.Logic.PL.CNF.PairedCrossover.incidenceRoutes_cover`: exact ordinary CNF literal incidences.
+* `Cslib.Logic.PL.CNF.PairedCrossover.routes_contact_check`: finite permitted-contact certificate.
+* `Cslib.Logic.PL.CNF.PairedCrossover.access_contact_check`: finite access isolation certificate.
+
+## 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 modification and its finite orthogonal certificates are original.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.CNF.PairedCrossover
+
+open Orthogonal
+
+/-- The clause position at an index. All indices in `incidenceRoutes` are certified in range. -/
+def clausePosition (i : ℕ) : Point := clausePositions.getD i (0, 0)
+
+/-- Every variable, including both lanes on each side. -/
+def variableList : List Variable :=
+  [.center] ++ (List.finRange 4).flatMap (fun s =>
+    (List.finRange 2).map (Variable.port s)) ++
+    Crossover.internalList.flatMap fun v => List.ofFn fun i : Fin 6 => Variable.copy v i
+
+/-- Every variable is included in the finite drawing vertex list. -/
+theorem mem_variableList : ∀ v, v ∈ variableList := by decide +kernel
+
+/-- The exact literal-incidence list of the ordinary CNF formula. -/
+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
+
+/-- The fixed formula and drawing have 78 clauses and 162 incidences. -/
+theorem drawing_sizes : clausePositions.length = 78 ∧ incidenceRoutes.length = 162 := by
+  decide +kernel
+
+/-- Variable vertices have distinct positions. -/
+theorem variablePosition_injective : Function.Injective variablePosition := by
+  have h : (variableList.map variablePosition).Nodup := by decide +kernel
+  exact fun v w => List.inj_on_of_nodup_map h (mem_variableList v) (mem_variableList w)
+
+/-- Clause vertices are pairwise distinct. -/
+theorem clausePositions_nodup : clausePositions.Nodup := by decide +kernel
+
+/-- No clause vertex is a variable vertex. -/
+theorem variablePosition_not_mem_clauses :
+    ∀ v, variablePosition v ∉ clausePositions := by decide +kernel
+
+/-- The only allowed contacts between two distinct incidence routes are shared graph endpoints. -/
+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 [])
+
+/-- A pair of different segments may meet only at a consecutive shared bend. -/
+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)) ∧
+  IsOrthogonal e.2.2 ∧
+  (∀ p ∈ e.2.2, 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220) ∧
+  e.2.2.Nodup ∧
+  ∀ a ∈ e.2.2.consecutivePairs, ∀ b ∈ e.2.2.consecutivePairs, a ≠ b →
+    segmentContactCheck (consecutiveContact a b) a.1 a.2 b.1 b.2 = true
+
+private instance (e : ℕ × Variable × Route) : Decidable (LocalSpec e) :=
+  inferInstanceAs (Decidable (_ ∧ _))
+
+private def rowCheck (e : ℕ × Variable × Route) : Bool :=
+  decide (LocalSpec e) &&
+  ((incidenceRoutes.all fun f => e == f ||
+      routeContactCheck (commonEndpoints e f) e.2.2 f.2.2) &&
+   ((variableList.all fun v => v == e.2.1 ||
+      routeContactCheck [] e.2.2 [variablePosition v]) &&
+    ((List.finRange 78).all fun i => i.val == e.1 ||
+      routeContactCheck [] e.2.2 [clausePosition i])))
+
+private def routeAt (i : Fin 162) : ℕ × Variable × Route :=
+  incidenceRoutes.getD i (0, .center, [])
+
+-- Separate closed certificates keep kernel reduction memory bounded per incidence row.
+
+private theorem row_0 : rowCheck (routeAt 0) = true := by decide +kernel
+
+private theorem row_1 : rowCheck (routeAt 1) = true := by decide +kernel
+private theorem row_2 : rowCheck (routeAt 2) = true := by decide +kernel
+private theorem row_3 : rowCheck (routeAt 3) = true := by decide +kernel
+private theorem row_4 : rowCheck (routeAt 4) = true := by decide +kernel
+private theorem row_5 : rowCheck (routeAt 5) = true := by decide +kernel
+private theorem row_6 : rowCheck (routeAt 6) = true := by decide +kernel
+private theorem row_7 : rowCheck (routeAt 7) = true := by decide +kernel
+private theorem row_8 : rowCheck (routeAt 8) = true := by decide +kernel
+private theorem row_9 : rowCheck (routeAt 9) = true := by decide +kernel
+private theorem row_10 : rowCheck (routeAt 10) = true := by decide +kernel
+
+private theorem row_11 : rowCheck (routeAt 11) = true := by decide +kernel
+private theorem row_12 : rowCheck (routeAt 12) = true := by decide +kernel
+private theorem row_13 : rowCheck (routeAt 13) = true := by decide +kernel
+private theorem row_14 : rowCheck (routeAt 14) = true := by decide +kernel
+private theorem row_15 : rowCheck (routeAt 15) = true := by decide +kernel
+private theorem row_16 : rowCheck (routeAt 16) = true := by decide +kernel
+private theorem row_17 : rowCheck (routeAt 17) = true := by decide +kernel
+private theorem row_18 : rowCheck (routeAt 18) = true := by decide +kernel
+private theorem row_19 : rowCheck (routeAt 19) = true := by decide +kernel
+private theorem row_20 : rowCheck (routeAt 20) = true := by decide +kernel
+
+private theorem row_21 : rowCheck (routeAt 21) = true := by decide +kernel
+private theorem row_22 : rowCheck (routeAt 22) = true := by decide +kernel
+private theorem row_23 : rowCheck (routeAt 23) = true := by decide +kernel
+private theorem row_24 : rowCheck (routeAt 24) = true := by decide +kernel
+private theorem row_25 : rowCheck (routeAt 25) = true := by decide +kernel
+private theorem row_26 : rowCheck (routeAt 26) = true := by decide +kernel
+private theorem row_27 : rowCheck (routeAt 27) = true := by decide +kernel
+private theorem row_28 : rowCheck (routeAt 28) = true := by decide +kernel
+private theorem row_29 : rowCheck (routeAt 29) = true := by decide +kernel
+private theorem row_30 : rowCheck (routeAt 30) = true := by decide +kernel
+
+private theorem row_31 : rowCheck (routeAt 31) = true := by decide +kernel
+private theorem row_32 : rowCheck (routeAt 32) = true := by decide +kernel
+private theorem row_33 : rowCheck (routeAt 33) = true := by decide +kernel
+private theorem row_34 : rowCheck (routeAt 34) = true := by decide +kernel
+private theorem row_35 : rowCheck (routeAt 35) = true := by decide +kernel
+private theorem row_36 : rowCheck (routeAt 36) = true := by decide +kernel
+private theorem row_37 : rowCheck (routeAt 37) = true := by decide +kernel
+private theorem row_38 : rowCheck (routeAt 38) = true := by decide +kernel
+private theorem row_39 : rowCheck (routeAt 39) = true := by decide +kernel
+private theorem row_40 : rowCheck (routeAt 40) = true := by decide +kernel
+
+private theorem row_41 : rowCheck (routeAt 41) = true := by decide +kernel
+private theorem row_42 : rowCheck (routeAt 42) = true := by decide +kernel
+private theorem row_43 : rowCheck (routeAt 43) = true := by decide +kernel
+private theorem row_44 : rowCheck (routeAt 44) = true := by decide +kernel
+private theorem row_45 : rowCheck (routeAt 45) = true := by decide +kernel
+private theorem row_46 : rowCheck (routeAt 46) = true := by decide +kernel
+private theorem row_47 : rowCheck (routeAt 47) = true := by decide +kernel
+private theorem row_48 : rowCheck (routeAt 48) = true := by decide +kernel
+private theorem row_49 : rowCheck (routeAt 49) = true := by decide +kernel
+private theorem row_50 : rowCheck (routeAt 50) = true := by decide +kernel
+
+private theorem row_51 : rowCheck (routeAt 51) = true := by decide +kernel
+private theorem row_52 : rowCheck (routeAt 52) = true := by decide +kernel
+private theorem row_53 : rowCheck (routeAt 53) = true := by decide +kernel
+private theorem row_54 : rowCheck (routeAt 54) = true := by decide +kernel
+private theorem row_55 : rowCheck (routeAt 55) = true := by decide +kernel
+private theorem row_56 : rowCheck (routeAt 56) = true := by decide +kernel
+private theorem row_57 : rowCheck (routeAt 57) = true := by decide +kernel
+private theorem row_58 : rowCheck (routeAt 58) = true := by decide +kernel
+private theorem row_59 : rowCheck (routeAt 59) = true := by decide +kernel
+private theorem row_60 : rowCheck (routeAt 60) = true := by decide +kernel
+
+private theorem row_61 : rowCheck (routeAt 61) = true := by decide +kernel
+private theorem row_62 : rowCheck (routeAt 62) = true := by decide +kernel
+private theorem row_63 : rowCheck (routeAt 63) = true := by decide +kernel
+private theorem row_64 : rowCheck (routeAt 64) = true := by decide +kernel
+private theorem row_65 : rowCheck (routeAt 65) = true := by decide +kernel
+private theorem row_66 : rowCheck (routeAt 66) = true := by decide +kernel
+private theorem row_67 : rowCheck (routeAt 67) = true := by decide +kernel
+private theorem row_68 : rowCheck (routeAt 68) = true := by decide +kernel
+private theorem row_69 : rowCheck (routeAt 69) = true := by decide +kernel
+private theorem row_70 : rowCheck (routeAt 70) = true := by decide +kernel
+
+private theorem row_71 : rowCheck (routeAt 71) = true := by decide +kernel
+private theorem row_72 : rowCheck (routeAt 72) = true := by decide +kernel
+private theorem row_73 : rowCheck (routeAt 73) = true := by decide +kernel
+private theorem row_74 : rowCheck (routeAt 74) = true := by decide +kernel
+private theorem row_75 : rowCheck (routeAt 75) = true := by decide +kernel
+private theorem row_76 : rowCheck (routeAt 76) = true := by decide +kernel
+private theorem row_77 : rowCheck (routeAt 77) = true := by decide +kernel
+private theorem row_78 : rowCheck (routeAt 78) = true := by decide +kernel
+private theorem row_79 : rowCheck (routeAt 79) = true := by decide +kernel
+private theorem row_80 : rowCheck (routeAt 80) = true := by decide +kernel
+
+private theorem row_81 : rowCheck (routeAt 81) = true := by decide +kernel
+private theorem row_82 : rowCheck (routeAt 82) = true := by decide +kernel
+private theorem row_83 : rowCheck (routeAt 83) = true := by decide +kernel
+private theorem row_84 : rowCheck (routeAt 84) = true := by decide +kernel
+private theorem row_85 : rowCheck (routeAt 85) = true := by decide +kernel
+private theorem row_86 : rowCheck (routeAt 86) = true := by decide +kernel
+private theorem row_87 : rowCheck (routeAt 87) = true := by decide +kernel
+private theorem row_88 : rowCheck (routeAt 88) = true := by decide +kernel
+private theorem row_89 : rowCheck (routeAt 89) = true := by decide +kernel
+private theorem row_90 : rowCheck (routeAt 90) = true := by decide +kernel
+
+private theorem row_91 : rowCheck (routeAt 91) = true := by decide +kernel
+private theorem row_92 : rowCheck (routeAt 92) = true := by decide +kernel
+private theorem row_93 : rowCheck (routeAt 93) = true := by decide +kernel
+private theorem row_94 : rowCheck (routeAt 94) = true := by decide +kernel
+private theorem row_95 : rowCheck (routeAt 95) = true := by decide +kernel
+private theorem row_96 : rowCheck (routeAt 96) = true := by decide +kernel
+private theorem row_97 : rowCheck (routeAt 97) = true := by decide +kernel
+private theorem row_98 : rowCheck (routeAt 98) = true := by decide +kernel
+private theorem row_99 : rowCheck (routeAt 99) = true := by decide +kernel
+private theorem row_100 : rowCheck (routeAt 100) = true := by decide +kernel
+
+private theorem row_101 : rowCheck (routeAt 101) = true := by decide +kernel
+private theorem row_102 : rowCheck (routeAt 102) = true := by decide +kernel
+private theorem row_103 : rowCheck (routeAt 103) = true := by decide +kernel
+private theorem row_104 : rowCheck (routeAt 104) = true := by decide +kernel
+private theorem row_105 : rowCheck (routeAt 105) = true := by decide +kernel
+private theorem row_106 : rowCheck (routeAt 106) = true := by decide +kernel
+private theorem row_107 : rowCheck (routeAt 107) = true := by decide +kernel
+private theorem row_108 : rowCheck (routeAt 108) = true := by decide +kernel
+private theorem row_109 : rowCheck (routeAt 109) = true := by decide +kernel
+private theorem row_110 : rowCheck (routeAt 110) = true := by decide +kernel
+
+private theorem row_111 : rowCheck (routeAt 111) = true := by decide +kernel
+private theorem row_112 : rowCheck (routeAt 112) = true := by decide +kernel
+private theorem row_113 : rowCheck (routeAt 113) = true := by decide +kernel
+private theorem row_114 : rowCheck (routeAt 114) = true := by decide +kernel
+private theorem row_115 : rowCheck (routeAt 115) = true := by decide +kernel
+private theorem row_116 : rowCheck (routeAt 116) = true := by decide +kernel
+private theorem row_117 : rowCheck (routeAt 117) = true := by decide +kernel
+private theorem row_118 : rowCheck (routeAt 118) = true := by decide +kernel
+private theorem row_119 : rowCheck (routeAt 119) = true := by decide +kernel
+private theorem row_120 : rowCheck (routeAt 120) = true := by decide +kernel
+
+private theorem row_121 : rowCheck (routeAt 121) = true := by decide +kernel
+private theorem row_122 : rowCheck (routeAt 122) = true := by decide +kernel
+private theorem row_123 : rowCheck (routeAt 123) = true := by decide +kernel
+private theorem row_124 : rowCheck (routeAt 124) = true := by decide +kernel
+private theorem row_125 : rowCheck (routeAt 125) = true := by decide +kernel
+private theorem row_126 : rowCheck (routeAt 126) = true := by decide +kernel
+private theorem row_127 : rowCheck (routeAt 127) = true := by decide +kernel
+private theorem row_128 : rowCheck (routeAt 128) = true := by decide +kernel
+private theorem row_129 : rowCheck (routeAt 129) = true := by decide +kernel
+private theorem row_130 : rowCheck (routeAt 130) = true := by decide +kernel
+
+private theorem row_131 : rowCheck (routeAt 131) = true := by decide +kernel
+private theorem row_132 : rowCheck (routeAt 132) = true := by decide +kernel
+private theorem row_133 : rowCheck (routeAt 133) = true := by decide +kernel
+private theorem row_134 : rowCheck (routeAt 134) = true := by decide +kernel
+private theorem row_135 : rowCheck (routeAt 135) = true := by decide +kernel
+private theorem row_136 : rowCheck (routeAt 136) = true := by decide +kernel
+private theorem row_137 : rowCheck (routeAt 137) = true := by decide +kernel
+private theorem row_138 : rowCheck (routeAt 138) = true := by decide +kernel
+private theorem row_139 : rowCheck (routeAt 139) = true := by decide +kernel
+private theorem row_140 : rowCheck (routeAt 140) = true := by decide +kernel
+
+private theorem row_141 : rowCheck (routeAt 141) = true := by decide +kernel
+private theorem row_142 : rowCheck (routeAt 142) = true := by decide +kernel
+private theorem row_143 : rowCheck (routeAt 143) = true := by decide +kernel
+private theorem row_144 : rowCheck (routeAt 144) = true := by decide +kernel
+private theorem row_145 : rowCheck (routeAt 145) = true := by decide +kernel
+private theorem row_146 : rowCheck (routeAt 146) = true := by decide +kernel
+private theorem row_147 : rowCheck (routeAt 147) = true := by decide +kernel
+private theorem row_148 : rowCheck (routeAt 148) = true := by decide +kernel
+private theorem row_149 : rowCheck (routeAt 149) = true := by decide +kernel
+private theorem row_150 : rowCheck (routeAt 150) = true := by decide +kernel
+
+private theorem row_151 : rowCheck (routeAt 151) = true := by decide +kernel
+private theorem row_152 : rowCheck (routeAt 152) = true := by decide +kernel
+private theorem row_153 : rowCheck (routeAt 153) = true := by decide +kernel
+
+private theorem row_154 : rowCheck (routeAt 154) = true := by decide +kernel
+private theorem row_155 : rowCheck (routeAt 155) = true := by decide +kernel
+private theorem row_156 : rowCheck (routeAt 156) = true := by decide +kernel
+private theorem row_157 : rowCheck (routeAt 157) = true := by decide +kernel
+private theorem row_158 : rowCheck (routeAt 158) = true := by decide +kernel
+private theorem row_159 : rowCheck (routeAt 159) = true := by decide +kernel
+private theorem row_160 : rowCheck (routeAt 160) = true := by decide +kernel
+private theorem row_161 : rowCheck (routeAt 161) = true := by decide +kernel
+
+-- Keep dispatch proofs small as well as the individual kernel certificates. In particular,
+-- no theorem elaborates the full 162-case split: six rows form a block, then 27 blocks cover all.
+private def blockIndex (q : Fin 27) (r : Fin 6) : Fin 162 :=
+  ⟨q.val * 6 + r.val, by omega⟩
+
+private theorem block_0 (r : Fin 6) : rowCheck (routeAt (blockIndex 0 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (0 : Fin 162)
+    exact row_0
+  · conv_lhs => arg 1; arg 1; change (1 : Fin 162)
+    exact row_1
+  · conv_lhs => arg 1; arg 1; change (2 : Fin 162)
+    exact row_2
+  · conv_lhs => arg 1; arg 1; change (3 : Fin 162)
+    exact row_3
+  · conv_lhs => arg 1; arg 1; change (4 : Fin 162)
+    exact row_4
+  · conv_lhs => arg 1; arg 1; change (5 : Fin 162)
+    exact row_5
+
+private theorem block_1 (r : Fin 6) : rowCheck (routeAt (blockIndex 1 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (6 : Fin 162)
+    exact row_6
+  · conv_lhs => arg 1; arg 1; change (7 : Fin 162)
+    exact row_7
+  · conv_lhs => arg 1; arg 1; change (8 : Fin 162)
+    exact row_8
+  · conv_lhs => arg 1; arg 1; change (9 : Fin 162)
+    exact row_9
+  · conv_lhs => arg 1; arg 1; change (10 : Fin 162)
+    exact row_10
+  · conv_lhs => arg 1; arg 1; change (11 : Fin 162)
+    exact row_11
+
+private theorem block_2 (r : Fin 6) : rowCheck (routeAt (blockIndex 2 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (12 : Fin 162)
+    exact row_12
+  · conv_lhs => arg 1; arg 1; change (13 : Fin 162)
+    exact row_13
+  · conv_lhs => arg 1; arg 1; change (14 : Fin 162)
+    exact row_14
+  · conv_lhs => arg 1; arg 1; change (15 : Fin 162)
+    exact row_15
+  · conv_lhs => arg 1; arg 1; change (16 : Fin 162)
+    exact row_16
+  · conv_lhs => arg 1; arg 1; change (17 : Fin 162)
+    exact row_17
+
+private theorem block_3 (r : Fin 6) : rowCheck (routeAt (blockIndex 3 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (18 : Fin 162)
+    exact row_18
+  · conv_lhs => arg 1; arg 1; change (19 : Fin 162)
+    exact row_19
+  · conv_lhs => arg 1; arg 1; change (20 : Fin 162)
+    exact row_20
+  · conv_lhs => arg 1; arg 1; change (21 : Fin 162)
+    exact row_21
+  · conv_lhs => arg 1; arg 1; change (22 : Fin 162)
+    exact row_22
+  · conv_lhs => arg 1; arg 1; change (23 : Fin 162)
+    exact row_23
+
+private theorem block_4 (r : Fin 6) : rowCheck (routeAt (blockIndex 4 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (24 : Fin 162)
+    exact row_24
+  · conv_lhs => arg 1; arg 1; change (25 : Fin 162)
+    exact row_25
+  · conv_lhs => arg 1; arg 1; change (26 : Fin 162)
+    exact row_26
+  · conv_lhs => arg 1; arg 1; change (27 : Fin 162)
+    exact row_27
+  · conv_lhs => arg 1; arg 1; change (28 : Fin 162)
+    exact row_28
+  · conv_lhs => arg 1; arg 1; change (29 : Fin 162)
+    exact row_29
+
+private theorem block_5 (r : Fin 6) : rowCheck (routeAt (blockIndex 5 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (30 : Fin 162)
+    exact row_30
+  · conv_lhs => arg 1; arg 1; change (31 : Fin 162)
+    exact row_31
+  · conv_lhs => arg 1; arg 1; change (32 : Fin 162)
+    exact row_32
+  · conv_lhs => arg 1; arg 1; change (33 : Fin 162)
+    exact row_33
+  · conv_lhs => arg 1; arg 1; change (34 : Fin 162)
+    exact row_34
+  · conv_lhs => arg 1; arg 1; change (35 : Fin 162)
+    exact row_35
+
+private theorem block_6 (r : Fin 6) : rowCheck (routeAt (blockIndex 6 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (36 : Fin 162)
+    exact row_36
+  · conv_lhs => arg 1; arg 1; change (37 : Fin 162)
+    exact row_37
+  · conv_lhs => arg 1; arg 1; change (38 : Fin 162)
+    exact row_38
+  · conv_lhs => arg 1; arg 1; change (39 : Fin 162)
+    exact row_39
+  · conv_lhs => arg 1; arg 1; change (40 : Fin 162)
+    exact row_40
+  · conv_lhs => arg 1; arg 1; change (41 : Fin 162)
+    exact row_41
+
+private theorem block_7 (r : Fin 6) : rowCheck (routeAt (blockIndex 7 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (42 : Fin 162)
+    exact row_42
+  · conv_lhs => arg 1; arg 1; change (43 : Fin 162)
+    exact row_43
+  · conv_lhs => arg 1; arg 1; change (44 : Fin 162)
+    exact row_44
+  · conv_lhs => arg 1; arg 1; change (45 : Fin 162)
+    exact row_45
+  · conv_lhs => arg 1; arg 1; change (46 : Fin 162)
+    exact row_46
+  · conv_lhs => arg 1; arg 1; change (47 : Fin 162)
+    exact row_47
+
+private theorem block_8 (r : Fin 6) : rowCheck (routeAt (blockIndex 8 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (48 : Fin 162)
+    exact row_48
+  · conv_lhs => arg 1; arg 1; change (49 : Fin 162)
+    exact row_49
+  · conv_lhs => arg 1; arg 1; change (50 : Fin 162)
+    exact row_50
+  · conv_lhs => arg 1; arg 1; change (51 : Fin 162)
+    exact row_51
+  · conv_lhs => arg 1; arg 1; change (52 : Fin 162)
+    exact row_52
+  · conv_lhs => arg 1; arg 1; change (53 : Fin 162)
+    exact row_53
+
+private theorem block_9 (r : Fin 6) : rowCheck (routeAt (blockIndex 9 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (54 : Fin 162)
+    exact row_54
+  · conv_lhs => arg 1; arg 1; change (55 : Fin 162)
+    exact row_55
+  · conv_lhs => arg 1; arg 1; change (56 : Fin 162)
+    exact row_56
+  · conv_lhs => arg 1; arg 1; change (57 : Fin 162)
+    exact row_57
+  · conv_lhs => arg 1; arg 1; change (58 : Fin 162)
+    exact row_58
+  · conv_lhs => arg 1; arg 1; change (59 : Fin 162)
+    exact row_59
+
+private theorem block_10 (r : Fin 6) : rowCheck (routeAt (blockIndex 10 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (60 : Fin 162)
+    exact row_60
+  · conv_lhs => arg 1; arg 1; change (61 : Fin 162)
+    exact row_61
+  · conv_lhs => arg 1; arg 1; change (62 : Fin 162)
+    exact row_62
+  · conv_lhs => arg 1; arg 1; change (63 : Fin 162)
+    exact row_63
+  · conv_lhs => arg 1; arg 1; change (64 : Fin 162)
+    exact row_64
+  · conv_lhs => arg 1; arg 1; change (65 : Fin 162)
+    exact row_65
+
+private theorem block_11 (r : Fin 6) : rowCheck (routeAt (blockIndex 11 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (66 : Fin 162)
+    exact row_66
+  · conv_lhs => arg 1; arg 1; change (67 : Fin 162)
+    exact row_67
+  · conv_lhs => arg 1; arg 1; change (68 : Fin 162)
+    exact row_68
+  · conv_lhs => arg 1; arg 1; change (69 : Fin 162)
+    exact row_69
+  · conv_lhs => arg 1; arg 1; change (70 : Fin 162)
+    exact row_70
+  · conv_lhs => arg 1; arg 1; change (71 : Fin 162)
+    exact row_71
+
+private theorem block_12 (r : Fin 6) : rowCheck (routeAt (blockIndex 12 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (72 : Fin 162)
+    exact row_72
+  · conv_lhs => arg 1; arg 1; change (73 : Fin 162)
+    exact row_73
+  · conv_lhs => arg 1; arg 1; change (74 : Fin 162)
+    exact row_74
+  · conv_lhs => arg 1; arg 1; change (75 : Fin 162)
+    exact row_75
+  · conv_lhs => arg 1; arg 1; change (76 : Fin 162)
+    exact row_76
+  · conv_lhs => arg 1; arg 1; change (77 : Fin 162)
+    exact row_77
+
+private theorem block_13 (r : Fin 6) : rowCheck (routeAt (blockIndex 13 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (78 : Fin 162)
+    exact row_78
+  · conv_lhs => arg 1; arg 1; change (79 : Fin 162)
+    exact row_79
+  · conv_lhs => arg 1; arg 1; change (80 : Fin 162)
+    exact row_80
+  · conv_lhs => arg 1; arg 1; change (81 : Fin 162)
+    exact row_81
+  · conv_lhs => arg 1; arg 1; change (82 : Fin 162)
+    exact row_82
+  · conv_lhs => arg 1; arg 1; change (83 : Fin 162)
+    exact row_83
+
+private theorem block_14 (r : Fin 6) : rowCheck (routeAt (blockIndex 14 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (84 : Fin 162)
+    exact row_84
+  · conv_lhs => arg 1; arg 1; change (85 : Fin 162)
+    exact row_85
+  · conv_lhs => arg 1; arg 1; change (86 : Fin 162)
+    exact row_86
+  · conv_lhs => arg 1; arg 1; change (87 : Fin 162)
+    exact row_87
+  · conv_lhs => arg 1; arg 1; change (88 : Fin 162)
+    exact row_88
+  · conv_lhs => arg 1; arg 1; change (89 : Fin 162)
+    exact row_89
+
+private theorem block_15 (r : Fin 6) : rowCheck (routeAt (blockIndex 15 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (90 : Fin 162)
+    exact row_90
+  · conv_lhs => arg 1; arg 1; change (91 : Fin 162)
+    exact row_91
+  · conv_lhs => arg 1; arg 1; change (92 : Fin 162)
+    exact row_92
+  · conv_lhs => arg 1; arg 1; change (93 : Fin 162)
+    exact row_93
+  · conv_lhs => arg 1; arg 1; change (94 : Fin 162)
+    exact row_94
+  · conv_lhs => arg 1; arg 1; change (95 : Fin 162)
+    exact row_95
+
+private theorem block_16 (r : Fin 6) : rowCheck (routeAt (blockIndex 16 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (96 : Fin 162)
+    exact row_96
+  · conv_lhs => arg 1; arg 1; change (97 : Fin 162)
+    exact row_97
+  · conv_lhs => arg 1; arg 1; change (98 : Fin 162)
+    exact row_98
+  · conv_lhs => arg 1; arg 1; change (99 : Fin 162)
+    exact row_99
+  · conv_lhs => arg 1; arg 1; change (100 : Fin 162)
+    exact row_100
+  · conv_lhs => arg 1; arg 1; change (101 : Fin 162)
+    exact row_101
+
+private theorem block_17 (r : Fin 6) : rowCheck (routeAt (blockIndex 17 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (102 : Fin 162)
+    exact row_102
+  · conv_lhs => arg 1; arg 1; change (103 : Fin 162)
+    exact row_103
+  · conv_lhs => arg 1; arg 1; change (104 : Fin 162)
+    exact row_104
+  · conv_lhs => arg 1; arg 1; change (105 : Fin 162)
+    exact row_105
+  · conv_lhs => arg 1; arg 1; change (106 : Fin 162)
+    exact row_106
+  · conv_lhs => arg 1; arg 1; change (107 : Fin 162)
+    exact row_107
+
+private theorem block_18 (r : Fin 6) : rowCheck (routeAt (blockIndex 18 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (108 : Fin 162)
+    exact row_108
+  · conv_lhs => arg 1; arg 1; change (109 : Fin 162)
+    exact row_109
+  · conv_lhs => arg 1; arg 1; change (110 : Fin 162)
+    exact row_110
+  · conv_lhs => arg 1; arg 1; change (111 : Fin 162)
+    exact row_111
+  · conv_lhs => arg 1; arg 1; change (112 : Fin 162)
+    exact row_112
+  · conv_lhs => arg 1; arg 1; change (113 : Fin 162)
+    exact row_113
+
+private theorem block_19 (r : Fin 6) : rowCheck (routeAt (blockIndex 19 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (114 : Fin 162)
+    exact row_114
+  · conv_lhs => arg 1; arg 1; change (115 : Fin 162)
+    exact row_115
+  · conv_lhs => arg 1; arg 1; change (116 : Fin 162)
+    exact row_116
+  · conv_lhs => arg 1; arg 1; change (117 : Fin 162)
+    exact row_117
+  · conv_lhs => arg 1; arg 1; change (118 : Fin 162)
+    exact row_118
+  · conv_lhs => arg 1; arg 1; change (119 : Fin 162)
+    exact row_119
+
+private theorem block_20 (r : Fin 6) : rowCheck (routeAt (blockIndex 20 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (120 : Fin 162)
+    exact row_120
+  · conv_lhs => arg 1; arg 1; change (121 : Fin 162)
+    exact row_121
+  · conv_lhs => arg 1; arg 1; change (122 : Fin 162)
+    exact row_122
+  · conv_lhs => arg 1; arg 1; change (123 : Fin 162)
+    exact row_123
+  · conv_lhs => arg 1; arg 1; change (124 : Fin 162)
+    exact row_124
+  · conv_lhs => arg 1; arg 1; change (125 : Fin 162)
+    exact row_125
+
+private theorem block_21 (r : Fin 6) : rowCheck (routeAt (blockIndex 21 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (126 : Fin 162)
+    exact row_126
+  · conv_lhs => arg 1; arg 1; change (127 : Fin 162)
+    exact row_127
+  · conv_lhs => arg 1; arg 1; change (128 : Fin 162)
+    exact row_128
+  · conv_lhs => arg 1; arg 1; change (129 : Fin 162)
+    exact row_129
+  · conv_lhs => arg 1; arg 1; change (130 : Fin 162)
+    exact row_130
+  · conv_lhs => arg 1; arg 1; change (131 : Fin 162)
+    exact row_131
+
+private theorem block_22 (r : Fin 6) : rowCheck (routeAt (blockIndex 22 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (132 : Fin 162)
+    exact row_132
+  · conv_lhs => arg 1; arg 1; change (133 : Fin 162)
+    exact row_133
+  · conv_lhs => arg 1; arg 1; change (134 : Fin 162)
+    exact row_134
+  · conv_lhs => arg 1; arg 1; change (135 : Fin 162)
+    exact row_135
+  · conv_lhs => arg 1; arg 1; change (136 : Fin 162)
+    exact row_136
+  · conv_lhs => arg 1; arg 1; change (137 : Fin 162)
+    exact row_137
+
+private theorem block_23 (r : Fin 6) : rowCheck (routeAt (blockIndex 23 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (138 : Fin 162)
+    exact row_138
+  · conv_lhs => arg 1; arg 1; change (139 : Fin 162)
+    exact row_139
+  · conv_lhs => arg 1; arg 1; change (140 : Fin 162)
+    exact row_140
+  · conv_lhs => arg 1; arg 1; change (141 : Fin 162)
+    exact row_141
+  · conv_lhs => arg 1; arg 1; change (142 : Fin 162)
+    exact row_142
+  · conv_lhs => arg 1; arg 1; change (143 : Fin 162)
+    exact row_143
+
+private theorem block_24 (r : Fin 6) : rowCheck (routeAt (blockIndex 24 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (144 : Fin 162)
+    exact row_144
+  · conv_lhs => arg 1; arg 1; change (145 : Fin 162)
+    exact row_145
+  · conv_lhs => arg 1; arg 1; change (146 : Fin 162)
+    exact row_146
+  · conv_lhs => arg 1; arg 1; change (147 : Fin 162)
+    exact row_147
+  · conv_lhs => arg 1; arg 1; change (148 : Fin 162)
+    exact row_148
+  · conv_lhs => arg 1; arg 1; change (149 : Fin 162)
+    exact row_149
+
+private theorem block_25 (r : Fin 6) : rowCheck (routeAt (blockIndex 25 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (150 : Fin 162)
+    exact row_150
+  · conv_lhs => arg 1; arg 1; change (151 : Fin 162)
+    exact row_151
+  · conv_lhs => arg 1; arg 1; change (152 : Fin 162)
+    exact row_152
+  · conv_lhs => arg 1; arg 1; change (153 : Fin 162)
+    exact row_153
+  · conv_lhs => arg 1; arg 1; change (154 : Fin 162)
+    exact row_154
+  · conv_lhs => arg 1; arg 1; change (155 : Fin 162)
+    exact row_155
+
+private theorem block_26 (r : Fin 6) : rowCheck (routeAt (blockIndex 26 r)) = true := by
+  fin_cases r
+  · conv_lhs => arg 1; arg 1; change (156 : Fin 162)
+    exact row_156
+  · conv_lhs => arg 1; arg 1; change (157 : Fin 162)
+    exact row_157
+  · conv_lhs => arg 1; arg 1; change (158 : Fin 162)
+    exact row_158
+  · conv_lhs => arg 1; arg 1; change (159 : Fin 162)
+    exact row_159
+  · conv_lhs => arg 1; arg 1; change (160 : Fin 162)
+    exact row_160
+  · conv_lhs => arg 1; arg 1; change (161 : Fin 162)
+    exact row_161
+
+private theorem blocks_checked (q : Fin 27) (r : Fin 6) :
+    rowCheck (routeAt (blockIndex q r)) = true := by
+  fin_cases q
+  · exact block_0 r
+  · exact block_1 r
+  · exact block_2 r
+  · exact block_3 r
+  · exact block_4 r
+  · exact block_5 r
+  · exact block_6 r
+  · exact block_7 r
+  · exact block_8 r
+  · exact block_9 r
+  · exact block_10 r
+  · exact block_11 r
+  · exact block_12 r
+  · exact block_13 r
+  · exact block_14 r
+  · exact block_15 r
+  · exact block_16 r
+  · exact block_17 r
+  · exact block_18 r
+  · exact block_19 r
+  · exact block_20 r
+  · exact block_21 r
+  · exact block_22 r
+  · exact block_23 r
+  · exact block_24 r
+  · exact block_25 r
+  · exact block_26 r
+
+private theorem rows_checked (i : Fin 162) : rowCheck (routeAt i) = true := by
+  let q : Fin 27 := ⟨i.val / 6, by omega⟩
+  let r : Fin 6 := ⟨i.val % 6, by omega⟩
+  have heq : blockIndex q r = i := by
+    apply Fin.ext
+    simp only [blockIndex, q, r]
+    omega
+  have h := blocks_checked q r
+  rwa [heq] at h
+
+private theorem row_checked (e : ℕ × Variable × Route) (he : e ∈ incidenceRoutes) :
+    rowCheck e = true := by
+  obtain ⟨i, rfl⟩ := List.mem_iff_get.mp he
+  have hi : i.val < 162 := by simpa only [drawing_sizes.2] using i.isLt
+  have h := rows_checked ⟨i.val, hi⟩
+  have heq : routeAt ⟨i.val, hi⟩ = incidenceRoutes.get i :=
+    List.getD_eq_get incidenceRoutes (0, .center, []) i
+  rwa [heq] at h
+
+private theorem local_checked (e : ℕ × Variable × Route) (he : e ∈ incidenceRoutes) :
+    LocalSpec e := by
+  have h := row_checked e he
+  simp only [rowCheck, Bool.and_eq_true, decide_eq_true_eq] at h
+  exact h.1
+
+/-- Every route starts at its clause and ends at its variable, with a valid clause index. -/
+theorem incidence_endpoints : ∀ e ∈ incidenceRoutes,
+    e.1 < 78 ∧ e.2.2.head? = some (clausePosition e.1) ∧
+      e.2.2.getLast? = some (variablePosition e.2.1) :=
+  fun e he => (local_checked e he).1
+
+/-- All incidence routes have proper axis-aligned segments. -/
+theorem incidence_orthogonal :
+    ∀ e ∈ incidenceRoutes, IsOrthogonal e.2.2 :=
+  fun e he => (local_checked e he).2.1
+
+/-- All listed core points are inside the smaller rectangle `[20,220]²`. -/
+theorem core_bounds : ∀ e ∈ incidenceRoutes, ∀ p ∈ e.2.2,
+    20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 :=
+  fun e he => (local_checked e he).2.2.1
+
+/-- Exactly 407 proper segments and 2192 units of total Manhattan wire length. -/
+theorem route_sizes :
+    (incidenceRoutes.map fun e => e.2.2.consecutivePairs.length).sum = 407 ∧
+      (incidenceRoutes.map fun e => wireLength e.2.2).sum = 2192 := by decide +kernel
+
+/-- Every incidence route lists each bend only once. -/
+theorem incidence_points_nodup : ∀ e ∈ incidenceRoutes, e.2.2.Nodup :=
+  fun e he => (local_checked e he).2.2.2.1
+
+/-- Finite simplicity certificate: distinct segments are disjoint except at a shared next bend. -/
+theorem incidence_simple_check : ∀ e ∈ incidenceRoutes,
+    ∀ a ∈ e.2.2.consecutivePairs, ∀ b ∈ e.2.2.consecutivePairs, a ≠ b →
+      segmentContactCheck (consecutiveContact a b) a.1 a.2 b.1 b.2 = true :=
+  fun e he => (local_checked e he).2.2.2.2
+
+/-- Exhaustive finite contact certificate for the fixed route table. -/
+theorem routes_contact_check : ∀ e ∈ incidenceRoutes, ∀ f ∈ incidenceRoutes,
+    e ≠ f → routeContactCheck (commonEndpoints e f) e.2.2 f.2.2 = true := by
+  intro e he f hf hne
+  have h := row_checked e he
+  simp only [rowCheck, Bool.and_eq_true] at h
+  have hf' := List.all_eq_true.mp h.2.1 f hf
+  simpa only [Bool.or_eq_true, beq_iff_eq, hne, false_or] using hf'
+
+/-- No route visits a nonincident variable vertex. -/
+theorem variable_avoidance_check : ∀ e ∈ incidenceRoutes, ∀ v,
+    v ≠ e.2.1 → routeContactCheck [] e.2.2 [variablePosition v] = true := by
+  intro e he v hv
+  have h := row_checked e he
+  simp only [rowCheck, Bool.and_eq_true] at h
+  have hv' := List.all_eq_true.mp h.2.2.1 v (mem_variableList v)
+  simpa only [Bool.or_eq_true, beq_iff_eq, hv, false_or] using hv'
+
+/-- No route visits a nonincident clause vertex. -/
+theorem clause_avoidance_check : ∀ e ∈ incidenceRoutes, ∀ i : Fin 78,
+    i.val ≠ e.1 → routeContactCheck [] e.2.2 [clausePosition i] = true := by
+  intro e he i hi
+  have h := row_checked e he
+  simp only [rowCheck, Bool.and_eq_true] at h
+  have hi' := List.all_eq_true.mp h.2.2.2 i (List.mem_finRange i)
+  simpa only [Bool.or_eq_true, beq_iff_eq, hi, false_or] using hi'
+
+/-- All eight access routes have their prescribed endpoints and proper orthogonal segments. -/
+theorem access_endpoints : ∀ s l, IsOrthogonal (accessRoute s l) ∧
+    (accessRoute s l).head? = some (boundaryPort s l) ∧
+      (accessRoute s l).getLast? = some (variablePosition (terminal s l)) := by decide +kernel
+
+/-- The eight access routes are mutually disjoint. -/
+theorem access_disjoint_check : ∀ p q : PairedPorts.Port, p ≠ q →
+    routeContactCheck [] (accessRoute p.1 p.2) (accessRoute q.1 q.2) = true :=
+  PairedPorts.access_disjoint_check
+
+/-- Access to a port can meet an incidence route only at that port. -/
+theorem access_contact_check : ∀ s l, ∀ e ∈ incidenceRoutes,
+    routeContactCheck (if e.2.1 = terminal s l then [variablePosition (terminal s l)] else [])
+      (accessRoute s l) e.2.2 = true := by decide +kernel
+
+end Cslib.Logic.PL.CNF.PairedCrossover
diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutData.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutData.lean
new file mode 100644
index 0000000000..f97d125606
--- /dev/null
+++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutData.lean
@@ -0,0 +1,253 @@
+/-
+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.PairedCrossover
+public import Complexity.Foundations.Geometry.Orthogonal.PairedPorts
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverLayoutData
+
+/-!
+# Orthogonal drawing data for the paired-port crossover
+
+The old internal drawing is retained. Each old terminal is replaced by ports at offsets 110
+and 130, with the new implication clause at the old terminal position. Only the eight old
+terminal incidence routes are rerouted. The shared paired accesses end at these eight ports.
+
+## Main definitions
+
+* `variablePosition`, `clausePositions`, `incidenceRoutes`: the 57-variable, 78-clause drawing.
+* `accessRoute`: the eight accesses from `Orthogonal.PairedPorts`.
+
+## References
+
+The unchanged core comes from [Lichtenstein1982, Figs. 4–5] and [Tromino2025, Fig. 8(b)].
+The paired terminal modification is original.
+Source credit for the core is in `CrossoverLayoutData`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.CNF.PairedCrossover
+
+open Orthogonal
+
+/-- The eight new ports use the shared paired interface; other vertices keep their positions. -/
+def variablePosition : Variable → Point
+  | .port s l => PairedPorts.variablePosition s l
+  | .center => Crossover.variablePosition .center
+  | .copy v i => Crossover.variablePosition (.copy v i)
+
+/-- The old clause positions followed by the four old terminal positions. -/
+def clausePositions : List Point :=
+  Crossover.clausePositions ++ [(20, 120), (220, 120), (120, 20), (120, 220)]
+
+/-- Exact clause-to-variable incidence routes in clause and literal order. -/
+def incidenceRoutes : List (ℕ × Variable × Route) :=
+  [
+    (0, .port 0 0, [(40, 120), (40, 119), (21, 119), (21, 110), (20, 110)]),
+    (0, .copy .aInnerLeft 5, [(40, 120), (56, 120)]),
+    (1, .port 0 1, [(40, 140), (37, 140), (37, 135), (33, 135), (33, 131), (29, 131), (29, 130),
+      (20, 130)]),
+    (1, .copy .aInnerLeft 4, [(40, 140), (40, 137), (45, 137), (45, 133), (49, 133), (49, 129),
+      (53, 129), (53, 125), (56, 125), (56, 124)]),
+    (2, .copy .aInnerLeft 0, [(60, 60), (59, 60), (59, 115), (60, 115), (60, 116)]),
+    (2, .copy .upperLeft 0, [(60, 60), (60, 63), (65, 63), (65, 67), (69, 67), (69, 71), (73, 71),
+      (73, 75), (77, 75), (77, 79), (81, 79), (81, 83), (85, 83), (85, 87), (89, 87), (89, 91),
+      (93, 91), (93, 95), (96, 95), (96, 96)]),
+    (2, .copy .bInnerTop 5, [(60, 60), (116, 60)]),
+    (3, .copy .aInnerLeft 3, [(60, 180), (59, 180), (59, 125), (60, 125), (60, 124)]),
+    (3, .copy .lowerLeft 4, [(60, 180), (60, 177), (65, 177), (65, 173), (69, 173), (69, 169), (73,
+      169), (73, 165), (77, 165), (77, 161), (81, 161), (81, 157), (85, 157), (85, 153), (89, 153),
+      (89, 149), (93, 149), (93, 145), (96, 145), (96, 144)]),
+    (3, .copy .bInnerBottom 5, [(60, 180), (116, 180)]),
+    (4, .copy .aInnerLeft 1, [(80, 100), (77, 100), (77, 105), (73, 105), (73, 109), (69, 109),
+      (69, 113), (65, 113), (65, 116), (64, 116)]),
+    (4, .copy .upperLeft 5, [(80, 100), (96, 100)]),
+    (5, .copy .upperLeft 4, [(80, 120), (80, 117), (85, 117), (85, 113), (89, 113), (89, 109), (93,
+      109), (93, 105), (96, 105), (96, 104)]),
+    (5, .copy .lowerLeft 0, [(80, 120), (80, 123), (85, 123), (85, 127), (89, 127), (89, 131), (93,
+      131), (93, 135), (96, 135), (96, 136)]),
+    (6, .copy .aInnerLeft 2, [(80, 140), (77, 140), (77, 135), (73, 135), (73, 131), (69, 131),
+      (69, 127), (65, 127), (65, 124), (64, 124)]),
+    (6, .copy .lowerLeft 5, [(80, 140), (96, 140)]),
+    (7, .port 2 0, [(100, 40), (100, 37), (105, 37), (105, 33), (109, 33), (109, 20), (110, 20)]),
+    (7, .copy .bInnerTop 0, [(100, 40), (100, 43), (105, 43), (105, 47), (109, 47), (109, 51),
+      (113, 51), (113, 55), (116, 55), (116, 56)]),
+    (8, .copy .upperLeft 1, [(100, 80), (100, 96)]),
+    (8, .copy .bInnerTop 4, [(100, 80), (100, 77), (105, 77), (105, 73), (109, 73), (109, 69),
+      (113, 69), (113, 65), (116, 65), (116, 64)]),
+    (9, .copy .upperLeft 3, [(100, 120), (100, 104)]),
+    (9, .copy .lowerLeft 1, [(100, 120), (100, 136)]),
+    (9, .center, [(100, 120), (120, 120)]),
+    (10, .copy .lowerLeft 3, [(100, 160), (100, 144)]),
+    (10, .copy .bInnerBottom 0, [(100, 160), (100, 163), (105, 163), (105, 167), (109, 167), (109,
+      171), (113, 171), (113, 175), (116, 175), (116, 176)]),
+    (11, .port 2 1, [(120, 40), (121, 40), (121, 21), (130, 21), (130, 20)]),
+    (11, .copy .bInnerTop 1, [(120, 40), (120, 56)]),
+    (12, .copy .upperLeft 2, [(120, 100), (104, 100)]),
+    (12, .copy .upperRight 5, [(120, 100), (136, 100)]),
+    (13, .copy .lowerLeft 2, [(120, 140), (104, 140)]),
+    (13, .copy .lowerRight 5, [(120, 140), (136, 140)]),
+    (14, .copy .bInnerBottom 4, [(120, 200), (120, 184)]),
+    (14, .port 3 0, [(120, 200), (120, 201), (110, 201), (110, 220)]),
+    (15, .copy .bInnerTop 3, [(140, 80), (137, 80), (137, 75), (133, 75), (133, 71), (129, 71),
+      (129, 67), (125, 67), (125, 64), (124, 64)]),
+    (15, .copy .upperRight 0, [(140, 80), (140, 96)]),
+    (16, .center, [(140, 120), (120, 120)]),
+    (16, .copy .upperRight 4, [(140, 120), (140, 104)]),
+    (16, .copy .lowerRight 0, [(140, 120), (140, 136)]),
+    (17, .copy .bInnerBottom 1, [(140, 160), (137, 160), (137, 165), (133, 165), (133, 169), (129,
+      169), (129, 173), (125, 173), (125, 176), (124, 176)]),
+    (17, .copy .lowerRight 4, [(140, 160), (140, 144)]),
+    (18, .copy .bInnerBottom 3, [(140, 200), (140, 197), (135, 197), (135, 193), (131, 193), (131,
+      189), (127, 189), (127, 185), (124, 185), (124, 184)]),
+    (18, .port 3 1, [(140, 200), (137, 200), (137, 205), (133, 205), (133, 209), (133, 213), (130,
+      213), (130, 220)]),
+    (19, .copy .upperRight 2, [(160, 100), (144, 100)]),
+    (19, .copy .aInnerRight 0, [(160, 100), (160, 103), (165, 103), (165, 107), (169, 107), (169,
+      111), (173, 111), (173, 115), (176, 115), (176, 116)]),
+    (20, .copy .upperRight 3, [(160, 120), (157, 120), (157, 115), (153, 115), (153, 111), (149,
+      111), (149, 107), (145, 107), (145, 104), (144, 104)]),
+    (20, .copy .lowerRight 1, [(160, 120), (160, 123), (155, 123), (155, 127), (151, 127), (151,
+      131), (147, 131), (147, 135), (144, 135), (144, 136)]),
+    (21, .copy .lowerRight 2, [(160, 140), (144, 140)]),
+    (21, .copy .aInnerRight 5, [(160, 140), (160, 137), (165, 137), (165, 133), (169, 133), (169,
+      129), (173, 129), (173, 125), (176, 125), (176, 124)]),
+    (22, .copy .bInnerTop 2, [(180, 60), (180, 59), (125, 59), (125, 60), (124, 60)]),
+    (22, .copy .upperRight 1, [(180, 60), (177, 60), (177, 65), (173, 65), (173, 69), (169, 69),
+      (169, 73), (165, 73), (165, 77), (161, 77), (161, 81), (157, 81), (157, 85), (153, 85), (153,
+      89), (149, 89), (149, 93), (145, 93), (145, 96), (144, 96)]),
+    (22, .copy .aInnerRight 1, [(180, 60), (180, 116)]),
+    (23, .copy .bInnerBottom 2, [(180, 180), (180, 181), (125, 181), (125, 180), (124, 180)]),
+    (23, .copy .lowerRight 3, [(180, 180), (177, 180), (177, 175), (173, 175), (173, 171), (169,
+      171), (169, 167), (165, 167), (165, 163), (161, 163), (161, 159), (157, 159), (157, 155),
+      (153, 155), (153, 151), (149, 151), (149, 147), (145, 147), (145, 144), (144, 144)]),
+    (23, .copy .aInnerRight 4, [(180, 180), (180, 124)]),
+    (24, .copy .aInnerRight 2, [(200, 100), (197, 100), (197, 105), (193, 105), (193, 109), (189,
+      109), (189, 113), (185, 113), (185, 116), (184, 116)]),
+    (24, .port 1 0, [(200, 100), (200, 103), (205, 103), (205, 107), (209, 107), (209, 110), (220,
+      110)]),
+    (25, .copy .aInnerRight 3, [(200, 120), (184, 120)]),
+    (25, .port 1 1, [(200, 120), (200, 121), (219, 121), (219, 130), (220, 130)]),
+    (26, .copy .aInnerLeft 0, [(62, 116), (60, 116)]),
+    (26, .copy .aInnerLeft 1, [(62, 116), (64, 116)]),
+    (27, .copy .aInnerLeft 1, [(64, 120), (64, 116)]),
+    (27, .copy .aInnerLeft 2, [(64, 120), (64, 124)]),
+    (28, .copy .aInnerLeft 2, [(62, 124), (64, 124)]),
+    (28, .copy .aInnerLeft 3, [(62, 124), (60, 124)]),
+    (29, .copy .aInnerLeft 3, [(58, 124), (60, 124)]),
+    (29, .copy .aInnerLeft 4, [(58, 124), (56, 124)]),
+    (30, .copy .aInnerLeft 4, [(56, 122), (56, 124)]),
+    (30, .copy .aInnerLeft 5, [(56, 122), (56, 120)]),
+    (31, .copy .aInnerLeft 5, [(56, 116), (56, 120)]),
+    (31, .copy .aInnerLeft 0, [(56, 116), (60, 116)]),
+    (32, .copy .upperLeft 0, [(98, 96), (96, 96)]),
+    (32, .copy .upperLeft 1, [(98, 96), (100, 96)]),
+    (33, .copy .upperLeft 1, [(104, 96), (100, 96)]),
+    (33, .copy .upperLeft 2, [(104, 96), (104, 100)]),
+    (34, .copy .upperLeft 2, [(104, 104), (104, 100)]),
+    (34, .copy .upperLeft 3, [(104, 104), (100, 104)]),
+    (35, .copy .upperLeft 3, [(98, 104), (100, 104)]),
+    (35, .copy .upperLeft 4, [(98, 104), (96, 104)]),
+    (36, .copy .upperLeft 4, [(96, 102), (96, 104)]),
+    (36, .copy .upperLeft 5, [(96, 102), (96, 100)]),
+    (37, .copy .upperLeft 5, [(96, 98), (96, 100)]),
+    (37, .copy .upperLeft 0, [(96, 98), (96, 96)]),
+    (38, .copy .lowerLeft 0, [(98, 136), (96, 136)]),
+    (38, .copy .lowerLeft 1, [(98, 136), (100, 136)]),
+    (39, .copy .lowerLeft 1, [(104, 136), (100, 136)]),
+    (39, .copy .lowerLeft 2, [(104, 136), (104, 140)]),
+    (40, .copy .lowerLeft 2, [(104, 144), (104, 140)]),
+    (40, .copy .lowerLeft 3, [(104, 144), (100, 144)]),
+    (41, .copy .lowerLeft 3, [(98, 144), (100, 144)]),
+    (41, .copy .lowerLeft 4, [(98, 144), (96, 144)]),
+    (42, .copy .lowerLeft 4, [(96, 142), (96, 144)]),
+    (42, .copy .lowerLeft 5, [(96, 142), (96, 140)]),
+    (43, .copy .lowerLeft 5, [(96, 138), (96, 140)]),
+    (43, .copy .lowerLeft 0, [(96, 138), (96, 136)]),
+    (44, .copy .bInnerTop 0, [(118, 56), (116, 56)]),
+    (44, .copy .bInnerTop 1, [(118, 56), (120, 56)]),
+    (45, .copy .bInnerTop 1, [(124, 56), (120, 56)]),
+    (45, .copy .bInnerTop 2, [(124, 56), (124, 60)]),
+    (46, .copy .bInnerTop 2, [(124, 62), (124, 60)]),
+    (46, .copy .bInnerTop 3, [(124, 62), (124, 64)]),
+    (47, .copy .bInnerTop 3, [(120, 64), (124, 64)]),
+    (47, .copy .bInnerTop 4, [(120, 64), (116, 64)]),
+    (48, .copy .bInnerTop 4, [(116, 62), (116, 64)]),
+    (48, .copy .bInnerTop 5, [(116, 62), (116, 60)]),
+    (49, .copy .bInnerTop 5, [(116, 58), (116, 60)]),
+    (49, .copy .bInnerTop 0, [(116, 58), (116, 56)]),
+    (50, .copy .bInnerBottom 0, [(120, 176), (116, 176)]),
+    (50, .copy .bInnerBottom 1, [(120, 176), (124, 176)]),
+    (51, .copy .bInnerBottom 1, [(124, 178), (124, 176)]),
+    (51, .copy .bInnerBottom 2, [(124, 178), (124, 180)]),
+    (52, .copy .bInnerBottom 2, [(124, 182), (124, 180)]),
+    (52, .copy .bInnerBottom 3, [(124, 182), (124, 184)]),
+    (53, .copy .bInnerBottom 3, [(122, 184), (124, 184)]),
+    (53, .copy .bInnerBottom 4, [(122, 184), (120, 184)]),
+    (54, .copy .bInnerBottom 4, [(116, 184), (120, 184)]),
+    (54, .copy .bInnerBottom 5, [(116, 184), (116, 180)]),
+    (55, .copy .bInnerBottom 5, [(116, 178), (116, 180)]),
+    (55, .copy .bInnerBottom 0, [(116, 178), (116, 176)]),
+    (56, .copy .upperRight 0, [(142, 96), (140, 96)]),
+    (56, .copy .upperRight 1, [(142, 96), (144, 96)]),
+    (57, .copy .upperRight 1, [(144, 98), (144, 96)]),
+    (57, .copy .upperRight 2, [(144, 98), (144, 100)]),
+    (58, .copy .upperRight 2, [(144, 102), (144, 100)]),
+    (58, .copy .upperRight 3, [(144, 102), (144, 104)]),
+    (59, .copy .upperRight 3, [(142, 104), (144, 104)]),
+    (59, .copy .upperRight 4, [(142, 104), (140, 104)]),
+    (60, .copy .upperRight 4, [(136, 104), (140, 104)]),
+    (60, .copy .upperRight 5, [(136, 104), (136, 100)]),
+    (61, .copy .upperRight 5, [(136, 96), (136, 100)]),
+    (61, .copy .upperRight 0, [(136, 96), (140, 96)]),
+    (62, .copy .lowerRight 0, [(142, 136), (140, 136)]),
+    (62, .copy .lowerRight 1, [(142, 136), (144, 136)]),
+    (63, .copy .lowerRight 1, [(144, 138), (144, 136)]),
+    (63, .copy .lowerRight 2, [(144, 138), (144, 140)]),
+    (64, .copy .lowerRight 2, [(144, 142), (144, 140)]),
+    (64, .copy .lowerRight 3, [(144, 142), (144, 144)]),
+    (65, .copy .lowerRight 3, [(142, 144), (144, 144)]),
+    (65, .copy .lowerRight 4, [(142, 144), (140, 144)]),
+    (66, .copy .lowerRight 4, [(136, 144), (140, 144)]),
+    (66, .copy .lowerRight 5, [(136, 144), (136, 140)]),
+    (67, .copy .lowerRight 5, [(136, 136), (136, 140)]),
+    (67, .copy .lowerRight 0, [(136, 136), (140, 136)]),
+    (68, .copy .aInnerRight 0, [(178, 116), (176, 116)]),
+    (68, .copy .aInnerRight 1, [(178, 116), (180, 116)]),
+    (69, .copy .aInnerRight 1, [(182, 116), (180, 116)]),
+    (69, .copy .aInnerRight 2, [(182, 116), (184, 116)]),
+    (70, .copy .aInnerRight 2, [(184, 118), (184, 116)]),
+    (70, .copy .aInnerRight 3, [(184, 118), (184, 120)]),
+    (71, .copy .aInnerRight 3, [(184, 124), (184, 120)]),
+    (71, .copy .aInnerRight 4, [(184, 124), (180, 124)]),
+    (72, .copy .aInnerRight 4, [(178, 124), (180, 124)]),
+    (72, .copy .aInnerRight 5, [(178, 124), (176, 124)]),
+    (73, .copy .aInnerRight 5, [(176, 120), (176, 124)]),
+    (73, .copy .aInnerRight 0, [(176, 120), (176, 116)]),
+    (74, .port 0 0, [(20, 120), (20, 110)]),
+    (74, .port 0 1, [(20, 120), (20, 130)]),
+    (75, .port 1 1, [(220, 120), (220, 130)]),
+    (75, .port 1 0, [(220, 120), (220, 110)]),
+    (76, .port 2 1, [(120, 20), (130, 20)]),
+    (76, .port 2 0, [(120, 20), (110, 20)]),
+    (77, .port 3 0, [(120, 220), (110, 220)]),
+    (77, .port 3 1, [(120, 220), (130, 220)])
+  ]
+
+/-- Boundary access points agree definitionally with the shared paired interface. -/
+def boundaryPort : Fin 4 → Fin 2 → Point := PairedPorts.boundaryPort
+
+/-- Straight shared accesses to the eight degree-two terminals. -/
+def accessRoute : Fin 4 → Fin 2 → Route := PairedPorts.accessRoute
+
+/-- The terminal coordinates are exactly the shared paired-port positions. -/
+theorem terminal_position (s : Fin 4) (l : Fin 2) :
+    variablePosition (terminal s l) = PairedPorts.variablePosition s l := rfl
+
+end Cslib.Logic.PL.CNF.PairedCrossover