Orthogonal drawing data for the paired-port crossover

The old internal drawing is retained. Each old terminal is replaced by ports at offsets 110 and 130, with the new implication clause at the old terminal position. Only the eight old terminal incidence routes are rerouted. The shared paired accesses end at these eight ports.

Main definitions

• variablePosition, clausePositions, incidenceRoutes: the 57-variable, 78-clause drawing. incidenceRoutes is the old route table lifted by liftIncidence, plus the bridge routes.
• accessRoute: the eight accesses from Orthogonal.PairedPorts.

References

The unchanged core comes from [Lichtenstein1982, Figs. 4–5] and [Tromino2025, Fig. 8(b)]. The paired terminal modification is original. Source credit for the core is in CrossoverLayoutData.

def Cslib.Logic.PL.CNF.PairedCrossover.variablePosition : Variable → Orthogonal.Point

The eight new ports use the shared paired interface; other vertices keep their positions.

def Cslib.Logic.PL.CNF.PairedCrossover.clausePositions : List Orthogonal.Point

The old clause positions followed by the four old terminal positions.

def Cslib.Logic.PL.CNF.PairedCrossover.liftIncidence : ℕ × Crossover.SplitVariable × Orthogonal.Route → ℕ × Variable × Orthogonal.Route

An incidence route of the old drawing in the paired drawing. The eight old terminal incidences are rerouted to the lane of the port that replaces their terminal, as chosen by mapLiteral; every other route is kept.

def Cslib.Logic.PL.CNF.PairedCrossover.incidenceRoutes : List (ℕ × Variable × Orthogonal.Route)

Exact clause-to-variable incidence routes in clause and literal order: the old routes, lifted by liftIncidence, followed by the routes of the four bridge clauses.

def Cslib.Logic.PL.CNF.PairedCrossover.boundaryPort : Fin 4 → Fin 2 → Orthogonal.Point

Boundary access points agree definitionally with the shared paired interface.

def Cslib.Logic.PL.CNF.PairedCrossover.accessRoute : Fin 4 → Fin 2 → Orthogonal.Route

Straight shared accesses to the eight degree-two terminals.

theorem Cslib.Logic.PL.CNF.PairedCrossover.terminal_position (s : Fin 4) (l : Fin 2) : variablePosition (terminal s l) = Orthogonal.PairedPorts.variablePosition s l

The terminal coordinates are exactly the shared paired-port positions.