Paired ports of a fixed square cell

Each side of [0,240]² has two ports, at offsets 110 and 130. Sides are ordered left, right, bottom, top. Lane zero always has the smaller coordinate; translation to an adjacent cell preserves the lane. Straight access routes end 20 units inside.

Main definitions

• boundaryPort, variablePosition, accessRoute: the eight paired accesses.
• oppositeSide, neighbor: matching sides and adjacent cell displacements.

Main results

• boundaryPort_shared: adjacent cells share the same port in the same lane.
• access_disjoint, access_boundary_isolation: continuous access separation.

References

This fixed geometric interface is original.

@[reducible, inline]

abbrev Cslib.Orthogonal.PairedPorts.Port : Type

A side and its lower- or higher-coordinate lane.

def Cslib.Orthogonal.PairedPorts.offset (l : Fin 2) : ℤ

The two lane coordinates.

def Cslib.Orthogonal.PairedPorts.boundaryPort (s : Fin 4) (l : Fin 2) : Point

Paired boundary ports, in left/right/bottom/top side order.

def Cslib.Orthogonal.PairedPorts.variablePosition (s : Fin 4) (l : Fin 2) : Point

The corresponding inner positions on the perimeter of [20,220]².

def Cslib.Orthogonal.PairedPorts.accessRoute (s : Fin 4) (l : Fin 2) : Route

Straight access from one boundary port to its corresponding inner position.

def Cslib.Orthogonal.PairedPorts.oppositeSide (s : Fin 4) : Fin 4

Opposite sides of neighboring cells.

def Cslib.Orthogonal.PairedPorts.neighbor (s : Fin 4) : Point

Displacement to the neighboring cell on the indicated side.

theorem Cslib.Orthogonal.PairedPorts.oppositeSide_involutive : Function.Involutive oppositeSide

Taking the opposite side twice recovers the original side.

theorem Cslib.Orthogonal.PairedPorts.boundaryPort_shared (p : Point) (s : Fin 4) (l : Fin 2) : cellOrigin 120 p + boundaryPort s l = cellOrigin 120 (p + neighbor s) + boundaryPort (oppositeSide s) l

Adjacent cells match ports without reversing the lane.

theorem Cslib.Orthogonal.PairedPorts.boundaryPort_injective : Function.Injective fun (p : Port) => boundaryPort p.1 p.2

All eight boundary positions are distinct.

theorem Cslib.Orthogonal.PairedPorts.variablePosition_injective : Function.Injective fun (p : Port) => variablePosition p.1 p.2

All eight inner positions are distinct.

theorem Cslib.Orthogonal.PairedPorts.variable_bounds (s : Fin 4) (l : Fin 2) : 20 ≤ (variablePosition s l).1 ∧ (variablePosition s l).1 ≤ 220 ∧ 20 ≤ (variablePosition s l).2 ∧ (variablePosition s l).2 ≤ 220

Every inner position lies in the smaller core square.

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

Every access is orthogonal, with its prescribed boundary and inner endpoints.

theorem Cslib.Orthogonal.PairedPorts.access_isSimple (s : Fin 4) (l : Fin 2) : IsSimple (accessRoute s l)

Every access is simple over its full real support.

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

Each access has one segment and 20 units of Manhattan length.

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

Finite certificate separating every pair of distinct accesses.

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

Distinct accesses have disjoint full real supports.

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

An access stays in the cell and touches its boundary only at the designated port.