Assignment semantics of the paired compiler

The actual clause blocks use ordinary CNF evaluation. Local rings and crossovers identify the four wire values within each cell; paired links identify consecutive cell values. The source assignment then determines every used output variable.

Main definitions

• Cslib.Complexity.SAT.ParsimoniousPlanar.wire: the actual two-lane entry and exit variables.

Main results

• Cslib.Complexity.SAT.ParsimoniousPlanar.eval_rawFormula_iff: exact clause-block semantics.

References

These are original composition proofs for the finite paired compiler.

def Cslib.Complexity.SAT.ParsimoniousPlanar.wire (sites : List Orthogonal.Point) (r : Orthogonal.Route) : List (Logic.PL.CNF.PairedWire.Cell Variable)

Every retained point contributes the entry and exit on each of its two lanes.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.map_fst_ordinaryClauses (p : Orthogonal.Point) : List.map Prod.fst (ordinaryClauses p) = Logic.PL.CNF.relabel (fun (v : Fin 4 × Fin 2) => (p, Sum.inl v)) OrdinaryRing.formula

The two local clause tables retain their exact formulas under variable tagging.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.map_fst_crossingClauses (p : Orthogonal.Point) : List.map Prod.fst (crossingClauses p) = Logic.PL.CNF.relabel (fun (v : Logic.PL.CNF.PairedCrossover.Variable) => (p, Sum.inr v)) Logic.PL.CNF.PairedCrossover.formula

The crossover clause table is exactly the renamed paired-port formula.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.eval_rawFormula_iff (φ : Logic.PL.CNF ℕ) (σ : Variable → Bool) : Logic.PL.CNF.eval σ (rawFormula φ) = true ↔ Logic.PL.CNF.eval σ (List.map Prod.fst (originalClauses φ (crossingSites φ))) = true ∧ (∀ p ∈ ordinaryCells φ, Logic.PL.CNF.eval (fun (v : Fin 4 × Fin 2) => σ (p, Sum.inl v)) OrdinaryRing.formula = true) ∧ (∀ p ∈ crossingSites φ, Logic.PL.CNF.eval (fun (v : Logic.PL.CNF.PairedCrossover.Variable) => σ (p, Sum.inr v)) Logic.PL.CNF.PairedCrossover.formula = true) ∧ ∀ o ∈ Logic.PL.occurrences φ, Logic.PL.CNF.eval σ (List.map Prod.fst (links (crossingSites φ) (occurrencePath φ o))) = true

The emitted formula evaluates precisely its original, ordinary, crossing, and link blocks.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.ordinary_port_value {φ : Logic.PL.CNF ℕ} {σ : Variable → Bool} (h : Logic.PL.CNF.eval σ (rawFormula φ) = true) {p : Orthogonal.Point} (hp : p ∈ ordinaryCells φ) (s : Fin 4) (lane : Fin 2) : σ (port (crossingSites φ) p s lane) = σ (p, Sum.inl (0, 0))

Ordinary cell ports all carry the same value.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.crossing_port_value {φ : Logic.PL.CNF ℕ} {σ : Variable → Bool} (h : Logic.PL.CNF.eval σ (rawFormula φ) = true) {p : Orthogonal.Point} (hp : p ∈ crossingSites φ) (s : Fin 4) (lane : Fin 2) : σ (port (crossingSites φ) p s lane) = if ↑s < 2 then σ (p, Sum.inr (Logic.PL.CNF.PairedCrossover.terminal 0 0)) else σ (p, Sum.inr (Logic.PL.CNF.PairedCrossover.terminal 2 0))

A crossing port carries the horizontal or vertical incoming value, independently of lane.

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

The paired wire has one cell for each retained path point.

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

The actual entry and exit variables at a retained path index.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.wire_cells_agree {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {σ : Variable → Bool} (h : Logic.PL.CNF.eval σ (rawFormula φ) = true) (o : Logic.PL.Occurrence ℕ) : o ∈ Logic.PL.occurrences φ → ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), c.Agree σ

All four actual entry and exit values within each retained wire cell agree.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.map_fst_links (sites : List Orthogonal.Point) (r : Orthogonal.Route) : List.map Prod.fst (links sites r) = Logic.PL.CNF.PairedWire.links (wire sites r)

Forgetting geometric annotations gives the generic paired-wire links exactly.

def Cslib.Complexity.SAT.ParsimoniousPlanar.sourceValue (φ : Logic.PL.CNF ℕ) (σ : Variable → Bool) (v : ℕ) : Bool

