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 [Lic82].
• MIT–ULB CompGeom Group, Undecidability of Tiling with a Tromino, Fig. 8(b) [MITULBCGGAA+25].

The paired modification and its finite orthogonal certificates are original.

def Cslib.Logic.PL.CNF.PairedCrossover.clausePosition (i : ℕ) : Orthogonal.Point

The clause position at an index. All indices in incidenceRoutes are certified in range.

def Cslib.Logic.PL.CNF.PairedCrossover.variableList : List Variable

Every variable, including both lanes on each side.

theorem Cslib.Logic.PL.CNF.PairedCrossover.mem_variableList (v : Variable) : v ∈ variableList

Every variable is included in the finite drawing vertex list.

theorem Cslib.Logic.PL.CNF.PairedCrossover.incidenceRoutes_cover : List.map (fun (e : ℕ × Variable × Orthogonal.Route) => (e.1, e.2.1)) incidenceRoutes = List.flatMap (fun (ci : Clause Variable × ℕ) => List.map (fun (l : Literal Variable) => (ci.2, l.1)) ci.1) (List.zipIdx formula)

The exact literal-incidence list of the ordinary CNF formula.

theorem Cslib.Logic.PL.CNF.PairedCrossover.drawing_sizes : clausePositions.length = 78 ∧ incidenceRoutes.length = 162

The fixed formula and drawing have 78 clauses and 162 incidences.

theorem Cslib.Logic.PL.CNF.PairedCrossover.variablePosition_injective : Function.Injective variablePosition

Variable vertices have distinct positions.

theorem Cslib.Logic.PL.CNF.PairedCrossover.clausePositions_nodup : clausePositions.Nodup

Clause vertices are pairwise distinct.

theorem Cslib.Logic.PL.CNF.PairedCrossover.variablePosition_not_mem_clauses (v : Variable) : variablePosition v ∉ clausePositions

No clause vertex is a variable vertex.

def Cslib.Logic.PL.CNF.PairedCrossover.commonEndpoints (e f : ℕ × Variable × Orthogonal.Route) : List Orthogonal.Point

The only allowed contacts between two distinct incidence routes are shared graph endpoints.

theorem Cslib.Logic.PL.CNF.PairedCrossover.incidence_endpoints (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → e.1 < 78 ∧ List.head? e.2.2 = some (clausePosition e.1) ∧ List.getLast? e.2.2 = some (variablePosition e.2.1)

Every route starts at its clause and ends at its variable, with a valid clause index.

theorem Cslib.Logic.PL.CNF.PairedCrossover.incidence_orthogonal (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → Orthogonal.IsOrthogonal e.2.2

All incidence routes have proper axis-aligned segments.

theorem Cslib.Logic.PL.CNF.PairedCrossover.core_bounds (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → ∀ p ∈ e.2.2, 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220

All listed core points are inside the smaller rectangle [20,220]².

theorem Cslib.Logic.PL.CNF.PairedCrossover.route_sizes : (List.map (fun (e : ℕ × Variable × Orthogonal.Route) => (List.consecutivePairs e.2.2).length) incidenceRoutes).sum = 407 ∧ (List.map (fun (e : ℕ × Variable × Orthogonal.Route) => Orthogonal.wireLength e.2.2) incidenceRoutes).sum = 2192

Exactly 407 proper segments and 2192 units of total Manhattan wire length.

theorem Cslib.Logic.PL.CNF.PairedCrossover.incidence_points_nodup (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → List.Nodup e.2.2

Every incidence route lists each bend only once.

theorem Cslib.Logic.PL.CNF.PairedCrossover.incidence_simple_check (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → ∀ a ∈ List.consecutivePairs e.2.2, ∀ b ∈ List.consecutivePairs e.2.2, a ≠ b → Orthogonal.segmentContactCheck (Orthogonal.consecutiveContact a b) a.1 a.2 b.1 b.2 = true

Finite simplicity certificate: distinct segments are disjoint except at a shared next bend.

theorem Cslib.Logic.PL.CNF.PairedCrossover.routes_contact_check (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → ∀ f ∈ incidenceRoutes, e ≠ f → Orthogonal.routeContactCheck (commonEndpoints e f) e.2.2 f.2.2 = true

Exhaustive finite contact certificate for the fixed route table.

theorem Cslib.Logic.PL.CNF.PairedCrossover.variable_avoidance_check (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → ∀ (v : Variable), v ≠ e.2.1 → Orthogonal.routeContactCheck [] e.2.2 [variablePosition v] = true

No route visits a nonincident variable vertex.

theorem Cslib.Logic.PL.CNF.PairedCrossover.clause_avoidance_check (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → ∀ (i : Fin 78), ↑i ≠ e.1 → Orthogonal.routeContactCheck [] e.2.2 [clausePosition ↑i] = true

No route visits a nonincident clause vertex.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_endpoints (s : Fin 4) (l : Fin 2) : Orthogonal.IsOrthogonal (accessRoute s l) ∧ List.head? (accessRoute s l) = some (boundaryPort s l) ∧ List.getLast? (accessRoute s l) = some (variablePosition (terminal s l))

All eight access routes have their prescribed endpoints and proper orthogonal segments.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_disjoint_check (p q : Orthogonal.PairedPorts.Port) : p ≠ q → Orthogonal.routeContactCheck [] (accessRoute p.1 p.2) (accessRoute q.1 q.2) = true

The eight access routes are mutually disjoint.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_contact_check (s : Fin 4) (l : Fin 2) (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → Orthogonal.routeContactCheck (if e.2.1 = terminal s l then [variablePosition (terminal s l)] else []) (accessRoute s l) e.2.2 = true

Access to a port can meet an incidence route only at that port.