Unique assignments in the actual paired compiler

Every occupied ordinary cell belongs to a retained occurrence path. Each selected crossing is occupied by a horizontal and a vertical occurrence path. The constant-wire theorem therefore determines both crossover inputs and every ordinary ring from the original assignment.

Main results

• Cslib.Complexity.SAT.ParsimoniousPlanar.crossing_axes_exist: actual selected crossings carry both independent signals.

References

These are original composition proofs using the canonical path occupancy certificates.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.crossing_axes_exist {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, List.length c ≤ 3) (hv : ∀ (v : ℕ), List.count v φ.vars ≤ 3) {p : Orthogonal.Point} (hp : p ∈ crossingSites φ) : ∃ o ∈ Logic.PL.occurrences φ, ∃ t ∈ Logic.PL.occurrences φ, p ∈ occurrencePath φ o ∧ p ∈ occurrencePath φ t ∧ Orthogonal.StraightThrough (occurrencePath φ o) p (1, 0) ∧ Orthogonal.StraightThrough (occurrencePath φ t) p (0, 1)

Every actual selected crossing is used by both a horizontal and a vertical occurrence.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.ordinary_occurrence_exists {φ : Logic.PL.CNF ℕ} {p : Orthogonal.Point} (hp : p ∈ ordinaryCells φ) : ∃ o ∈ Logic.PL.occurrences φ, p ∈ List.dropLast (occurrencePath φ o)

Every retained ordinary cell lies on an actual source occurrence path.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.ordinary_value_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) {p : Orthogonal.Point} (hp : p ∈ ordinaryCells φ) {o : Logic.PL.Occurrence ℕ} (hpo : p ∈ List.dropLast (occurrencePath φ o)) : σ (p, Sum.inl (0, 0)) = sourceValue φ σ o.2.2.1

A satisfying ordinary ring's value is determined by any occurrence retaining its cell.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.crossing_axis_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) {p : Orthogonal.Point} (hp : p ∈ crossingSites φ) {o : Logic.PL.Occurrence ℕ} (ho : o ∈ Logic.PL.occurrences φ) (hpo : p ∈ occurrencePath φ o) (axis : Bool) (hs : Orthogonal.StraightThrough (occurrencePath φ o) p (if axis = true then (0, 1) else (1, 0))) : σ (p, Sum.inr (Logic.PL.CNF.PairedCrossover.terminal (if axis = true then 2 else 0) 0)) = sourceValue φ σ o.2.2.1

Each crossover input is exactly the source value on its occupying axis.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.ordinary_assignments_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) (hτ : Logic.PL.CNF.eval τ (rawFormula φ) = true) (he : ∀ v ∈ φ.vars, sourceValue φ σ v = sourceValue φ τ v) {p : Orthogonal.Point} (hp : p ∈ ordinaryCells φ) (v : OrdinaryRing.Variable) : σ (p, Sum.inl v) = τ (p, Sum.inl v)

Source agreement forces agreement on every variable of every emitted ordinary ring.

theorem Cslib.Complexity.SAT.ParsimoniousPlanar.crossing_assignments_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) (hτ : Logic.PL.CNF.eval τ (rawFormula φ) = true) (he : ∀ v ∈ φ.vars, sourceValue φ σ v = sourceValue φ τ v) {p : Orthogonal.Point} (hp : p ∈ crossingSites φ) (v : Logic.PL.CNF.PairedCrossover.Variable) : σ (p, Sum.inr v) = τ (p, Sum.inr v)

Source agreement forces agreement on every variable of every emitted crossover.