feat(planar-SAT): prove paired compiler model-count preservation

Complexity.lean

@@ -812,9 +812,13 @@ public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverL
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.Occurrence
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.OrdinaryRing
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCompile
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCorrectness
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCounting
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayout
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutChecks
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutData
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedSemantics
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathBounds
 public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathData

Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCompile.lean

@@ -0,0 +1,158 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathData
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.OrdinaryRing
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayout
+public import Complexity.Foundations.Geometry.Orthogonal.PairedSpokes
+public import Complexity.Logics.Propositional.CNF.Compact
+
+/-!
+# A finite compiler with paired wire ports
+
+Canonical incidence paths and their crossing sites are reused. Each ordinary retained cell
+contains a fixed implication ring whose eight ports carry the same value. A crossing cell
+contains a crossover with two equal ports on each side. Each gap receives opposite implications
+on its two separate ports. Consequently the adjacent signal values must agree.
+
+Original clause cells contain no auxiliary variables. Their final incidences use one of the two
+ports facing the clause, with four disjoint offset spokes inside the clause cell. Unused ports
+belong to their cell's implication ring and introduce no independent choices.
+
+## Main definitions
+
+* `Cslib.Complexity.SAT.ParsimoniousPlanar.placedClauses`: actual clauses and geometric data.
+* `Cslib.Complexity.SAT.ParsimoniousPlanar.formula`: compact natural-number output labels.
+* `Cslib.Complexity.SAT.ParsimoniousPlanar.positions`, `.routes`: finite drawing data.
+
+## References
+
+The paired assembly is original. The crossover's source credit is documented in `PairedCrossover`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Complexity.SAT.ParsimoniousPlanar
+
+open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal
+
+/-- An ordinary ring port or a local crossover variable, together with its unit-cell index. -/
+abbrev Variable := Point × ((Fin 4 × Fin 2) ⊕ PairedCrossover.Variable)
+
+/-- A clause, its position, and one incidence route per literal, in literal order. -/
+abbrev PlacedClause := Clause Variable × Point × List Route
+
+/-- Reuse the already-certified canonical unit paths. -/
+abbrev paths := PlanarCompile.paths
+
+/-- Reuse the selected crossing cells. -/
+abbrev crossingSites := PlanarCompile.crossingSites
+
+/-- Reuse the occurrence-indexed canonical unit path. -/
+abbrev occurrencePath := PlanarCompile.occurrencePath
+
+/-- Side facing a unit neighbor, in left/right/bottom/top order. -/
+abbrev side := PlanarCompile.side
+
+/-- The center of a macrocell of side 240. -/
+abbrev center := PlanarCompile.center
+
+/-- All occupied retained ordinary cells, listed without repetitions. -/
+def ordinaryCells (φ : CNF ℕ) : List Point :=
+  let occupied := ((paths φ).flatMap List.dropLast).filter fun p => decide (p ∉ crossingSites φ)
+  selectDistinct occupied (List.replicate occupied.length true)
+
+/-- The signal variable on a particular side and lane of a cell. -/
+def port (sites : List Point) (p : Point) (s : Fin 4) (lane : Fin 2) : Variable :=
+  (p, if p ∈ sites then .inr (PairedCrossover.terminal s lane) else .inl (s, lane))
+
+/-- Signal presented toward the neighboring cell on one lane. -/
+def signal (sites : List Point) (p q : Point) (lane : Fin 2) : Variable :=
+  port sites p (side p q) lane
+
+/-- The actual displayed position of a structured variable. -/
+def variablePosition (v : Variable) : Point :=
+  cellOrigin 120 v.1 + v.2.elim
+    (fun p => PairedPorts.variablePosition p.1 p.2) PairedCrossover.variablePosition
+
+/-- The shared side point for a specified lane. -/
+def boundary (p : Point) (s : Fin 4) (lane : Fin 2) : Point :=
+  cellOrigin 120 p + PairedPorts.boundaryPort s lane
+
+/-- A straight route from a cell boundary to its presented signal. -/
+def access (sites : List Point) (p q : Point) (lane : Fin 2) : Route :=
+  [boundary p (side p q) lane, variablePosition (signal sites p q lane)]
+
+/-- The clause on lane zero goes forward; the clause on lane one goes backward. -/
+def link (sites : List Point) (p q : Point) (lane : Fin 2) : PlacedClause :=
+  let a := signal sites p q lane
+  let b := signal sites q p lane
+  let ra := access sites p q lane
+  let rb := access sites q p lane
+  (if lane = 0 then [(a, false), (b, true)] else [(b, false), (a, true)],
+    boundary p (side p q) lane, if lane = 0 then [ra, rb] else [rb, ra])
+
+/-- Two implication clauses per gap, excluding the final step into the original clause. -/
+def links (sites : List Point) (r : Route) : List PlacedClause :=
+  r.dropLast.consecutivePairs.flatMap fun e => [link sites e.1 e.2 0, link sites e.1 e.2 1]
+
+/-- Final literal and its incidence route from the original clause center. -/
+def lastLiteral (sites : List Point) (r : Route) (positive : Bool) : Literal Variable × Route :=
+  let p := r.getD (r.length - 2) (0, 0)
+  let q := r.getLastD (0, 0)
+  let s := side q p
+  let lane := PairedPorts.spokeLane s
+  ((signal sites p q lane, positive),
+    [center q, cellOrigin 120 q + PairedPorts.spokeElbow s, boundary q s lane,
+      variablePosition (signal sites p q lane)])
+
+/-- Original clauses keep their order, arity and literal signs. -/
+def originalClauses (φ : CNF ℕ) (sites : List Point) : List PlacedClause :=
+  φ.zipIdx.map fun (c, i) =>
+    let ls := c.zipIdx.map fun (l, j) =>
+      lastLiteral sites (occurrencePath φ (i, j, l)) l.2
+    (ls.map Prod.fst, center (Layout.center (φ.distinctVars.length + i)), ls.map Prod.snd)
+
+/-- The ordinary fixed implication ring in an occupied cell. -/
+def ordinaryClauses (p : Point) : List PlacedClause :=
+  OrdinaryRing.formula.zipIdx.map fun (c, i) =>
+    (c.relabel (fun v => (p, .inl v)),
+      cellOrigin 120 p + OrdinaryRing.clausePositions.getD i (0, 0),
+      (OrdinaryRing.incidenceRoutes.filter fun e => e.1 == i).map fun e =>
+        translate (cellOrigin 120 p) e.2.2)
+
+/-- The paired-port crossover in a selected crossing cell. -/
+def crossingClauses (p : Point) : List PlacedClause :=
+  PairedCrossover.formula.zipIdx.map fun (c, i) =>
+    (c.relabel (fun v => (p, .inr v)),
+      cellOrigin 120 p + PairedCrossover.clausePositions.getD i (0, 0),
+      (PairedCrossover.incidenceRoutes.filter fun e => e.1 == i).map fun e =>
+        translate (cellOrigin 120 p) e.2.2)
+
+/-- The actual finite output, with no clauses for unoccupied ordinary cells. -/
+def placedClauses (φ : CNF ℕ) : List PlacedClause :=
+  let sites := crossingSites φ
+  originalClauses φ sites ++ (ordinaryCells φ).flatMap ordinaryClauses ++
+    sites.flatMap crossingClauses ++
+      (Cslib.Logic.PL.occurrences φ).flatMap fun o => links sites (occurrencePath φ o)
+
+/-- Output formula with structured variable names. -/
+def rawFormula (φ : CNF ℕ) : CNF Variable := (placedClauses φ).map Prod.fst
+
+/-- Compact natural-number labels for the actual formula. -/
+def formula (φ : CNF ℕ) : CNF ℕ := (rawFormula φ).compact
+
+/-- Positions ordered by the final formula's distinct variables, then its clauses. -/
+def positions (φ : CNF ℕ) : List Point :=
+  (rawFormula φ).distinctVars.map variablePosition ++ (placedClauses φ).map fun c => c.2.1
+
+/-- Incidence routes ordered by clauses and by literal positions. -/
+def routes (φ : CNF ℕ) : List Route := (placedClauses φ).flatMap fun c => c.2.2
+
+end Cslib.Complexity.SAT.ParsimoniousPlanar

Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCorrectness.lean

