Gluing clause templates to ordered-port collars

Templates of side 180000 are translated, and optionally reflected, into the central square of the side-540000 collar. A clause-to-inner-boundary prefix then extends along its reversed collar route. The continuous certificates compose through their unique common endpoint.

Main definitions

• collarPoint, collarRoute: the common affine placement of an inner template.
• collarPrefixRoute: a placed local prefix followed by its inner-to-outer collar.
• collaredPrefixGeometry: the actual finite placed template and its extended incidences.

Main results

• isSimple_collarPrefixRoute, isOrthogonal_collarPrefixRoute.
• support_collarPrefixRoute, wireLength_collarPrefixRoute.

References

These finite local-placement and gluing constructions are original.

def Cslib.Complexity.SAT.ExactOne.collarOffset (reflected : Bool) : Orthogonal.Point

Translation part of the reflected or unreflected inner-template placement.

def Cslib.Complexity.SAT.ExactOne.collarPoint (reflected : Bool) (p : Orthogonal.Point) : Orthogonal.Point

Place a point of the side-180000 template inside the central collar square.

def Cslib.Complexity.SAT.ExactOne.collarReal (reflected : Bool) (p : ℝ × ℝ) : ℝ × ℝ

The corresponding placement in the real plane.

def Cslib.Complexity.SAT.ExactOne.collarRoute (reflected : Bool) (r : Orthogonal.Route) : Orthogonal.Route

Place an entire local route.

theorem Cslib.Complexity.SAT.ExactOne.collarRoute_eq_map (reflected : Bool) (r : Orthogonal.Route) : collarRoute reflected r = List.map (collarPoint reflected) r

Route placement is pointwise placement of the finite list.

theorem Cslib.Complexity.SAT.ExactOne.realPoint_collarPoint (reflected : Bool) (p : Orthogonal.Point) : Orthogonal.realPoint (collarPoint reflected p) = collarReal reflected (Orthogonal.realPoint p)

Placement commutes with inclusion of the integer lattice.

theorem Cslib.Complexity.SAT.ExactOne.collarReal_injective (reflected : Bool) : Function.Injective (collarReal reflected)

The common affine placement does not identify real points.

theorem Cslib.Complexity.SAT.ExactOne.collarPoint_injective (reflected : Bool) : Function.Injective (collarPoint reflected)

The common affine placement does not identify integer vertices.

theorem Cslib.Complexity.SAT.ExactOne.support_collarRoute (reflected : Bool) (r : Orthogonal.Route) : Orthogonal.support (collarRoute reflected r) = collarReal reflected '' Orthogonal.support r

Placement maps the full continuous support.

theorem Cslib.Complexity.SAT.ExactOne.mem_support_collarRoute_iff (reflected : Bool) (r : Orthogonal.Route) (p : ℝ × ℝ) : collarReal reflected p ∈ Orthogonal.support (collarRoute reflected r) ↔ p ∈ Orthogonal.support r

Membership in a placed support is exactly placed membership.

theorem Cslib.Complexity.SAT.ExactOne.isOrthogonal_collarRoute (reflected : Bool) {r : Orthogonal.Route} (hr : Orthogonal.IsOrthogonal r) : Orthogonal.IsOrthogonal (collarRoute reflected r)

Placement preserves proper orthogonality.

theorem Cslib.Complexity.SAT.ExactOne.isSimple_collarRoute (reflected : Bool) {r : Orthogonal.Route} (hr : Orthogonal.IsSimple r) : Orthogonal.IsSimple (collarRoute reflected r)

Placement preserves continuous simplicity.

theorem Cslib.Complexity.SAT.ExactOne.wireLength_collarRoute (reflected : Bool) (r : Orthogonal.Route) : Orthogonal.wireLength (collarRoute reflected r) = Orthogonal.wireLength r

Placement preserves total Manhattan wire length.

theorem Cslib.Complexity.SAT.ExactOne.consecutivePairs_length_collarRoute (reflected : Bool) (r : Orthogonal.Route) : (List.consecutivePairs (collarRoute reflected r)).length = (List.consecutivePairs r).length

Placement preserves the listed segment count.

