A fixed degree-three crossover

Each of the eight degree-six internal variables is replaced by six cyclically ordered copies, with one directed implication between each consecutive pair. The four boundary variables and central variable retain their two occurrences. This is a fixed template, not a generic splitter.

Main definitions

• Cslib.Logic.PL.CNF.Crossover.SplitVariable: the 53 variables of the template.
• Cslib.Logic.PL.CNF.Crossover.splitFormula: its 74 clauses.

Main results

• Cslib.Logic.PL.CNF.Crossover.split_occurrences_le_three: internal degree bound.
• Cslib.Logic.PL.CNF.Crossover.split_terminal_occurrences: degree-two attachment 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 fixed local six-copy replacement is original.

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

The eight original internal variables that need local splitting.

• aInnerLeft : Internal
• upperLeft : Internal
• lowerLeft : Internal
• bInnerTop : Internal
• bInnerBottom : Internal
• upperRight : Internal
• lowerRight : Internal
• aInnerRight : Internal

@[instance_reducible]

instance Cslib.Logic.PL.CNF.Crossover.instDecidableEqInternal : DecidableEq Internal

@[instance_reducible]

instance Cslib.Logic.PL.CNF.Crossover.instReprInternal : Repr Internal

def Cslib.Logic.PL.CNF.Crossover.instReprInternal.repr : Internal → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Logic.PL.CNF.Crossover.instFintypeInternal : Fintype Internal

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

The five unsplit variables and six local copies of each degree-six variable.

• aLeft : SplitVariable
• aRight : SplitVariable
• bTop : SplitVariable
• bBottom : SplitVariable
• center : SplitVariable
• copy (v : Internal) (i : Fin 6) : SplitVariable

@[instance_reducible]

instance Cslib.Logic.PL.CNF.Crossover.instDecidableEqSplitVariable : DecidableEq SplitVariable

def Cslib.Logic.PL.CNF.Crossover.instDecidableEqSplitVariable.decEq (x✝ x✝¹ : SplitVariable) : Decidable (x✝ = x✝¹)

def Cslib.Logic.PL.CNF.Crossover.instReprSplitVariable.repr : SplitVariable → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Logic.PL.CNF.Crossover.instReprSplitVariable : Repr SplitVariable

@[instance_reducible]

instance Cslib.Logic.PL.CNF.Crossover.instFintypeSplitVariable : Fintype SplitVariable

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

The original variable represented by a split variable.

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

A distinguished representative of every original variable.

def Cslib.Logic.PL.CNF.Crossover.splitClauses : CNF SplitVariable

The original 26 clauses, using the cyclic copy determined by each local incidence ray.

def Cslib.Logic.PL.CNF.Crossover.ring (v : Internal) : CNF SplitVariable

The six implications around one fixed local square, in cyclic order.

def Cslib.Logic.PL.CNF.Crossover.internalList : List Internal

Fixed ordered list of the eight local split squares.

def Cslib.Logic.PL.CNF.Crossover.splitFormula : CNF SplitVariable

The degree-three crossover: original split clauses followed by eight implication rings.

def Cslib.Logic.PL.CNF.Crossover.splitTerminal : Fin 4 → SplitVariable

The four attachment variables, ordered left/right/top/bottom.

theorem Cslib.Logic.PL.CNF.Crossover.relabel_splitClauses : relabel SplitVariable.origin splitClauses = formula

Every original clause is recovered by forgetting its local copy index.

theorem Cslib.Logic.PL.CNF.Crossover.card_splitVariable : Fintype.card SplitVariable = 53

There are exactly 53 variable names.

theorem Cslib.Logic.PL.CNF.Crossover.length_splitFormula : List.length splitFormula = 74

There are exactly 74 clauses.

theorem Cslib.Logic.PL.CNF.Crossover.width_splitFormula (c : Clause SplitVariable) : c ∈ splitFormula → List.length c ≤ 3

Every clause has width at most three.

theorem Cslib.Logic.PL.CNF.Crossover.splitClauses_distinct_variables (c : Clause SplitVariable) : c ∈ splitFormula → (List.map Prod.fst c).Nodup

No clause repeats a variable, so literal-incidence degree equals clause occurrence degree.

theorem Cslib.Logic.PL.CNF.Crossover.split_occurrences_le_three (v : SplitVariable) : splitFormula.occurrences v ≤ 3

Every variable occurs in at most three clauses.

theorem Cslib.Logic.PL.CNF.Crossover.split_terminal_occurrences (i : Fin 4) : splitFormula.occurrences (splitTerminal i) = 2

Each boundary variable has two internal occurrences and capacity for one external clause.

theorem Cslib.Logic.PL.CNF.Crossover.eval_ring_iff (σ : SplitVariable → Bool) (v : Internal) : eval σ (ring v) = true ↔ ∀ (i : Fin 6), σ (SplitVariable.copy v i) = σ (SplitVariable.copy v 0)

A local implication ring forces all six copies to agree.

theorem Cslib.Logic.PL.CNF.Crossover.mem_internalList (v : Internal) : v ∈ internalList

Every internal variable belongs to the fixed ordered list.

theorem Cslib.Logic.PL.CNF.Crossover.eval_splitClauses_of_agree (σ : SplitVariable → Bool) (h : ∀ (v : Internal) (i : Fin 6), σ (SplitVariable.copy v i) = σ (SplitVariable.copy v 0)) : eval σ splitClauses = eval (σ ∘ representative) formula

Once each local ring agrees, evaluation is exactly evaluation of the original clauses.

theorem Cslib.Logic.PL.CNF.Crossover.eval_splitFormula_iff (σ : SplitVariable → Bool) : eval σ splitFormula = true ↔ eval (σ ∘ representative) formula = true ∧ ∀ (v : Internal) (i : Fin 6), σ (SplitVariable.copy v i) = σ (SplitVariable.copy v 0)

Exact semantics of the fixed degree-three template.

theorem Cslib.Logic.PL.CNF.Crossover.eval_splitFormula_lift (σ : Variable → Bool) (h : eval σ formula = true) : eval (σ ∘ SplitVariable.origin) splitFormula = true

Any original satisfying assignment lifts by assigning its value to every local copy.

theorem Cslib.Logic.PL.CNF.Crossover.split_boundary_eq_of_holds {σ : SplitVariable → Bool} (h : eval σ splitFormula = true) : σ SplitVariable.aLeft = σ SplitVariable.aRight ∧ σ SplitVariable.bTop = σ SplitVariable.bBottom

Satisfying the split crossover forces the two pairs of opposite ports to agree.

theorem Cslib.Logic.PL.CNF.Crossover.exists_split_holds (a b : Bool) : ∃ (σ : SplitVariable → Bool), eval σ splitFormula = true ∧ σ SplitVariable.aLeft = a ∧ σ SplitVariable.aRight = a ∧ σ SplitVariable.bTop = b ∧ σ SplitVariable.bBottom = b

Two arbitrary independent Boolean signals extend to a satisfying degree-three crossover.