@@ -0,0 +1,179 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedSemantics
+public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths
+import Complexity.Computability.Complexity.Problems.SAT.Planar.PathAssignments
+import Complexity.Foundations.Data.List.Filter
+import Mathlib.Data.List.GetD
+
+/-!
+# 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.
+-/
+
+@[expose] public section
+
+namespace Cslib.Complexity.SAT.ParsimoniousPlanar
+
+open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal
+
+/-- Every actual selected crossing is used by both a horizontal and a vertical occurrence. -/
+theorem crossing_axes_exist {φ : CNF ℕ}
+    (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3)
+    {p : Point} (hp : p ∈ crossingSites φ) :
+    ∃ o ∈ Cslib.Logic.PL.occurrences φ, ∃ t ∈ Cslib.Logic.PL.occurrences φ,
+      p ∈ occurrencePath φ o ∧ p ∈ occurrencePath φ t ∧
+        StraightThrough (occurrencePath φ o) p (1, 0) ∧
+          StraightThrough (occurrencePath φ t) p (0, 1) := by
+  have hc := ((PlanarCompile.mem_crossingSites φ p).1 hp).2.2
+  rw [← PlanarCompile.occurrencePaths_eq_paths] at hc
+  obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := List.exists_pair_indices_of_two_le_filter_contains _ p hc
+  have hi' : i < (Cslib.Logic.PL.occurrences φ).length := by
+    simpa only [List.length_map] using hi
+  have hj' : j < (Cslib.Logic.PL.occurrences φ).length := by
+    simpa only [List.length_map] using hj
+  simp only [List.getElem_map] at hpi hpj
+  have hoi := List.getElem_mem hi'
+  have hoj := List.getElem_mem hj'
+  have hot : (Cslib.Logic.PL.occurrences φ)[i] ≠ (Cslib.Logic.PL.occurrences φ)[j] := by
+    intro he
+    exact hij ((Cslib.Logic.PL.occurrences_nodup φ).getElem_inj_iff.1 he)
+  rcases PlanarCompile.occurrencePath_crossing_straight hw hv hoi hp hpi with hs | hs <;>
+    rcases PlanarCompile.occurrencePath_crossing_straight hw hv hoj hp hpj with ht | ht
+  · exact False.elim (hot (PlanarCompile.crossing_axis_occurrence_eq hw hv hoi hoj hp
+      hpi hpj (Or.inl rfl) hs ht))
+  · exact ⟨_, hoi, _, hoj, hpi, hpj, hs, ht⟩
+  · exact ⟨_, hoj, _, hoi, hpj, hpi, ht, hs⟩
+  · exact False.elim (hot (PlanarCompile.crossing_axis_occurrence_eq hw hv hoi hoj hp
+      hpi hpj (Or.inr rfl) hs ht))
+
+/-- Every retained ordinary cell lies on an actual source occurrence path. -/
+theorem ordinary_occurrence_exists {φ : CNF ℕ} {p : Point} (hp : p ∈ ordinaryCells φ) :
+    ∃ o ∈ Cslib.Logic.PL.occurrences φ, p ∈ (occurrencePath φ o).dropLast := by
+  obtain ⟨⟨r, hr, hpr⟩, _⟩ := (mem_ordinaryCells φ p).1 hp
+  change r ∈ PlanarCompile.paths φ at hr
+  rw [← PlanarCompile.occurrencePaths_eq_paths] at hr
+  obtain ⟨o, ho, rfl⟩ := List.mem_map.mp hr
+  exact ⟨o, ho, hpr⟩
+
+/-- A satisfying ordinary ring's value is determined by any occurrence retaining its cell. -/
+theorem ordinary_value_source {φ : CNF ℕ}
+    (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3)
+    {σ : Variable → Bool} (h : (rawFormula φ).eval σ = true)
+    {p : Point} (hp : p ∈ ordinaryCells φ) {o : Occurrence ℕ}
+    (ho : o ∈ Cslib.Logic.PL.occurrences φ) (hpo : p ∈ (occurrencePath φ o).dropLast) :
+    σ (p, Sum.inl (0, 0)) = sourceValue φ σ o.2.2.1 := by
+  obtain ⟨k, hk, heq⟩ := List.mem_iff_getElem.mp hpo
+  have hk' : k < (occurrencePath φ o).length - 1 := by
+    simpa only [List.length_dropLast] using hk
+  have hwi : k < (wire (crossingSites φ) (occurrencePath φ o)).length := by
+    rwa [length_wire]
+  have hc := (wire_values_source hw hv h ho _ (List.getElem_mem hwi) 0).1
+  rw [getElem_wire _ _ _ hk'] at hc
+  rw [← List.getElem_dropLast hk, heq] at hc
+  simpa only [signal, ordinary_port_value h hp] using hc
+
+/-- Each crossover input is exactly the source value on its occupying axis. -/
+theorem crossing_axis_value {φ : CNF ℕ}
+    (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3)
+    {σ : Variable → Bool} (h : (rawFormula φ).eval σ = true)
+    {p : Point} (hp : p ∈ crossingSites φ) {o : Occurrence ℕ}
+    (ho : o ∈ Cslib.Logic.PL.occurrences φ) (hpo : p ∈ occurrencePath φ o)
+    (axis : Bool)
+    (hs : StraightThrough (occurrencePath φ o) p (if axis then (0, 1) else (1, 0))) :
+    σ (p, Sum.inr (PairedCrossover.terminal (if axis then 2 else 0) 0)) =
+      sourceValue φ σ o.2.2.1 := by
+  obtain ⟨k, hk, heq⟩ := List.mem_iff_getElem.mp hpo
+  obtain ⟨_, hnext, hnb⟩ := hs.getD_neighbors (PlanarCompile.occurrencePath_nodup ho) hk heq
+  have hk' : k < (occurrencePath φ o).length - 1 := by omega
+  have hwi : k < (wire (crossingSites φ) (occurrencePath φ o)).length := by
+    rwa [length_wire]
+  have hc := (wire_values_source hw hv h ho _ (List.getElem_mem hwi) 0).1
+  rw [getElem_wire _ _ _ hk', heq] at hc
+  cases axis with
+  | false =>
+    have hl : side p (p - (1, 0)) = 0 := by
+      simpa [PairedPorts.neighbor, sub_eq_add_neg] using side_neighbor p 0
+    have hr : side p (p + (1, 0)) = 1 := by
+      simpa [PairedPorts.neighbor] using side_neighbor p 1
+    rcases hnb with ⟨hprev, _⟩ | ⟨hprev, _⟩
+    all_goals
+      simp only [Bool.false_eq_true, ↓reduceIte] at hprev ⊢
+      simp only [signal, hprev, hl, hr] at hc
+      rw [crossing_port_value h hp] at hc
+      simpa using hc
+  | true =>
+    have hb : side p (p - (0, 1)) = 2 := by
+      simpa [PairedPorts.neighbor, sub_eq_add_neg] using side_neighbor p 2
+    have ht : side p (p + (0, 1)) = 3 := by
+      simpa [PairedPorts.neighbor] using side_neighbor p 3
+    rcases hnb with ⟨hprev, _⟩ | ⟨hprev, _⟩
+    all_goals
+      simp only [↓reduceIte] at hprev ⊢
+      simp only [signal, hprev, hb, ht] at hc
+      rw [crossing_port_value h hp] at hc
+      simpa using hc
+
+/-- Source agreement forces agreement on every variable of every emitted ordinary ring. -/
+theorem ordinary_assignments_agree {φ : CNF ℕ}
+    (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3)
+    {σ τ : Variable → Bool} (hσ : (rawFormula φ).eval σ = true)
+    (hτ : (rawFormula φ).eval τ = true)
+    (he : ∀ v ∈ φ.vars, sourceValue φ σ v = sourceValue φ τ v)
+    {p : Point} (hp : p ∈ ordinaryCells φ) (v : OrdinaryRing.Variable) :
+    σ (p, Sum.inl v) = τ (p, Sum.inl v) := by
+  obtain ⟨o, ho, hpo⟩ := ordinary_occurrence_exists hp
+  have hs := (OrdinaryRing.eval_formula_iff _).1
+    (((eval_rawFormula_iff φ σ).1 hσ).2.1 p hp) v
+  have ht := (OrdinaryRing.eval_formula_iff _).1
+    (((eval_rawFormula_iff φ τ).1 hτ).2.1 p hp) v
+  exact hs.trans ((ordinary_value_source hw hv hσ hp ho hpo).trans
+    ((he _ (variable_mem_of_mem_occurrences ho)).trans
+      ((ordinary_value_source hw hv hτ hp ho hpo).symm.trans ht.symm)))
+
+/-- Source agreement forces agreement on every variable of every emitted crossover. -/
+theorem crossing_assignments_agree {φ : CNF ℕ}
+    (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3)
+    {σ τ : Variable → Bool} (hσ : (rawFormula φ).eval σ = true)
+    (hτ : (rawFormula φ).eval τ = true)
+    (he : ∀ v ∈ φ.vars, sourceValue φ σ v = sourceValue φ τ v)
+    {p : Point} (hp : p ∈ crossingSites φ) (v : PairedCrossover.Variable) :
+    σ (p, Sum.inr v) = τ (p, Sum.inr v) := by
+  obtain ⟨o, ho, t, ht, hpo, hpt, hhor, hver⟩ := crossing_axes_exist hw hv hp
+  have ha : σ (p, Sum.inr (PairedCrossover.terminal 0 0)) =
+      τ (p, Sum.inr (PairedCrossover.terminal 0 0)) :=
+    (crossing_axis_value hw hv hσ hp ho hpo false hhor).trans
+      ((he _ (variable_mem_of_mem_occurrences ho)).trans
+        (crossing_axis_value hw hv hτ hp ho hpo false hhor).symm)
+  have hb : σ (p, Sum.inr (PairedCrossover.terminal 2 0)) =
+      τ (p, Sum.inr (PairedCrossover.terminal 2 0)) :=
+    (crossing_axis_value hw hv hσ hp ht hpt true hver).trans
+      ((he _ (variable_mem_of_mem_occurrences ht)).trans
+        (crossing_axis_value hw hv hτ hp ht hpt true hver).symm)
+  have hs := congrFun (PairedCrossover.eq_canonicalExtension_of_holds
+    (((eval_rawFormula_iff φ σ).1 hσ).2.2.1 p hp)) v
+  have ht := congrFun (PairedCrossover.eq_canonicalExtension_of_holds
+    (((eval_rawFormula_iff φ τ).1 hτ).2.2.1 p hp)) v
+  exact hs.trans (by rw [ha, hb]; exact ht.symm)
+
+
+end Cslib.Complexity.SAT.ParsimoniousPlanar