def Cslib.Complexity.SAT.ExactOne.innerTemplatePort (i : Fin 3) : Orthogonal.Point

The fixed north/west/east ports of an unplaced inner template.

theorem Cslib.Complexity.SAT.ExactOne.collarPoint_innerTemplatePort (reflected : Bool) (i : Fin 3) : collarPoint reflected (innerTemplatePort i) = collarInnerPort reflected i

Placement identifies the inner template ports with the collar's inner endpoints.

theorem Cslib.Complexity.SAT.ExactOne.support_inPointBox_of_points {r : Orthogonal.Route} {c : Orthogonal.Point} {radius : ℕ} (hr : ∀ q ∈ r, Orthogonal.inPointBox c radius (Orthogonal.realPoint q)) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support r) : Orthogonal.inPointBox c radius p

Pointwise box bounds extend to the full real polygonal support.

theorem Cslib.Complexity.SAT.ExactOne.collarPoint_in_innerBox (reflected : Bool) {q : Orthogonal.Point} (hq : 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) : Orthogonal.inPointBox (270000, 270000) 90000 (Orthogonal.realPoint (collarPoint reflected q))

Placed points of the original template lie in the collar's closed inner square.

theorem Cslib.Complexity.SAT.ExactOne.collarRoute_in_innerBox (reflected : Bool) {r : Orthogonal.Route} (hr : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (collarRoute reflected r)) : Orthogonal.inPointBox (270000, 270000) 90000 p

A placed local route stays inside the collar's closed inner square.

def Cslib.Complexity.SAT.ExactOne.collarPrefixRoute (s : PortAssignment) (i : Fin 3) (r : Orthogonal.Route) : Orthogonal.Route

Extend an inner clause-to-boundary prefix along the reversed annular connector.

theorem Cslib.Complexity.SAT.ExactOne.isOrthogonal_collarPrefixRoute {s : PortAssignment} (hs : s.Distinct) {i : Fin 3} {r : Orthogonal.Route} (hr : List.getLast? r = some (innerTemplatePort i)) (ho : Orthogonal.IsOrthogonal r) : Orthogonal.IsOrthogonal (collarPrefixRoute s i r)

Extending a local prefix preserves proper orthogonality.

theorem Cslib.Complexity.SAT.ExactOne.support_collarPrefixRoute {s : PortAssignment} (hs : s.Distinct) {i : Fin 3} {r : Orthogonal.Route} (hr : List.getLast? r = some (innerTemplatePort i)) : Orthogonal.support (collarPrefixRoute s i r) = Orthogonal.support (collarRoute (collarReflected s) r) ∪ Orthogonal.support ((collarRoutes s).getD ↑i [])

The support of an extended prefix is precisely the union of its placed local support and its annular connector.

theorem Cslib.Complexity.SAT.ExactOne.isSimple_collarPrefixRoute {s : PortAssignment} (hs : s.Distinct) {i : Fin 3} {r : Orthogonal.Route} (hr : List.getLast? r = some (innerTemplatePort i)) (hsr : Orthogonal.IsSimple r) (hb : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) : Orthogonal.IsSimple (collarPrefixRoute s i r)

Local prefix and annular connector glue to a continuously simple route.

theorem Cslib.Complexity.SAT.ExactOne.wireLength_collarPrefixRoute {s : PortAssignment} (hs : s.Distinct) {i : Fin 3} {r : Orthogonal.Route} (hr : List.getLast? r = some (innerTemplatePort i)) : Orthogonal.wireLength (collarPrefixRoute s i r) = Orthogonal.wireLength r + Orthogonal.wireLength ((collarRoutes s).getD ↑i [])

Extending a prefix adds exactly the annular connector's wire length.

theorem Cslib.Complexity.SAT.ExactOne.consecutivePairs_length_collarPrefixRoute {s : PortAssignment} (hs : s.Distinct) {i : Fin 3} {r : Orthogonal.Route} (hr : List.getLast? r = some (innerTemplatePort i)) : (List.consecutivePairs (collarPrefixRoute s i r)).length = (List.consecutivePairs r).length + (List.consecutivePairs ((collarRoutes s).getD ↑i [])).length

