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

The paired-terminal modification and its continuous orthogonal certificates are original.

theorem Cslib.Logic.PL.CNF.PairedCrossover.core_support_interior {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support e.2.2) : 0 < p.1 ∧ p.1 < 240 ∧ 0 < p.2 ∧ p.2 < 240

Every real point of the core drawing is strictly inside the outer 240-by-240 box.

theorem Cslib.Logic.PL.CNF.PairedCrossover.incidence_simple {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) {a b : Orthogonal.Point × Orthogonal.Point} (ha : a ∈ List.consecutivePairs e.2.2) (hb : b ∈ List.consecutivePairs e.2.2) (hne : a ≠ b) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.segment a.1 a.2) (hq : p ∈ Orthogonal.segment b.1 b.2) : ∃ q ∈ Orthogonal.consecutiveContact a b, p = Orthogonal.realPoint q

Distinct segments of a route intersect only at their consecutive shared bend.

theorem Cslib.Logic.PL.CNF.PairedCrossover.incidence_isSimple {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) : Orthogonal.IsSimple e.2.2

Every incidence route is simple in the shared continuous polygonal-route semantics.

theorem Cslib.Logic.PL.CNF.PairedCrossover.routes_contact {e f : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) (hf : f ∈ incidenceRoutes) (hne : e ≠ f) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support e.2.2) (hq : p ∈ Orthogonal.support f.2.2) : ∃ q ∈ commonEndpoints e f, p = Orthogonal.realPoint q

Every continuous intersection of distinct incidence routes is a shared graph endpoint.

theorem Cslib.Logic.PL.CNF.PairedCrossover.variable_not_mem_support {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) {v : Variable} (hv : v ≠ e.2.1) : Orthogonal.realPoint (variablePosition v) ∉ Orthogonal.support e.2.2

Continuous incidence routes avoid every nonincident variable vertex.

theorem Cslib.Logic.PL.CNF.PairedCrossover.clause_not_mem_support {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) {i : Fin 78} (hi : ↑i ≠ e.1) : Orthogonal.realPoint (clausePosition ↑i) ∉ Orthogonal.support e.2.2

Continuous incidence routes avoid every nonincident clause vertex.

theorem Cslib.Logic.PL.CNF.PairedCrossover.incidenceEndpoints_nodup : (List.map (fun (e : ℕ × Variable × Orthogonal.Route) => (e.1, e.2.1)) incidenceRoutes).Nodup

Every literal incidence appears exactly once in the route list.

theorem Cslib.Logic.PL.CNF.PairedCrossover.variable_bounds (v : Variable) : 20 ≤ (variablePosition v).1 ∧ (variablePosition v).1 ≤ 220 ∧ 20 ≤ (variablePosition v).2 ∧ (variablePosition v).2 ≤ 220

Every variable vertex lies in the core rectangle.

theorem Cslib.Logic.PL.CNF.PairedCrossover.clause_bounds (p : Orthogonal.Point) : p ∈ clausePositions → 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220

Every clause vertex lies in the core rectangle.

theorem Cslib.Logic.PL.CNF.PairedCrossover.variables_used (v : Variable) : v ∈ formula.vars

Each of the 57 variable names is genuinely used by the fixed formula.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_variable_avoidance_check (s : Fin 4) (l : Fin 2) (v : Variable) : v ≠ terminal s l → Orthogonal.routeContactCheck [] (accessRoute s l) [variablePosition v] = true

No access route visits any other variable vertex.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_clause_avoidance_check (s : Fin 4) (l : Fin 2) (p : Orthogonal.Point) : p ∈ clausePositions → Orthogonal.routeContactCheck [] (accessRoute s l) [p] = true

No access route visits a clause vertex.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_variable_not_mem {s : Fin 4} {l : Fin 2} {v : Variable} (hv : v ≠ terminal s l) : Orthogonal.realPoint (variablePosition v) ∉ Orthogonal.support (accessRoute s l)

The full real access route avoids every other variable vertex.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_clause_not_mem {s : Fin 4} {l : Fin 2} {p : Orthogonal.Point} (hp : p ∈ clausePositions) : Orthogonal.realPoint p ∉ Orthogonal.support (accessRoute s l)

The full real access route avoids every clause vertex.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_route_sizes (s : Fin 4) (l : Fin 2) : (List.consecutivePairs (accessRoute s l)).length = 1 ∧ Orthogonal.wireLength (accessRoute s l) = 20

Each access route has one segment and 20 units of wire length.

theorem Cslib.Logic.PL.CNF.PairedCrossover.full_route_sizes : (List.map (fun (e : ℕ × Variable × Orthogonal.Route) => (List.consecutivePairs e.2.2).length) incidenceRoutes).sum + (List.flatMap (fun (s : Fin 4) => List.map (fun (l : Fin 2) => (List.consecutivePairs (accessRoute s l)).length) (List.finRange 2)) (List.finRange 4)).sum = 415 ∧ (List.map (fun (e : ℕ × Variable × Orthogonal.Route) => Orthogonal.wireLength e.2.2) incidenceRoutes).sum + (List.flatMap (fun (s : Fin 4) => List.map (fun (l : Fin 2) => Orthogonal.wireLength (accessRoute s l)) (List.finRange 2)) (List.finRange 4)).sum = 2352

Including all eight accesses gives 415 segments and total wire length 2352.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_isSimple (s : Fin 4) (l : Fin 2) : Orthogonal.IsSimple (accessRoute s l)

Each straight access is simple over its full real support.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_disjoint {p q : Orthogonal.PairedPorts.Port} (h : p ≠ q) : Disjoint (Orthogonal.support (accessRoute p.1 p.2)) (Orthogonal.support (accessRoute q.1 q.2))

Distinct accesses have disjoint full real support.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_contact {s : Fin 4} {l : Fin 2} {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (accessRoute s l)) (hq : p ∈ Orthogonal.support e.2.2) : e.2.1 = terminal s l ∧ p = Orthogonal.realPoint (variablePosition (terminal s l))

Every continuous contact between an access and the core is its associated port.

theorem Cslib.Logic.PL.CNF.PairedCrossover.access_boundary_isolation {s : Fin 4} {l : Fin 2} {p : ℝ × ℝ} (hp : p ∈ Orthogonal.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 = Orthogonal.realPoint (boundaryPort s l))

Only the designated boundary point of an access lies on the outer box boundary.