Certified annular routing for ordered clause ports

All 24 ordered injections into the four side midpoints have three mutually disjoint simple orthogonal connector routes. Every connector meets the closed inner template square only at its prescribed endpoint. The certificates control entire real supports.

Main definitions

• routeBoxContactCheck: a finite route/closed-square contact certificate.
• CollarCheck: endpoint, simplicity, bounds, disjointness, and inner-square checks.

Main results

• collar_check: complete finite certificates for every valid ordered assignment.
• collar_core_contact, collar_disjoint: full continuous isolation consequences.

References

The finite annular routing certificates and proofs are original.

def Cslib.Complexity.SAT.ExactOne.routeBoxContactCheck (allowed : List Orthogonal.Point) (r : Orthogonal.Route) (c : Orthogonal.Point) (radius : ℕ) : Bool

A bounding-box contact test between every route segment and a closed square.

theorem Cslib.Complexity.SAT.ExactOne.routeBoxContactCheck_sound {allowed : List Orthogonal.Point} {r : Orthogonal.Route} {c : Orthogonal.Point} {radius : ℕ} (h : routeBoxContactCheck allowed r c radius = true) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support r) (hc : Orthogonal.inPointBox c radius p) : ∃ q ∈ allowed, p = Orthogonal.realPoint q

The finite square checker controls all real points of the route.

def Cslib.Complexity.SAT.ExactOne.CollarCheck (s : PortAssignment) : Prop

Complete finite conditions on the annular connector family.

@[instance_reducible]

instance Cslib.Complexity.SAT.ExactOne.instDecidableCollarCheck (s : PortAssignment) : Decidable (CollarCheck s)

theorem Cslib.Complexity.SAT.ExactOne.collar_check (s : PortAssignment) : s.Distinct → CollarCheck s

Every ordered injection has its complete annular routing certificate.

theorem Cslib.Complexity.SAT.ExactOne.collar_isSimple {s : PortAssignment} (hs : s.Distinct) (i : Fin 3) : Orthogonal.IsSimple ((collarRoutes s).getD ↑i [])

Every collar route is continuously simple.

theorem Cslib.Complexity.SAT.ExactOne.collar_disjoint {s : PortAssignment} (hs : s.Distinct) {i j : Fin 3} (hij : i ≠ j) : Disjoint (Orthogonal.support ((collarRoutes s).getD ↑i [])) (Orthogonal.support ((collarRoutes s).getD ↑j []))

Distinct collar routes have disjoint full real supports.

theorem Cslib.Complexity.SAT.ExactOne.collar_core_contact {s : PortAssignment} (hs : s.Distinct) {i : Fin 3} {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support ((collarRoutes s).getD ↑i [])) (hc : Orthogonal.inPointBox (270000, 270000) 90000 p) : p = Orthogonal.realPoint (collarInnerPort (collarReflected s) i)

A collar route meets the closed inner template square only at its prescribed endpoint.

theorem Cslib.Complexity.SAT.ExactOne.collar_route_costs (s : PortAssignment) : s.Distinct → ∀ (i : Fin 3), (List.consecutivePairs ((collarRoutes s).getD ↑i [])).length ≤ 7 ∧ Orthogonal.wireLength ((collarRoutes s).getD ↑i []) ≤ 600000

Each connector has at most seven segments and wire length at most 600000.

theorem Cslib.Complexity.SAT.ExactOne.collar_total_wireLength (s : PortAssignment) : s.Distinct → (List.map Orthogonal.wireLength (collarRoutes s)).sum ≤ 1780000

The entire three-connector family has wire length at most 1780000.