Finite collars for every ordered three-port assignment

An inner square of side 180000 is centered inside a square of side 540000. Three disjoint orthogonal routes connect the inner north/west/east accesses to any three distinct outer side midpoints. A reflection of the inner layout selects the appropriate cyclic orientation. The tables use only multiples of 10000 and have at most seven segments per route.

Main definitions

• PortAssignment: three ordered sides, using left/right/bottom/top as 0/1/2/3.
• collarReflected, collarRoutes: the finite orientation and connector tables.
• collarOuterPort, collarInnerPort: prescribed exterior and interior endpoints.

References

These finite annular routing tables are original.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.ExactOne.PortAssignment : Type

Three ordered outer sides; the geometry certificate assumes they are distinct.

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

The three designated sides are distinct.

@[instance_reducible]

instance Cslib.Complexity.SAT.ExactOne.instDecidableDistinct (s : PortAssignment) : Decidable s.Distinct

def Cslib.Complexity.SAT.ExactOne.PortAssignment.side (s : PortAssignment) (i : Fin 3) : Fin 4

Side assigned to an indexed terminal.

def Cslib.Complexity.SAT.ExactOne.collarAssignments : List PortAssignment

All 24 ordered injections into the four outer sides.

def Cslib.Complexity.SAT.ExactOne.collarReflections : List Bool

Finite reflection choices, in collarAssignments order.

def Cslib.Complexity.SAT.ExactOne.collarRouteTable : List (List Orthogonal.Route)

All connector tables, with routes oriented from the outer boundary to the inner square.

def Cslib.Complexity.SAT.ExactOne.collarReflected (s : PortAssignment) : Bool

The reflection required for the selected ordered assignment.

def Cslib.Complexity.SAT.ExactOne.collarRoutes (s : PortAssignment) : List Orthogonal.Route

Three outer-to-inner collar routes. Invalid repeated-side assignments use an empty default.

def Cslib.Complexity.SAT.ExactOne.collarOuterPort (s : Fin 4) : Orthogonal.Point

Exterior midpoint in left/right/bottom/top order.

def Cslib.Complexity.SAT.ExactOne.collarInnerPort (reflected : Bool) (i : Fin 3) : Orthogonal.Point

The translated inner port, including the selected horizontal reflection.