refactor(Foundations): consolidate shared geometry and counting helpers

Complexity/Computability/Circuit/Arithmetic/VP.lean

@@ -250,9 +250,6 @@ theorem IsProjection.trans {P : MvPolynomial υ K} {Q : MvPolynomial σ K} {R :
   obtain ⟨ρ', rfl⟩ := hQR
   exact ⟨_, (projection_projection ρ ρ' R).symm⟩
 
-private theorem totalDegree_X_le (i : σ) : (X i : MvPolynomial σ K).totalDegree ≤ 1 :=
-  (totalDegree_monomial_le _ _).trans (by simp)
-
 /-- Substituting polynomials of degree at most one does not raise the degree. -/
 private theorem totalDegree_aeval_le {g : τ → MvPolynomial σ K}
     (hg : ∀ i, (g i).totalDegree ≤ 1) (P : MvPolynomial τ K) :
@@ -272,7 +269,7 @@ theorem totalDegree_projection_le (ρ : τ → σ ⊕ K) (P : MvPolynomial τ K)
     (projection ρ P).totalDegree ≤ P.totalDegree :=
   totalDegree_aeval_le (fun i => by
     rcases ρ i with k | a
-    · exact totalDegree_X_le k
+    · exact (totalDegree_monomial_le _ _).trans (by simp)
     · simp) P
 
 end Projection

Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean

@@ -93,15 +93,6 @@ def certifiedSet (enc : α ↪ List Bool) (N c : Polynomial ℕ) (R : α × List
 
 namespace SetLowerBound
 
-/-! ### Bit-string helpers -/
-
-/-- A string has no bit `true` exactly when it is zero. -/
-private theorem not_any_ofFn_eq_true_iff {k : ℕ} (v : BitString k) :
-    (!(List.ofFn v).any fun b => b) = true ↔ v = 0 := by
-  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, List.any_eq_false, List.mem_ofFn,
-    forall_exists_index, forall_apply_eq_imp_iff, Bool.not_eq_true]
-  exact ⟨fun h => funext h, fun h i => by rw [h]; rfl⟩
-
 /-! ### Amplification and normalisation -/
 
 /-- Five elements of `S`, followed by `T` bits whose first `ℓ` bits are `false`. -/
@@ -207,7 +198,7 @@ private theorem verifier_ofFn_append {N c m T : Polynomial ℕ} {ℓ : α → 
     rw [BitString.LinearHash.wordHash_eq_ofFn, List.ofFn_add, BitString.ofList_ofFn_append]
     rfl
   rw [hdrop, hdrop', htake, List.take_left' List.length_ofFn, hhash, hoffset,
-    ← BitString.ofFn_add, not_any_ofFn_eq_true_iff, and_assoc]
+    ← BitString.ofFn_add, BitString.not_any_ofFn_eq_true_iff, and_assoc]
   refine and_congr ⟨fun h i => ?_, fun h i hi => ?_⟩ Iff.rfl
   · have := h i i.2
     rwa [BitString.listRow_eq_ofFn (count := 5) _ i, BitString.listRow_eq_ofFn (count := 5) _ i,

Complexity/Computability/Complexity/Classes/Toda/Counting.lean

@@ -159,13 +159,6 @@ theorem computableInPolyTime_subsetTest {γ : Type} {input : γ ↪ List Bool}
   unfold subsetTest
   fun_prop
 
-/-- A bit string `z` has no `true` bits in `List.ofFn z` if and only if `z = 0`. -/
-private theorem not_any_ofFn_eq_true_iff {Z : ℕ} (z : Fin Z → Bool) :
-    (!(List.ofFn z).any fun b => b) = true ↔ z = 0 := by
-  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, List.any_eq_false, List.mem_ofFn,
-    forall_exists_index, forall_apply_eq_imp_iff, Bool.not_eq_true]
-  exact ⟨fun h => funext h, fun h i => congrFun h i⟩
-
 /-- The block-level predicate corresponding to `subsetTest`: the first `k` blocks are accepted and
 strictly increasing in lexicographic order, and the remaining blocks are zero. -/
 private def SubsetBlockPred (acc : List Bool → Bool) {K Z k : ℕ} (hk : k ≤ K)

Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingFits.lean

@@ -117,14 +117,6 @@ private theorem local_clause_bounds (p : ClauseProfile) (s : PortAssignment) (i
   obtain ⟨a, ha, rfl⟩ := List.mem_map.mp hq
   exact collarPoint_bounds _ (prefix_clause_bounds p a ha)
 
-private theorem collarRoute_points_bounds (reflected : Bool) {r : Route}
-    (hr : ∀ q ∈ r, Rect 180000 180000 q) :
-    ∀ q ∈ collarRoute reflected r, Rect 540000 540000 q := by
-  intro q hq
-  rw [collarRoute_eq_map] at hq
-  obtain ⟨a, ha, rfl⟩ := List.mem_map.mp hq
-  exact collarPoint_bounds _ (hr a ha)
-
 private theorem local_route_bounds (p : ClauseProfile) (s : PortAssignment)
     {e : LocalIncidence}
     (he : e ∈ (collaredPrefixGeometry (profilePrefixGeometry p) s).incidenceRoutes) :

Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingRoutes.lean

@@ -42,16 +42,6 @@ namespace Cslib.Complexity.SAT.ExactOne
 
 open Cslib.Logic.PL Orthogonal
 
-private theorem collarRoute_points_bounds (reflected : Bool) {r : Route}
-    (hr : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) :
-    ∀ q ∈ collarRoute reflected r,
-      0 ≤ q.1 ∧ q.1 ≤ 540000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 540000 := by
-  intro q hq
-  rw [collarRoute_eq_map] at hq
-  obtain ⟨a, ha, rfl⟩ := List.mem_map.mp hq
-  have hb := hr a ha
-  cases reflected <;> dsimp [collarPoint, collarOffset, mirrorPoint] <;> omega
-
 private theorem collarPrefixRoute_points_bounds {s : PortAssignment} (hs : s.Distinct)
     (i : Fin 3) {r : Route}
     (hr : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) :

Complexity/Computability/Complexity/Problems/SAT/ExactOne/GeometryProfilesCollar.lean

@@ -345,4 +345,16 @@ theorem profileCollarRoute_outer_boundary_contact (p : ClauseProfile)
       (collarRoute_in_innerBox _ (profile_prefix_incidence_bounds p h he) hz)
     exact False.elim (List.not_mem_nil hq)
 
+/-- If every point of a route lies in the `180000`-by-`180000` inner square, then every point of
+its collared route lies in the `540000`-by-`540000` outer square. -/
+theorem collarRoute_points_bounds (reflected : Bool) {r : Route}
+    (hr : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) :
+    ∀ q ∈ collarRoute reflected r,
+      0 ≤ q.1 ∧ q.1 ≤ 540000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 540000 := by
+  intro q hq
+  rw [collarRoute_eq_map] at hq
+  obtain ⟨a, ha, rfl⟩ := List.mem_map.mp hq
+  have hb := hr a ha
+  cases reflected <;> dsimp [collarPoint, collarOffset, mirrorPoint] <;> omega
+
 end Cslib.Complexity.SAT.ExactOne

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

@@ -50,37 +50,14 @@ namespace Cslib.Logic.PL.CNF.Crossover
 
 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 : ℕ × SplitVariable × 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]
+  have h := support_bounds_of_points (x₀ := 20) (x₁ := 220) (y₀ := 20) (y₁ := 220)
+    (core_bounds e he) hp
+  norm_num at h
+  exact ⟨by linarith [h.1], by linarith [h.2.1], by linarith [h.2.2.1], by linarith [h.2.2.2]⟩
 
 /-- Distinct segments of a route intersect only at their consecutive shared bend. -/
 theorem incidence_simple {e : ℕ × SplitVariable × Route} (he : e ∈ incidenceRoutes)
@@ -197,15 +174,6 @@ theorem access_contact {i : Fin 4} {e : ℕ × SplitVariable × Route}
     exact ⟨h, hq' ▸ hpq⟩
   · exact False.elim (List.not_mem_nil hq)
 
-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⟩
-
 /-- Every point of an access route lies in the outer box. Its only boundary point is the
 prescribed geometric access port; all other access points are strictly inside. -/
 theorem access_boundary_isolation {i : Fin 4} {p : ℝ × ℝ}

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

@@ -82,14 +82,8 @@ private theorem cellBound_path {φ : CNF ℕ} {r : Route} (hr : r ∈ paths φ)
 
 private theorem cellBound_occurrencePath {φ : CNF ℕ} {o : Occurrence ℕ}
     (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p : Point} (hp : p ∈ occurrencePath φ o) :
-    CellBound φ p := by
-  have hi : (Cslib.Logic.PL.occurrences φ).idxOf o < (paths φ).length := by
-    rw [PlanarCompile.paths_length, ← Cslib.Logic.PL.length_occurrences]
-    exact List.idxOf_lt_length_of_mem ho
-  apply cellBound_path (r := occurrencePath φ o) _ hp
-  change (paths φ).getD ((Cslib.Logic.PL.occurrences φ).idxOf o) [] ∈ paths φ
-  rw [List.getD_eq_getElem _ _ hi]
-  exact List.getElem_mem hi
+    CellBound φ p :=
+  cellBound_path (PlanarCompile.occurrencePath_mem_paths ho) hp
 
 private theorem cellBound_crossing {φ : CNF ℕ} {p : Point} (hp : p ∈ crossingSites φ) :
     CellBound φ p := by
@@ -270,9 +264,7 @@ private theorem link_bounds {φ : CNF ℕ} (sites : List Point) (lane : Fin 2) {
 
 private theorem cellBound_ordinary {φ : CNF ℕ} {p : Point} (hp : p ∈ ordinaryCells φ) :
     CellBound φ p := by
-  have hmem : p ∈ (paths φ).flatMap List.dropLast ∧ p ∉ crossingSites φ := by
-    simpa [ordinaryCells, mem_selectDistinct_replicate] using hp
-  obtain ⟨r, hr, hp⟩ := List.mem_flatMap.mp hmem.1
+  obtain ⟨⟨r, hr, hp⟩, -⟩ := (mem_ordinaryCells φ p).1 hp
   exact cellBound_path hr ((List.dropLast_subset _) hp)
 
 private theorem placedClauses_bounds (φ : CNF ℕ) :
@@ -333,41 +325,6 @@ theorem positions_length_le (φ : CNF ℕ) :
   rw [length_vars_rawFormula, ← length_vars_formula] at hv
   omega
 
-private theorem cost_signal_position (sites : List Point) (p q : Point) (l : Fin 2) :
-    variablePosition (signal sites p q l) =
-      cellOrigin 120 p + PairedPorts.variablePosition (side p q) l := by
-  simp only [signal, port, variablePosition]
-  split_ifs <;> rfl
-
-/-- Actual accesses are translations of the fixed paired-port accesses. -/
-private theorem cost_access_eq_translate (sites : List Point) (p q : Point) (l : Fin 2) :
-    access sites p q l = translate (cellOrigin 120 p) (PairedPorts.accessRoute (side p q) l) := by
-  rw [access, cost_signal_position]
-  simp only [boundary, PairedPorts.accessRoute, translate, List.map_cons, List.map_nil]
-  simp only [add_comm]
-
-private def finalLocalRoute (s : Fin 4) : Route :=
-  [(120, 120), PairedPorts.spokeElbow s, PairedPorts.boundaryPort s (PairedPorts.spokeLane s),
-    cellOrigin 120 (PairedPorts.neighbor s) +
-      PairedPorts.variablePosition (PairedPorts.oppositeSide s) (PairedPorts.spokeLane s)]
-
-private theorem finalRoute_eq_translate (sites : List Point) {p q : Point}
-    (h : Orthogonal.length p q = 1) :
-    [center q, cellOrigin 120 q + PairedPorts.spokeElbow (side q p),
-      boundary q (side q p) (PairedPorts.spokeLane (side q p)),
-      variablePosition (signal sites p q (PairedPorts.spokeLane (side q p)))] =
-      translate (cellOrigin 120 q) (finalLocalRoute (side q p)) := by
-  rw [cost_signal_position]
-  have hrev : Orthogonal.length q p = 1 := by
-    simp only [Orthogonal.length] at h ⊢
-    omega
-  rcases q with ⟨x, y⟩
-  rcases PlanarCompile.unit_neighbor_cases hrev with rfl | rfl | rfl | rfl <;>
-    simp [translate, finalLocalRoute, side, PlanarCompile.side, center, PlanarCompile.center,
-      boundary, cellOrigin, PairedPorts.neighbor, PairedPorts.oppositeSide,
-      PairedPorts.variablePosition, PairedPorts.boundaryPort, PairedPorts.spokeLane,
-      PairedPorts.spokeElbow, PairedPorts.offset, Prod.ext_iff] <;> omega
-
 private theorem original_route_count (φ : CNF ℕ) (sites : List Point) :
     ((originalClauses φ sites).map fun c => c.2.2.length).sum = φ.vars.length := by
   rw [CNF.length_vars]
@@ -452,7 +409,7 @@ private theorem crossing_route_costs (p : Point) :
 
 private theorem access_wire_cost (sites : List Point) (p q : Point) (lane : Fin 2) :
     wireLength (access sites p q lane) = 20 := by
-  rw [cost_access_eq_translate, wireLength_translate]
+  rw [access_eq_translate, wireLength_translate]
   exact (PairedPorts.access_route_sizes _ _).2
 
 private theorem lastLiteral_wire_cost (sites : List Point) (r : Route) (b : Bool)

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

@@ -155,4 +155,52 @@ def positions (φ : CNF ℕ) : List Point :=
 /-- Incidence routes ordered by clauses and by literal positions. -/
 def routes (φ : CNF ℕ) : List Route := (placedClauses φ).flatMap fun c => c.2.2
 
+/-- A point receives an ordinary ring exactly when a retained path uses it outside a crossing. -/
+theorem mem_ordinaryCells (φ : CNF ℕ) (p : Point) :
+    p ∈ ordinaryCells φ ↔
+      (∃ r ∈ paths φ, p ∈ r.dropLast) ∧ p ∉ crossingSites φ := by
+  simp [ordinaryCells, mem_selectDistinct_replicate, List.mem_flatMap]
+
+/-- No ordinary ring is emitted twice. -/
+theorem ordinaryCells_nodup (φ : CNF ℕ) : (ordinaryCells φ).Nodup :=
+  nodup_selectDistinct _ _
+
+/-- The compiler's presented signal always has the shared inner access position. -/
+theorem signal_position (sites : List Point) (p q : Point) (l : Fin 2) :
+    variablePosition (signal sites p q l) =
+      cellOrigin 120 p + PairedPorts.variablePosition (side p q) l := by
+  simp only [signal, port, variablePosition]
+  split_ifs <;> rfl
+
+/-- Actual accesses are translations of the fixed paired-port accesses. -/
+theorem access_eq_translate (sites : List Point) (p q : Point) (l : Fin 2) :
+    access sites p q l = translate (cellOrigin 120 p) (PairedPorts.accessRoute (side p q) l) := by
+  rw [access, signal_position]
+  simp only [boundary, PairedPorts.accessRoute, translate, List.map_cons, List.map_nil]
+  simp only [add_comm]
+
+/-- Local template of the final incidence route inside a clause cell. -/
+def finalLocalRoute (s : Fin 4) : Route :=
+  [(120, 120), PairedPorts.spokeElbow s, PairedPorts.boundaryPort s (PairedPorts.spokeLane s),
+    cellOrigin 120 (PairedPorts.neighbor s) +
+      PairedPorts.variablePosition (PairedPorts.oppositeSide s) (PairedPorts.spokeLane s)]
+
+/-- Actual final literal routes are translations of `finalLocalRoute`. -/
+theorem finalRoute_eq_translate (sites : List Point) {p q : Point}
+    (h : Orthogonal.length p q = 1) :
+    [center q, cellOrigin 120 q + PairedPorts.spokeElbow (side q p),
+      boundary q (side q p) (PairedPorts.spokeLane (side q p)),
+      variablePosition (signal sites p q (PairedPorts.spokeLane (side q p)))] =
+      translate (cellOrigin 120 q) (finalLocalRoute (side q p)) := by
+  rw [signal_position]
+  have hrev : Orthogonal.length q p = 1 := by
+    simp only [Orthogonal.length] at h ⊢
+    omega
+  rcases q with ⟨x, y⟩
+  rcases PlanarCompile.unit_neighbor_cases hrev with rfl | rfl | rfl | rfl <;>
+    simp [translate, finalLocalRoute, side, PlanarCompile.side, center, PlanarCompile.center,
+      boundary, cellOrigin, PairedPorts.neighbor, PairedPorts.oppositeSide,
+      PairedPorts.variablePosition, PairedPorts.boundaryPort, PairedPorts.spokeLane,
+      PairedPorts.spokeElbow, PairedPorts.offset, Prod.ext_iff] <;> omega
+
 end Cslib.Complexity.SAT.ParsimoniousPlanar

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

@@ -64,7 +64,8 @@ theorem source_cell_mem_ordinary {φ : CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) :
     rw [← List.getElem_dropLast hi]
     exact List.getElem_mem _
   exact (mem_ordinaryCells φ _).2
-    ⟨⟨_, occurrencePath_mem_paths ho, hret⟩, PlanarCompile.source_center_not_crossing ho⟩
+    ⟨⟨_, PlanarCompile.occurrencePath_mem_paths ho, hret⟩,
+      PlanarCompile.source_center_not_crossing ho⟩
 
 /-- Every used source representative is an occurring variable of the actual raw output. -/
 theorem sourceVariable_mem_rawFormula {φ : CNF ℕ} {v : ℕ} (hv : v ∈ φ.vars) :

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

@@ -48,37 +48,14 @@ 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]
+  have h := support_bounds_of_points (x₀ := 20) (x₁ := 220) (y₀ := 20) (y₁ := 220)
+    (core_bounds e he) hp
+  norm_num at h
+  exact ⟨by linarith [h.1], by linarith [h.2.1], by linarith [h.2.2.1], by linarith [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)