The finite crossover relation

The 26 clauses formalize Lichtenstein’s crossover [Lichtenstein1982, Figs. 4–5], drawn on a grid by MIT–ULB CompGeom Group [Tromino2025, Fig. 8(b)]. The Lean table is adapted from edemaine/lean-trominoes at 6d5b36c15cec6cb18d30137b7f1c7fb92ea24332, PlanarThreeSATGadgets.lean. This file uses the ordinary CNF semantics. Geometry and local degree reduction are separate.

Main definitions

• Cslib.Logic.PL.CNF.Crossover.formula: the fixed 13-variable, 26-clause formula.

Main results

• Cslib.Logic.PL.CNF.Crossover.extends_iff: opposite boundary values agree independently.
• Cslib.Logic.PL.CNF.Crossover.terminal_occurrences: each terminal has two internal incidences, leaving capacity for one external implication under the degree-three bound.

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 clause table and truth-table certificate adapt the Lean source cited above.

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

Variables named by their role in the fixed crossover.

• aLeft : Variable
• aInnerLeft : Variable
• upperLeft : Variable
• lowerLeft : Variable
• bTop : Variable
• bInnerTop : Variable
• center : Variable
• bInnerBottom : Variable
• bBottom : Variable
• upperRight : Variable
• lowerRight : Variable
• aInnerRight : Variable
• aRight : Variable

@[instance_reducible]

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

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

@[instance_reducible]

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

@[instance_reducible]

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

Explicit enumeration avoids relying on generated metaprogram data for the finite certificate.

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

The fixed crossover clauses, in the source figure's order.

def Cslib.Logic.PL.CNF.Crossover.assignment (aLeft aRight bTop bBottom aInnerLeft upperLeft lowerLeft bInnerTop center bInnerBottom upperRight lowerRight aInnerRight : Bool) : Variable → Bool

Assemble four boundary values and nine internal values into an assignment.

def Cslib.Logic.PL.CNF.Crossover.Extends (aLeft aRight bTop bBottom : Bool) : Prop

A boundary assignment extends to all nine internal crossover variables.

@[instance_reducible]

instance Cslib.Logic.PL.CNF.Crossover.instDecidableExtends (aLeft aRight bTop bBottom : Bool) : Decidable (Extends aLeft aRight bTop bBottom)

theorem Cslib.Logic.PL.CNF.Crossover.extends_iff (aLeft aRight bTop bBottom : Bool) : Extends aLeft aRight bTop bBottom ↔ aLeft = aRight ∧ bTop = bBottom

Exhaustive certificate for Lichtenstein’s crossover [Lichtenstein1982, Figs. 4–5], as drawn in [Tromino2025, Fig. 8(b)]: horizontal and vertical values propagate independently.

theorem Cslib.Logic.PL.CNF.Crossover.boundary_eq_of_holds {σ : Variable → Bool} (holds : eval σ formula = true) : σ Variable.aLeft = σ Variable.aRight ∧ σ Variable.bTop = σ Variable.bBottom

Every satisfying assignment to the crossover propagates each boundary value to the opposite port. This is the soundness direction needed when a crossover embedded in a larger formula is projected back to its two original wires.

theorem Cslib.Logic.PL.CNF.Crossover.exists_holds_of_boundary_eq {aLeft aRight bTop bBottom : Bool} (horizontal : aLeft = aRight) (vertical : bTop = bBottom) : ∃ (σ : Variable → Bool), eval σ formula = true ∧ σ Variable.aLeft = aLeft ∧ σ Variable.aRight = aRight ∧ σ Variable.bTop = bTop ∧ σ Variable.bBottom = bBottom

Conversely, two independently propagated boundary values can always be extended to a satisfying assignment of the whole crossover.

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

The four boundary variables, in left/right/top/bottom order.

theorem Cslib.Logic.PL.CNF.Crossover.length_formula : List.length formula = 26

The formula has exactly 26 clauses.

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

Every clause has width at most three.

theorem Cslib.Logic.PL.CNF.Crossover.occurrences_le_six (v : Variable) : formula.occurrences v ≤ 6

Original internal variables have degree at most six, before local splitting.

theorem Cslib.Logic.PL.CNF.Crossover.terminal_occurrences (i : Fin 4) : formula.occurrences (terminal i) = 2

A terminal uses two internal incidences, leaving one external clause incidence.