The source value is read at one fixed port of its ordinary source cell.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.wire_ne_nil {φ : Logic.PL.CNF ℕ} {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : wire (crossingSites φ) (occurrencePath φ o) ≠ []

Actual occurrence wires are nonempty.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.wire_first_value {φ : Logic.PL.CNF ℕ} {σ : Variable → Bool} (h : Logic.PL.CNF.eval σ (rawFormula φ) = true) {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) (fallback : Logic.PL.CNF.PairedWire.Cell Variable) : σ ((wire (crossingSites φ) (occurrencePath φ o)).headD fallback 0).1 = sourceValue φ σ o.2.2.1

The actual first entry has the source cell's value.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.wire_values_source {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {σ : Variable → Bool} (h : Logic.PL.CNF.eval σ (rawFormula φ) = true) {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) (c : Logic.PL.CNF.PairedWire.Cell Variable) : c ∈ wire (crossingSites φ) (occurrencePath φ o) → ∀ (lane : Fin 2), σ (c lane).1 = sourceValue φ σ o.2.2.1 ∧ σ (c lane).2 = sourceValue φ σ o.2.2.1

Every actual entry and exit along an occurrence wire has exactly its source value.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.lastLiteral_value_of_wire (sites : List Orthogonal.Point) (r : Orthogonal.Route) (positive value : Bool) (σ : Variable → Bool) (hlen : 2 ≤ List.length r) (hcompat : ∀ c ∈ wire sites r, ∀ (lane : Fin 2), σ (c lane).1 = value ∧ σ (c lane).2 = value) : σ (lastLiteral sites r positive).1.1 = value

Constant values along a nonempty retained wire determine its final literal.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.lastLiteral_value {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {σ : Variable → Bool} (h : Logic.PL.CNF.eval σ (rawFormula φ) = true) {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) : σ (lastLiteral (crossingSites φ) (occurrencePath φ o) o.2.2.2).1.1 = sourceValue φ σ o.2.2.1

The literal emitted at an occurrence has precisely its source variable's value.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.eval_originalClauses_of_values (φ : Logic.PL.CNF ℕ) (sites : List Orthogonal.Point) (σ : Variable → Bool) (τ : ℕ → Bool) (hvalues : ∀ o ∈ Logic.PL.occurrences φ, σ (lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1 = τ o.2.2.1) : Logic.PL.CNF.eval σ (List.map Prod.fst (originalClauses φ sites)) = Logic.PL.CNF.eval τ φ

Replacing occurrence variables by equal-valued endpoint variables preserves evaluation.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.eval_source_of_rawFormula {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {σ : Variable → Bool} (h : Logic.PL.CNF.eval σ (rawFormula φ) = true) : Logic.PL.CNF.eval (sourceValue φ σ) φ = true

Every satisfying output assignment projects to a satisfying source assignment.

def Cslib.Complexity.SAT.ParsimoniousPlanar.liftAssignment (σ : PlanarCompile.Variable → Bool) : Variable → Bool

Lift compatible values on the original path cells to the new local templates.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.liftAssignment_signal (sites : List Orthogonal.Point) (σ : PlanarCompile.Variable → Bool) (hcross : ∀ p ∈ sites, Logic.PL.CNF.eval (fun (v : Logic.PL.CNF.Crossover.SplitVariable) => σ (p, some v)) Logic.PL.CNF.Crossover.splitFormula = true) (p q : Orthogonal.Point) (lane : Fin 2) : liftAssignment σ (signal sites p q lane) = σ (PlanarCompile.signal sites p q)

The lifted paired signal is the original signal on either lane.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.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), ∀ (lane : Fin 2), σ (c lane).1 = τ o.2.2.1 ∧ σ (c lane).2 = τ o.2.2.1) ∧ (∀ p ∈ ordinaryCells φ, Logic.PL.CNF.eval (fun (v : Fin 4 × Fin 2) => σ (p, Sum.inl v)) OrdinaryRing.formula = true) ∧ ∀ p ∈ crossingSites φ, Logic.PL.CNF.eval (fun (v : Logic.PL.CNF.PairedCrossover.Variable) => σ (p, Sum.inr v)) Logic.PL.CNF.PairedCrossover.formula = true

Every source assignment has compatible values in every local template and on both lanes.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.eval_rawFormula_of_compatible {φ : Logic.PL.CNF ℕ} (τ : ℕ → Bool) (σ : Variable → Bool) (hcompat : ∀ o ∈ Logic.PL.occurrences φ, ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), ∀ (lane : Fin 2), σ (c lane).1 = τ o.2.2.1 ∧ σ (c lane).2 = τ o.2.2.1) (hord : ∀ p ∈ ordinaryCells φ, Logic.PL.CNF.eval (fun (v : Fin 4 × Fin 2) => σ (p, Sum.inl v)) OrdinaryRing.formula = true) (hcross : ∀ p ∈ crossingSites φ, Logic.PL.CNF.eval (fun (v : Logic.PL.CNF.PairedCrossover.Variable) => σ (p, Sum.inr v)) Logic.PL.CNF.PairedCrossover.formula = true) (h : Logic.PL.CNF.eval τ φ = true) : Logic.PL.CNF.eval σ (rawFormula φ) = true

Compatible local assignments satisfy the actual output if the source holds.