Extending a prefix adds exactly the annular connector's listed segments.

theorem Cslib.Complexity.SAT.ExactOne.disjoint_collarRoute_connector {s : PortAssignment} (hs : s.Distinct) {i : Fin 3} {r : Orthogonal.Route} (hb : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) (hi : Orthogonal.realPoint (innerTemplatePort i) ∉ Orthogonal.support r) : Disjoint (Orthogonal.support (collarRoute (collarReflected s) r)) (Orthogonal.support ((collarRoutes s).getD ↑i []))

A placed core route avoiding an inner port is disjoint from that port's annular connector.

theorem Cslib.Complexity.SAT.ExactOne.collarPrefixRoute_contact {s : PortAssignment} (hs : s.Distinct) {i j : Fin 3} (hij : i ≠ j) {r t : Orthogonal.Route} (hr : List.getLast? r = some (innerTemplatePort i)) (ht : List.getLast? t = some (innerTemplatePort j)) (hbr : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) (hbt : ∀ q ∈ t, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) (hri : Orthogonal.realPoint (innerTemplatePort j) ∉ Orthogonal.support r) (htj : Orthogonal.realPoint (innerTemplatePort i) ∉ Orthogonal.support t) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (collarPrefixRoute s i r)) (hq : p ∈ Orthogonal.support (collarPrefixRoute s j t)) : ∃ q ∈ Orthogonal.support r, q ∈ Orthogonal.support t ∧ p = collarReal (collarReflected s) q

Intersections between two distinct extended prefixes come entirely from intersections of their original local routes. The two local routes must avoid each other's inner port.

theorem Cslib.Complexity.SAT.ExactOne.collarPrefixRoute_not_mem_corePoint {s : PortAssignment} (hs : s.Distinct) {i : Fin 3} {r : Orthogonal.Route} (hr : List.getLast? r = some (innerTemplatePort i)) {q : Orthogonal.Point} (hq : 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) (hqi : q ≠ innerTemplatePort i) (hn : Orthogonal.realPoint q ∉ Orthogonal.support r) : Orthogonal.realPoint (collarPoint (collarReflected s) q) ∉ Orthogonal.support (collarPrefixRoute s i r)

An extended prefix avoids a placed inner-template vertex when its local route avoids that vertex and it is not the prefix's own boundary terminal.

def Cslib.Complexity.SAT.ExactOne.collarBoundaryRoute : Orthogonal.Route

The perimeter of the outer collar square.

theorem Cslib.Complexity.SAT.ExactOne.collar_outer_boundary_contact {s : PortAssignment} (hs : s.Distinct) {i : Fin 3} {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support ((collarRoutes s).getD ↑i [])) (hb : p ∈ Orthogonal.support collarBoundaryRoute) : p = Orthogonal.realPoint (collarOuterPort (s.side i))

The collar's full support meets its outer perimeter only at its own assigned port.

theorem Cslib.Complexity.SAT.ExactOne.collarPrefixRoute_outer_boundary_contact {s : PortAssignment} (hs : s.Distinct) {i : Fin 3} {r : Orthogonal.Route} (hr : List.getLast? r = some (innerTemplatePort i)) (hbr : ∀ q ∈ r, 0 ≤ q.1 ∧ q.1 ≤ 180000 ∧ 0 ≤ q.2 ∧ q.2 ≤ 180000) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (collarPrefixRoute s i r)) (hb : p ∈ Orthogonal.support collarBoundaryRoute) : p = Orthogonal.realPoint (collarOuterPort (s.side i))

The full support of an extended prefix meets the outer perimeter only at its assigned source port.

def Cslib.Complexity.SAT.ExactOne.terminalIndex (g : LocalGeometry) (v : ℕ) : Fin 3

Position of an exposed variable in the ordered terminal list, with an irrelevant default for malformed local data containing more than three terminals.

def Cslib.Complexity.SAT.ExactOne.collaredPrefixGeometry (g : LocalGeometry) (s : PortAssignment) : LocalGeometry

Place a finite prefix template and extend its source incidences to arbitrary ordered outer sides. Source ghost positions follow those same outer ports; actual internal vertices and all clause positions receive the common affine placement.