Directed wires for CNF substitution

A wire lists pairs of cell entry and exit variables, from its source to its clause. Local constraints must equate the two values in each cell. One binary implication joins each exit to the next entry. Positive literals direct that implication backwards; negative literals direct it forwards. In either case, a true literal at the final exit implies the source literal. Constant values satisfy every link.

These are conditional composition rules. They construct no layout and do not establish that any particular generator satisfies the local equalities or endpoint conditions.

Main definitions

• Cslib.Logic.PL.CNF.DirectedWire.links: one directed binary clause per cell gap.
• Cslib.Logic.PL.CNF.DirectedWire.assemble: endpoint clauses and links for indexed occurrences.

Main results

• Cslib.Logic.PL.CNF.DirectedWire.propagate: literal truth propagates from final exit to entry.
• Cslib.Logic.PL.CNF.DirectedWire.eval_links_of_constant: constant signals satisfy the links.
• Cslib.Logic.PL.CNF.DirectedWire.length_links: exact clause count, including empty wires.
• Cslib.Logic.PL.CNF.DirectedWire.eval_assemble_sound: projection under local constraints.
• Cslib.Logic.PL.CNF.DirectedWire.eval_assemble_complete: compatibility-based completeness.
• Cslib.Logic.PL.CNF.DirectedWire.length_assemble, Cslib.Logic.PL.CNF.DirectedWire.length_vars_assemble: exact total resource counts.

References

The polarity-directed composition and cell-pair construction are original.

def Cslib.Logic.PL.CNF.DirectedWire.link {V : Type u_1} (b : Bool) (previous next : V) : Clause V

A positive literal propagates truth backwards; a negative literal propagates falsity backwards by a forward implication. This reuses the ordinary implication-clause constructor.

def Cslib.Logic.PL.CNF.DirectedWire.links {V : Type u_1} (b : Bool) (cells : List (V × V)) : CNF V

One binary implication between each consecutive pair of cells, using its exit and entry.

theorem Cslib.Logic.PL.CNF.DirectedWire.eval_link_iff {V : Type u_1} (σ : V → Bool) (b : Bool) (previous next : V) : Clause.eval σ (link b previous next) = true ↔ σ next = b → σ previous = b

A link enforces exactly the direction needed for its literal's truth.

theorem Cslib.Logic.PL.CNF.DirectedWire.eval_links_iff {V : Type u_1} (σ : V → Bool) (b : Bool) (cells : List (V × V)) : eval σ (links b cells) = true ↔ ∀ p ∈ cells.consecutivePairs, σ p.2.1 = b → σ p.1.2 = b

All links hold exactly when literal truth propagates across every gap.

@[simp]

theorem Cslib.Logic.PL.CNF.DirectedWire.links_nil {V : Type u_1} (b : Bool) : links b [] = []

Empty and singleton cell lists have no intercell clauses.

@[simp]

theorem Cslib.Logic.PL.CNF.DirectedWire.links_singleton {V : Type u_1} (b : Bool) (cell : V × V) : links b [cell] = []

A single cell needs only its own local equality, with no additional wire clauses.

theorem Cslib.Logic.PL.CNF.DirectedWire.links_cons_cons {V : Type u_1} (b : Bool) (first next : V × V) (rest : List (V × V)) : links b (first :: next :: rest) = link b first.2 next.1 :: links b (next :: rest)

Splitting off the first gap leaves the links of the nonempty tail.

theorem Cslib.Logic.PL.CNF.DirectedWire.propagate {V : Type u_1} (σ : V → Bool) (b : Bool) (first : V × V) (rest : List (V × V)) (hcells : ∀ c ∈ first :: rest, σ c.1 = σ c.2) (hlinks : eval σ (links b (first :: rest)) = true) (hlast : σ ((first :: rest).getLastD first).2 = b) : σ first.1 = b

Given local entry/exit equality in each cell, final literal truth implies initial truth.

theorem Cslib.Logic.PL.CNF.DirectedWire.propagate_of_ne_nil {V : Type u_1} (σ : V → Bool) (b : Bool) (fallback : V) (cells : List (V × V)) (hne : cells ≠ []) (hcells : ∀ c ∈ cells, σ c.1 = σ c.2) (hlinks : eval σ (links b cells) = true) (hlast : σ (cells.getLastD (fallback, fallback)).2 = b) : σ (cells.headD (fallback, fallback)).1 = b

The propagation rule for a possibly empty list, with nonemptiness stated explicitly. The fallback only makes the endpoint expressions total; it is unused under this hypothesis.

theorem Cslib.Logic.PL.CNF.DirectedWire.eval_links_of_constant {V : Type u_1} (σ : V → Bool) (b value : Bool) (cells : List (V × V)) (h : ∀ c ∈ cells, σ c.1 = value ∧ σ c.2 = value) : eval σ (links b cells) = true

Assigning a common value to all entries and exits satisfies every directed link.

theorem Cslib.Logic.PL.CNF.DirectedWire.length_links_eq_gaps {V : Type u_1} (b : Bool) (cells : List (V × V)) : List.length (links b cells) = cells.consecutivePairs.length

There is exactly one clause per consecutive gap.

theorem Cslib.Logic.PL.CNF.DirectedWire.length_links {V : Type u_1} (b : Bool) (cells : List (V × V)) : List.length (links b cells) = cells.length - 1

A nonempty wire has one fewer link than cells; an empty wire has zero links.

theorem Cslib.Logic.PL.CNF.DirectedWire.length_link {V : Type u_1} (b : Bool) (previous next : V) : List.length (link b previous next) = 2

