Compatible assignments on canonical paths

The optional crossover tags are retained only as a logical assignment bridge for the paired compiler. There is no second output formula or drawing. A compatible assignment carries each source value along its path and satisfies each selected fixed crossover.

Main definitions

• Cslib.Complexity.SAT.PlanarCompile.Variable, .signal, .wire: the logical path bridge.

Main results

• Cslib.Complexity.SAT.PlanarCompile.occurrencePath_crossing_straight.
• Cslib.Complexity.SAT.PlanarCompile.source_center_not_crossing.
• Cslib.Complexity.SAT.PlanarCompile.ordinary_cell_source_eq.
• Cslib.Complexity.SAT.PlanarCompile.crossing_axis_occurrence_eq.
• Cslib.Complexity.SAT.PlanarCompile.exists_compatible_assignment.

References

These are the shared canonical incidence-path constructions and certificates.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.PlanarCompile.Variable : Type

A cell's ordinary signal, or a local variable of its crossover.

def Cslib.Complexity.SAT.PlanarCompile.signal (sites : List Orthogonal.Point) (p q : Orthogonal.Point) : Variable

The signal presented by a cell toward a neighboring cell.

def Cslib.Complexity.SAT.PlanarCompile.wire (sites : List Orthogonal.Point) (r : Orthogonal.Route) : List (Variable × Variable)

Every cell before the original clause vertex contributes an entry/exit signal pair. At the source endpoint the unused entry defaults to the source's own ordinary signal.

theorem Cslib.Complexity.SAT.PlanarCompile.length_wire (sites : List Orthogonal.Point) (r : Orthogonal.Route) : (wire sites r).length = List.length r - 1

A path contributes one signal cell for each point before its final clause vertex.

theorem Cslib.Complexity.SAT.PlanarCompile.wire_ne_nil (sites : List Orthogonal.Point) (r : Orthogonal.Route) (h : 2 ≤ List.length r) : wire sites r ≠ []

Every path of at least two points yields a nonempty cell wire.

theorem Cslib.Complexity.SAT.PlanarCompile.getElem_wire (sites : List Orthogonal.Point) (r : Orthogonal.Route) (i : ℕ) (hi : i < List.length r - 1) : (wire sites r)[i] = (signal sites r[i] (List.getD r (i - 1) r[i]), signal sites r[i] (List.getD r (i + 1) r[i]))

Exact indexed cell signals in the executable wire list.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrence_edgeEndpoint {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) (side : Bool) : (incidenceGraph φ).edgeEndpoint (List.idxOf o (Logic.PL.occurrences φ)) side = if side = true then φ.distinctVars.length + o.1 else List.idxOf o.2.2.1 φ.distinctVars

The actual graph edge has the occurrence's original variable and clause labels.

theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePath_crossing_straight {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) {p : Orthogonal.Point} (hp : p ∈ crossingSites φ) (hpi : p ∈ occurrencePath φ o) : Orthogonal.StraightThrough (occurrencePath φ o) p (1, 0) ∨ Orthogonal.StraightThrough (occurrencePath φ o) p (0, 1)

A selected crossing is traversed straight along one coordinate axis by each occupying path.

theorem Cslib.Complexity.SAT.PlanarCompile.source_center_not_crossing {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : Orthogonal.Layout.center (List.idxOf o.2.2.1 φ.distinctVars) ∉ crossingSites φ

The initial source center is excluded from the actual selected crossing list.

theorem Cslib.Complexity.SAT.PlanarCompile.wire_first_entry {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) (fallback : Variable) : ((wire (crossingSites φ) (occurrencePath φ o)).headD (fallback, fallback)).1 = (Orthogonal.Layout.center (List.idxOf o.2.2.1 φ.distinctVars), none)

The executable first entry is the original variable's ordinary cell signal.

theorem Cslib.Complexity.SAT.PlanarCompile.shared_ordinary_cell_center {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {o t : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) (ht : t ∈ Logic.PL.occurrences φ) (hot : o ≠ t) {p : Orthogonal.Point} (hp : p ∉ crossingSites φ) (hpo : p ∈ occurrencePath φ o) (hpt : p ∈ occurrencePath φ t) : p ∈ (incidenceGraph φ).orthogonalPositions

Two different occurrence paths sharing an ordinary cell meet at a declared vertex center.

theorem Cslib.Complexity.SAT.PlanarCompile.clause_center_not_mem_dropLast {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : Orthogonal.Layout.center (φ.distinctVars.length + o.1) ∉ List.dropLast (occurrencePath φ o)

No retained wire cell is the clause-center endpoint removed by dropLast.

theorem Cslib.Complexity.SAT.PlanarCompile.dropLast_center_eq_source {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) {p : Orthogonal.Point} (hp : p ∈ List.dropLast (occurrencePath φ o)) (hc : p ∈ (incidenceGraph φ).orthogonalPositions) : p = Orthogonal.Layout.center (List.idxOf o.2.2.1 φ.distinctVars)

A retained cell at a declared center is the source-variable center of its occurrence.

theorem Cslib.Complexity.SAT.PlanarCompile.ordinary_cell_source_eq {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {o t : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) (ht : t ∈ Logic.PL.occurrences φ) {p : Orthogonal.Point} (hp : p ∉ crossingSites φ) (hpo : p ∈ List.dropLast (occurrencePath φ o)) (hpt : p ∈ List.dropLast (occurrencePath φ t)) : o.2.2.1 = t.2.2.1

All occurrences using an ordinary retained cell have the same original variable.

theorem Cslib.Complexity.SAT.PlanarCompile.crossing_axis_occurrence_eq {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {o t : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) (ht : t ∈ Logic.PL.occurrences φ) {p d : Orthogonal.Point} (hp : p ∈ crossingSites φ) (hpo : p ∈ occurrencePath φ o) (hpt : p ∈ occurrencePath φ t) (hs : Orthogonal.StraightThrough (occurrencePath φ o) p d) (hts : Orthogonal.StraightThrough (occurrencePath φ t) p d) : o = t

At a crossing, at most one occurrence path goes straight through in a given direction.

theorem Cslib.Complexity.SAT.PlanarCompile.exists_compatible_assignment {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) (τ : ℕ → Bool) : ∃ (σ : Variable → Bool), (∀ o ∈ Logic.PL.occurrences φ, ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), σ c.1 = τ o.2.2.1 ∧ σ c.2 = τ o.2.2.1) ∧ ∀ p ∈ crossingSites φ, Logic.PL.CNF.eval (fun (v : Logic.PL.CNF.Crossover.SplitVariable) => σ (p, some v)) Logic.PL.CNF.Crossover.splitFormula = true

Every source assignment extends compatibly to all actual wire cells and crossover blocks. The choice of auxiliary values is logical; this theorem makes no computational claim.