A crossover with two attachment ports per side

Each old terminal is replaced by two ports and one implication between them. Together with its two old incidences this forms an implication chain between two equal internal copies. Consequently both ports have the old terminal's uniquely determined value. Each port has two internal incidences and room for one external incidence. The unchanged internal core comes from Lichtenstein's crossover [Lichtenstein1982, Figs. 4–5], as drawn in [Tromino2025, Fig. 8(b)].

Main definitions

• PairedCrossover.formula: the 57-variable, 78-clause paired-port template.
• PairedCrossover.canonicalExtension: its full assignment from two input bits.

Main results

• PairedCrossover.existsUnique_holds: a unique full satisfying assignment for each input pair.
• PairedCrossover.eval_formula_iff: split-formula semantics with paired-terminal agreement.
• PairedCrossover.eq_canonicalExtension_of_holds: uniqueness of the full extension.
• PairedCrossover.terminal_occurrences: two internal incidences at each of the eight ports.

References

• David Lichtenstein, Planar Formulae and Their Uses, Figs. 4–5 [Lic82].
• MIT–ULB CompGeom Group, Undecidability of Tiling with a Tromino, Fig. 8(b) [MITULBCGGAA+25].

The paired-terminal replacement and its uniqueness proof are original.

inductive Cslib.Logic.PL.CNF.PairedCrossover.Variable : Type

Eight boundary ports, the unsplit center, and the old 48 internal copies.

• port (side : Fin 4) (lane : Fin 2) : Variable
• center : Variable
• copy (v : Crossover.Internal) (i : Fin 6) : Variable

@[instance_reducible]

instance Cslib.Logic.PL.CNF.PairedCrossover.instDecidableEqVariable : DecidableEq Variable

def Cslib.Logic.PL.CNF.PairedCrossover.instDecidableEqVariable.decEq (x✝ x✝¹ : Variable) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Logic.PL.CNF.PairedCrossover.instReprVariable : Repr Variable

def Cslib.Logic.PL.CNF.PairedCrossover.instReprVariable.repr : Variable → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Logic.PL.CNF.PairedCrossover.instFintypeVariable : Fintype Variable

def Cslib.Logic.PL.CNF.PairedCrossover.terminal : Fin 4 → Fin 2 → Variable

The eight attachment ports in left/right/bottom/top geometric order, with two lanes per side. The source variables .bTop and .bBottom retain their historical names.

def Cslib.Logic.PL.CNF.PairedCrossover.Variable.origin : Variable → Crossover.SplitVariable

Forget the lane of a boundary port.

def Cslib.Logic.PL.CNF.PairedCrossover.representative : Crossover.SplitVariable → Variable

Choose lane zero as the representative of each old terminal.

def Cslib.Logic.PL.CNF.PairedCrossover.mapLiteral : Literal Crossover.SplitVariable → Literal Variable

Replace each old boundary literal by the port at that incidence's geometric lane.

def Cslib.Logic.PL.CNF.PairedCrossover.bridges : CNF Variable

One directed implication joins the paired ports on each side.

def Cslib.Logic.PL.CNF.PairedCrossover.formula : CNF Variable

Preserve the old 74 clauses with their terminal incidences separated, then add four bridges.

def Cslib.Logic.PL.CNF.PairedCrossover.chainStart : Fin 4 → Variable

The internal copy at the start of each terminal's implication chain.

def Cslib.Logic.PL.CNF.PairedCrossover.chainEnd : Fin 4 → Variable

The internal copy at the end of each terminal's implication chain.

def Cslib.Logic.PL.CNF.PairedCrossover.firstLane : Fin 4 → Fin 2

The first lane in each directed chain.

def Cslib.Logic.PL.CNF.PairedCrossover.chain : Fin 4 → CNF Variable

Three existing clauses form a chain between two equal internal copies.

theorem Cslib.Logic.PL.CNF.PairedCrossover.eval_formula_iff (σ : Variable → Bool) : eval σ formula = true ↔ eval (σ ∘ representative) Crossover.splitFormula = true ∧ ∀ (s : Fin 4), σ (terminal s 0) = σ (terminal s 1)

Exact semantics: the old split formula together with agreement of each paired terminal.

def Cslib.Logic.PL.CNF.PairedCrossover.canonicalExtension (a b : Bool) : Variable → Bool

The explicit unique full assignment, including both lanes on every side.

theorem Cslib.Logic.PL.CNF.PairedCrossover.eval_canonicalExtension (a b : Bool) : eval (canonicalExtension a b) formula = true

The explicit full assignment satisfies the paired-port formula.

theorem Cslib.Logic.PL.CNF.PairedCrossover.terminal_values_canonicalExtension (a b : Bool) (s : Fin 4) (l : Fin 2) : canonicalExtension a b (terminal s l) = if ↑s < 2 then a else b

Both lanes on the left and right carry a; both lanes on the top and bottom carry b.

theorem Cslib.Logic.PL.CNF.PairedCrossover.eq_canonicalExtension_of_holds {σ : Variable → Bool} (h : eval σ formula = true) : σ = canonicalExtension (σ (terminal 0 0)) (σ (terminal 2 0))

Every satisfying full assignment is determined by the left and top lane-zero inputs.

theorem Cslib.Logic.PL.CNF.PairedCrossover.terminal_value_of_holds {σ : Variable → Bool} (h : eval σ formula = true) (s : Fin 4) (l : Fin 2) : σ (terminal s l) = if ↑s < 2 then σ (terminal 0 0) else σ (terminal 2 0)

All satisfying terminal values are the horizontal or vertical input value.

theorem Cslib.Logic.PL.CNF.PairedCrossover.eval_representative_of_holds {σ : Variable → Bool} (h : eval σ formula = true) : eval (σ ∘ representative) Crossover.splitFormula = true

Projecting a satisfying paired assignment recovers a satisfying old split assignment.

theorem Cslib.Logic.PL.CNF.PairedCrossover.existsUnique_holds (a b : Bool) : ∃! σ : Variable → Bool, eval σ formula = true ∧ σ (terminal 0 0) = a ∧ σ (terminal 2 0) = b

Every two-bit input has exactly one satisfying full assignment.

theorem Cslib.Logic.PL.CNF.PairedCrossover.card_variable : Fintype.card Variable = 57

The template uses exactly 57 variables.

theorem Cslib.Logic.PL.CNF.PairedCrossover.length_formula : List.length formula = 78

The template has exactly 78 clauses.

theorem Cslib.Logic.PL.CNF.PairedCrossover.width_formula (c : Clause Variable) : c ∈ formula → List.length c ≤ 3

All clauses have width at most three.

theorem Cslib.Logic.PL.CNF.PairedCrossover.distinct_variables (c : Clause Variable) : c ∈ formula → (List.map Prod.fst c).Nodup

No clause repeats a variable.

theorem Cslib.Logic.PL.CNF.PairedCrossover.occurrences_le_three (v : Variable) : formula.occurrences v ≤ 3

Every variable has at most three internal incidences.

theorem Cslib.Logic.PL.CNF.PairedCrossover.terminal_occurrences (s : Fin 4) (l : Fin 2) : formula.occurrences (terminal s l) = 2

Each of the eight ports has exactly two internal incidences.