Every directed link has exactly two literals, even if its endpoints coincide.

theorem Cslib.Logic.PL.CNF.DirectedWire.length_of_mem_links {V : Type u_1} (b : Bool) (cells : List (V × V)) {c : Clause V} (hc : c ∈ links b cells) : List.length c = 2

Every clause of the wire is binary.

theorem Cslib.Logic.PL.CNF.DirectedWire.length_vars_links {V : Type u_1} (b : Bool) (cells : List (V × V)) : (links b cells).vars.length = 2 * (cells.length - 1)

There are exactly two literal occurrences per gap, with multiplicities retained.

def Cslib.Logic.PL.CNF.DirectedWire.replacementClauses {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (fallback : W) : CNF W

Replace each original literal by the final exit variable on its occurrence's wire, retaining its polarity and its clause/literal position.

def Cslib.Logic.PL.CNF.DirectedWire.allLinks {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) : CNF W

The directed-link clauses for every original literal occurrence, including duplicates.

def Cslib.Logic.PL.CNF.DirectedWire.assemble {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (fallback : W) : CNF W

Original clauses at their wire endpoints, followed by all directed links. Local cell constraints, such as crossover formulas, are supplied separately by the caller.

theorem Cslib.Logic.PL.CNF.DirectedWire.eval_replacementClauses_iff {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (fallback : W) (σ : W → Bool) : eval σ (replacementClauses φ wire fallback) = true ↔ ∀ c ∈ List.zipIdx φ, ∃ l ∈ List.zipIdx c.1, σ ((wire (c.2, l.2, l.1)).getLastD (fallback, fallback)).2 = l.1.2

Evaluation of the replacement clauses, indexed by the original clause and literal positions.

theorem Cslib.Logic.PL.CNF.DirectedWire.eval_allLinks_iff {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (σ : W → Bool) : eval σ (allLinks φ wire) = true ↔ ∀ o ∈ PL.occurrences φ, eval σ (links o.2.2.2 (wire o)) = true

The global link block holds exactly when every occurrence's wire links hold.

theorem Cslib.Logic.PL.CNF.DirectedWire.eval_assemble_sound {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (fallback : W) (τ : V → Bool) (σ : W → Bool) (hne : ∀ o ∈ PL.occurrences φ, wire o ≠ []) (hcells : ∀ o ∈ PL.occurrences φ, ∀ c ∈ wire o, σ c.1 = σ c.2) (hfirst : ∀ o ∈ PL.occurrences φ, σ ((wire o).headD (fallback, fallback)).1 = τ o.2.2.1) (h : eval σ (assemble φ wire fallback) = true) : eval τ φ = true

Satisfaction projects back to the ordinary source formula when the caller proves local cell equality and agreement between the first entries and source variable values.

theorem Cslib.Logic.PL.CNF.DirectedWire.eval_assemble_complete {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (fallback : W) (τ : V → Bool) (σ : W → Bool) (hne : ∀ o ∈ PL.occurrences φ, wire o ≠ []) (hcompat : ∀ o ∈ PL.occurrences φ, ∀ c ∈ wire o, σ c.1 = τ o.2.2.1 ∧ σ c.2 = τ o.2.2.1) (h : eval τ φ = true) : eval σ (assemble φ wire fallback) = true

A source satisfying assignment extends through the link assembly whenever the caller supplies one compatible target assignment constant along each occurrence's nonempty wire. This is an assignment-level conditional result, not an existence theorem for such a target.

theorem Cslib.Logic.PL.CNF.DirectedWire.map_length_replacementClauses {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (fallback : W) : List.map List.length (replacementClauses φ wire fallback) = List.map List.length φ

Clause replacement preserves all original clause widths.

theorem Cslib.Logic.PL.CNF.DirectedWire.length_allLinks {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) : List.length (allLinks φ wire) = (List.map (fun (o : Occurrence V) => (wire o).length - 1) (PL.occurrences φ)).sum

The link block has one clause per gap of each occurrence's wire.

theorem Cslib.Logic.PL.CNF.DirectedWire.length_assemble {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (fallback : W) : List.length (assemble φ wire fallback) = List.length φ + (List.map (fun (o : Occurrence V) => (wire o).length - 1) (PL.occurrences φ)).sum

Exact total clause count: original clauses plus all intercell gaps.

theorem Cslib.Logic.PL.CNF.DirectedWire.length_vars_replacementClauses {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (fallback : W) : (replacementClauses φ wire fallback).vars.length = φ.vars.length

Endpoint replacement preserves the number of source literal occurrences.

theorem Cslib.Logic.PL.CNF.DirectedWire.length_vars_allLinks {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) : (allLinks φ wire).vars.length = 2 * (List.map (fun (o : Occurrence V) => (wire o).length - 1) (PL.occurrences φ)).sum

The global link block contributes exactly two literals per gap.

theorem Cslib.Logic.PL.CNF.DirectedWire.length_vars_assemble {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (fallback : W) : (assemble φ wire fallback).vars.length = φ.vars.length + 2 * (List.map (fun (o : Occurrence V) => (wire o).length - 1) (PL.occurrences φ)).sum

Exact total literal count, with no distinctness assumptions on signal variables.

theorem Cslib.Logic.PL.CNF.DirectedWire.width_assemble {V : Type u_1} {W : Type u_2} (φ : CNF V) (wire : Occurrence V → List (W × W)) (fallback : W) {k : ℕ} (hwidth : ∀ c ∈ φ, List.length c ≤ k) (c : Clause W) : c ∈ assemble φ wire fallback → List.length c ≤ max k 2

Source clause widths are preserved and every added clause is binary.