From 2e46423bd7a284eae78c5dcff1cf72b0828699ca Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Mon, 26 Oct 2026 07:52:02 -0400 Subject: [PATCH] feat(planar-SAT): use the parsimonious compiler for planar 3SAT-3 Part of #1144, split from the internally reviewed parsimonious planar SAT development. All six local validation gates and hygiene checks pass. No selected abstract changes. AI-assisted implementation and internal review with Codex gpt-6.1-sol; outside-fleet coordinator review remains required. --- Complexity.lean | 9 - .../Problems/PlanarThreeSATThree.lean | 86 +- .../Problems/SAT/Planar/Bounds.lean | 355 ---- .../Problems/SAT/Planar/Compile.lean | 116 -- .../Problems/SAT/Planar/Completeness.lean | 60 - .../Problems/SAT/Planar/Correctness.lean | 109 -- .../Problems/SAT/Planar/Geometry.lean | 1740 ----------------- .../Problems/SAT/Planar/Occurrence.lean | 531 ----- .../Problems/SAT/Planar/PolyTime.lean | 502 ----- .../Problems/SAT/Planar/Semantics.lean | 235 --- .../Complexity/Problems/SAT/Planar/Size.lean | 193 -- ComplexityTests/PlanarThreeSATThree.lean | 7 +- guide/ComplexityGuide/NPCompleteness.lean | 6 +- 13 files changed, 73 insertions(+), 3876 deletions(-) delete mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/Bounds.lean delete mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/Compile.lean delete mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/Completeness.lean delete mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/Correctness.lean delete mode 100755 Complexity/Computability/Complexity/Problems/SAT/Planar/Geometry.lean delete mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/Occurrence.lean delete mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/PolyTime.lean delete mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/Semantics.lean delete mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/Size.lean diff --git a/Complexity.lean b/Complexity.lean index 78506ce6d..2cf1ee1f9 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -812,15 +812,9 @@ public import Complexity.Computability.Complexity.Problems.SAT public import Complexity.Computability.Complexity.Problems.SAT.Incidence public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Compact public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Degree -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Bounds -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Completeness -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Correctness public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverLayout public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverLayoutChecks public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverLayoutData -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.PairedBounds public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCompile @@ -841,9 +835,6 @@ public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathGeomet public import Complexity.Computability.Complexity.Problems.SAT.Planar.PathPolyTime public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths.Occupancy -public import Complexity.Computability.Complexity.Problems.SAT.Planar.PolyTime -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Semantics -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Size public import Complexity.Computability.Complexity.Problems.SAT.PolyTime public import Complexity.Computability.Complexity.Problems.SATUNSAT public import Complexity.Computability.Complexity.Problems.STCON diff --git a/Complexity/Computability/Complexity/Problems/PlanarThreeSATThree.lean b/Complexity/Computability/Complexity/Problems/PlanarThreeSATThree.lean index 348bdac80..a9c4c4862 100644 --- a/Complexity/Computability/Complexity/Problems/PlanarThreeSATThree.lean +++ b/Complexity/Computability/Complexity/Problems/PlanarThreeSATThree.lean @@ -11,12 +11,13 @@ public import Complexity.Computability.Complexity.Problems.ThreeSATThree public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Size public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalDrawing.Encoding -public import Complexity.Computability.Complexity.Problems.SAT.Planar.PolyTime -import Complexity.Computability.Complexity.Problems.SAT.Planar.Completeness -import Complexity.Computability.Complexity.Problems.SAT.Planar.Occurrence -import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry -import Complexity.Computability.Complexity.Problems.SAT.Planar.Size -import Complexity.Computability.Complexity.Problems.SAT.Planar.Bounds +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedPolyTime +public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Counting +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCounting +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedOccurrence +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedGeometry +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedSize +import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedBounds import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat @@ -37,6 +38,9 @@ with all contacts interpreted on full real segments. Parallel literal incidences requires its existence. The total compiler rejects inputs outside the syntactic restrictions by returning one empty clause and a one-vertex drawing. +The compiler is parsimonious: its paired implications force equality along each wire, and the +local rings and crossover have unique extensions. Counts refer only to occurring variables. + ## Main definitions * `PlanarThreeSATThree`, `DrawnPlanarThreeSATThree`: formula and supplied-drawing problems. @@ -49,13 +53,19 @@ by returning one empty clause and a one-vertex drawing. * `computableInPolyTime_toDrawnPlanarThreeSATThree`, `computableInPolyTime_toPlanarThreeSATThree`: native polynomial-time computation. * `satisfiable_toPlanarThreeSAT_iff`: total correctness after occurrence splitting. +* `modelCount_toPlanarThreeSATThree`, `modelCount_toPlanarThreeSAT`: exact count preservation + on valid source syntax. * `toDrawnPlanarThreeSAT_fits`, `toDrawnPlanarThreeSAT_costs`: explicit linear grid sides and quadratic formula, incidence-route, segment and Manhattan wire costs, measured against the original formula's clause and literal counts. ## References -The finite tiling construction is original; the fixed crossover is credited in `Crossover`. +* Parsimonious planarization: Theorem 3.2 and Claim 3.3 of + [Hunt, Marathe, Radhakrishnan and Stearns][HuntMaratheRadhakrishnanStearns1998]. + +The paired-port tiling, degree-three templates and explicit grid bounds are original. +The fixed crossover's source credit is documented in `Crossover`. -/ @[expose] public section @@ -77,7 +87,8 @@ def DrawnPlanarThreeSATThree : Set (CNF ℕ × Graph.OrthogonalDrawing) := unsatisfiable empty clause with its isolated clause vertex. -/ def toDrawnPlanarThreeSATThree (φ : CNF ℕ) : CNF ℕ × Graph.OrthogonalDrawing := if ThreeSATThree.syntaxCheck φ then - (SAT.PlanarCompile.formula φ, SAT.PlanarCompile.positions φ, SAT.PlanarCompile.routes φ) + (SAT.ParsimoniousPlanar.formula φ, + SAT.ParsimoniousPlanar.positions φ, SAT.ParsimoniousPlanar.routes φ) else ([[]], [(0, 0)], []) /-- Forget the drawing emitted by the total compiler. -/ @@ -113,7 +124,7 @@ theorem width_toPlanarThreeSATThree (φ : CNF ℕ) : ∀ c ∈ toPlanarThreeSATThree φ, c.length ≤ 3 := by by_cases hg : ThreeSATThree.syntaxCheck φ = true · simpa only [toPlanarThreeSATThree, toDrawnPlanarThreeSATThree, hg, ↓reduceIte] using - SAT.PlanarCompile.width_formula ((ThreeSATThree.syntaxCheck_iff φ).1 hg).1 + SAT.ParsimoniousPlanar.width_formula ((ThreeSATThree.syntaxCheck_iff φ).1 hg).1 · simp [toPlanarThreeSATThree, toDrawnPlanarThreeSATThree, hg] /-- The actual total output has at most three literal positions for every variable. -/ @@ -122,9 +133,31 @@ theorem count_vars_toPlanarThreeSATThree (φ : CNF ℕ) : by_cases hg : ThreeSATThree.syntaxCheck φ = true · have hs := (ThreeSATThree.syntaxCheck_iff φ).1 hg simpa only [toPlanarThreeSATThree, toDrawnPlanarThreeSATThree, hg, ↓reduceIte] using - SAT.PlanarCompile.count_vars_formula_le_three hs.1 hs.2 + SAT.ParsimoniousPlanar.count_vars_formula_le_three hs.1 hs.2 · simp [toPlanarThreeSATThree, toDrawnPlanarThreeSATThree, hg, CNF.vars] +/-- Valid width-three, occurrence-three inputs preserve their exact number of models. -/ +theorem modelCount_toPlanarThreeSATThree (φ : CNF ℕ) + (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : + (toPlanarThreeSATThree φ).modelCount = φ.modelCount := by + have hg := (ThreeSATThree.syntaxCheck_iff φ).2 ⟨hw, hv⟩ + simpa only [toPlanarThreeSATThree, toDrawnPlanarThreeSATThree, hg, ↓reduceIte] using + SAT.ParsimoniousPlanar.modelCount_formula φ hw hv + +/-- The total planar compiler preserves syntax-guarded counts, including rejected inputs. -/ +theorem sharpThreeSATThree_toPlanarThreeSATThree (φ : CNF ℕ) : + SharpThreeSATThree (toPlanarThreeSATThree φ) = SharpThreeSATThree φ := by + have hout := (ThreeSATThree.syntaxCheck_iff (toPlanarThreeSATThree φ)).2 + ⟨width_toPlanarThreeSATThree φ, count_vars_toPlanarThreeSATThree φ⟩ + simp only [SharpThreeSATThree, hout, ↓reduceIte] + by_cases hg : ThreeSATThree.syntaxCheck φ = true + · have hs := (ThreeSATThree.syntaxCheck_iff φ).1 hg + rw [modelCount_toPlanarThreeSATThree φ hs.1 hs.2] + simp only [hg, ↓reduceIte] + · simp only [toPlanarThreeSATThree, toDrawnPlanarThreeSATThree, hg, + Bool.false_eq_true, ite_false] + decide + /-- The total output is satisfiable exactly on the source 3SAT-3 language. -/ theorem satisfiable_toPlanarThreeSATThree_iff (φ : CNF ℕ) : (toPlanarThreeSATThree φ).Satisfiable ↔ φ ∈ ThreeSATThree := by @@ -132,7 +165,7 @@ theorem satisfiable_toPlanarThreeSATThree_iff (φ : CNF ℕ) : · have hs := (ThreeSATThree.syntaxCheck_iff φ).1 hg have he : (toPlanarThreeSATThree φ).Satisfiable ↔ φ.Satisfiable := by simpa only [toPlanarThreeSATThree, toDrawnPlanarThreeSATThree, hg, ↓reduceIte] using - SAT.PlanarCompile.satisfiable_formula_iff hs.1 hs.2 + SAT.ParsimoniousPlanar.satisfiable_formula_iff φ hs.1 hs.2 exact he.trans ⟨fun h => ⟨hs.1, hs.2, h⟩, fun h => h.2.2⟩ · have hn : φ ∉ ThreeSATThree := by intro h @@ -147,7 +180,7 @@ theorem isPlanarOrthogonalDrawing_toDrawnPlanarThreeSATThree (φ : CNF ℕ) : by_cases hg : ThreeSATThree.syntaxCheck φ = true · have hs := (ThreeSATThree.syntaxCheck_iff φ).1 hg simpa only [toPlanarThreeSATThree, toDrawnPlanarThreeSATThree, hg, ↓reduceIte] using - SAT.PlanarCompile.isPlanarOrthogonalDrawing hs.1 hs.2 + SAT.ParsimoniousPlanar.isPlanarOrthogonalDrawing hs.1 hs.2 · simpa [toPlanarThreeSATThree, toDrawnPlanarThreeSATThree, hg] using rejection_drawing @@ -203,8 +236,8 @@ theorem toDrawnPlanarThreeSATThree_fits (φ : CNF ℕ) : (1920 * (φ.numVars + φ.length + φ.vars.length + 1)) := by by_cases hg : ThreeSATThree.syntaxCheck φ = true · simpa only [toDrawnPlanarThreeSATThree, hg, ↓reduceIte] using - Graph.drawingFits_mono (SAT.PlanarCompile.drawing_fits φ) - (SAT.PlanarCompile.gridWidth_le φ) (SAT.PlanarCompile.gridHeight_le φ) + Graph.drawingFits_mono (SAT.ParsimoniousPlanar.drawing_fits φ) + (SAT.ParsimoniousPlanar.gridWidth_le φ) (SAT.ParsimoniousPlanar.gridHeight_le φ) · have hn : (0 : ℤ) ≤ φ.numVars + φ.length + φ.vars.length + 1 := by positivity simpa [toDrawnPlanarThreeSATThree, hg, Graph.drawingFits] using hn @@ -212,15 +245,16 @@ theorem toDrawnPlanarThreeSATThree_fits (φ : CNF ℕ) : theorem toDrawnPlanarThreeSATThree_costs (φ : CNF ℕ) : let out := toDrawnPlanarThreeSATThree φ let s := φ.numVars + φ.length + φ.vars.length + 1 - out.1.length ≤ 600 * s ^ 2 ∧ out.1.vars.length ≤ 1210 * s ^ 2 ∧ - out.2.2.length ≤ 1210 * s ^ 2 ∧ Graph.drawingSegmentCount out.2 ≤ 23000 * s ^ 2 ∧ - Graph.drawingWireLength out.2 ≤ 300000 * s ^ 2 := by + out.1.length ≤ 5000 * s ^ 2 ∧ out.1.vars.length ≤ 10000 * s ^ 2 ∧ + out.2.2.length ≤ 10000 * s ^ 2 ∧ Graph.drawingSegmentCount out.2 ≤ 12000 * s ^ 2 ∧ + Graph.drawingWireLength out.2 ≤ 400000 * s ^ 2 := by dsimp only by_cases hg : ThreeSATThree.syntaxCheck φ = true · simp only [toDrawnPlanarThreeSATThree, hg, ↓reduceIte] - exact ⟨SAT.PlanarCompile.length_formula_le φ, SAT.PlanarCompile.length_vars_formula_le φ, - SAT.PlanarCompile.routes_length_le φ, SAT.PlanarCompile.drawingSegmentCount_le φ, - SAT.PlanarCompile.drawingWireLength_le φ⟩ + exact ⟨SAT.ParsimoniousPlanar.length_formula_le φ, + SAT.ParsimoniousPlanar.length_vars_formula_le φ, + SAT.ParsimoniousPlanar.routes_length_le φ, SAT.ParsimoniousPlanar.drawingSegmentCount_le φ, + SAT.ParsimoniousPlanar.drawingWireLength_le φ⟩ · have hsize : 1 ≤ φ.numVars + φ.length + φ.vars.length + 1 := by omega have hvars : CNF.vars ([[]] : CNF ℕ) = [] := rfl simp only [toDrawnPlanarThreeSATThree, hg] @@ -248,6 +282,12 @@ theorem computableInPolyTime_toPlanarThreeSAT : (ComputableInPolyTime.fst encCNF Graph.encOrthogonalDrawing).comp computableInPolyTime_toDrawnPlanarThreeSAT +/-- Occurrence splitting and planarization preserve all models of width-three inputs. -/ +theorem modelCount_toPlanarThreeSAT (φ : CNF ℕ) (hw : ∀ c ∈ φ, c.length ≤ 3) : + (toPlanarThreeSAT φ).modelCount = φ.modelCount := + (modelCount_toPlanarThreeSATThree (toThreeSATThree φ) (width_toThreeSATThree φ) + (count_vars_toThreeSATThree_le φ)).trans (modelCount_toThreeSATThree φ hw) + /-- The total output is satisfiable exactly when the original input belongs to 3SAT. -/ theorem satisfiable_toPlanarThreeSAT_iff (φ : CNF ℕ) : (toPlanarThreeSAT φ).Satisfiable ↔ φ ∈ ThreeSAT := @@ -285,9 +325,9 @@ theorem toDrawnPlanarThreeSAT_fits (φ : CNF ℕ) : theorem toDrawnPlanarThreeSAT_costs (φ : CNF ℕ) : let out := toDrawnPlanarThreeSAT φ let s := φ.length + φ.vars.length + 1 - out.1.length ≤ 29400 * s ^ 2 ∧ out.1.vars.length ≤ 59290 * s ^ 2 ∧ - out.2.2.length ≤ 59290 * s ^ 2 ∧ Graph.drawingSegmentCount out.2 ≤ 1127000 * s ^ 2 ∧ - Graph.drawingWireLength out.2 ≤ 14700000 * s ^ 2 := by + out.1.length ≤ 245000 * s ^ 2 ∧ out.1.vars.length ≤ 490000 * s ^ 2 ∧ + out.2.2.length ≤ 490000 * s ^ 2 ∧ Graph.drawingSegmentCount out.2 ≤ 588000 * s ^ 2 ∧ + Graph.drawingWireLength out.2 ≤ 19600000 * s ^ 2 := by have hb := size_toThreeSATThree_le φ have hs : ((toThreeSATThree φ).numVars + (toThreeSATThree φ).length + (toThreeSATThree φ).vars.length + 1) ^ 2 ≤ diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Bounds.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Bounds.lean deleted file mode 100644 index 53f6ab0f9..000000000 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Bounds.lean +++ /dev/null @@ -1,355 +0,0 @@ -/- -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.PathBounds -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile -public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalDrawing -import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry -import Complexity.Computability.Complexity.Problems.SAT.Planar.Size -import Complexity.Computability.Complexity.Problems.Graph.OrthogonalPath -import Mathlib.Data.List.GetD -import Mathlib.Tactic.FinCases -import Mathlib.Tactic.Linarith -import Mathlib.Tactic.NormNum -import Mathlib.Tactic.SplitIfs - -/-! -# Explicit grid and wire bounds for the actual planarization compiler - -For an input incidence graph with `n` vertices and `m` literal incidences, the emitted integer -points fit a rectangle of width `240 (8n + 1)` and height `240 (8n + 2m + 1)`. These are linear -in the source's combinatorial incidence size. The bounds hold for the actual emitted lists, -including empty clauses and repeated literal incidences. Writing -`S = φ.numVars + φ.length + φ.vars.length + 1`, there are at most `1210 S²` routes, -`23000 S²` segments and `300000 S²` units of Manhattan wire. The constants follow from the -fixed template costs and uniform per-route bounds. - -## Main definitions - -* `gridWidth`, `gridHeight`: explicit grid sides of the tiled output. - -## Main results - -* `drawing_fits`: bounds on every actual vertex and incidence-route point. -* `gridWidth_le`, `gridHeight_le`: common linear bounds in source incidence size. -* `routes_length_le`, `drawingSegmentCount_le`, `drawingWireLength_le`: explicit quadratic - bounds on the actual output route data. - -## References - -These bounds concern the original finite compiler in `Compile` and its 240-square template. --/ - -@[expose] public section - -namespace Cslib.Complexity.SAT.PlanarCompile -open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal - -private def CellBound (φ : CNF ℕ) (p : Point) : Prop := - 0 ≤ p.1 ∧ p.1 ≤ 8 * ((SAT.incidenceGraph φ).1.length : ℤ) ∧ - 0 ≤ p.2 ∧ p.2 ≤ 8 * ((SAT.incidenceGraph φ).1.length : ℤ) + - 2 * (SAT.incidenceGraph φ).2.length - -private def OutputBound (φ : CNF ℕ) (p : Point) : Prop := - 0 ≤ p.1 ∧ p.1 ≤ gridWidth φ ∧ 0 ≤ p.2 ∧ p.2 ≤ gridHeight φ - -private theorem outputBound_add {φ : CNF ℕ} {p a : Point} (hp : CellBound φ p) - (ha : 0 ≤ a.1 ∧ a.1 ≤ 240 ∧ 0 ≤ a.2 ∧ a.2 ≤ 240) : - OutputBound φ (cellOrigin 120 p + a) := by - simp only [OutputBound, gridWidth, gridHeight, Prod.fst_add, Prod.snd_add, cellOrigin, - Nat.cast_mul, Nat.cast_add, Nat.cast_ofNat] - dsimp only [CellBound] at hp - norm_num at * - constructor - · nlinarith [hp.1, ha.1] - constructor - · nlinarith [hp.2.1, ha.2.1] - constructor <;> nlinarith [hp.2.2.1, hp.2.2.2, ha.2.2.1, ha.2.2.2] - -private theorem cellBound_path {φ : CNF ℕ} {r : Route} (hr : r ∈ paths φ) - {p : Point} (hp : p ∈ r) : CellBound φ p := by - change r ∈ (SAT.incidenceGraph φ).unitPaths at hr - obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hr - have hi' : i < (SAT.incidenceGraph φ).2.length := by simpa using hi - have hp' : p ∈ (SAT.incidenceGraph φ).unitPath i := by - simpa only [Graph.unitPath, List.getD_eq_getElem _ _ hi] using hp - exact Graph.unitPath_bounds _ (fun _ he => SAT.incidenceGraph_endpoints he) - (fun _ he => SAT.incidenceGraph_loopless he) hi' hp' - -private theorem cellBound_occurrencePath {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) {p : Point} (hp : p ∈ occurrencePath φ o) : - CellBound φ p := by - have hi : (Cslib.Logic.PL.occurrences φ).idxOf o < (paths φ).length := by - rw [paths_length, ← Cslib.Logic.PL.length_occurrences] - exact List.idxOf_lt_length_of_mem ho - apply cellBound_path (r := occurrencePath φ o) _ hp - rw [occurrencePath, List.getD_eq_getElem _ _ hi] - exact List.getElem_mem hi - -private theorem cellBound_crossing {φ : CNF ℕ} {p : Point} (hp : p ∈ crossingSites φ) : - CellBound φ p := by - have hlen := (mem_crossingSites φ p).mp hp |>.2.2 - have hnonempty : ((paths φ).filter fun r => r.contains p) ≠ [] := by - intro he - rw [he] at hlen - simp at hlen - obtain ⟨r, hr⟩ := List.exists_mem_of_ne_nil _ hnonempty - obtain ⟨hr, hp⟩ := List.mem_filter.mp hr - exact cellBound_path hr (List.contains_iff_mem.mp hp) - -private theorem cellBound_clause {φ : CNF ℕ} {i : ℕ} (hi : i < φ.length) : - CellBound φ (Layout.center (φ.distinctVars.length + i)) := by - have hn : φ.distinctVars.length + i < (SAT.incidenceGraph φ).1.length := by - simp only [SAT.length_vertices_incidenceGraph, CNF.length_distinctVars] - omega - simp only [CellBound, Layout.center, Nat.cast_add] - omega - -private theorem outputBound_variable {φ : CNF ℕ} {v : Variable} (hv : CellBound φ v.1) : - OutputBound φ (variablePosition v) := by - apply outputBound_add hv - cases h : v.2 with - | none => norm_num - | some w => - have hw := Crossover.variable_bounds w - simp only [Option.elim_some] - omega - -private theorem outputBound_access {φ : CNF ℕ} (sites : List Point) {p q a : Point} - (hp : CellBound φ p) (ha : a ∈ access sites p q) : OutputBound φ a := by - unfold access at ha - split at ha - · obtain ⟨b, hb, rfl⟩ := List.mem_map.mp ha - rw [add_comm] - apply outputBound_add hp - simp only [Crossover.accessRoute, List.mem_cons, List.not_mem_nil, or_false] at hb - rcases hb with rfl | rfl - · generalize side p q = s - fin_cases s <;> decide - · have hw := Crossover.variable_bounds (Crossover.splitTerminal (side p q)) - omega - · simp only [List.mem_cons, List.not_mem_nil, or_false] at ha - rcases ha with rfl | rfl - · unfold cellPort - apply outputBound_add hp - generalize side p q = s - fin_cases s <;> decide - · exact outputBound_add hp (by norm_num) - -private theorem outputBound_center {φ : CNF ℕ} {p : Point} (hp : CellBound φ p) : - OutputBound φ (center p) := outputBound_add hp (by norm_num) - -private theorem outputBound_port {φ : CNF ℕ} {p : Point} (hp : CellBound φ p) (s : Fin 4) : - OutputBound φ (cellPort 120 p s) := by - unfold cellPort - apply outputBound_add hp - fin_cases s <;> decide - -private theorem lastLiteral_bounds {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) (sites : List Point) : - OutputBound φ (variablePosition (lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1) ∧ - ∀ a ∈ (lastLiteral sites (occurrencePath φ o) o.2.2.2).2, OutputBound φ a := by - let r := occurrencePath φ o - have hlen : 2 ≤ r.length := occurrencePath_length_ge_two ho - have hp : CellBound φ (r.getD (r.length - 2) (0, 0)) := by - apply cellBound_occurrencePath ho - rw [List.getD_eq_getElem _ _ (show r.length - 2 < r.length by omega)] - exact List.getElem_mem _ - have hq : CellBound φ (r.getLastD (0, 0)) := by - rw [List.getLastD_eq_getLast?, (occurrencePath_endpoints ho).2, Option.getD_some] - exact cellBound_clause (Cslib.Logic.PL.mem_occurrences.mp ho).1 - change OutputBound φ (variablePosition (signal sites (r.getD (r.length - 2) (0, 0)) - (r.getLastD (0, 0)))) ∧ _ - constructor - · exact outputBound_variable hp - · intro a ha - change a ∈ center (r.getLastD (0, 0)) :: - access sites (r.getD (r.length - 2) (0, 0)) (r.getLastD (0, 0)) at ha - rcases List.mem_cons.mp ha with rfl | ha - · exact outputBound_center hq - · exact outputBound_access sites hp ha - -private def ClauseBound (φ : CNF ℕ) (pc : PlacedClause) : Prop := - OutputBound φ pc.2.1 ∧ - (∀ l ∈ pc.1, OutputBound φ (variablePosition l.1)) ∧ - ∀ r ∈ pc.2.2, ∀ a ∈ r, OutputBound φ a - -private theorem originalClauses_bounds (φ : CNF ℕ) (sites : List Point) : - ∀ pc ∈ originalClauses φ sites, ClauseBound φ pc := by - intro pc hpc - obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc - refine ⟨outputBound_center (cellBound_clause (List.mem_zipIdx' hci).1), ?_, ?_⟩ - · intro l hl - obtain ⟨lr, hlr, rfl⟩ := List.mem_map.mp hl - obtain ⟨lj, hlj, rfl⟩ := List.mem_map.mp hlr - have ho : (ci.2, lj.2, lj.1) ∈ Cslib.Logic.PL.occurrences φ := - List.mem_flatMap.mpr ⟨ci, hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩ - exact (lastLiteral_bounds ho sites).1 - · intro r hr a ha - obtain ⟨lr, hlr, rfl⟩ := List.mem_map.mp hr - obtain ⟨lj, hlj, rfl⟩ := List.mem_map.mp hlr - have ho : (ci.2, lj.2, lj.1) ∈ Cslib.Logic.PL.occurrences φ := - List.mem_flatMap.mpr ⟨ci, hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩ - exact (lastLiteral_bounds ho sites).2 a ha - -private theorem crossingClauses_bounds {φ : CNF ℕ} {p : Point} (hp : CellBound φ p) : - ∀ pc ∈ crossingClauses p, ClauseBound φ pc := by - intro pc hpc - obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc - refine ⟨?_, ?_, ?_⟩ - · apply outputBound_add hp - have hi : ci.2 < Crossover.clausePositions.length := by - rw [Crossover.drawing_sizes.1] - exact (Crossover.length_splitFormula ▸ (List.mem_zipIdx' hci).1) - have hb := Crossover.clause_bounds _ (List.getElem_mem hi) - rw [List.getD_eq_getElem _ _ hi] - omega - · intro l hl - obtain ⟨v, _, rfl⟩ := List.mem_map.mp hl - exact outputBound_variable hp - · intro r hr a ha - obtain ⟨e, he, rfl⟩ := List.mem_map.mp hr - obtain ⟨b, hb, rfl⟩ := List.mem_map.mp ha - rw [add_comm] - apply outputBound_add hp - have h := Crossover.core_bounds e (List.mem_filter.mp he).1 b hb - omega - -private theorem link_bounds {φ : CNF ℕ} (sites : List Point) (positive : Bool) {p q : Point} - (hp : CellBound φ p) (hq : CellBound φ q) : ClauseBound φ (link sites positive p q) := by - have hvp := outputBound_variable (v := signal sites p q) hp - have hvq := outputBound_variable (v := signal sites q p) hq - refine ⟨outputBound_port hp _, ?_, ?_⟩ - · intro l hl - cases positive <;> - simp only [link, Bool.false_eq_true, ↓reduceIte, List.mem_cons, - List.not_mem_nil, or_false] at hl <;> - rcases hl with rfl | rfl <;> assumption - · intro r hr a ha - cases positive <;> - simp only [link, Bool.false_eq_true, ↓reduceIte, List.mem_cons, - List.not_mem_nil, or_false] at hr <;> - rcases hr with rfl | rfl - · exact outputBound_access sites hp ha - · exact outputBound_access sites hq ha - · exact outputBound_access sites hq ha - · exact outputBound_access sites hp ha - -private theorem placedClauses_bounds (φ : CNF ℕ) : - ∀ pc ∈ placedClauses φ, ClauseBound φ pc := by - intro pc hpc - rcases List.mem_append.mp hpc with hpc | hpc - · rcases List.mem_append.mp hpc with hpc | hpc - · exact originalClauses_bounds φ _ pc hpc - · obtain ⟨p, hp, hpc⟩ := List.mem_flatMap.mp hpc - exact crossingClauses_bounds (cellBound_crossing hp) pc hpc - · obtain ⟨o, ho, hpc⟩ := List.mem_flatMap.mp hpc - obtain ⟨e, he, rfl⟩ := List.mem_map.mp hpc - have he' := List.of_mem_zip he - have hp := cellBound_occurrencePath ho ((List.dropLast_subset _ ) he'.1) - have hq := cellBound_occurrencePath ho - ((List.dropLast_subset _) (List.mem_of_mem_tail he'.2)) - exact link_bounds _ _ hp hq - -/-- Every emitted vertex and route point lies in the explicit nonnegative grid rectangle. -This quantitative statement does not assert geometric planarity. -/ -theorem drawing_fits (φ : CNF ℕ) : - Graph.drawingFits (positions φ, routes φ) (gridWidth φ) (gridHeight φ) := by - constructor - · intro p hp - rcases List.mem_append.mp hp with hp | hp - · obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hp - obtain ⟨c, hc, b, hv⟩ := CNF.mem_vars.mp (CNF.mem_distinctVars.mp hv) - obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hc - exact (placedClauses_bounds φ pc hpc).2.1 (v, b) hv - · obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hp - exact (placedClauses_bounds φ pc hpc).1 - · intro r hr p hp - obtain ⟨pc, hpc, hr⟩ := List.mem_flatMap.mp hr - exact (placedClauses_bounds φ pc hpc).2.2 r hr p hp - -private theorem access_cost (sites : List Point) (p q : Point) : - wireLength (access sites p q) ≤ 240 ∧ - (access sites p q).consecutivePairs.length ≤ 19 := by - constructor - · rw [access_wireLength] - split_ifs <;> decide - · rw [access_eq_pair] - change (1 : ℕ) ≤ 19 - decide - -private theorem coreRoute_cost : ∀ e ∈ Crossover.incidenceRoutes, - wireLength e.2.2 ≤ 72 ∧ e.2.2.consecutivePairs.length ≤ 19 := by decide +kernel - -private theorem routes_cost (φ : CNF ℕ) : - ∀ r ∈ routes φ, wireLength r ≤ 240 ∧ r.consecutivePairs.length ≤ 19 := by - intro r hr - obtain ⟨pc, hpc, hr⟩ := List.mem_flatMap.mp hr - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨p, _, hpc⟩) | ⟨o, _, hpc⟩ - · obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc - obtain ⟨lr, hlr, hlreq⟩ := List.mem_map.mp hr - obtain ⟨lj, hlj, rfl⟩ := List.mem_map.mp hlr - have ho : (ci.2, lj.2, lj.1) ∈ Cslib.Logic.PL.occurrences φ := - List.mem_flatMap.mpr ⟨ci, hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩ - dsimp only [lastLiteral] at hlreq - subst r - constructor - · exact finalRoute_wireLength_le _ (occurrencePath_last_unit ho) - · rw [access_eq_pair] - change (2 : ℕ) ≤ 19 - decide - · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc - obtain ⟨e, he, rfl⟩ := List.mem_map.mp hr - have he' := (List.mem_filter.mp he).1 - have hb := coreRoute_cost e he' - constructor - · rw [wireLength_translate] - exact hb.1.trans (by decide) - · simpa [translate, List.consecutivePairs] using hb.2 - · obtain ⟨e, _, rfl⟩ := List.mem_map.mp hpc - cases hpos : o.2.2.2 <;> - simp only [link, hpos, Bool.false_eq_true, ↓reduceIte, List.mem_cons, - List.not_mem_nil, or_false] at hr <;> - rcases hr with rfl | rfl <;> exact access_cost _ _ _ - -/-- The actual output has at most 1210 times the squared source incidence size routes. -/ -theorem routes_length_le (φ : CNF ℕ) : - (routes φ).length ≤ 1210 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by - rw [routes_length, SAT.length_edges_incidenceGraph] - exact length_vars_formula_le φ - -/-- The actual total Manhattan wire length is explicitly quadratic in source incidence size. -/ -theorem drawingWireLength_le (φ : CNF ℕ) : - Graph.drawingWireLength (positions φ, routes φ) ≤ - 300000 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by - have hb : ((routes φ).map wireLength).sum ≤ (routes φ).length * 240 := by - calc - _ ≤ ((routes φ).map fun _ => 240).sum := - List.sum_le_sum fun r hr => (routes_cost φ r hr).1 - _ = _ := by simp - have hr := routes_length_le φ - change ((routes φ).map wireLength).sum ≤ _ - nlinarith - -/-- The actual number of listed route segments is explicitly quadratic in source incidence size. -/ -theorem drawingSegmentCount_le (φ : CNF ℕ) : - Graph.drawingSegmentCount (positions φ, routes φ) ≤ - 23000 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by - have hb : ((routes φ).map fun r => r.consecutivePairs.length).sum ≤ - (routes φ).length * 19 := by - calc - _ ≤ ((routes φ).map fun _ => 19).sum := - List.sum_le_sum fun r hr => (routes_cost φ r hr).2 - _ = _ := by simp - have hr := routes_length_le φ - change ((routes φ).map fun r => r.consecutivePairs.length).sum ≤ _ - nlinarith - -end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Compile.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Compile.lean deleted file mode 100644 index 5b4c8d96e..000000000 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Compile.lean +++ /dev/null @@ -1,116 +0,0 @@ -/- -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.PathAssignments -public import Complexity.Computability.Complexity.Problems.SAT.Incidence -public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalLayout -public import Complexity.Foundations.Geometry.Orthogonal.Subdivision -public import Complexity.Foundations.Geometry.Orthogonal.Macrocell -public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverLayout -public import Complexity.Logics.Propositional.CNF.Compact - -/-! -# Finite orthogonal planarization data - -The compiler replaces each integer unit of an incidence route by a square of side 240. -An ordinary occupied square contains one signal variable. A crossing square contains the -fixed degree-three crossover. Each step between squares contributes one binary implication, -except the last step into an original clause, which supplies its original literal incidence. -The implication direction depends on that literal's polarity. - -This module defines the actual finite output, including clause positions and incidence routes. -Correctness and resource certificates are separate from these executable definitions. - -## Main definitions - -* `Cslib.Complexity.SAT.PlanarCompile.paths`: bounded unit expansions of canonical routes. -* `Cslib.Complexity.SAT.PlanarCompile.crossingSites`: occupied nonvertex crossing candidates. -* `Cslib.Complexity.SAT.PlanarCompile.placedClauses`: clauses with their geometric data. -* `Cslib.Complexity.SAT.PlanarCompile.rawFormula`, `formula`: structured and compact outputs. - -## References - -The global assembly is original. The fixed crossover is credited in `Crossover`. --/ - -@[expose] public section - -namespace Cslib.Complexity.SAT.PlanarCompile - -open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal - -/-- A clause, its position, and one route per literal in literal order. -/ -abbrev PlacedClause := Clause Variable × Point × List Route - -/-- Geometric position of a structured output variable. -/ -def variablePosition (v : Variable) : Point := - cellOrigin 120 v.1 + v.2.elim (120, 120) Crossover.variablePosition - -/-- A route from a cell's side midpoint to its presented signal. -/ -def access (sites : List Point) (p q : Point) : Route := - if p ∈ sites then translate (cellOrigin 120 p) (Crossover.accessRoute (side p q)) - else [cellPort 120 p (side p q), center p] - -/-- One implication at the common side midpoint of adjacent occupied cells. -Positive literals propagate toward the source, negative literals toward the clause. -/ -def link (sites : List Point) (positive : Bool) (p q : Point) : PlacedClause := - let a := signal sites p q - let b := signal sites q p - let ra := access sites p q - let rb := access sites q p - (if positive then [(b, false), (a, true)] else [(a, false), (b, true)], - cellPort 120 p (side p q), if positive then [rb, ra] else [ra, rb]) - -/-- Link clauses along an occurrence path, omitting its final step into the original clause. -/ -def links (sites : List Point) (positive : Bool) (r : Route) : List PlacedClause := - r.dropLast.consecutivePairs.map fun e => link sites positive e.1 e.2 - -/-- The final signal and incidence route replacing one original literal. -/ -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) - ((signal sites p q, positive), center q :: access sites p q) - -/-- Original clauses retain their order and literal polarities. -/ -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 translated fixed gadget in a crossing square. -/ -def crossingClauses (p : Point) : List PlacedClause := - Crossover.splitFormula.zipIdx.map fun (c, i) => - (c.relabel (fun v => (p, some v)), - cellOrigin 120 p + Crossover.clausePositions.getD i (0, 0), - (Crossover.incidenceRoutes.filter fun e => e.1 == i).map fun e => - translate (cellOrigin 120 p) e.2.2) - -/-- The complete finite output, with all original, crossover and link clauses. -/ -def placedClauses (φ : CNF ℕ) : List PlacedClause := - let sites := crossingSites φ - originalClauses φ sites ++ sites.flatMap crossingClauses ++ - (Cslib.Logic.PL.occurrences φ).flatMap fun o => links sites o.2.2.2 (occurrencePath φ o) - -/-- The planarization formula before compacting its structured variable names. -/ -def rawFormula (φ : CNF ℕ) : CNF Variable := (placedClauses φ).map Prod.fst - -/-- Compact natural-number labels, using the existing CNF compaction operation. -/ -def formula (φ : CNF ℕ) : CNF ℕ := (rawFormula φ).compact - -/-- Positions in the order of the output's distinct variables, then of its clauses. -/ -def positions (φ : CNF ℕ) : List Point := - ((rawFormula φ).distinctVars.map variablePosition) ++ - ((placedClauses φ).map fun c => c.2.1) - -/-- Incidence routes in output clause order and literal order. -/ -def routes (φ : CNF ℕ) : List Route := (placedClauses φ).flatMap fun c => c.2.2 - -end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Completeness.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Completeness.lean deleted file mode 100644 index 3056a8b93..000000000 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Completeness.lean +++ /dev/null @@ -1,60 +0,0 @@ -/- -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.PathAssignments -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Correctness -import Mathlib.Data.List.GetD -import Mathlib.Tactic.SplitIfs - -/-! -# Compatible assignments for the actual planar compiler - -An ordinary occupied cell carries its source variable's value. At a selected crossing the -horizontal and vertical source values independently extend through the fixed crossover. - -## Main definitions - -Compiler data and CNF semantics are reused unchanged. - -## Main results - -* `Cslib.Complexity.SAT.PlanarCompile.exists_compatible_assignment`: compatible actual wires - and independent satisfying crossover blocks for every source assignment. -* `Cslib.Complexity.SAT.PlanarCompile.satisfiable_formula_iff`: actual satisfiability equivalence - under source width and literal-occurrence bounds of three. - -## References - -These are original logical composition proofs for the finite compiler. --/ - -@[expose] public section - -namespace Cslib.Complexity.SAT.PlanarCompile - -open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal - -/-- An actual raw compiler output has a satisfying extension of every source model. -/ -theorem satisfiable_rawFormula_of_source {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - (h : φ.Satisfiable) : (rawFormula φ).Satisfiable := by - obtain ⟨τ, hτ⟩ := h - obtain ⟨σ, hcompat, hcross⟩ := exists_compatible_assignment hw hv τ - exact ⟨σ, eval_rawFormula_complete_of_compatible φ τ σ - (fun _ ho => occurrencePath_length_ge_two ho) hcompat hcross hτ⟩ - -/-- The actual compact compiler preserves satisfiability under source width and literal-count -bounds of three. Geometry, degree bounds, and running time are separate compiler properties. -/ -theorem satisfiable_formula_iff {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : - (formula φ).Satisfiable ↔ φ.Satisfiable := - ⟨satisfiable_source_of_formula hw hv, fun h => - (CNF.satisfiable_compact (rawFormula φ)).2 (satisfiable_rawFormula_of_source hw hv h)⟩ - -end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Correctness.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Correctness.lean deleted file mode 100644 index dc8fde83a..000000000 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Correctness.lean +++ /dev/null @@ -1,109 +0,0 @@ -/- -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.PathAssignments -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Semantics -public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Degree -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths -import Mathlib.Data.List.GetD -import Mathlib.Tactic.SplitIfs - -/-! -# Logical correctness along the actual incidence paths - -The actual compiler's occurrence paths are the canonical graph unit paths. This module uses -those path certificates to discharge endpoint and local signal conditions of the wire semantics. - -## Main definitions - -All compiler data and CNF operations are reused from their existing modules. - -## Main results - -* `Cslib.Complexity.SAT.PlanarCompile.satisfiable_source_of_formula`: actual compiler soundness - under source width and literal-occurrence bounds of three. - -## References - -These are original logical composition proofs for the finite compiler. --/ - -@[expose] public section - -namespace Cslib.Complexity.SAT.PlanarCompile - -open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal - -/-- An actual crossover whose path goes straight through a cell equates the two signals read -by the executable neighbor lookups, in either traversal direction. -/ -theorem signals_eq_of_straight {φ : CNF ℕ} {σ : Variable → Bool} - (hraw : (rawFormula φ).eval σ = true) {p : Point} (hp : p ∈ crossingSites φ) - {r : Route} (hn : r.Nodup) {k : ℕ} (hk : k < r.length) (heq : r[k] = p) - (hstraight : StraightThrough r p (1, 0) ∨ StraightThrough r p (0, 1)) : - σ (signal (crossingSites φ) p (r.getD (k - 1) p)) = - σ (signal (crossingSites φ) p (r.getD (k + 1) p)) := by - rcases hstraight with hs | hs - · obtain ⟨_, _, hnb⟩ := hs.getD_neighbors hn hk heq - rcases hnb with ⟨hprev, hnext⟩ | ⟨hprev, hnext⟩ - · rw [hprev, hnext] - exact horizontal_signal_eq hraw hp - · rw [hprev, hnext] - exact (horizontal_signal_eq hraw hp).symm - · obtain ⟨_, _, hnb⟩ := hs.getD_neighbors hn hk heq - rcases hnb with ⟨hprev, hnext⟩ | ⟨hprev, hnext⟩ - · rw [hprev, hnext] - exact vertical_signal_eq hraw hp - · rw [hprev, hnext] - exact (vertical_signal_eq hraw hp).symm - -/-- Actual cell entry/exit values agree: ordinary cells share one variable, while selected -crossings use the certified opposite ports of the fixed crossover. -/ -theorem wire_cells_agree {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {σ : Variable → Bool} (hraw : (rawFormula φ).eval σ = true) : - ∀ o ∈ Cslib.Logic.PL.occurrences φ, - ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), σ c.1 = σ c.2 := by - intro o ho c hc - unfold wire at hc - obtain ⟨⟨p, k⟩, hpk, rfl⟩ := List.mem_map.mp hc - have hget := List.mem_zipIdx_iff_getElem?.mp hpk - obtain ⟨hk, heq⟩ := List.getElem?_eq_some_iff.mp hget - have hk' : k < (occurrencePath φ o).length := by - simp only [List.length_dropLast] at hk - omega - have heq' : (occurrencePath φ o)[k] = p := by - rw [← List.getElem_dropLast hk] - exact heq - have hpi : p ∈ occurrencePath φ o := by - rw [← heq'] - exact List.getElem_mem hk' - by_cases hp : p ∈ crossingSites φ - · exact signals_eq_of_straight hraw hp (occurrencePath_nodup ho) hk' heq' - (occurrencePath_crossing_straight hw hv ho hp hpi) - · simp only [signal, hp, ite_false] - -/-- Under the actual source width and literal-incidence bounds, raw output satisfaction -implies source satisfaction. No local wire equality or endpoint assumption remains. -/ -theorem eval_source_of_rawFormula {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {σ : Variable → Bool} (hraw : (rawFormula φ).eval σ = true) : - φ.eval (fun v => σ (Layout.center (φ.distinctVars.idxOf v), none)) = true := by - apply eval_rawFormula_sound_of_cells φ _ σ - (fun _ ho => occurrencePath_length_ge_two ho) (wire_cells_agree hw hv hraw) ?_ hraw - intro o ho - rw [wire_first_entry ho] - -/-- Compaction preserves the soundness direction for the actual natural-labelled output. -/ -theorem satisfiable_source_of_formula {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - (h : (formula φ).Satisfiable) : φ.Satisfiable := by - obtain ⟨σ, hσ⟩ := (CNF.satisfiable_compact (rawFormula φ)).1 h - exact ⟨_, eval_source_of_rawFormula hw hv hσ⟩ - -end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Geometry.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Geometry.lean deleted file mode 100755 index e5ccff659..000000000 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Geometry.lean +++ /dev/null @@ -1,1740 +0,0 @@ -/- -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.PathGeometry -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths -public import Complexity.Computability.Complexity.Problems.Graph.OrthogonalDrawing -public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Degree -public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Compact -public import Complexity.Logics.Propositional.CNF.Compact.Relabel -import Mathlib.Data.List.GetD -import Mathlib.Data.List.Nodup -import Mathlib.Data.List.Flatten -import Mathlib.Data.List.Forall2 -import Mathlib.Tactic.FinCases -import Mathlib.Tactic.Linarith -import Mathlib.Tactic.NormNum -import Mathlib.Tactic.Push - -/-! -# Geometry of the actual finite planar SAT compiler - -The lemmas refer to the executable routes and positions in `PlanarCompile` and to their -complete real supports. Cell-local statements cover both the fixed crossover access and -ordinary center spokes. Their translated supports are confined to the corresponding square. - -## Main results - -* `Cslib.Complexity.SAT.PlanarCompile.access_eq_pair`: the actual access route endpoints. -* `Cslib.Complexity.SAT.PlanarCompile.access_orthogonal`, - `Cslib.Complexity.SAT.PlanarCompile.access_simple`: local route certificates. -* `Cslib.Complexity.SAT.PlanarCompile.routes_regular`: all actual emitted routes are simple - and orthogonal. -* `Cslib.Complexity.SAT.PlanarCompile.routes_length`, - `Cslib.Complexity.SAT.PlanarCompile.positions_length`: counts match the final incidence graph. -* `Cslib.Complexity.SAT.PlanarCompile.variablePosition_injOn_rawVars`: distinct actual variable - names have distinct displayed positions. -* `Cslib.Complexity.SAT.PlanarCompile.pathPorts_nodup`: all directed unit-cell ports of the - actual paths are distinct under the source width and occurrence bounds. -* `Cslib.Complexity.SAT.PlanarCompile.positions_nodup`: every actual output vertex has a - distinct displayed position under those same source bounds. -* `Cslib.Complexity.SAT.PlanarCompile.routes_endpoints`: actual incidence-order endpoints, - including repeated literal occurrences and compact variable indices. -* `Cslib.Complexity.SAT.PlanarCompile.isPlanarOrthogonalDrawing`: the actual emitted formula, - positions and routes form a complete planar orthogonal drawing under source clause width - at most three and literal occurrence count at most three. Simplicity, vertex avoidance and - contacts use full real supports, including the fixed crossing templates and final clause steps. - -## References - -The global assembly and coordinate arguments are original. The fixed crossover and its -continuous certificates are credited in `CrossoverLayout`. --/ - -@[expose] public section - -namespace Cslib.Complexity.SAT.PlanarCompile - -open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal - -/-- The fixed gadget and cell API use the same four geometric boundary points. -/ -theorem cellPort_eq_boundaryPort (p : Point) (s : Fin 4) : - cellPort 120 p s = cellOrigin 120 p + Crossover.boundaryPort s := by - fin_cases s <;> rfl - -/-- Every actual access route is a single segment from its cell port to its signal variable. -/ -theorem access_eq_pair (sites : List Point) (p q : Point) : - access sites p q = [cellPort 120 p (side p q), variablePosition (signal sites p q)] := by - by_cases hp : p ∈ sites - · simp only [access, hp, ↓reduceIte, Crossover.accessRoute, translate, List.map_cons, - List.map_nil, signal, variablePosition, Option.elim_some, cellPort_eq_boundaryPort] - simp only [add_comm] - · simp [access, hp, signal, variablePosition, center] - -private theorem spoke_orthogonal (s : Fin 4) : - IsOrthogonal [Crossover.boundaryPort s, (120, 120)] := by - fin_cases s <;> norm_num [IsOrthogonal, List.consecutivePairs, AxisAligned, - Crossover.boundaryPort] - -private theorem pair_simple (a b : Point) (h : a ≠ b) : IsSimple [a, b] := by - simp [IsSimple, List.consecutivePairs, h] - -/-- Ordinary access spokes are translates of the same four local straight segments. -/ -theorem access_eq_spoke {sites : List Point} {p : Point} (hp : p ∉ sites) (q : Point) : - access sites p q = translate (cellOrigin 120 p) - [Crossover.boundaryPort (side p q), (120, 120)] := by - simp [access, hp, translate, cellPort_eq_boundaryPort, center, add_comm] - -/-- The actual access route is proper and orthogonal in both kinds of occupied cell. -/ -theorem access_orthogonal (sites : List Point) (p q : Point) : - IsOrthogonal (access sites p q) := by - by_cases hp : p ∈ sites - · simp only [access, hp, ↓reduceIte, isOrthogonal_translate_iff] - exact (Crossover.access_endpoints (side p q)).1 - · rw [access_eq_spoke hp, isOrthogonal_translate_iff] - exact spoke_orthogonal _ - -/-- The actual access route is continuously simple in both kinds of occupied cell. -/ -theorem access_simple (sites : List Point) (p q : Point) : IsSimple (access sites p q) := by - rw [access_eq_pair] - apply pair_simple - have h := access_orthogonal sites p q - rw [access_eq_pair] at h - exact (h (cellPort 120 p (side p q), variablePosition (signal sites p q)) - (by simp [List.consecutivePairs])).2 - -/-- Every structured output variable is strictly inside the cell named by its first coordinate. -This includes all gadget variables, not only those selected as access terminals. -/ -theorem variablePosition_mem_openCell (v : Variable) : - realPoint (variablePosition v) ∈ openCell 120 v.1 := by - rcases v with ⟨p, v⟩ - cases v with - | none => exact center_mem_openCell (by decide) p - | some v => - rw [variablePosition, Option.elim_some, realPoint_add, add_comm, - mem_openCell_add_origin_iff] - have h := Crossover.variable_bounds v - simp only [realPoint] - norm_num - exact_mod_cast (show 0 < (Crossover.variablePosition v).1 ∧ - (Crossover.variablePosition v).1 < 240 ∧ 0 < (Crossover.variablePosition v).2 ∧ - (Crossover.variablePosition v).2 < 240 by omega) - -/-- Every translated fixed-gadget incidence stays in the open cell of that gadget. -/ -theorem crossingRoute_mem_openCell {e : ℕ × Crossover.SplitVariable × Route} - (he : e ∈ Crossover.incidenceRoutes) (c : Point) {p : ℝ × ℝ} - (hp : p ∈ support (translate (cellOrigin 120 c) e.2.2)) : p ∈ openCell 120 c := by - rw [support_translate] at hp - obtain ⟨p, hp, rfl⟩ := hp - rw [mem_openCell_add_origin_iff] - simpa only [Int.reduceMul, Int.cast_ofNat] using Crossover.core_support_interior he hp - -private theorem mem_support_pair {a b : Point} {p : ℝ × ℝ} : - p ∈ support [a, b] ↔ p ∈ segment a b := by - rw [support_cons_cons] - have hs : p ∈ support [b] ↔ p = realPoint b := by - simp [support, List.consecutivePairs] - rw [Set.mem_union, hs] - exact ⟨fun h => h.elim id (fun h => h ▸ _root_.right_mem_segment ℝ _ _), Or.inl⟩ - -private theorem spoke_boundary_isolation (s : Fin 4) {p : ℝ × ℝ} - (hp : p ∈ support [Crossover.boundaryPort s, (120, 120)]) : - 0 ≤ p.1 ∧ p.1 ≤ 240 ∧ 0 ≤ p.2 ∧ p.2 ≤ 240 ∧ - (p.1 = 0 ∨ p.1 = 240 ∨ p.2 = 0 ∨ p.2 = 240 → - p = realPoint (Crossover.boundaryPort s)) := by - rw [mem_support_pair] at hp - fin_cases s <;> - norm_num [Crossover.boundaryPort, Orthogonal.segment, realPoint, mem_horizontal, - mem_vertical, Set.mem_uIcc] at hp ⊢ - all_goals - rcases hp with ⟨heq, hlo, hhi⟩ - refine ⟨by linarith, by linarith, by linarith, by linarith, ?_⟩ - intro h - rcases h with h | h | h | h <;> apply Prod.ext <;> norm_num <;> linarith - -private theorem access_eq_translate (sites : List Point) (p q : Point) : - access sites p q = translate (cellOrigin 120 p) - (if p ∈ sites then Crossover.accessRoute (side p q) - else [Crossover.boundaryPort (side p q), (120, 120)]) := by - by_cases hp : p ∈ sites - · simp [access, hp] - · simpa only [hp, ↓reduceIte] using access_eq_spoke hp q - -/-- The actual access has no boundary contact except its designated midpoint port. -/ -theorem access_support_cell (sites : List Point) (c q : Point) {p : ℝ × ℝ} - (hp : p ∈ support (access sites c q)) : - p ∈ closedCell 120 c ∧ - (p ∈ openCell 120 c ∨ p = realPoint (cellPort 120 c (side c q))) := by - rw [access_eq_translate, support_translate] at hp - obtain ⟨p, hp, rfl⟩ := hp - have hb : 0 ≤ p.1 ∧ p.1 ≤ 240 ∧ 0 ≤ p.2 ∧ p.2 ≤ 240 ∧ - (p.1 = 0 ∨ p.1 = 240 ∨ p.2 = 0 ∨ p.2 = 240 → - p = realPoint (Crossover.boundaryPort (side c q))) := by - by_cases hc : c ∈ sites - · simp only [hc, ↓reduceIte] at hp - exact Crossover.access_boundary_isolation hp - · simp only [hc, ↓reduceIte] at hp - exact spoke_boundary_isolation _ hp - constructor - · rw [mem_closedCell_add_origin_iff] - norm_num - exact ⟨hb.1, hb.2.1, hb.2.2.1, hb.2.2.2.1⟩ - · by_cases h : p.1 = 0 ∨ p.1 = 240 ∨ p.2 = 0 ∨ p.2 = 240 - · right - rw [hb.2.2.2.2 h, cellPort_eq_boundaryPort, realPoint_add, add_comm] - · left - rw [mem_openCell_add_origin_iff] - norm_num - push Not at h - exact ⟨lt_of_le_of_ne hb.1 (Ne.symm h.1), lt_of_le_of_ne hb.2.1 h.2.1, - lt_of_le_of_ne hb.2.2.1 (Ne.symm h.2.2.1), lt_of_le_of_ne hb.2.2.2.1 h.2.2.2⟩ - -/-- Access routes from distinct cells can meet only at their two equal designated ports. -/ -theorem access_contact_of_distinct_cells (sites otherSites : List Point) - {c d : Point} (hcd : c ≠ d) - (a b : Point) {p : ℝ × ℝ} - (hc : p ∈ support (access sites c a)) (hd : p ∈ support (access otherSites d b)) : - p = realPoint (cellPort 120 c (side c a)) ∧ - p = realPoint (cellPort 120 d (side d b)) := by - obtain ⟨hcclosed, hcopen | hcport⟩ := access_support_cell sites c a hc - · exact False.elim (Set.disjoint_left.mp - (disjoint_openCell_closedCell (by decide) hcd) hcopen - (access_support_cell otherSites d b hd).1) - · refine ⟨hcport, ?_⟩ - obtain ⟨_, hdopen | hdport⟩ := access_support_cell otherSites d b hd - · exact False.elim (Set.disjoint_left.mp - (disjoint_openCell_closedCell (by decide) hcd.symm) hdopen hcclosed) - · exact hdport - -private theorem spoke_contact_check : ∀ i j : Fin 4, i ≠ j → - routeContactCheck [(120, 120)] [Crossover.boundaryPort i, (120, 120)] - [Crossover.boundaryPort j, (120, 120)] = true := by decide - -/-- Distinct sides of an ordinary cell contact only at its signal center. -/ -theorem ordinary_access_contact {sites : List Point} {c : Point} (hc : c ∉ sites) - (a b : Point) (hs : side c a ≠ side c b) {p : ℝ × ℝ} - (ha : p ∈ support (access sites c a)) (hb : p ∈ support (access sites c b)) : - p = realPoint (center c) := by - rw [access_eq_spoke hc, support_translate] at ha - obtain ⟨p, ha, rfl⟩ := ha - rw [access_eq_spoke hc] at hb - have hb' := (mem_support_translate_iff _ _ _).mp hb - obtain ⟨q, hq, hpq⟩ := routeContactCheck_sound - (spoke_contact_check _ _ hs) ha hb' - have : q = (120, 120) := List.mem_singleton.mp hq - subst q - rw [hpq, center, realPoint_add, add_comm] - -/-- Distinct access sides of a crossing cell have disjoint real supports. -/ -theorem crossing_access_disjoint {sites : List Point} {c : Point} (hc : c ∈ sites) - (a b : Point) (hs : side c a ≠ side c b) : - Disjoint (support (access sites c a)) (support (access sites c b)) := by - rw [Set.disjoint_left] - intro p ha hb - simp only [access, hc, ↓reduceIte] at ha hb - have ha' := (mem_support_translate_iff (cellOrigin 120 c) (Crossover.accessRoute (side c a)) - (p - realPoint (cellOrigin 120 c))).mp - (by simpa only [sub_add_cancel] using ha) - have hb' := (mem_support_translate_iff (cellOrigin 120 c) (Crossover.accessRoute (side c b)) - (p - realPoint (cellOrigin 120 c))).mp - (by simpa only [sub_add_cancel] using hb) - exact Set.disjoint_left.mp (Crossover.access_disjoint hs) ha' hb' - -/-- Compact labels retain the compiler's structured variable order and displayed positions. -/ -theorem positions_getD_variable (φ : CNF ℕ) {v : Variable} - (hv : v ∈ (rawFormula φ).vars) : - (positions φ).getD ((formula φ).distinctVars.idxOf ((rawFormula φ).vars.idxOf v)) (0, 0) = - variablePosition v := by - rw [formula, CNF.idxOf_distinctVars_compact _ hv] - have hi := List.idxOf_lt_length_of_mem (CNF.mem_distinctVars.mpr hv) - rw [positions, List.getD_append _ _ _ _ (by simpa only [List.length_map] using hi)] - rw [List.getD_eq_getElem _ _ (by simpa only [List.length_map] using hi), List.getElem_map] - congr 1 - exact List.getElem_idxOf hi - -private theorem three_simple {a b c : Point} (hn : [a, b, c].Nodup) - (hc : segmentContactCheck [b] a b b c = true) : IsSimple [a, b, c] := by - have hcontact : EndpointContacts a b b c := by - intro p hp hq - obtain ⟨q, hq, hpq⟩ := segmentContactCheck_sound hc hp hq - have hqb : q = b := List.mem_singleton.mp hq - exact ⟨Or.inr (hqb ▸ hpq), Or.inl (hqb ▸ hpq)⟩ - refine ⟨hn, ?_⟩ - intro e he f hf hne - simp only [List.consecutivePairs, List.tail_cons, List.zip_cons_cons, List.zip_nil_right, - List.mem_cons, List.not_mem_nil, or_false] at he hf - rcases he with rfl | rfl <;> rcases hf with rfl | rfl - · exact False.elim (hne rfl) - · exact hcontact - · exact hcontact.symm - · exact False.elim (hne rfl) - -private def finalLocalRoute (s : Fin 4) (crossing : Bool) : Route := - [2 • Crossover.boundaryPort s - (120, 120), Crossover.boundaryPort s, - if crossing then Crossover.variablePosition (Crossover.splitTerminal s) else (120, 120)] - -private theorem finalLocalRoute_simple (s : Fin 4) (crossing : Bool) : - IsSimple (finalLocalRoute s crossing) := by - unfold finalLocalRoute - apply three_simple - · fin_cases s <;> cases crossing <;> decide - · fin_cases s <;> cases crossing <;> decide - -private theorem finalLocalRoute_orthogonal (s : Fin 4) (crossing : Bool) : - IsOrthogonal (finalLocalRoute s crossing) := by - fin_cases s <;> cases crossing <;> - norm_num [finalLocalRoute, Crossover.boundaryPort, Crossover.variablePosition, - Crossover.splitTerminal, IsOrthogonal, List.consecutivePairs, AxisAligned] - -private theorem neighbor_center {p q : Point} (h : Orthogonal.length p q = 1) : - center q = 2 • Crossover.boundaryPort (side p q) - (120, 120) + cellOrigin 120 p := by - rcases p with ⟨px, py⟩ - rcases unit_neighbor_cases h with rfl | rfl | rfl | rfl <;> - norm_num [center, side, Crossover.boundaryPort, cellOrigin, two_nsmul, - Prod.ext_iff] <;> omega - -/-- The final-literal route is a translated straight three-point route for every unit step. -/ -private theorem finalRoute_eq_translate (sites : List Point) {p q : Point} - (h : Orthogonal.length p q = 1) : - center q :: access sites p q = translate (cellOrigin 120 p) - (finalLocalRoute (side p q) (decide (p ∈ sites))) := by - rw [neighbor_center h] - by_cases hp : p ∈ sites <;> - simp [access, hp, translate, finalLocalRoute, Crossover.accessRoute, - cellPort_eq_boundaryPort, center, add_comm] - -/-- The actual final incidence across a unit step is continuously simple. -/ -theorem finalRoute_simple (sites : List Point) {p q : Point} - (h : Orthogonal.length p q = 1) : IsSimple (center q :: access sites p q) := by - rw [finalRoute_eq_translate sites h, isSimple_translate_iff] - exact finalLocalRoute_simple _ _ - -/-- The actual final incidence across a unit step is proper and orthogonal. -/ -theorem finalRoute_orthogonal (sites : List Point) {p q : Point} - (h : Orthogonal.length p q = 1) : IsOrthogonal (center q :: access sites p q) := by - rw [finalRoute_eq_translate sites h, isOrthogonal_translate_iff] - exact finalLocalRoute_orthogonal _ _ - -/-- Access length is exactly 20 inside a crossing cell and 120 inside an ordinary cell. -/ -theorem access_wireLength (sites : List Point) (p q : Point) : - wireLength (access sites p q) = if p ∈ sites then 20 else 120 := by - by_cases hp : p ∈ sites - · simp only [access, hp, ↓reduceIte, wireLength_translate] - exact (Crossover.access_route_sizes _).2 - · rw [access_eq_spoke hp, wireLength_translate] - simp only [hp, ↓reduceIte] - generalize side p q = s - fin_cases s <;> decide - -/-- A final literal route across one unit step uses at most 240 units of wire. -/ -theorem finalRoute_wireLength_le (sites : List Point) {p q : Point} - (h : Orthogonal.length p q = 1) : - wireLength (center q :: access sites p q) ≤ 240 := by - rw [finalRoute_eq_translate sites h, wireLength_translate] - generalize side p q = s - generalize decide (p ∈ sites) = crossing - fin_cases s <;> cases crossing <;> decide - -/-- A final literal route is the ordinary clause-cell spoke followed by its neighbor's access. -This equality concerns the full real supports and includes the shared boundary midpoint. -/ -theorem support_finalRoute (sites : List Point) {p q : Point} - (h : Orthogonal.length p q = 1) : - support (center q :: access sites p q) = - support (access [] q p) ∪ support (access sites p q) := by - rw [access_eq_pair sites p q, access_eq_pair [] q p, support_cons_cons] - have hs (a b : Point) : support [a, b] = segment a b := - Set.ext fun _ => mem_support_pair - rw [hs (cellPort 120 q (side q p))] - simp only [signal, List.not_mem_nil, ↓reduceIte, variablePosition, Option.elim_none] - rw [← shared_cellPort h] - congr 1 - exact _root_.segment_symm ℝ _ _ - -/-- The final route starts at its original clause center and ends at the presented signal. -/ -theorem finalRoute_endpoints (sites : List Point) (p q : Point) : - (center q :: access sites p q).head? = some (center q) ∧ - (center q :: access sites p q).getLast? = - some (variablePosition (signal sites p q)) := by - rw [access_eq_pair] - exact ⟨rfl, rfl⟩ - -/-- The two binary-link incidences are simple actual access routes. -/ -theorem link_routes_simple (sites : List Point) (positive : Bool) (p q : Point) : - ∀ r ∈ (link sites positive p q).2.2, IsSimple r := by - cases positive <;> simp only [link, Bool.false_eq_true, ↓reduceIte, List.mem_cons, - List.not_mem_nil, or_false, forall_eq_or_imp, forall_eq] <;> - exact ⟨access_simple _ _ _, access_simple _ _ _⟩ - -/-- The two binary-link incidences are proper actual orthogonal access routes. -/ -theorem link_routes_orthogonal (sites : List Point) (positive : Bool) (p q : Point) : - ∀ r ∈ (link sites positive p q).2.2, IsOrthogonal r := by - cases positive <;> simp only [link, Bool.false_eq_true, ↓reduceIte, List.mem_cons, - List.not_mem_nil, or_false, forall_eq_or_imp, forall_eq] <;> - exact ⟨access_orthogonal _ _ _, access_orthogonal _ _ _⟩ - -/-- Literal and route ordering in an actual binary link gives the declared geometric endpoints. -/ -theorem link_endpoints (sites : List Point) (positive : Bool) {p q : Point} - (h : Orthogonal.length p q = 1) {l : Literal Variable} {r : Route} - (hlr : (l, r) ∈ (link sites positive p q).1.zip (link sites positive p q).2.2) : - r.head? = some (link sites positive p q).2.1 ∧ - r.getLast? = some (variablePosition l.1) := by - cases positive <;> - simp only [link, Bool.false_eq_true, ↓reduceIte, List.zip_cons_cons, List.zip_nil_right, - List.mem_cons, List.not_mem_nil, or_false] at hlr ⊢ <;> - rcases hlr with e | e <;> cases e <;> - simp [access_eq_pair, ← shared_cellPort h] - -/-- An ordinary signal name occurs exactly in an ordinary cell. -/ -theorem signal_none_iff (sites : List Point) (p q : Point) : - (signal sites p q).2 = none ↔ p ∉ sites := by - simp [signal] - -/-- Every variable actually emitted by the compiler has the appropriate cell kind. -In particular, the ordinary center name is never emitted inside a crossover cell. -/ -theorem raw_variable_cell_kind (φ : CNF ℕ) {v : Variable} - (hv : v ∈ (rawFormula φ).vars) : - v.2 = none ↔ v.1 ∉ crossingSites φ := by - obtain ⟨c, hc, b, hv⟩ := CNF.mem_vars.mp hv - obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hc - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨p, hp, hpc⟩) | ⟨o, _, hpc⟩ - · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc - obtain ⟨lr, hlr, hlreq⟩ := List.mem_map.mp hv - obtain ⟨lj, _, rfl⟩ := List.mem_map.mp hlr - have heq := congrArg Prod.fst hlreq - simp only [lastLiteral] at heq - subst v - exact signal_none_iff _ _ _ - · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc - obtain ⟨l, _, hl⟩ := List.mem_map.mp hv - have heq := congrArg Prod.fst hl - dsimp only at heq - subst v - simp [hp] - · obtain ⟨e, _, rfl⟩ := List.mem_map.mp hpc - cases hpos : o.2.2.2 <;> - simp only [link, hpos, Bool.false_eq_true, ↓reduceIte, List.mem_cons, - List.not_mem_nil, or_false] at hv <;> - rcases hv with hv | hv <;> - have heq := congrArg Prod.fst hv <;> dsimp only at heq <;> subst v <;> - exact signal_none_iff _ _ _ - -/-- Actual structured variable names have distinct positions, including across different cells. -/ -theorem variablePosition_injOn_rawVars (φ : CNF ℕ) : - Set.InjOn variablePosition {v | v ∈ (rawFormula φ).vars} := by - intro v hv w hw heq - have hreal := congrArg realPoint heq - have hvcell := variablePosition_mem_openCell v - have hwcell := variablePosition_mem_openCell w - rw [← hreal] at hwcell - have hcell : v.1 = w.1 := cell_eq_of_mem_open_closed (by decide) hvcell - ⟨hwcell.1.le, hwcell.2.1.le, hwcell.2.2.1.le, hwcell.2.2.2.le⟩ - rcases v with ⟨p, v⟩ - rcases w with ⟨q, w⟩ - change p = q at hcell - subst q - have hvkind := raw_variable_cell_kind φ hv - have hwkind := raw_variable_cell_kind φ hw - cases v <;> cases w - · rfl - · cases hwkind.mpr (hvkind.mp rfl) - · cases hvkind.mpr (hwkind.mp rfl) - · simp only [variablePosition, Option.elim_some, add_right_inj] at heq - exact congrArg (fun x => (p, some x)) (Crossover.variablePosition_injective heq) - -private theorem idxOf_range_eq {i n : ℕ} (hi : i < n) : (List.range n).idxOf i = i := by - have h := (List.nodup_range : (List.range n).Nodup).idxOf_getElem i - (by simpa only [List.length_range] using hi) - rw [List.getElem_range] at h - exact h - -/-- Every route actually emitted by the compiler is proper, orthogonal and continuously simple. -The source degree bounds are needed for global separation, not for this local certificate. -/ -theorem routes_regular (φ : CNF ℕ) : - ∀ r ∈ routes φ, IsOrthogonal r ∧ IsSimple r := by - intro r hr - obtain ⟨pc, hpc, hr⟩ := List.mem_flatMap.mp hr - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨p, _, hpc⟩) | ⟨o, _, hpc⟩ - · obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc - obtain ⟨lr, hlr, hlreq⟩ := List.mem_map.mp hr - obtain ⟨lj, hlj, rfl⟩ := List.mem_map.mp hlr - have ho : (ci.2, lj.2, lj.1) ∈ Cslib.Logic.PL.occurrences φ := by - exact List.mem_flatMap.mpr ⟨ci, hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩ - dsimp only [lastLiteral] at hlreq - subst r - exact ⟨finalRoute_orthogonal _ (occurrencePath_last_unit ho), - finalRoute_simple _ (occurrencePath_last_unit ho)⟩ - · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc - obtain ⟨e, he, rfl⟩ := List.mem_map.mp hr - have he' := (List.mem_filter.mp he).1 - exact ⟨(isOrthogonal_translate_iff _ _).mpr (Crossover.incidence_orthogonal e he'), - (isSimple_translate_iff _ _).mpr (Crossover.incidence_isSimple he')⟩ - · obtain ⟨e, _, rfl⟩ := List.mem_map.mp hpc - exact ⟨link_routes_orthogonal _ _ _ _ r hr, link_routes_simple _ _ _ _ r hr⟩ - -private theorem crossing_route_count : ∀ i : Fin 74, - (Crossover.incidenceRoutes.filter fun e => e.1 == i.val).length = - (Crossover.splitFormula.getD i.val []).length := by decide +kernel - -/-- Every actual placed clause supplies exactly one route for each of its literal occurrences. -/ -theorem placedClause_route_count (φ : CNF ℕ) : - ∀ pc ∈ placedClauses φ, pc.2.2.length = pc.1.length := by - intro pc hpc - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨p, _, hpc⟩) | ⟨o, _, hpc⟩ - · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc - simp - · obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc - have hi : ci.2 < 74 := by - have h := (List.mem_zipIdx hci).2.1 - simpa only [Nat.zero_add, Crossover.length_splitFormula] using h - have hc := (List.mem_zipIdx hci).2.2 - simp only [Nat.sub_zero] at hc - have hcount := crossing_route_count ⟨ci.2, hi⟩ - rw [List.getD_eq_getElem Crossover.splitFormula [] - (by simpa only [Crossover.length_splitFormula] using hi)] at hcount - simpa only [List.length_map, Clause.length_relabel, hc] using hcount - · obtain ⟨e, _, rfl⟩ := List.mem_map.mp hpc - cases o.2.2.2 <;> rfl - -/-- The actual route count matches the listed edges of the final compact incidence graph. -/ -theorem routes_length (φ : CNF ℕ) : - (routes φ).length = (SAT.incidenceGraph (formula φ)).2.length := by - rw [SAT.length_edges_incidenceGraph] - rw [formula, CNF.compact, CNF.vars_relabel, List.length_map] - simp only [routes, List.length_flatMap, CNF.vars, List.length_map, - List.length_flatten, rawFormula, List.map_map, - Function.comp_def] - congr 1 - apply List.map_congr_left - exact fun pc hpc => placedClause_route_count φ pc hpc - -/-- The actual position list has exactly the final compact graph's declared vertex count. -/ -theorem positions_length (φ : CNF ℕ) : - (positions φ).length = (SAT.incidenceGraph (formula φ)).1.length := by - simp [positions, SAT.incidenceGraph, formula, CNF.distinctVars_compact, rawFormula] - -/-- The final compact output has exactly the same ordered incidence graph as the raw output. -/ -theorem incidenceGraph_formula (φ : CNF ℕ) : - SAT.incidenceGraph (formula φ) = SAT.incidenceGraph (rawFormula φ) := - SAT.incidenceGraph_compact _ - -/-- The actual displayed variable positions have no repetitions. -/ -theorem variablePositions_nodup (φ : CNF ℕ) : - ((rawFormula φ).distinctVars.map variablePosition).Nodup := - (CNF.nodup_distinctVars _).map_on (fun _ hv _ hw => - variablePosition_injOn_rawVars φ (CNF.mem_distinctVars.mp hv) (CNF.mem_distinctVars.mp hw)) - -/-- Every geometric side midpoint lies in its own closed real cell. -/ -theorem cellPort_mem_closedCell (c : Point) (s : Fin 4) : - realPoint (cellPort 120 c s) ∈ closedCell 120 c := by - rw [cellPort_eq_boundaryPort, realPoint_add, add_comm, mem_closedCell_add_origin_iff] - fin_cases s <;> norm_num [Crossover.boundaryPort, realPoint] - -/-- A geometric side midpoint is outside every open cell, including both cells sharing it. -/ -theorem cellPort_not_mem_openCell (c d : Point) (s : Fin 4) : - realPoint (cellPort 120 c s) ∉ openCell 120 d := by - intro hp - have heq : d = c := cell_eq_of_mem_open_closed (by decide) hp (cellPort_mem_closedCell c s) - subst d - rw [cellPort_eq_boundaryPort, realPoint_add, add_comm, mem_openCell_add_origin_iff] at hp - fin_cases s <;> norm_num [Crossover.boundaryPort, realPoint] at hp - -/-- No binary-link clause position is a variable position, even in a neighboring cell. -/ -theorem link_position_ne_variable (sites : List Point) (positive : Bool) (p q : Point) - (v : Variable) : (link sites positive p q).2.1 ≠ variablePosition v := by - intro h - apply cellPort_not_mem_openCell p v.1 (side p q) - rw [show cellPort 120 p (side p q) = variablePosition v from h] - exact variablePosition_mem_openCell v - -/-- Every translated crossover clause position lies strictly inside its gadget cell. -/ -theorem crossingClause_mem_openCell {c : Point} {pc : PlacedClause} - (hpc : pc ∈ crossingClauses c) : realPoint pc.2.1 ∈ openCell 120 c := by - obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc - have hi : ci.2 < Crossover.clausePositions.length := by - have h := (List.mem_zipIdx hci).2.1 - simpa only [Nat.zero_add, Crossover.length_splitFormula, Crossover.drawing_sizes.1] using h - have hp : Crossover.clausePositions.getD ci.2 (0, 0) ∈ Crossover.clausePositions := by - rw [List.getD_eq_getElem _ _ hi] - exact List.getElem_mem hi - have hb := Crossover.clause_bounds _ hp - rw [realPoint_add, add_comm, mem_openCell_add_origin_iff] - simp only [realPoint] - norm_num - exact_mod_cast (show 0 < (Crossover.clausePositions.getD ci.2 (0, 0)).1 ∧ - (Crossover.clausePositions.getD ci.2 (0, 0)).1 < 240 ∧ - 0 < (Crossover.clausePositions.getD ci.2 (0, 0)).2 ∧ - (Crossover.clausePositions.getD ci.2 (0, 0)).2 < 240 by omega) - -/-- Original clause positions are pairwise distinct, including repeated and empty clauses. -/ -theorem originalPositions_nodup (φ : CNF ℕ) (sites : List Point) : - ((originalClauses φ sites).map fun pc => pc.2.1).Nodup := by - rw [List.Nodup, List.pairwise_iff_getElem] - intro i j hi hj hij heq - simp only [originalClauses, List.getElem_map, List.getElem_zipIdx] at heq - have hc := center_injective heq - have hx := congrArg Prod.fst hc - simp only [Layout.center] at hx - omega - -/-- Each translated crossover keeps the fixed clause-position order. -/ -theorem crossingClause_positions (c : Point) : - (crossingClauses c).map (fun pc => pc.2.1) = - Crossover.clausePositions.map (cellOrigin 120 c + ·) := by - apply List.ext_getElem - · simp [crossingClauses, Crossover.length_splitFormula, Crossover.drawing_sizes.1] - · intro i hi hj - simp only [crossingClauses, List.getElem_map, List.getElem_zipIdx, Nat.zero_add] - rw [List.getD_eq_getElem _ _ (by simpa only [List.length_map] using hj)] - -/-- Every crossover has pairwise distinct actual clause positions. -/ -theorem crossingClause_positions_nodup (c : Point) : - ((crossingClauses c).map fun pc => pc.2.1).Nodup := by - rw [crossingClause_positions] - exact Crossover.clausePositions_nodup.map (fun _ _ h => add_left_cancel h) - -/-- Different selected crossing cells contribute disjoint lists of interior clause positions. -/ -theorem crossingPositions_nodup {sites : List Point} (hn : sites.Nodup) : - ((sites.flatMap crossingClauses).map fun pc => pc.2.1).Nodup := by - rw [List.map_flatMap] - apply List.nodup_flatMap.mpr - refine ⟨fun c _ => crossingClause_positions_nodup c, hn.imp ?_⟩ - intro c d hcd p hp hq - obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hp - obtain ⟨pd, hpd, heq⟩ := List.mem_map.mp hq - have hc := crossingClause_mem_openCell hpc - have hd := crossingClause_mem_openCell hpd - rw [heq] at hd - exact Set.disjoint_left.mp (disjoint_openCell (by decide) hcd) hc hd - -/-- Original and crossover clause positions cannot coincide. -/ -theorem original_crossing_positions_disjoint (φ : CNF ℕ) : - List.Disjoint ((originalClauses φ (crossingSites φ)).map fun pc => pc.2.1) - (((crossingSites φ).flatMap crossingClauses).map fun pc => pc.2.1) := by - intro p hp hq - obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hp - obtain ⟨pd, hpd, heq⟩ := List.mem_map.mp hq - obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc - obtain ⟨c, hc, hpd⟩ := List.mem_flatMap.mp hpd - have hpos := crossingClause_mem_openCell hpd - rw [heq] at hpos - have hcenter := center_mem_openCell (r := 120) (by decide) - (Layout.center (φ.distinctVars.length + ci.2)) - have hcell := cell_eq_of_mem_open_closed (by decide) hcenter - ⟨hpos.1.le, hpos.2.1.le, hpos.2.2.1.le, hpos.2.2.2.le⟩ - have hi : ci.2 < φ.length := by simpa only [Nat.zero_add] using (List.mem_zipIdx hci).2.1 - exact clause_cell_not_mem_crossingSites φ hi (hcell ▸ hc) - -private theorem consecutivePairs_dropLast (r : Route) : - r.dropLast.consecutivePairs = r.consecutivePairs.dropLast := by - induction r with - | nil => rfl - | cons a r ih => - cases r with - | nil => rfl - | cons b r => - cases r with - | nil => rfl - | cons c r => - simp only [List.dropLast_cons_cons, List.consecutivePairs, List.tail_cons, - List.zip_cons_cons] at ih ⊢ - exact congrArg ((a, b) :: ·) ih - -/-- Binary-clause positions are a sublist of the distinct actual unit-step midpoints. -/ -theorem linkPositions_sublist_midpoints (φ : CNF ℕ) : - (((Cslib.Logic.PL.occurrences φ).flatMap fun o => - links (crossingSites φ) o.2.2.2 (occurrencePath φ o)).map fun pc => pc.2.1).Sublist - ((paths φ).flatMap fun r => r.consecutivePairs.map fun e => - cellPort 120 e.1 (side e.1 e.2)) := by - rw [← occurrencePaths_eq_paths φ, List.flatMap_map] - simp only [List.map_flatMap, links, List.map_map, Function.comp_def, link] - apply List.Sublist.flatMap_right - intro o _ - apply List.Sublist.map - rw [consecutivePairs_dropLast] - exact List.dropLast_sublist _ - -/-- All actual binary-link clauses have distinct positions, including between parallel paths. -/ -theorem linkPositions_nodup {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : - ((((Cslib.Logic.PL.occurrences φ).flatMap fun o => - links (crossingSites φ) o.2.2.2 (occurrencePath φ o)).map fun pc => pc.2.1)).Nodup := - (pathMidpoints_nodup hw hv).sublist (linkPositions_sublist_midpoints φ) - -private theorem link_position_not_open {sites : List Point} {positive : Bool} {r : Route} - {pc : PlacedClause} (hpc : pc ∈ links sites positive r) (c : Point) : - realPoint pc.2.1 ∉ openCell 120 c := by - obtain ⟨e, _, rfl⟩ := List.mem_map.mp hpc - exact cellPort_not_mem_openCell _ c _ - -private theorem original_link_positions_disjoint (φ : CNF ℕ) : - List.Disjoint ((originalClauses φ (crossingSites φ)).map fun pc => pc.2.1) - (((Cslib.Logic.PL.occurrences φ).flatMap fun o => - links (crossingSites φ) o.2.2.2 (occurrencePath φ o)).map fun pc => pc.2.1) := by - intro p hp hq - obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hp - obtain ⟨pd, hpd, heq⟩ := List.mem_map.mp hq - obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc - obtain ⟨_, _, hpd⟩ := List.mem_flatMap.mp hpd - apply link_position_not_open hpd (Layout.center (φ.distinctVars.length + ci.2)) - rw [heq] - exact center_mem_openCell (by decide) _ - -private theorem crossing_link_positions_disjoint (φ : CNF ℕ) : - List.Disjoint (((crossingSites φ).flatMap crossingClauses).map fun pc => pc.2.1) - (((Cslib.Logic.PL.occurrences φ).flatMap fun o => - links (crossingSites φ) o.2.2.2 (occurrencePath φ o)).map fun pc => pc.2.1) := by - intro p hp hq - obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hp - obtain ⟨pd, hpd, heq⟩ := List.mem_map.mp hq - obtain ⟨c, _, hpc⟩ := List.mem_flatMap.mp hpc - obtain ⟨_, _, hpd⟩ := List.mem_flatMap.mp hpd - apply link_position_not_open hpd c - rw [heq] - exact crossingClause_mem_openCell hpc - -/-- All actual output clauses have distinct displayed positions. Boundary clauses, interior -crossover clauses and original source clauses are separated in the full real-cell geometry. -/ -theorem clausePositions_nodup {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : - ((placedClauses φ).map fun pc => pc.2.1).Nodup := by - simp only [placedClauses, List.map_append] - apply List.Nodup.append - · exact (originalPositions_nodup φ _).append - (crossingPositions_nodup (crossingSites_nodup φ)) (original_crossing_positions_disjoint φ) - · exact linkPositions_nodup hw hv - · intro p hp hq - rcases List.mem_append.mp hp with hp | hp - · exact original_link_positions_disjoint φ hp hq - · exact crossing_link_positions_disjoint φ hp hq - -private theorem penultimate_mem_dropLast {r : Route} (h : 2 ≤ r.length) : - r.getD (r.length - 2) (0, 0) ∈ r.dropLast := by - have hk : r.length - 2 < r.dropLast.length := by simp only [List.length_dropLast]; omega - rw [List.getD_eq_getElem _ _ (by omega), ← List.getElem_dropLast hk] - exact List.getElem_mem hk - -/-- Every emitted variable cell is a selected crossing or lies before the final clause point -of an actual source occurrence path. -/ -theorem raw_variable_cell_membership (φ : CNF ℕ) {v : Variable} - (hv : v ∈ (rawFormula φ).vars) : - v.1 ∈ crossingSites φ ∨ ∃ o ∈ Cslib.Logic.PL.occurrences φ, - v.1 ∈ (occurrencePath φ o).dropLast := by - obtain ⟨c, hc, b, hv⟩ := CNF.mem_vars.mp hv - obtain ⟨pc, hpc, rfl⟩ := List.mem_map.mp hc - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨p, hp, hpc⟩) | ⟨o, ho, hpc⟩ - · obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc - obtain ⟨lr, hlr, hlreq⟩ := List.mem_map.mp hv - obtain ⟨lj, hlj, rfl⟩ := List.mem_map.mp hlr - have ho : (ci.2, lj.2, lj.1) ∈ Cslib.Logic.PL.occurrences φ := - List.mem_flatMap.mpr ⟨ci, hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩ - have heq := congrArg Prod.fst hlreq - dsimp only [lastLiteral] at heq - subst v - exact Or.inr ⟨_, ho, penultimate_mem_dropLast (occurrencePath_length_ge_two ho)⟩ - · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc - obtain ⟨l, _, hl⟩ := List.mem_map.mp hv - have heq := congrArg Prod.fst hl - dsimp only at heq - subst v - exact Or.inl hp - · obtain ⟨e, he, rfl⟩ := List.mem_map.mp hpc - cases hpos : o.2.2.2 <;> - simp only [link, hpos, Bool.false_eq_true, ↓reduceIte, List.mem_cons, - List.not_mem_nil, or_false] at hv <;> - rcases hv with hv | hv <;> - have heq := congrArg Prod.fst hv <;> dsimp only at heq <;> subst v - all_goals first - | exact Or.inr ⟨o, ho, (List.of_mem_zip he).1⟩ - | exact Or.inr ⟨o, ho, List.mem_of_mem_tail (List.of_mem_zip he).2⟩ - -/-- Actual output variables never occupy a source clause cell. -/ -theorem raw_variable_not_clause_cell {φ : CNF ℕ} {v : Variable} - (hv : v ∈ (rawFormula φ).vars) {i : ℕ} (hi : i < φ.length) : - v.1 ≠ Layout.center (φ.distinctVars.length + i) := by - intro h - rcases raw_variable_cell_membership φ hv with hsite | ⟨o, ho, hp⟩ - · exact clause_cell_not_mem_crossingSites φ hi (h ▸ hsite) - · exact clause_cell_not_mem_path_dropLast ho hi (h ▸ hp) - -private theorem crossing_position_ne_raw_variable {φ : CNF ℕ} {c : Point} - (hc : c ∈ crossingSites φ) {pc : PlacedClause} (hpc : pc ∈ crossingClauses c) - {v : Variable} (hv : v ∈ (rawFormula φ).vars) : pc.2.1 ≠ variablePosition v := by - intro hpos - have hpcopen := crossingClause_mem_openCell hpc - have hvopen := variablePosition_mem_openCell v - rw [hpos] at hpcopen - have hcell : c = v.1 := cell_eq_of_mem_open_closed (by decide) hpcopen - ⟨hvopen.1.le, hvopen.2.1.le, hvopen.2.2.1.le, hvopen.2.2.2.le⟩ - rcases v with ⟨p, v⟩ - change c = p at hcell - subst p - cases v with - | none => exact (raw_variable_cell_kind φ hv).mp rfl hc - | some v => - have hmem : pc.2.1 ∈ (crossingClauses c).map (fun pc => pc.2.1) := - List.mem_map_of_mem hpc - rw [crossingClause_positions] at hmem - obtain ⟨q, hq, heq⟩ := List.mem_map.mp hmem - have heq' : q = Crossover.variablePosition v := add_left_cancel (heq.trans hpos) - exact Crossover.variablePosition_not_mem_clauses v (heq' ▸ hq) - -/-- The actual variable and clause position lists are disjoint. This includes empty original -clauses and excludes variable vertices from all binary-clause boundary positions. -/ -theorem variable_clause_positions_disjoint (φ : CNF ℕ) : - List.Disjoint ((rawFormula φ).distinctVars.map variablePosition) - ((placedClauses φ).map fun pc => pc.2.1) := by - intro p hp hq - obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hp - have hv' := CNF.mem_distinctVars.mp hv - obtain ⟨pc, hpc, hpos⟩ := List.mem_map.mp hq - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨c, hc, hpc⟩) | ⟨o, _, hpc⟩ - · obtain ⟨⟨c, i⟩, hci, rfl⟩ := List.mem_map.mp hpc - dsimp only at hpos - have hcenter := center_mem_openCell (r := 120) (by decide) - (Layout.center (φ.distinctVars.length + i)) - change realPoint (center (Layout.center (φ.distinctVars.length + i))) ∈ _ at hcenter - rw [hpos] at hcenter - have hvopen := variablePosition_mem_openCell v - have hcell : Layout.center (φ.distinctVars.length + i) = v.1 := - cell_eq_of_mem_open_closed (by decide) hcenter - ⟨hvopen.1.le, hvopen.2.1.le, hvopen.2.2.1.le, hvopen.2.2.2.le⟩ - have hi : i < φ.length := by - simpa only [Nat.zero_add] using (List.mem_zipIdx hci).2.1 - exact raw_variable_not_clause_cell hv' hi hcell.symm - · exact crossing_position_ne_raw_variable hc hpc hv' hpos - · obtain ⟨e, _, rfl⟩ := List.mem_map.mp hpc - exact link_position_ne_variable _ _ _ _ v hpos - -/-- All actual displayed output vertices have distinct integer positions. -/ -theorem positions_nodup {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : (positions φ).Nodup := - (variablePositions_nodup φ).append (clausePositions_nodup hw hv) - (variable_clause_positions_disjoint φ) - -private theorem originalClause_endpoints {φ : CNF ℕ} {sites : List Point} - {pc : PlacedClause} (hpc : pc ∈ originalClauses φ sites) - {l : Literal Variable} {r : Route} (hlr : (l, r) ∈ pc.1.zip pc.2.2) : - r.head? = some pc.2.1 ∧ r.getLast? = some (variablePosition l.1) := by - obtain ⟨⟨c, i⟩, hci, rfl⟩ := List.mem_map.mp hpc - dsimp only at hlr ⊢ - rw [← List.zip_of_prod rfl rfl] at hlr - obtain ⟨⟨sourceLiteral, j⟩, hlj, heq⟩ := List.mem_map.mp hlr - have ho : (i, j, sourceLiteral) ∈ Cslib.Logic.PL.occurrences φ := - List.mem_flatMap.mpr ⟨(c, i), hci, List.mem_map.mpr ⟨(sourceLiteral, j), hlj, rfl⟩⟩ - dsimp only [lastLiteral] at heq - obtain ⟨rfl, rfl⟩ := Prod.mk.inj heq - have hlast : (occurrencePath φ (i, j, sourceLiteral)).getLastD (0, 0) = - Layout.center (φ.distinctVars.length + i) := by - rw [List.getLastD_eq_getLast?, (occurrencePath_endpoints ho).2] - rfl - simpa only [hlast] using finalRoute_endpoints sites - ((occurrencePath φ (i, j, sourceLiteral)).getD - ((occurrencePath φ (i, j, sourceLiteral)).length - 2) (0, 0)) - ((occurrencePath φ (i, j, sourceLiteral)).getLastD (0, 0)) - -private theorem crossing_literal_routes_cover : ∀ i : Fin 74, - ((Crossover.splitFormula.getD i.val []).zip - ((Crossover.incidenceRoutes.filter fun e => e.1 == i.val).map fun e => e.2.2)).all - (fun lr => decide ((i.val, lr.1.1, lr.2) ∈ Crossover.incidenceRoutes)) = true := by - decide +kernel - -private theorem crossingClause_endpoints {c : Point} {pc : PlacedClause} - (hpc : pc ∈ crossingClauses c) {l : Literal Variable} {r : Route} - (hlr : (l, r) ∈ pc.1.zip pc.2.2) : - r.head? = some pc.2.1 ∧ r.getLast? = some (variablePosition l.1) := by - obtain ⟨⟨sourceClause, i⟩, hci, rfl⟩ := List.mem_map.mp hpc - have hi : i < 74 := by - simpa only [Nat.zero_add, Crossover.length_splitFormula] using (List.mem_zipIdx hci).2.1 - have hc : sourceClause = Crossover.splitFormula.getD i [] := by - rw [List.getD_eq_getElem _ _ (by simpa only [Crossover.length_splitFormula] using hi)] - simpa only [Nat.sub_zero] using (List.mem_zipIdx hci).2.2 - change (l, r) ∈ - (sourceClause.map (Prod.map (fun v => (c, some v)) id)).zip - ((Crossover.incidenceRoutes.filter fun e => e.1 == i).map - (fun e => translate (cellOrigin 120 c) e.2.2)) at hlr - have hmap : ((Crossover.incidenceRoutes.filter fun e => e.1 == i).map - (fun e => translate (cellOrigin 120 c) e.2.2)) = - ((Crossover.incidenceRoutes.filter fun e => e.1 == i).map fun e => e.2.2).map - (translate (cellOrigin 120 c)) := by rw [List.map_map]; rfl - rw [hmap, List.zip_map] at hlr - obtain ⟨⟨oldLiteral, oldRoute⟩, hold, heq⟩ := List.mem_map.mp hlr - rw [hc] at hold - have he : (i, oldLiteral.1, oldRoute) ∈ Crossover.incidenceRoutes := - of_decide_eq_true (List.all_eq_true.mp (crossing_literal_routes_cover ⟨i, hi⟩) _ hold) - change (((c, some oldLiteral.1), oldLiteral.2), - translate (cellOrigin 120 c) oldRoute) = (l, r) at heq - obtain ⟨rfl, rfl⟩ := Prod.mk.inj heq - have hend := Crossover.incidence_endpoints _ he - constructor - · simp only [translate, List.head?_map, hend.2.1, Option.map_some] - congr 1 - exact add_comm _ _ - · simp only [translate, List.getLast?_map, hend.2.2, Option.map_some, - variablePosition, Option.elim_some] - congr 1 - exact add_comm _ _ - -/-- Every literal/route pair in every actual placed clause has the declared endpoints. -The statement retains literal order, including all original repeated literal occurrences. -/ -theorem placedClause_endpoints (φ : CNF ℕ) {pc : PlacedClause} (hpc : pc ∈ placedClauses φ) - {l : Literal Variable} {r : Route} (hlr : (l, r) ∈ pc.1.zip pc.2.2) : - r.head? = some pc.2.1 ∧ r.getLast? = some (variablePosition l.1) := by - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨_, _, hpc⟩) | ⟨o, ho, hpc⟩ - · exact originalClause_endpoints hpc hlr - · exact crossingClause_endpoints hpc hlr - · obtain ⟨e, he, rfl⟩ := List.mem_map.mp hpc - have he' : e ∈ (occurrencePath φ o).consecutivePairs := by - rw [consecutivePairs_dropLast] at he - exact (List.dropLast_sublist _).subset he - exact link_endpoints _ _ (occurrencePath_unit ho he') hlr - -private theorem positions_getD_raw_variable (φ : CNF ℕ) {v : Variable} - (hv : v ∈ (rawFormula φ).vars) : - (positions φ).getD ((rawFormula φ).distinctVars.idxOf v) (0, 0) = variablePosition v := by - have hi := List.idxOf_lt_length_of_mem (CNF.mem_distinctVars.mpr hv) - rw [positions, List.getD_append _ _ _ _ (by simpa only [List.length_map] using hi)] - rw [List.getD_eq_getElem _ _ (by simpa only [List.length_map] using hi), List.getElem_map] - congr 1 - exact List.getElem_idxOf hi - -/-- The graph's actual variable vertex index resolves to its emitted structured position. -/ -theorem drawingPosition_raw_variable (φ : CNF ℕ) {v : Variable} - (hv : v ∈ (rawFormula φ).vars) : - Graph.drawingPosition (SAT.incidenceGraph (rawFormula φ)) (positions φ, routes φ) - ((rawFormula φ).distinctVars.idxOf v) = variablePosition v := by - have hi := List.idxOf_lt_length_of_mem (CNF.mem_distinctVars.mpr hv) - change (positions φ).getD ((List.range _).idxOf ((rawFormula φ).distinctVars.idxOf v)) - (0, 0) = _ - rw [idxOf_range_eq (by omega)] - exact positions_getD_raw_variable φ hv - -/-- The graph's actual clause vertex index resolves to the placed clause at that index. -/ -theorem drawingPosition_raw_clause (φ : CNF ℕ) {i : ℕ} (hi : i < (placedClauses φ).length) : - Graph.drawingPosition (SAT.incidenceGraph (rawFormula φ)) (positions φ, routes φ) - ((rawFormula φ).distinctVars.length + i) = ((placedClauses φ)[i]).2.1 := by - change (positions φ).getD ((List.range _).idxOf ((rawFormula φ).distinctVars.length + i)) - (0, 0) = _ - have hlen : (rawFormula φ).length = (placedClauses φ).length := by - simp only [rawFormula, List.length_map] - rw [idxOf_range_eq (by omega), positions, - List.getD_append_right _ _ _ _ (by simp only [List.length_map]; omega)] - simp only [List.length_map, Nat.add_sub_cancel_left] - rw [List.getD_eq_getElem _ _ (by simpa only [List.length_map] using hi), List.getElem_map] - -private theorem forall₂_flatMap_same {A B C : Type*} {R : B → C → Prop} - (xs : List A) (f : A → List B) (g : A → List C) - (h : ∀ a ∈ xs, List.Forall₂ R (f a) (g a)) : - List.Forall₂ R (xs.flatMap f) (xs.flatMap g) := by - induction xs with - | nil => exact List.Forall₂.nil - | cons a xs ih => - exact List.rel_append (h a List.mem_cons_self) - (ih (fun b hb => h b (List.mem_cons_of_mem _ hb))) - -private theorem map_zipIdx_ignore {A B : Type*} (xs : List A) (f : A → B) : - (xs.zipIdx.map fun a => f a.1) = xs.map f := by - calc - _ = (xs.zipIdx.map Prod.fst).map f := by rw [List.map_map]; rfl - _ = _ := by rw [List.zipIdx_map_fst] - -private theorem raw_edges_eq (φ : CNF ℕ) : - (SAT.incidenceGraph (rawFormula φ)).2 = - (placedClauses φ).zipIdx.flatMap fun pci => pci.1.1.map fun l => - ((rawFormula φ).distinctVars.idxOf l.1, (rawFormula φ).distinctVars.length + pci.2) := by - simp only [SAT.incidenceGraph, Cslib.Logic.PL.occurrences, rawFormula, List.zipIdx_map, - List.flatMap_map, List.map_flatMap, List.map_map, Function.comp_def, - Prod.map_fst, Prod.map_snd, id_eq, List.idxOf, beq_eq_decide] - congr 1 - funext pci - simpa only [rawFormula, List.idxOf, beq_eq_decide] using - map_zipIdx_ignore pci.1.1 (fun l => - ((rawFormula φ).distinctVars.idxOf l.1, (rawFormula φ).distinctVars.length + pci.2)) - -private theorem raw_routes_eq (φ : CNF ℕ) : - routes φ = (placedClauses φ).zipIdx.flatMap (fun pci => pci.1.2.2) := by - calc - _ = ((placedClauses φ).zipIdx.map Prod.fst).flatMap (fun pc => pc.2.2) := by - rw [List.zipIdx_map_fst] - rfl - _ = _ := by rw [List.flatMap_map] - -private theorem raw_routes_endpoints (φ : CNF ℕ) : - List.Forall₂ (fun e r => - r.head? = some (Graph.drawingPosition (SAT.incidenceGraph (rawFormula φ)) - (positions φ, routes φ) e.2) ∧ - r.getLast? = some (Graph.drawingPosition (SAT.incidenceGraph (rawFormula φ)) - (positions φ, routes φ) e.1)) - (SAT.incidenceGraph (rawFormula φ)).2 (routes φ) := by - rw [raw_edges_eq, raw_routes_eq] - apply forall₂_flatMap_same - intro pci hpci - rcases pci with ⟨pc, i⟩ - have hpc := List.fst_mem_of_mem_zipIdx hpci - have hi : i < (placedClauses φ).length := by - simpa only [Nat.zero_add] using (List.mem_zipIdx hpci).2.1 - have hget : pc = (placedClauses φ)[i] := by - simpa only [Nat.sub_zero] using (List.mem_zipIdx hpci).2.2 - apply List.forall₂_map_left_iff.mpr - apply List.forall₂_iff_zip.mpr - refine ⟨(placedClause_route_count φ pc hpc).symm, ?_⟩ - intro l r hlr - have hends := placedClause_endpoints φ hpc hlr - have hvar : l.1 ∈ (rawFormula φ).vars := by - exact CNF.mem_vars.mpr ⟨pc.1, List.mem_map_of_mem hpc, l.2, (List.of_mem_zip hlr).1⟩ - change r.head? = some (Graph.drawingPosition (SAT.incidenceGraph (rawFormula φ)) - (positions φ, routes φ) ((rawFormula φ).distinctVars.length + i)) ∧ - r.getLast? = some (Graph.drawingPosition (SAT.incidenceGraph (rawFormula φ)) - (positions φ, routes φ) ((rawFormula φ).distinctVars.idxOf l.1)) - rw [drawingPosition_raw_clause φ hi, drawingPosition_raw_variable φ hvar, ← hget] - exact hends - -/-- Every actual indexed route has its actual incident graph vertices as endpoints, in -clause-to-variable order. Compaction and repeated edge occurrences preserve that order. -/ -theorem routes_endpoints (φ : CNF ℕ) {i : ℕ} - (hi : i < (SAT.incidenceGraph (formula φ)).2.length) : - let r := (routes φ).getD i [] - r.head? = some (Graph.drawingPosition (SAT.incidenceGraph (formula φ)) - (positions φ, routes φ) (SAT.incidenceGraph (formula φ)).2[i].2) ∧ - r.getLast? = some (Graph.drawingPosition (SAT.incidenceGraph (formula φ)) - (positions φ, routes φ) (SAT.incidenceGraph (formula φ)).2[i].1) := by - simp only [incidenceGraph_formula] at hi ⊢ - have hir : i < (routes φ).length := by - rwa [routes_length, incidenceGraph_formula] - have h := (raw_routes_endpoints φ).get hi hir - simpa only [List.get_eq_getElem, List.getD_eq_getElem _ _ hir] using h - -private theorem access_variable_contact {sites : List Point} {c q : Point} {v : Variable} - (hkind : v.2 = none ↔ v.1 ∉ sites) - (hp : realPoint (variablePosition v) ∈ support (access sites c q)) : - v = signal sites c q := by - have hcell : v.1 = c := cell_eq_of_mem_open_closed (by decide) - (variablePosition_mem_openCell v) (access_support_cell sites c q hp).1 - rcases v with ⟨a, v⟩ - change a = c at hcell - subst a - by_cases hc : c ∈ sites - · cases v with - | none => exact False.elim (hkind.mp rfl hc) - | some v => - simp only [access, hc, ↓reduceIte, variablePosition, Option.elim_some, - realPoint_add, add_comm (realPoint (cellOrigin 120 c))] at hp - have hp' := (mem_support_translate_iff _ _ _).mp hp - have hv : v = Crossover.splitTerminal (side c q) := by - by_contra h - exact Crossover.access_variable_not_mem h hp' - simp [signal, hc, hv] - · have hv := hkind.mpr hc - simp only at hv - subst v - simp [signal, hc] - -private theorem core_variable_contact {sites : List Point} {c : Point} - (hc : c ∈ sites) {e : ℕ × Crossover.SplitVariable × Route} - (he : e ∈ Crossover.incidenceRoutes) {v : Variable} - (hkind : v.2 = none ↔ v.1 ∉ sites) - (hp : realPoint (variablePosition v) ∈ - support (translate (cellOrigin 120 c) e.2.2)) : v = (c, some e.2.1) := by - have hcell : c = v.1 := cell_eq_of_mem_open_closed (by decide) - (crossingRoute_mem_openCell he c hp) - (let h := variablePosition_mem_openCell v - ⟨h.1.le, h.2.1.le, h.2.2.1.le, h.2.2.2.le⟩) - rcases v with ⟨a, v⟩ - change c = a at hcell - subst a - cases v with - | none => exact False.elim (hkind.mp rfl hc) - | some v => - simp only [variablePosition, Option.elim_some, realPoint_add, - add_comm (realPoint (cellOrigin 120 c))] at hp - have hp' := (mem_support_translate_iff _ _ _).mp hp - have hv : v = e.2.1 := by - by_contra h - exact Crossover.variable_not_mem_support he h hp' - exact congrArg (fun v => (c, some v)) hv - -/-- An actual route can meet a displayed variable only at its variable endpoint. -/ -theorem route_variable_contact (φ : CNF ℕ) {r : Route} (hr : r ∈ routes φ) - {v : Variable} (hv : v ∈ (rawFormula φ).vars) - (hp : realPoint (variablePosition v) ∈ support r) : - r.getLast? = some (variablePosition v) := by - obtain ⟨pc, hpc, hr⟩ := List.mem_flatMap.mp hr - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨c, hc, hpc⟩) | ⟨o, ho, hpc⟩ - · obtain ⟨⟨c, i⟩, hci, rfl⟩ := List.mem_map.mp hpc - obtain ⟨lr, hlr, heq⟩ := List.mem_map.mp hr - obtain ⟨⟨l, j⟩, hlj, rfl⟩ := List.mem_map.mp hlr - have ho : (i, j, l) ∈ Cslib.Logic.PL.occurrences φ := - List.mem_flatMap.mpr ⟨(c, i), hci, List.mem_map.mpr ⟨(l, j), hlj, rfl⟩⟩ - dsimp only [lastLiteral] at heq - subst r - rw [support_finalRoute _ (occurrencePath_last_unit ho)] at hp - rcases hp with hp | hp - · have hcell : v.1 = (occurrencePath φ (i, j, l)).getLastD (0, 0) := - cell_eq_of_mem_open_closed (by decide) (variablePosition_mem_openCell v) - (access_support_cell [] _ _ hp).1 - have hend := (occurrencePath_endpoints ho).2 - rw [List.getLastD_eq_getLast?, hend] at hcell - have hi : i < φ.length := by - simpa only [Nat.zero_add] using (List.mem_zipIdx hci).2.1 - exact False.elim (raw_variable_not_clause_cell hv hi hcell) - · have heq := access_variable_contact (raw_variable_cell_kind φ hv) hp - exact heq ▸ (finalRoute_endpoints _ _ _).2 - · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc - obtain ⟨e, he, rfl⟩ := List.mem_map.mp hr - have he' := (List.mem_filter.mp he).1 - have heq := core_variable_contact hc he' (raw_variable_cell_kind φ hv) hp - subst v - simp only [translate, List.getLast?_map, (Crossover.incidence_endpoints _ he').2.2, - Option.map_some, variablePosition, Option.elim_some, add_comm] - · obtain ⟨e, _, rfl⟩ := List.mem_map.mp hpc - cases hpos : o.2.2.2 <;> - simp only [link, hpos, Bool.false_eq_true, ↓reduceIte, List.mem_cons, - List.not_mem_nil, or_false] at hr <;> - rcases hr with rfl | rfl <;> - have heq := access_variable_contact (raw_variable_cell_kind φ hv) hp <;> - rw [heq, access_eq_pair] <;> rfl - -private def lastStep (r : Route) : Point × Point := - (r.getD (r.length - 2) (0, 0), r.getLastD (0, 0)) - -private theorem lastStep_mem {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) : - lastStep (occurrencePath φ o) ∈ (occurrencePath φ o).consecutivePairs := by - let r := occurrencePath φ o - have hlen : 2 ≤ r.length := occurrencePath_length_ge_two ho - have hk : r.length - 2 < r.consecutivePairs.length := by - simp only [List.consecutivePairs, List.length_zip, List.length_tail] - omega - have heq : r.consecutivePairs[r.length - 2] = lastStep r := by - simp only [List.consecutivePairs, List.getElem_zip, List.getElem_tail, lastStep] - rw [List.getD_eq_getElem _ _ (by omega), List.getLastD_eq_getLast?, - List.getLast?_eq_getElem?, List.getElem?_eq_getElem (by omega), Option.getD_some] - congr 1 - congr 1 - omega - rw [← heq] - exact List.getElem_mem hk - -private theorem occurrence_step_unique {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {o t : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) - (ht : t ∈ Cslib.Logic.PL.occurrences φ) {e f : Point × Point} - (he : e ∈ (occurrencePath φ o).consecutivePairs) - (hf : f ∈ (occurrencePath φ t).consecutivePairs) - (h : cellPort 120 e.1 (side e.1 e.2) = cellPort 120 f.1 (side f.1 f.2)) : - o = t ∧ e = f := by - let mids := fun o => (occurrencePath φ o).consecutivePairs.map fun e => - cellPort 120 e.1 (side e.1 e.2) - have hn : ((Cslib.Logic.PL.occurrences φ).flatMap mids).Nodup := by - simpa only [← occurrencePaths_eq_paths φ, List.flatMap_map] using - pathMidpoints_nodup hw hv - have houter := (List.nodup_flatMap.mp hn).2 - have hme : cellPort 120 e.1 (side e.1 e.2) ∈ mids o := List.mem_map_of_mem he - have hmf : cellPort 120 e.1 (side e.1 e.2) ∈ mids t := h ▸ List.mem_map_of_mem hf - have hot : o = t := by - obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp ho - obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp ht - rcases Nat.lt_trichotomy i j with hij | rfl | hji - · exact False.elim ((List.pairwise_iff_getElem.mp houter i j hi hj hij) hme hmf) - · rfl - · exact False.elim ((List.pairwise_iff_getElem.mp houter j i hj hi hji) hmf hme) - refine ⟨hot, ?_⟩ - subst t - have hlocal := (List.nodup_flatMap.mp hn).1 o ho - obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp he - obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp hf - have hi' : i < (mids o).length := by simpa only [mids, List.length_map] using hi - have hj' : j < (mids o).length := by simpa only [mids, List.length_map] using hj - have hij := hlocal.eq_of_getElem_eq hi' hj' (by simpa only [mids, List.getElem_map] using h) - subst j - rfl - -private theorem lastStep_not_prefix {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) : - lastStep (occurrencePath φ o) ∉ (occurrencePath φ o).dropLast.consecutivePairs := by - intro he - have hp : (occurrencePath φ o).getLastD (0, 0) ∈ (occurrencePath φ o).dropLast := - List.mem_of_mem_tail (List.of_mem_zip he).2 - rw [List.getLastD_eq_getLast?, (occurrencePath_endpoints ho).2] at hp - exact clause_cell_not_mem_path_dropLast ho (Cslib.Logic.PL.mem_occurrences.mp ho).1 hp - -private def RouteEnd (r : Route) (a : Point) : Prop := - r.head? = some a ∨ r.getLast? = some a - -private inductive AccessPiece (φ : CNF ℕ) : Route → Point → Point → Prop where - | link {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) {e : Point × Point} - (he : e ∈ (occurrencePath φ o).dropLast.consecutivePairs) : - AccessPiece φ (access (crossingSites φ) e.1 e.2) e.1 e.2 - | reverseLink {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) - {e : Point × Point} (he : e ∈ (occurrencePath φ o).dropLast.consecutivePairs) : - AccessPiece φ (access (crossingSites φ) e.2 e.1) e.2 e.1 - | finalIn {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) : - AccessPiece φ - (center (lastStep (occurrencePath φ o)).2 :: - access (crossingSites φ) (lastStep (occurrencePath φ o)).1 - (lastStep (occurrencePath φ o)).2) - (lastStep (occurrencePath φ o)).1 (lastStep (occurrencePath φ o)).2 - | finalOut {o : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) : - AccessPiece φ - (center (lastStep (occurrencePath φ o)).2 :: - access (crossingSites φ) (lastStep (occurrencePath φ o)).1 - (lastStep (occurrencePath φ o)).2) - (lastStep (occurrencePath φ o)).2 (lastStep (occurrencePath φ o)).1 - -private theorem prefixStep_mem {φ : CNF ℕ} {o : Occurrence ℕ} {e : Point × Point} - (he : e ∈ (occurrencePath φ o).dropLast.consecutivePairs) : - e ∈ (occurrencePath φ o).consecutivePairs := by - rw [consecutivePairs_dropLast] at he - exact (List.dropLast_sublist _).subset he - -private theorem lastStep_target_not_crossing {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) : - (lastStep (occurrencePath φ o)).2 ∉ crossingSites φ := by - change (occurrencePath φ o).getLastD (0, 0) ∉ crossingSites φ - rw [List.getLastD_eq_getLast?, (occurrencePath_endpoints ho).2] - exact clause_cell_not_mem_crossingSites φ (Cslib.Logic.PL.mem_occurrences.mp ho).1 - -private theorem AccessPiece.inner_endpoint {φ : CNF ℕ} {r : Route} {c q : Point} - (h : AccessPiece φ r c q) : RouteEnd r (variablePosition (signal (crossingSites φ) c q)) := by - cases h with - | link ho he => exact Or.inr (by rw [access_eq_pair]; rfl) - | reverseLink ho he => exact Or.inr (by rw [access_eq_pair]; rfl) - | finalIn ho => exact Or.inr (finalRoute_endpoints _ _ _).2 - | finalOut ho => - exact Or.inl (by simp [signal, lastStep_target_not_crossing ho, variablePosition, center]) - -private theorem AccessPiece.source {φ : CNF ℕ} {r : Route} {c q : Point} - (h : AccessPiece φ r c q) : - ∃ o ∈ Cslib.Logic.PL.occurrences φ, ∃ e ∈ (occurrencePath φ o).consecutivePairs, - cellPort 120 c (side c q) = cellPort 120 e.1 (side e.1 e.2) ∧ - ((e ∈ (occurrencePath φ o).dropLast.consecutivePairs ∧ - r = access (crossingSites φ) c q) ∨ - (e = lastStep (occurrencePath φ o) ∧ - r = center e.2 :: access (crossingSites φ) e.1 e.2)) := by - cases h with - | link ho he => exact ⟨_, ho, _, prefixStep_mem he, rfl, Or.inl ⟨he, rfl⟩⟩ - | reverseLink ho he => - exact ⟨_, ho, _, prefixStep_mem he, - (shared_cellPort (occurrencePath_unit ho (prefixStep_mem he))).symm, - Or.inl ⟨he, rfl⟩⟩ - | finalIn ho => exact ⟨_, ho, _, lastStep_mem ho, rfl, Or.inr ⟨rfl, rfl⟩⟩ - | finalOut ho => - exact ⟨_, ho, _, lastStep_mem ho, (shared_cellPort (occurrencePath_last_unit ho)).symm, - Or.inr ⟨rfl, rfl⟩⟩ - -private theorem accessPieces_same_port {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {r s : Route} {c q d t : Point} (hr : AccessPiece φ r c q) (hs : AccessPiece φ s d t) - (h : cellPort 120 c (side c q) = cellPort 120 d (side d t)) : - (r = access (crossingSites φ) c q ∧ s = access (crossingSites φ) d t) ∨ r = s := by - obtain ⟨o, ho, e, he, hport, hr⟩ := hr.source - obtain ⟨u, hu, f, hf, hport', hs⟩ := hs.source - obtain ⟨rfl, rfl⟩ := occurrence_step_unique hw hv ho hu he hf - (hport.symm.trans (h.trans hport')) - rcases hr with ⟨hprefix, hr⟩ | ⟨hfinal, hr⟩ <;> - rcases hs with ⟨hprefix', hs⟩ | ⟨hfinal', hs⟩ - · exact Or.inl ⟨hr, hs⟩ - · exact False.elim (lastStep_not_prefix ho (hfinal' ▸ hprefix)) - · exact False.elim (lastStep_not_prefix ho (hfinal ▸ hprefix')) - · exact Or.inr (hr.trans hs.symm) - -private theorem route_support_cases {φ : CNF ℕ} {r : Route} (hr : r ∈ routes φ) - {p : ℝ × ℝ} (hp : p ∈ support r) : - (∃ c ∈ crossingSites φ, ∃ e ∈ Crossover.incidenceRoutes, - r = translate (cellOrigin 120 c) e.2.2) ∨ - ∃ c q, AccessPiece φ r c q ∧ p ∈ support (access (crossingSites φ) c q) := by - obtain ⟨pc, hpc, hr⟩ := List.mem_flatMap.mp hr - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨c, hc, hpc⟩) | ⟨o, ho, hpc⟩ - · obtain ⟨ci, hci, rfl⟩ := List.mem_map.mp hpc - obtain ⟨lr, hlr, heq⟩ := List.mem_map.mp hr - obtain ⟨lj, hlj, rfl⟩ := List.mem_map.mp hlr - have ho : (ci.2, lj.2, lj.1) ∈ Cslib.Logic.PL.occurrences φ := - List.mem_flatMap.mpr ⟨ci, hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩ - dsimp only [lastLiteral] at heq - subst r - rw [support_finalRoute _ (occurrencePath_last_unit ho)] at hp - rcases hp with hp | hp - · have heq : access [] (lastStep (occurrencePath φ (ci.2, lj.2, lj.1))).2 - (lastStep (occurrencePath φ (ci.2, lj.2, lj.1))).1 = - access (crossingSites φ) (lastStep (occurrencePath φ (ci.2, lj.2, lj.1))).2 - (lastStep (occurrencePath φ (ci.2, lj.2, lj.1))).1 := by - simp [access, lastStep_target_not_crossing ho] - exact Or.inr ⟨_, _, AccessPiece.finalOut ho, heq ▸ hp⟩ - · exact Or.inr ⟨_, _, AccessPiece.finalIn ho, hp⟩ - · obtain ⟨ci, _, rfl⟩ := List.mem_map.mp hpc - obtain ⟨e, he, rfl⟩ := List.mem_map.mp hr - exact Or.inl ⟨c, hc, e, (List.mem_filter.mp he).1, rfl⟩ - · obtain ⟨e, he, rfl⟩ := List.mem_map.mp hpc - cases hpos : o.2.2.2 <;> - simp only [link, hpos, Bool.false_eq_true, ↓reduceIte, List.mem_cons, - List.not_mem_nil, or_false] at hr <;> rcases hr with rfl | rfl - all_goals first - | exact Or.inr ⟨_, _, AccessPiece.link ho he, hp⟩ - | exact Or.inr ⟨_, _, AccessPiece.reverseLink ho he, hp⟩ - -private theorem accessPieces_contact {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {r s : Route} {c q d t : Point} (hr : AccessPiece φ r c q) (hs : AccessPiece φ s d t) - (hne : r ≠ s) {p : ℝ × ℝ} - (hp : p ∈ support (access (crossingSites φ) c q)) - (hq : p ∈ support (access (crossingSites φ) d t)) : - ∃ a : Point, p = realPoint a ∧ RouteEnd r a ∧ RouteEnd s a := by - by_cases hcd : c = d - · subst d - by_cases hside : side c q = side c t - · have hport : cellPort 120 c (side c q) = cellPort 120 c (side c t) := congrArg _ hside - rcases accessPieces_same_port hw hv hr hs hport with ⟨hr', hs'⟩ | heq - · apply False.elim - apply hne - rw [hr', hs', access_eq_pair, access_eq_pair] - simp only [signal, hside] - · exact False.elim (hne heq) - · by_cases hc : c ∈ crossingSites φ - · exact False.elim (Set.disjoint_left.mp (crossing_access_disjoint hc q t hside) hp hq) - · have hp' := ordinary_access_contact hc q t hside hp hq - refine ⟨center c, hp', ?_, ?_⟩ - · simpa only [signal, hc, ↓reduceIte, variablePosition, Option.elim_none, center] using - hr.inner_endpoint - · simpa only [signal, hc, ↓reduceIte, variablePosition, Option.elim_none, center] using - hs.inner_endpoint - · have hcontact := access_contact_of_distinct_cells (crossingSites φ) (crossingSites φ) - hcd q t hp hq - have hport := realPoint_injective (hcontact.1.symm.trans hcontact.2) - rcases accessPieces_same_port hw hv hr hs hport with ⟨hr', hs'⟩ | heq - · refine ⟨cellPort 120 c (side c q), hcontact.1, Or.inl ?_, Or.inl ?_⟩ - · rw [hr', access_eq_pair]; rfl - · rw [hs', access_eq_pair, ← hport]; rfl - · exact False.elim (hne heq) - -private theorem RouteEnd.translate {r : Route} {a : Point} (h : RouteEnd r a) (v : Point) : - RouteEnd (translate v r) (a + v) := by - rcases h with h | h - · exact Or.inl (by simp only [Orthogonal.translate, List.head?_map, h, Option.map_some]) - · exact Or.inr (by simp only [Orthogonal.translate, List.getLast?_map, h, Option.map_some]) - -private theorem core_local_contact {e f : ℕ × Crossover.SplitVariable × Route} - (he : e ∈ Crossover.incidenceRoutes) (hf : f ∈ Crossover.incidenceRoutes) (hne : e ≠ f) - {p : ℝ × ℝ} (hp : p ∈ support e.2.2) (hq : p ∈ support f.2.2) : - ∃ a : Point, p = realPoint a ∧ RouteEnd e.2.2 a ∧ RouteEnd f.2.2 a := by - obtain ⟨a, ha, hpa⟩ := Crossover.routes_contact he hf hne hp hq - refine ⟨a, hpa, ?_⟩ - simp only [Crossover.commonEndpoints, List.mem_append] at ha - rcases ha with ha | ha - · split_ifs at ha with hclause - · obtain rfl := List.mem_singleton.mp ha - exact ⟨Or.inl (Crossover.incidence_endpoints _ he).2.1, - Or.inl (by simpa only [hclause] using (Crossover.incidence_endpoints _ hf).2.1)⟩ - · exact False.elim (List.not_mem_nil ha) - · split_ifs at ha with hvar - · obtain rfl := List.mem_singleton.mp ha - exact ⟨Or.inr (Crossover.incidence_endpoints _ he).2.2, - Or.inr (by simpa only [hvar] using (Crossover.incidence_endpoints _ hf).2.2)⟩ - · exact False.elim (List.not_mem_nil ha) - -private theorem core_core_contact {c d : Point} {e f : ℕ × Crossover.SplitVariable × Route} - (he : e ∈ Crossover.incidenceRoutes) (hf : f ∈ Crossover.incidenceRoutes) - (hne : translate (cellOrigin 120 c) e.2.2 ≠ translate (cellOrigin 120 d) f.2.2) - {p : ℝ × ℝ} (hp : p ∈ support (translate (cellOrigin 120 c) e.2.2)) - (hq : p ∈ support (translate (cellOrigin 120 d) f.2.2)) : - ∃ a : Point, p = realPoint a ∧ RouteEnd (translate (cellOrigin 120 c) e.2.2) a ∧ - RouteEnd (translate (cellOrigin 120 d) f.2.2) a := by - have hpc := crossingRoute_mem_openCell he c hp - have hqc := crossingRoute_mem_openCell hf d hq - have hcd : c = d := cell_eq_of_mem_open_closed (by decide) hpc - ⟨hqc.1.le, hqc.2.1.le, hqc.2.2.1.le, hqc.2.2.2.le⟩ - subst d - have hef : e ≠ f := fun h => hne (h ▸ rfl) - let x := p - realPoint (cellOrigin 120 c) - have hx : x + realPoint (cellOrigin 120 c) = p := sub_add_cancel _ _ - have hp' : x ∈ support e.2.2 := - (mem_support_translate_iff _ _ _).mp (hx ▸ hp) - have hq' : x ∈ support f.2.2 := - (mem_support_translate_iff _ _ _).mp (hx ▸ hq) - obtain ⟨a, hxa, ha, hb⟩ := core_local_contact he hf hef hp' hq' - refine ⟨a + cellOrigin 120 c, ?_, ha.translate _, hb.translate _⟩ - rw [realPoint_add, ← hxa, hx] - -private theorem core_access_contact {φ : CNF ℕ} {r : Route} {c d q : Point} - (hc : c ∈ crossingSites φ) {e : ℕ × Crossover.SplitVariable × Route} - (he : e ∈ Crossover.incidenceRoutes) (hr : AccessPiece φ r d q) - {p : ℝ × ℝ} (hp : p ∈ support (translate (cellOrigin 120 c) e.2.2)) - (hq : p ∈ support (access (crossingSites φ) d q)) : - ∃ a : Point, p = realPoint a ∧ RouteEnd (translate (cellOrigin 120 c) e.2.2) a ∧ - RouteEnd r a := by - have hcd : c = d := cell_eq_of_mem_open_closed (by decide) - (crossingRoute_mem_openCell he c hp) (access_support_cell _ _ _ hq).1 - subst d - let x := p - realPoint (cellOrigin 120 c) - have hx : x + realPoint (cellOrigin 120 c) = p := sub_add_cancel _ _ - have hp' : x ∈ support e.2.2 := - (mem_support_translate_iff _ _ _).mp (hx ▸ hp) - have hq' : x ∈ support (Crossover.accessRoute (side c q)) := by - apply (mem_support_translate_iff (cellOrigin 120 c) _ _).mp - simpa only [access, hc, ↓reduceIte, hx] using hq - obtain ⟨hevar, hxp⟩ := Crossover.access_contact he hq' hp' - refine ⟨variablePosition (signal (crossingSites φ) c q), ?_, ?_, hr.inner_endpoint⟩ - · simp only [signal, hc, ↓reduceIte, variablePosition, Option.elim_some, realPoint_add] - rw [← hxp, add_comm, hx] - · have hend : RouteEnd e.2.2 (Crossover.variablePosition (Crossover.splitTerminal (side c q))) := - Or.inr (by simpa only [hevar] using (Crossover.incidence_endpoints _ he).2.2) - simpa only [signal, hc, ↓reduceIte, variablePosition, Option.elim_some, add_comm] using - hend.translate (cellOrigin 120 c) - -/-- Distinct actual routes meet only at endpoints of both routes, over the complete real plane. -The proof uses actual unit-step ownership, including the omitted final binary link. -/ -theorem route_contacts {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {r s : Route} (hr : r ∈ routes φ) (hs : s ∈ routes φ) (hne : r ≠ s) - {p : ℝ × ℝ} (hp : p ∈ support r) (hq : p ∈ support s) : - ∃ a : Point, p = realPoint a ∧ - (r.head? = some a ∨ r.getLast? = some a) ∧ - (s.head? = some a ∨ s.getLast? = some a) := by - rcases route_support_cases hr hp with ⟨c, hc, e, he, rfl⟩ | ⟨c, q, hr', hp'⟩ - · rcases route_support_cases hs hq with ⟨d, _, f, hf, rfl⟩ | ⟨d, t, hs', hq'⟩ - · exact core_core_contact he hf hne hp hq - · exact core_access_contact hc he hs' hp hq' - · rcases route_support_cases hs hq with ⟨d, hd, f, hf, rfl⟩ | ⟨d, t, hs', hq'⟩ - · obtain ⟨a, hpa, hfend, hrend⟩ := core_access_contact hd hf hr' hq hp' - exact ⟨a, hpa, hrend, hfend⟩ - · exact accessPieces_contact hw hv hr' hs' hne hp' hq' - -private theorem lastLiteral_route_injective {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {o t : Occurrence ℕ} (ho : o ∈ Cslib.Logic.PL.occurrences φ) - (ht : t ∈ Cslib.Logic.PL.occurrences φ) {b b' : Bool} - (h : (lastLiteral (crossingSites φ) (occurrencePath φ o) b).2 = - (lastLiteral (crossingSites φ) (occurrencePath φ t) b').2) : o = t := by - have hmid := congrArg (fun r : Route => r.getD 1 (0, 0)) h - simp only [lastLiteral, access_eq_pair, List.getD_cons_succ, - List.getD_cons_zero] at hmid - exact (occurrence_step_unique hw hv ho ht (lastStep_mem ho) (lastStep_mem ht) hmid).1 - -private theorem originalClause_routes_nodup_at {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {c : Clause ℕ} {i : ℕ} (hci : (c, i) ∈ φ.zipIdx) : - ((c.zipIdx.map fun lj => - lastLiteral (crossingSites φ) (occurrencePath φ (i, lj.2, lj.1)) lj.1.2).map - Prod.snd).Nodup := by - rw [List.map_map] - have hn : c.zipIdx.Nodup := by - apply List.Nodup.of_map Prod.snd - rw [List.zipIdx_map_snd] - exact List.nodup_range' _ - apply hn.map_on - intro lj hlj mk hmk heq - have ho : (i, lj.2, lj.1) ∈ Cslib.Logic.PL.occurrences φ := - List.mem_flatMap.mpr ⟨(c, i), hci, List.mem_map.mpr ⟨lj, hlj, rfl⟩⟩ - have ht : (i, mk.2, mk.1) ∈ Cslib.Logic.PL.occurrences φ := - List.mem_flatMap.mpr ⟨(c, i), hci, List.mem_map.mpr ⟨mk, hmk, rfl⟩⟩ - have hot := lastLiteral_route_injective hw hv ho ht (b := lj.1.2) (b' := mk.1.2) heq - have hjl := Prod.mk.inj (Prod.mk.inj hot).2 - exact Prod.ext hjl.2 hjl.1 - -private theorem originalClause_routes_nodup {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {pc : PlacedClause} (hpc : pc ∈ originalClauses φ (crossingSites φ)) : pc.2.2.Nodup := by - obtain ⟨⟨c, i⟩, hci, rfl⟩ := List.mem_map.mp hpc - exact originalClause_routes_nodup_at hw hv hci - -private theorem crossing_routes_nodup_check : ∀ i : Fin 74, - ((Crossover.incidenceRoutes.filter fun e => e.1 == i.val).map fun e => e.2.2).Nodup := by - decide +kernel - -private theorem crossingClause_routes_nodup {c : Point} {pc : PlacedClause} - (hpc : pc ∈ crossingClauses c) : pc.2.2.Nodup := by - obtain ⟨⟨sourceClause, i⟩, hci, rfl⟩ := List.mem_map.mp hpc - have hi : i < 74 := by - simpa only [Nat.zero_add, Crossover.length_splitFormula] using (List.mem_zipIdx hci).2.1 - change ((Crossover.incidenceRoutes.filter fun e => e.1 == i).map - (fun e => translate (cellOrigin 120 c) e.2.2)).Nodup - have hn := (crossing_routes_nodup_check ⟨i, hi⟩).map - (f := translate (cellOrigin 120 c)) - (fun _ _ h => (List.map_inj_right (fun _ _ h => add_right_cancel h)).mp h) - simpa only [List.map_map, Function.comp_def] using hn - -private theorem access_reverse_ne {sites : List Point} {p q : Point} - (h : Orthogonal.length p q = 1) : access sites p q ≠ access sites q p := by - intro heq - have hvar := congrArg List.getLast? heq - simp only [access_eq_pair, List.getLast?_cons_cons, List.getLast?_singleton, - Option.some.injEq] at hvar - have hp := variablePosition_mem_openCell (signal sites p q) - have hq := variablePosition_mem_openCell (signal sites q p) - rw [← hvar] at hq - have hpq : p = q := cell_eq_of_mem_open_closed (by decide) hp - ⟨hq.1.le, hq.2.1.le, hq.2.2.1.le, hq.2.2.2.le⟩ - subst q - simp [Orthogonal.length] at h - -private theorem placedClause_routes_nodup {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {pc : PlacedClause} (hpc : pc ∈ placedClauses φ) : pc.2.2.Nodup := by - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨_, _, hpc⟩) | ⟨o, ho, hpc⟩ - · exact originalClause_routes_nodup hw hv hpc - · exact crossingClause_routes_nodup hpc - · obtain ⟨e, he, rfl⟩ := List.mem_map.mp hpc - have hne := access_reverse_ne (sites := crossingSites φ) - (occurrencePath_unit ho (prefixStep_mem he)) - cases o.2.2.2 <;> simp [link, hne, Ne.symm hne] - -/-- Distinct incidence occurrences have distinct actual route lists. -/ -theorem routes_nodup {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : (routes φ).Nodup := by - apply List.nodup_flatMap.mpr - refine ⟨fun _ hpc => placedClause_routes_nodup hw hv hpc, ?_⟩ - have hn := clausePositions_nodup hw hv - rw [List.Nodup, List.pairwise_map] at hn - apply hn.imp_of_mem - intro pc pd hpc hpd hpos r hr hs - have hhead (pc : PlacedClause) (hpc : pc ∈ placedClauses φ) (hr : r ∈ pc.2.2) : - r.head? = some pc.2.1 := by - obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hr - have hi' : i < pc.1.length := by rwa [← placedClause_route_count φ pc hpc] - have hzip : (pc.1[i], pc.2.2[i]) ∈ pc.1.zip pc.2.2 := by - have hk : i < (pc.1.zip pc.2.2).length := by simp only [List.length_zip]; omega - simpa only [List.getElem_zip] using (List.getElem_mem hk) - exact (placedClause_endpoints φ hpc hzip).1 - exact hpos (Option.some.inj ((hhead pc hpc hr).symm.trans (hhead pd hpd hs))) - -private theorem route_declared_endpoints (φ : CNF ℕ) {r : Route} (hr : r ∈ routes φ) : - ∃ pc ∈ placedClauses φ, ∃ v ∈ (rawFormula φ).vars, - r.head? = some pc.2.1 ∧ r.getLast? = some (variablePosition v) := by - obtain ⟨pc, hpc, hr⟩ := List.mem_flatMap.mp hr - obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hr - have hi' : i < pc.1.length := by rwa [← placedClause_route_count φ pc hpc] - have hzip : (pc.1[i], pc.2.2[i]) ∈ pc.1.zip pc.2.2 := by - have hk : i < (pc.1.zip pc.2.2).length := by simp only [List.length_zip]; omega - simpa only [List.getElem_zip] using (List.getElem_mem hk) - refine ⟨pc, hpc, (pc.1[i]).1, ?_, placedClause_endpoints φ hpc hzip⟩ - exact CNF.mem_vars.mpr ⟨pc.1, List.mem_map_of_mem hpc, (pc.1[i]).2, - List.getElem_mem hi'⟩ - -private theorem variable_ne_clause {φ : CNF ℕ} {v : Variable} - (hv : v ∈ (rawFormula φ).vars) {pc : PlacedClause} (hpc : pc ∈ placedClauses φ) : - variablePosition v ≠ pc.2.1 := by - intro h - apply variable_clause_positions_disjoint φ - (List.mem_map_of_mem (CNF.mem_distinctVars.mpr hv)) - rw [h] - exact List.mem_map_of_mem hpc - -private theorem routeEnd_clause_is_head {φ : CNF ℕ} {r : Route} (hr : r ∈ routes φ) - {pc : PlacedClause} (hpc : pc ∈ placedClauses φ) (hend : RouteEnd r pc.2.1) : - r.head? = some pc.2.1 := by - rcases hend with h | h - · exact h - · obtain ⟨_, _, v, hv, _, hlast⟩ := route_declared_endpoints φ hr - exact False.elim (variable_ne_clause hv hpc (Option.some.inj (hlast.symm.trans h))) - -private theorem route_originalClause_contact {φ : CNF ℕ} {r : Route} (hr : r ∈ routes φ) - {pc : PlacedClause} (hpc : pc ∈ originalClauses φ (crossingSites φ)) - (hp : realPoint pc.2.1 ∈ support r) : r.head? = some pc.2.1 := by - have hpc' : pc ∈ placedClauses φ := List.mem_append_left _ (List.mem_append_left _ hpc) - apply routeEnd_clause_is_head hr hpc' - obtain ⟨⟨clause, i⟩, hci, rfl⟩ := List.mem_map.mp hpc - have hi : i < φ.length := by - simpa only [Nat.zero_add] using (List.mem_zipIdx hci).2.1 - have hsite := clause_cell_not_mem_crossingSites φ hi - change realPoint (center (Layout.center (φ.distinctVars.length + i))) ∈ support r at hp - change RouteEnd r (center (Layout.center (φ.distinctVars.length + i))) - rcases route_support_cases hr hp with ⟨c, hc, e, he, rfl⟩ | ⟨c, q, hpiece, hp'⟩ - · have hcore := crossingRoute_mem_openCell he c hp - have hcenter := center_mem_openCell (r := 120) (by decide) - (Layout.center (φ.distinctVars.length + i)) - have heq : Layout.center (φ.distinctVars.length + i) = c := - cell_eq_of_mem_open_closed (by decide) hcenter - ⟨hcore.1.le, hcore.2.1.le, hcore.2.2.1.le, hcore.2.2.2.le⟩ - exact False.elim (hsite (heq ▸ hc)) - · have heq := access_variable_contact - (v := (Layout.center (φ.distinctVars.length + i), none)) - (sites := crossingSites φ) (by simp [hsite]) hp' - have hend := hpiece.inner_endpoint - rw [← heq] at hend - simpa only [variablePosition, Option.elim_none, center] using hend - -private theorem splitClause_nonempty : ∀ c ∈ Crossover.splitFormula, c ≠ [] := by - decide +kernel - -private theorem placedClause_nonempty_or_original {φ : CNF ℕ} {pc : PlacedClause} - (hpc : pc ∈ placedClauses φ) : - pc.1 ≠ [] ∨ pc ∈ originalClauses φ (crossingSites φ) := by - simp only [placedClauses, List.mem_append, List.mem_flatMap] at hpc - rcases hpc with (hpc | ⟨_, _, hpc⟩) | ⟨_, _, hpc⟩ - · exact Or.inr hpc - · obtain ⟨⟨c, i⟩, hci, rfl⟩ := List.mem_map.mp hpc - exact Or.inl (by - simpa only [Clause.relabel, ne_eq, List.map_eq_nil_iff] using - splitClause_nonempty c (List.fst_mem_of_mem_zipIdx hci)) - · obtain ⟨e, _, rfl⟩ := List.mem_map.mp hpc - exact Or.inl (by cases ‹Occurrence ℕ›.2.2.2 <;> simp [link]) - -/-- An actual route can meet a displayed clause only at its clause endpoint. -The source bounds are used by the global contact certificate; empty original clauses are -handled separately by their source-center geometry. -/ -theorem route_clause_contact {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {r : Route} (hr : r ∈ routes φ) {pc : PlacedClause} (hpc : pc ∈ placedClauses φ) - (hp : realPoint pc.2.1 ∈ support r) : r.head? = some pc.2.1 := by - rcases placedClause_nonempty_or_original hpc with hne | horg - · have hi : 0 < pc.2.2.length := by - rw [placedClause_route_count φ pc hpc] - exact List.length_pos_iff.mpr hne - have hi' : 0 < pc.1.length := List.length_pos_iff.mpr hne - let s := pc.2.2[0] - have hs : s ∈ routes φ := List.mem_flatMap.mpr ⟨pc, hpc, List.getElem_mem hi⟩ - have hzip : (pc.1[0], s) ∈ pc.1.zip pc.2.2 := by - have hk : 0 < (pc.1.zip pc.2.2).length := by simp only [List.length_zip]; omega - simpa only [List.getElem_zip] using (List.getElem_mem hk) - have hhead := (placedClause_endpoints φ hpc hzip).1 - by_cases hrs : r = s - · exact hrs ▸ hhead - · have hq : realPoint pc.2.1 ∈ support s := - Or.inl ⟨pc.2.1, List.mem_of_head? hhead, rfl⟩ - obtain ⟨a, hpa, hend, _⟩ := route_contacts hw hv hr hs hrs hp hq - have heq := realPoint_injective hpa - exact routeEnd_clause_is_head hr hpc (heq ▸ hend) - · exact route_originalClause_contact hr horg hp - -private theorem drawingPosition_eq_getD {φ : CNF ℕ} {v : ℕ} - (hv : v ∈ (SAT.incidenceGraph (formula φ)).1) : - Graph.drawingPosition (SAT.incidenceGraph (formula φ)) (positions φ, routes φ) v = - (positions φ).getD v (0, 0) := by - simp only [SAT.incidenceGraph, List.mem_range] at hv - simp only [Graph.drawingPosition, SAT.incidenceGraph] - rw [idxOf_range_eq hv] - -private theorem declared_position_index_lt {φ : CNF ℕ} {v : ℕ} - (hv : v ∈ (SAT.incidenceGraph (formula φ)).1) : v < (positions φ).length := by - rw [positions_length] - simpa only [SAT.incidenceGraph, List.mem_range, List.length_range] using hv - -private theorem drawingPosition_mem {φ : CNF ℕ} {v : ℕ} - (hv : v ∈ (SAT.incidenceGraph (formula φ)).1) : - Graph.drawingPosition (SAT.incidenceGraph (formula φ)) (positions φ, routes φ) v ∈ - positions φ := by - rw [drawingPosition_eq_getD hv, List.getD_eq_getElem _ _ (declared_position_index_lt hv)] - exact List.getElem_mem _ - -private theorem drawingPosition_injective {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {a b : ℕ} (ha : a ∈ (SAT.incidenceGraph (formula φ)).1) - (hb : b ∈ (SAT.incidenceGraph (formula φ)).1) - (heq : Graph.drawingPosition (SAT.incidenceGraph (formula φ)) (positions φ, routes φ) a = - Graph.drawingPosition (SAT.incidenceGraph (formula φ)) - (positions φ, routes φ) b) : a = b := by - have hi := declared_position_index_lt ha - have hj := declared_position_index_lt hb - rw [drawingPosition_eq_getD ha, drawingPosition_eq_getD hb, - List.getD_eq_getElem _ _ hi, List.getD_eq_getElem _ _ hj] at heq - exact (positions_nodup hw hv).eq_of_getElem_eq hi hj heq - -private theorem indexed_route_mem {φ : CNF ℕ} {i : ℕ} - (hi : i < (SAT.incidenceGraph (formula φ)).2.length) : - (routes φ).getD i [] ∈ routes φ := by - have hir : i < (routes φ).length := by rwa [routes_length] - rw [List.getD_eq_getElem _ _ hir] - exact List.getElem_mem hir - -/-- Every actual indexed route avoids all nonincident displayed vertices. -/ -theorem routes_avoid_vertices {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {i : ℕ} (hi : i < (SAT.incidenceGraph (formula φ)).2.length) - {v : ℕ} (hvertex : v ∈ (SAT.incidenceGraph (formula φ)).1) - (hp : realPoint (Graph.drawingPosition (SAT.incidenceGraph (formula φ)) - (positions φ, routes φ) v) ∈ support ((routes φ).getD i [])) : - v = (SAT.incidenceGraph (formula φ)).2[i].1 ∨ - v = (SAT.incidenceGraph (formula φ)).2[i].2 := by - have hend := routes_endpoints φ hi - have hdecl := SAT.incidenceGraph_endpoints (List.getElem_mem hi) - have hmem := drawingPosition_mem hvertex - change Graph.drawingPosition (SAT.incidenceGraph (formula φ)) (positions φ, routes φ) v ∈ - (rawFormula φ).distinctVars.map variablePosition ++ - (placedClauses φ).map (fun pc => pc.2.1) at hmem - simp only [List.mem_append, List.mem_map] at hmem - rcases hmem with ⟨w, hwmem, heq⟩ | ⟨pc, hpc, heq⟩ - · rw [← heq] at hp - have hlast := route_variable_contact φ (indexed_route_mem hi) - (CNF.mem_distinctVars.mp hwmem) hp - apply Or.inl - apply drawingPosition_injective hw hv hvertex hdecl.1 - exact heq.symm.trans (Option.some.inj (hlast.symm.trans hend.2)) - · rw [← heq] at hp - have hhead := route_clause_contact hw hv (indexed_route_mem hi) hpc hp - apply Or.inr - apply drawingPosition_injective hw hv hvertex hdecl.2 - exact heq.symm.trans (Option.some.inj (hhead.symm.trans hend.1)) - -private theorem indexed_endpoint_declared {φ : CNF ℕ} {i : ℕ} - (hi : i < (SAT.incidenceGraph (formula φ)).2.length) {a : Point} - (ha : RouteEnd ((routes φ).getD i []) a) : - ∃ v ∈ (SAT.incidenceGraph (formula φ)).1, - (v = (SAT.incidenceGraph (formula φ)).2[i].1 ∨ - v = (SAT.incidenceGraph (formula φ)).2[i].2) ∧ - a = Graph.drawingPosition (SAT.incidenceGraph (formula φ)) (positions φ, routes φ) v := by - have hend := routes_endpoints φ hi - have hdecl := SAT.incidenceGraph_endpoints (List.getElem_mem hi) - rcases ha with ha | ha - · exact ⟨_, hdecl.2, Or.inr rfl, Option.some.inj (ha.symm.trans hend.1)⟩ - · exact ⟨_, hdecl.1, Or.inl rfl, Option.some.inj (ha.symm.trans hend.2)⟩ - -/-- Contacts between distinct incidence indices are exactly at common displayed graph vertices. -/ -theorem routes_contacts {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - {i : ℕ} (hi : i < (SAT.incidenceGraph (formula φ)).2.length) - {j : ℕ} (hj : j < (SAT.incidenceGraph (formula φ)).2.length) (hij : i ≠ j) - {p : ℝ × ℝ} (hp : p ∈ support ((routes φ).getD i [])) - (hq : p ∈ support ((routes φ).getD j [])) : - ∃ v ∈ (SAT.incidenceGraph (formula φ)).1, - (v = (SAT.incidenceGraph (formula φ)).2[i].1 ∨ - v = (SAT.incidenceGraph (formula φ)).2[i].2) ∧ - (v = (SAT.incidenceGraph (formula φ)).2[j].1 ∨ - v = (SAT.incidenceGraph (formula φ)).2[j].2) ∧ - p = realPoint (Graph.drawingPosition (SAT.incidenceGraph (formula φ)) - (positions φ, routes φ) v) := by - have hir : i < (routes φ).length := by rwa [routes_length] - have hjr : j < (routes φ).length := by rwa [routes_length] - have hne : (routes φ).getD i [] ≠ (routes φ).getD j [] := by - rw [List.getD_eq_getElem _ _ hir, List.getD_eq_getElem _ _ hjr] - exact fun h => hij ((routes_nodup hw hv).eq_of_getElem_eq hir hjr h) - obtain ⟨a, hpa, ha, hb⟩ := route_contacts hw hv - (indexed_route_mem hi) (indexed_route_mem hj) hne hp hq - obtain ⟨v, hv', hvi, hav⟩ := indexed_endpoint_declared hi ha - obtain ⟨w, hw', hwj, haw⟩ := indexed_endpoint_declared hj hb - have heq : v = w := drawingPosition_injective hw hv hv' hw' (hav.symm.trans haw) - exact ⟨v, hv', hvi, heq ▸ hwj, hpa.trans (congrArg realPoint hav)⟩ - -/-- The executable planar SAT compiler supplies an actual planar orthogonal drawing. -Only the source clause-width and literal-occurrence bounds are assumed. Every contact, -avoidance and simplicity assertion uses full real segment support. -/ -theorem isPlanarOrthogonalDrawing {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : - Graph.IsPlanarOrthogonalDrawing (SAT.incidenceGraph (formula φ)) - (positions φ, routes φ) where - vertexCount := positions_length φ - edgeCount := routes_length φ - labelsNodup := List.nodup_range - positionsNodup := positions_nodup hw hv - endpointsDeclared := fun _ => SAT.incidenceGraph_endpoints - loopless := fun _ => SAT.incidenceGraph_loopless - endpoints := fun _ hi => Or.inr (routes_endpoints φ hi) - orthogonal := fun _ hi => (routes_regular φ _ (indexed_route_mem hi)).1 - simple := fun _ hi => (routes_regular φ _ (indexed_route_mem hi)).2 - avoidsVertices := fun _ hi _ hvertex => routes_avoid_vertices hw hv hi hvertex - contacts := fun _ hi _ hj hij _ hp hq => routes_contacts hw hv hi hj hij hp hq - -end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Occurrence.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Occurrence.lean deleted file mode 100644 index a24066603..000000000 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Occurrence.lean +++ /dev/null @@ -1,531 +0,0 @@ -/- -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.PathGeometry -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths.Occupancy -public import Complexity.Computability.Complexity.Problems.SAT.Incidence.Degree -public import Complexity.Logics.Propositional.CNF.Compact.Relabel -import Mathlib.Algebra.BigOperators.Ring.List -import Mathlib.Data.List.GetD - -/-! -# Literal occurrences in the actual planarization output - -All bounds count literal positions, including repetitions within one clause. External incidences -are compared with the directed halves of the actual canonical unit paths. The final clause-cell -half is permitted in this comparison, so the comparison only overcounts the emitted variables. -The existing `CNF.vars` counts literal positions; `ClauseSet.occurrences` counts mentioning clauses -and does not suffice when a source clause repeats a variable. - -## Main definitions - -* `Cslib.Complexity.SAT.PlanarCompile.pathHalfEdges`: both directed halves of each unit step. -* `Cslib.Complexity.SAT.PlanarCompile.pathSignals`: signal names presented by these halves. - -## Main results - -* `Cslib.Complexity.SAT.PlanarCompile.count_vars_rawFormula_le_three`, - `.count_vars_formula_le_three`: the actual structured and compact outputs preserve the bound - of three literal occurrences under the source width and literal-count bounds. -* `Cslib.Complexity.SAT.PlanarCompile.count_links_lastLiteral_le`: every emitted external literal - is bounded by the corresponding actual path halves. - -## References - -This literal-position accounting is original and uses the imported fixed crossover template. --/ - -@[expose] public section - -namespace Cslib.Complexity.SAT.PlanarCompile - -open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal - -/-- Both directed cell halves of every consecutive step, in path order. -/ -def pathHalfEdges (r : Route) : List (Point × Point) := - r.consecutivePairs.flatMap fun e => [e, e.swap] - -/-- The actual signal presented by every directed cell half of a path. -/ -def pathSignals (sites : List Point) (r : Route) : List Variable := - (pathHalfEdges r).map fun e => signal sites e.1 e.2 - -private theorem pathSignals_cons_cons (sites : List Point) (a b : Point) (r : Route) : - pathSignals sites (a :: b :: r) = - [signal sites a b, signal sites b a] ++ pathSignals sites (b :: r) := rfl - -private theorem links_cons_cons_cons (sites : List Point) (positive : Bool) - (a b c : Point) (r : Route) : - links sites positive (a :: b :: c :: r) = - link sites positive a b :: links sites positive (b :: c :: r) := rfl - -private theorem lastLiteral_cons_cons_cons (sites : List Point) (positive : Bool) - (a b c : Point) (r : Route) : - lastLiteral sites (a :: b :: c :: r) positive = - lastLiteral sites (b :: c :: r) positive := by - simp [lastLiteral] - -private theorem count_link (sites : List Point) (positive : Bool) (a b : Point) (v : Variable) : - ((link sites positive a b).1.map Prod.fst).count v = - ([signal sites a b, signal sites b a]).count v := by - cases positive <;> simp [link, List.count_cons, Nat.add_comm] - -/-- Links and the final original literal use only the corresponding actual path halves. -The unused reverse half at the original clause center is intentionally retained on the right. -/ -theorem count_links_lastLiteral_le (sites : List Point) (positive : Bool) (r : Route) - (hlen : 2 ≤ r.length) (v : Variable) : - (CNF.vars ((links sites positive r).map Prod.fst)).count v + - [(lastLiteral sites r positive).1.1].count v ≤ (pathSignals sites r).count v := by - induction r with - | nil => simp at hlen - | cons a r ih => - cases r with - | nil => simp at hlen - | cons b r => - cases r with - | nil => - simp [links, lastLiteral, pathSignals, pathHalfEdges, List.consecutivePairs, - CNF.vars, List.count_cons] - | cons c r => - have ht := ih (by simp : 2 ≤ (b :: c :: r).length) - rw [links_cons_cons_cons, List.map_cons, CNF.vars, List.flatten_cons, - List.map_append, List.count_append, lastLiteral_cons_cons_cons, - pathSignals_cons_cons, List.count_append] - change ((link sites positive a b).1.map Prod.fst).count v + - (CNF.vars ((links sites positive (b :: c :: r)).map Prod.fst)).count v + - [(lastLiteral sites (b :: c :: r) positive).1.1].count v ≤ _ - rw [count_link] - omega - -private theorem signal_eq_none_iff (sites : List Point) (a b p : Point) : - signal sites a b = (p, none) ↔ a = p ∧ p ∉ sites := by - by_cases h : a = p - · subst a - simp [signal] - · simp [signal, Prod.mk.injEq, h] - -private theorem signal_beq_none (sites : List Point) (a b p : Point) (hp : p ∉ sites) : - (signal sites a b == (p, none)) = (a == p) := by - apply Bool.eq_iff_iff.mpr - simp only [beq_iff_eq, signal_eq_none_iff, hp, not_false_eq_true, and_true] - -/-- Ordinary-cell path occurrences are exactly its incoming and outgoing adjacency positions. -/ -theorem count_pathSignals_none (sites : List Point) (r : Route) (p : Point) (hp : p ∉ sites) : - (pathSignals sites r).count (p, none) = r.dropLast.count p + r.tail.count p := by - induction r with - | nil => rfl - | cons a r ih => - cases r with - | nil => simp [pathSignals, pathHalfEdges, List.consecutivePairs] - | cons b r => - rw [pathSignals_cons_cons, List.count_append] - simp only [List.count_cons, List.count_nil, Nat.zero_add, signal_beq_none sites _ _ p hp, - List.dropLast_cons_cons, List.tail_cons] at * - omega - -/-- A simple path contributes at most two literal halves at one ordinary cell. -/ -theorem count_pathSignals_none_le_two (sites : List Point) (r : Route) (p : Point) - (hp : p ∉ sites) (hn : r.Nodup) : (pathSignals sites r).count (p, none) ≤ 2 := by - rw [count_pathSignals_none sites r p hp] - have hd := List.nodup_iff_count_le_one.mp (hn.sublist (List.dropLast_sublist _)) p - have ht := List.nodup_iff_count_le_one.mp hn.tail p - omega - -private theorem pathSignals_cell_mem {sites : List Point} {r : Route} {v : Variable} - (hv : v ∈ pathSignals sites r) : v.1 ∈ r := by - obtain ⟨e, he, rfl⟩ := List.mem_map.mp hv - obtain ⟨f, hf, he⟩ := List.mem_flatMap.mp he - have hm := List.of_mem_zip hf - simp only [List.mem_cons, List.not_mem_nil, or_false] at he - rcases he with rfl | rfl - · exact hm.1 - · exact List.mem_of_mem_tail hm.2 - -private theorem count_pathSignals_eq_zero_of_not_mem {sites : List Point} {r : Route} - {p : Point} (hp : p ∉ r) (v : Option Crossover.SplitVariable) : - (pathSignals sites r).count (p, v) = 0 := by - rw [List.count_eq_zero] - exact fun h => hp (pathSignals_cell_mem h) - -private theorem count_pathSignals_none_of_site {sites : List Point} {r : Route} - {p : Point} (hp : p ∈ sites) : (pathSignals sites r).count (p, none) = 0 := by - rw [List.count_eq_zero] - intro hm - obtain ⟨e, _, he⟩ := List.mem_map.mp hm - exact (signal_eq_none_iff sites e.1 e.2 p).mp he |>.2 hp - -private theorem count_pathSignals_none_head {sites : List Point} {r : Route} {p : Point} - (hp : p ∉ sites) (hn : r.Nodup) (hh : r.head? = some p) : - (pathSignals sites r).count (p, none) ≤ 1 := by - obtain ⟨tail, rfl⟩ := List.head?_eq_some_iff.mp hh - rw [count_pathSignals_none _ _ _ hp] - have ht : tail.count p = 0 := List.count_eq_zero.mpr (List.nodup_cons.mp hn).1 - have hd := List.nodup_iff_count_le_one.mp - (hn.sublist (List.dropLast_sublist _)) p - simp only [List.tail_cons, ht, Nat.add_zero] - exact hd - -private theorem count_pathSignals_none_last {sites : List Point} {r : Route} {p : Point} - (hp : p ∉ sites) (hn : r.Nodup) (hh : r.getLast? = some p) : - (pathSignals sites r).count (p, none) ≤ 1 := by - obtain ⟨initial, rfl⟩ := List.getLast?_eq_some_iff.mp hh - rw [count_pathSignals_none _ _ _ hp] - have hm : p ∉ initial := by - have hdis := (List.nodup_append.mp hn).2.2 - exact fun h => hdis p h p (by simp) rfl - have hd : (initial ++ [p]).dropLast.count p = 0 := by simp [List.count_eq_zero.mpr hm] - rw [hd, Nat.zero_add] - exact List.nodup_iff_count_le_one.mp hn.tail p - -private theorem vars_originalClauses (φ : CNF ℕ) (sites : List Point) : - CNF.vars ((originalClauses φ sites).map Prod.fst) = - (Cslib.Logic.PL.occurrences φ).map - (fun o => (lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1) := by - simp [originalClauses, Cslib.Logic.PL.occurrences, CNF.vars, List.map_flatten, - List.map_map, Function.comp_def, List.flatMap_def] - -private theorem vars_crossingClauses (p : Point) : - CNF.vars ((crossingClauses p).map Prod.fst) = - Crossover.splitFormula.vars.map (fun v => (p, some v)) := by - have h : (crossingClauses p).map Prod.fst = - Crossover.splitFormula.relabel (fun v => (p, some v)) := by - simpa only [crossingClauses, CNF.relabel, List.map_map, Function.comp_def] using - congrArg (List.map (fun c : Clause Crossover.SplitVariable => - c.relabel (fun v => (p, some v)))) - (List.zipIdx_map_fst (l := Crossover.splitFormula) 0) - rw [h, CNF.vars_relabel] - -private theorem count_vars_append (φ ψ : CNF Variable) (v : Variable) : - (φ ++ ψ).vars.count v = φ.vars.count v + ψ.vars.count v := by - simp [CNF.vars] - -private theorem count_external_blocks_le {φ : CNF ℕ} (sites : List Point) (os : List (Occurrence ℕ)) - (hpaths : ∀ o ∈ os, 2 ≤ (occurrencePath φ o).length) (v : Variable) : - (CNF.vars ((os.flatMap fun o => links sites o.2.2.2 (occurrencePath φ o)).map - Prod.fst)).count v + - (os.map (fun o => (lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1)).count v ≤ - (os.flatMap fun o => pathSignals sites (occurrencePath φ o)).count v := by - induction os with - | nil => simp [CNF.vars] - | cons o os ih => - have ht := ih (fun a ha => hpaths a (List.mem_cons_of_mem _ ha)) - have ho := count_links_lastLiteral_le sites o.2.2.2 (occurrencePath φ o) - (hpaths o List.mem_cons_self) v - rw [List.flatMap_cons, List.map_append, count_vars_append, List.map_cons, - List.count_cons, List.flatMap_cons, List.count_append] - have hc : [(lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1].count v = - if (lastLiteral sites (occurrencePath φ o) o.2.2.2).1.1 == v then 1 else 0 := by - simp [List.count_cons] - rw [hc] at ho - omega - -/-- Internal variable names supplied by all selected translated crossover templates. -/ -def crossingSignals (φ : CNF ℕ) : List Variable := - (crossingSites φ).flatMap fun p => Crossover.splitFormula.vars.map (fun v => (p, some v)) - -/-- Both directed halves of every actual source incidence path. -/ -def allPathSignals (φ : CNF ℕ) : List Variable := - (Cslib.Logic.PL.occurrences φ).flatMap fun o => - pathSignals (crossingSites φ) (occurrencePath φ o) - -/-- The path-half enumeration also follows the actual compiler path-list order. -/ -theorem allPathSignals_eq_flatMap (φ : CNF ℕ) : - allPathSignals φ = (paths φ).flatMap (pathSignals (crossingSites φ)) := by - rw [← occurrencePaths_eq_paths, List.flatMap_map] - rfl - -private theorem idxOf_range_of_lt {i n : ℕ} (hi : i < n) : (List.range n).idxOf i = i := by - have h := (List.nodup_range : (List.range n).Nodup).idxOf_getElem i - (by simpa only [List.length_range] using hi) - rw [List.getElem_range] at h - exact h - -/-- A source center belongs to an actual occurrence path exactly at one of its two endpoints. -/ -theorem occurrencePath_center_iff {φ : CNF ℕ} {o : Occurrence ℕ} - (ho : o ∈ Cslib.Logic.PL.occurrences φ) {w : ℕ} - (hw : w < φ.distinctVars.length + φ.length) : - Layout.center w ∈ occurrencePath φ o ↔ - w = φ.distinctVars.idxOf o.2.2.1 ∨ w = φ.distinctVars.length + o.1 := by - have hi : (Cslib.Logic.PL.occurrences φ).idxOf o < (SAT.incidenceGraph φ).2.length := by - simpa only [SAT.incidenceGraph, List.length_map] using List.idxOf_lt_length_of_mem ho - have he : (SAT.incidenceGraph φ).2[(Cslib.Logic.PL.occurrences φ).idxOf o] = - (φ.distinctVars.idxOf o.2.2.1, φ.distinctVars.length + o.1) := by - simp only [SAT.incidenceGraph, List.getElem_map] - rw [List.getElem_idxOf (List.idxOf_lt_length_of_mem ho)] - have hb := SAT.incidenceGraph_bipartite (List.getElem_mem hi) - rw [he] at hb - have h := Graph.unitPath_center_iff (SAT.incidenceGraph φ) - (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) hi - (by simpa [SAT.incidenceGraph] using hw) - rw [he] at h - change Layout.center w ∈ occurrencePath φ o ↔ - w = (List.range _).idxOf (φ.distinctVars.idxOf o.2.2.1) ∨ - w = (List.range _).idxOf (φ.distinctVars.length + o.1) at h - rw [idxOf_range_of_lt (by omega), idxOf_range_of_lt hb.2.2] at h - exact h - -/-- At every source center, all path-half incidences are bounded by its actual graph degree. -/ -theorem count_allPathSignals_center_le (φ : CNF ℕ) {w : ℕ} - (hw : w < φ.distinctVars.length + φ.length) : - (allPathSignals φ).count (Layout.center w, none) ≤ - (SAT.incidenceGraph φ).incidenceVertices.count w := by - have hsite : Layout.center w ∉ crossingSites φ := by - intro hm - have hc := (mem_crossingSites φ _).mp hm |>.2.1 - apply hc - simp only [Graph.orthogonalPositions, List.mem_map] - exact ⟨w, by simpa [SAT.incidenceGraph] using hw, rfl⟩ - have hpath (o : Occurrence ℕ) (ho : o ∈ Cslib.Logic.PL.occurrences φ) : - (pathSignals (crossingSites φ) (occurrencePath φ o)).count (Layout.center w, none) ≤ - [φ.distinctVars.idxOf o.2.2.1, φ.distinctVars.length + o.1].count w := by - by_cases hm : Layout.center w ∈ occurrencePath φ o - · rcases (occurrencePath_center_iff ho hw).mp hm with he | he - · have hc := count_pathSignals_none_head hsite (occurrencePath_nodup ho) - (he.symm ▸ (occurrencePath_endpoints ho).1) - have hpos : 0 < [φ.distinctVars.idxOf o.2.2.1, φ.distinctVars.length + o.1].count w := - List.count_pos_iff.mpr (by simp [he]) - omega - · have hc := count_pathSignals_none_last hsite (occurrencePath_nodup ho) - (he.symm ▸ (occurrencePath_endpoints ho).2) - have hpos : 0 < [φ.distinctVars.idxOf o.2.2.1, φ.distinctVars.length + o.1].count w := - List.count_pos_iff.mpr (by simp [he]) - omega - · rw [count_pathSignals_eq_zero_of_not_mem hm] - exact Nat.zero_le _ - simp only [allPathSignals, Graph.incidenceVertices, SAT.incidenceGraph, List.flatMap_map, - List.count_flatMap] - exact List.sum_le_sum hpath - -private theorem paths_nodup {φ : CNF ℕ} {r : Route} (hr : r ∈ paths φ) : r.Nodup := by - obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hr - have hi' : i < (SAT.incidenceGraph φ).2.length := by - simpa only [paths_eq_unitPaths, Graph.unitPaths_length] using hi - have h := Graph.unitPath_nodup (SAT.incidenceGraph φ) - (fun _ => SAT.incidenceGraph_endpoints) (fun _ => SAT.incidenceGraph_loopless) hi' - change ((paths φ).getD i []).Nodup at h - rwa [List.getD_eq_getElem _ _ hi] at h - -private theorem count_pathSignals_filter_le (sites : List Point) (rs : List Route) - (hn : ∀ r ∈ rs, r.Nodup) (p : Point) (hp : p ∉ sites) : - (rs.flatMap (pathSignals sites)).count (p, none) ≤ - 2 * (rs.filter fun r => r.contains p).length := by - induction rs with - | nil => simp - | cons r rs ih => - have ht := ih (fun s hs => hn s (List.mem_cons_of_mem _ hs)) - rw [List.flatMap_cons, List.count_append] - by_cases hm : p ∈ r - · have hc := count_pathSignals_none_le_two sites r p hp (hn r List.mem_cons_self) - have hf : ((r :: rs).filter fun r => r.contains p) = - r :: rs.filter (fun r => r.contains p) := by simp [hm] - rw [hf, List.length_cons] - omega - · rw [count_pathSignals_eq_zero_of_not_mem hm, Nat.zero_add] - have hf : ((r :: rs).filter fun r => r.contains p) = rs.filter (fun r => r.contains p) := by - simp [hm] - rwa [hf] - -/-- An ordinary nonvertex cell contributes at most two actual path halves in total. -/ -theorem count_allPathSignals_nonvertex_le_two {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) {p : Point} - (hp : p ∉ crossingSites φ) (hc : p ∉ (SAT.incidenceGraph φ).orthogonalPositions) : - (allPathSignals φ).count (p, none) ≤ 2 := by - rw [allPathSignals_eq_flatMap] - have h := count_pathSignals_filter_le (crossingSites φ) (paths φ) - (fun _ => paths_nodup) p hp - have hf := paths_filter_length_le_one hw hv hp hc - omega - -private theorem count_allPathSignals_none_of_site {φ : CNF ℕ} {p : Point} - (hp : p ∈ crossingSites φ) : (allPathSignals φ).count (p, none) = 0 := by - rw [allPathSignals_eq_flatMap] - induction paths φ with - | nil => rfl - | cons r rs ih => - rw [List.flatMap_cons, List.count_append, count_pathSignals_none_of_site hp, ih] - -/-- Ordinary variables in the actual output path list have at most three literal incidences. -/ -theorem count_allPathSignals_none_le_three {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) (p : Point) : - (allPathSignals φ).count (p, none) ≤ 3 := by - by_cases hs : p ∈ crossingSites φ - · rw [count_allPathSignals_none_of_site hs] - decide - · by_cases hc : p ∈ (SAT.incidenceGraph φ).orthogonalPositions - · obtain ⟨w, hwmem, rfl⟩ := List.mem_map.mp hc - have hw' : w < φ.distinctVars.length + φ.length := by - simpa [SAT.incidenceGraph] using List.mem_range.mp hwmem - exact (count_allPathSignals_center_le φ hw').trans (SAT.incidenceGraph_degree_le hw hv w) - · exact (count_allPathSignals_nonvertex_le_two hw hv hs hc).trans (by decide) - -/-- Every directed cell side in the actual source paths, including clause endpoints. -/ -def allPathPorts (φ : CNF ℕ) : List (Point × Fin 4) := - (paths φ).flatMap fun r => r.consecutivePairs.flatMap fun e => - [(e.1, side e.1 e.2), (e.2, side e.2 e.1)] - -private def portSignal (sites : List Point) (e : Point × Fin 4) : Variable := - (e.1, if e.1 ∈ sites then some (Crossover.splitTerminal e.2) else none) - -private theorem allPathSignals_eq_map (φ : CNF ℕ) : - allPathSignals φ = (allPathPorts φ).map (portSignal (crossingSites φ)) := by - have h : allPathSignals φ = - ((Cslib.Logic.PL.occurrences φ).map (occurrencePath φ)).flatMap - (pathSignals (crossingSites φ)) := by - rw [List.flatMap_map] - rfl - rw [h, occurrencePaths_eq_paths] - unfold pathSignals pathHalfEdges allPathPorts portSignal signal - simp [List.map_flatMap] - -private theorem splitTerminal_injective : Function.Injective Crossover.splitTerminal := by decide - -private theorem count_portSignal_terminal (sites : List Point) (p : Point) (i : Fin 4) - (hp : p ∈ sites) (l : List (Point × Fin 4)) : - (l.map (portSignal sites)).count (p, some (Crossover.splitTerminal i)) = l.count (p, i) := by - have he (e : Point × Fin 4) : - (portSignal sites e == (p, some (Crossover.splitTerminal i))) = (e == (p, i)) := by - apply Bool.eq_iff_iff.mpr - simp only [beq_iff_eq] - rcases e with ⟨q, j⟩ - by_cases hq : q = p - · subst q - simp [portSignal, hp, splitTerminal_injective.eq_iff] - · simp [portSignal, Prod.mk.injEq, hq] - induction l with - | nil => rfl - | cons e l ih => simp only [List.map_cons, List.count_cons, he, ih] - -/-- A selected crossover terminal has at most one external literal half in the actual paths. -/ -theorem count_allPathSignals_terminal_le_one {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) - (p : Point) (i : Fin 4) (hp : p ∈ crossingSites φ) : - (allPathSignals φ).count (p, some (Crossover.splitTerminal i)) ≤ 1 := by - rw [allPathSignals_eq_map, count_portSignal_terminal _ _ _ hp] - exact List.nodup_iff_count_le_one.mp (pathPorts_nodup hw hv) _ - -private theorem tagged_template_count (p q : Point) (v : Crossover.SplitVariable) : - (Crossover.splitFormula.vars.map (fun w => (q, some w))).count (p, some v) = - if q = p then Crossover.splitFormula.vars.count v else 0 := by - by_cases h : q = p - · subst q - rw [ite_eq_left rfl] - exact List.count_map_of_injective _ (fun w => (p, some w)) - (fun _ _ he => Option.some.inj (congrArg Prod.snd he)) _ - · rw [ite_eq_right h, List.count_eq_zero] - intro hm - obtain ⟨w, _, he⟩ := List.mem_map.mp hm - exact h (congrArg Prod.fst he) - -private theorem count_tagged_templates (ps : List Point) (p : Point) - (v : Crossover.SplitVariable) : - (ps.flatMap fun q => Crossover.splitFormula.vars.map (fun w => (q, some w))).count - (p, some v) = ps.count p * Crossover.splitFormula.vars.count v := by - induction ps with - | nil => simp - | cons q ps ih => - rw [List.flatMap_cons, List.count_append, tagged_template_count, List.count_cons, ih] - by_cases h : q = p <;> simp [h, beq_iff_eq, Nat.add_mul, Nat.add_comm] - -/-- Translated templates have the exact literal counts of one template at a selected site. -/ -theorem count_crossingSignals_some (φ : CNF ℕ) (p : Point) (v : Crossover.SplitVariable) : - (crossingSignals φ).count (p, some v) = - (crossingSites φ).count p * Crossover.splitFormula.vars.count v := - count_tagged_templates _ _ _ - -/-- Ordinary signal names never occur inside a crossover template. -/ -theorem count_crossingSignals_none (φ : CNF ℕ) (p : Point) : - (crossingSignals φ).count (p, none) = 0 := by - rw [List.count_eq_zero] - simp [crossingSignals] - -/-- The comparison uses the actual emitted formula. It only adds unused clause-cell halves. -/ -theorem count_vars_rawFormula_le (φ : CNF ℕ) (v : Variable) : - (rawFormula φ).vars.count v ≤ (crossingSignals φ).count v + (allPathSignals φ).count v := by - have he := count_external_blocks_le (φ := φ) (crossingSites φ) - (Cslib.Logic.PL.occurrences φ) (fun _ => occurrencePath_length_ge_two) v - have hc : (CNF.vars (((crossingSites φ).flatMap crossingClauses).map Prod.fst)).count v = - (crossingSignals φ).count v := by - unfold crossingSignals - induction crossingSites φ with - | nil => simp [CNF.vars] - | cons p ps ih => - rw [List.flatMap_cons, List.map_append, count_vars_append, vars_crossingClauses, - List.flatMap_cons, List.count_append, ih] - simp only [rawFormula, placedClauses, List.map_append, count_vars_append, - vars_originalClauses, hc] - unfold allPathSignals - omega - -/-- The fixed template has at most three literal positions per internal variable. -/ -theorem count_vars_splitFormula : ∀ v, Crossover.splitFormula.vars.count v ≤ 3 := by - decide +kernel - -/-- Every terminal has exactly two internal literal positions, leaving one external incidence. -/ -theorem count_vars_splitTerminal : - ∀ i, Crossover.splitFormula.vars.count (Crossover.splitTerminal i) = 2 := by - decide +kernel - -private theorem count_allPathSignals_nonterminal {φ : CNF ℕ} (p : Point) - (v : Crossover.SplitVariable) (hv : ¬ ∃ i, Crossover.splitTerminal i = v) : - (allPathSignals φ).count (p, some v) = 0 := by - rw [List.count_eq_zero] - intro hm - obtain ⟨o, _, hm⟩ := List.mem_flatMap.mp hm - obtain ⟨e, _, he⟩ := List.mem_map.mp hm - have hs := congrArg Prod.snd he - by_cases hp : e.1 ∈ crossingSites φ - · have heq : Crossover.splitTerminal (side e.1 e.2) = v := by - simpa [signal, hp] using hs - exact hv ⟨_, heq⟩ - · simp [signal, hp] at hs - -private theorem count_allPathSignals_some_of_not_site {φ : CNF ℕ} {p : Point} - (hp : p ∉ crossingSites φ) (v : Crossover.SplitVariable) : - (allPathSignals φ).count (p, some v) = 0 := by - rw [List.count_eq_zero] - intro hm - obtain ⟨o, _, hm⟩ := List.mem_flatMap.mp hm - obtain ⟨e, _, he⟩ := List.mem_map.mp hm - have hcell : e.1 = p := congrArg Prod.fst he - have hs := congrArg Prod.snd he - simp [signal, hcell, hp] at hs - -/-- The actual structured planarization formula has at most three literal occurrences of -any variable, counting repetitions within clauses. No drawing or degree certificate is assumed. -/ -theorem count_vars_rawFormula_le_three {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : - ∀ v, (rawFormula φ).vars.count v ≤ 3 := by - rintro ⟨p, v⟩ - have hcompare := count_vars_rawFormula_le φ (p, v) - cases v with - | none => - rw [count_crossingSignals_none, Nat.zero_add] at hcompare - exact hcompare.trans (count_allPathSignals_none_le_three hw hv p) - | some v => - have hsite : (crossingSites φ).count p ≤ 1 := - List.nodup_iff_count_le_one.mp (crossingSites_nodup φ) p - rw [count_crossingSignals_some] at hcompare - by_cases ht : ∃ i, Crossover.splitTerminal i = v - · obtain ⟨i, rfl⟩ := ht - rw [count_vars_splitTerminal] at hcompare - by_cases hp : p ∈ crossingSites φ - · have hext := count_allPathSignals_terminal_le_one hw hv p i hp - omega - · rw [List.count_eq_zero.mpr hp, count_allPathSignals_some_of_not_site hp] at hcompare - omega - · rw [count_allPathSignals_nonterminal p v ht, Nat.add_zero] at hcompare - exact hcompare.trans ((Nat.mul_le_mul hsite (count_vars_splitFormula v)).trans (by simp)) - -/-- Injective compaction preserves the actual three-literal-occurrence bound. -/ -theorem count_vars_formula_le_three {φ : CNF ℕ} - (hw : ∀ c ∈ φ, c.length ≤ 3) (hv : ∀ v, φ.vars.count v ≤ 3) : - ∀ v, (formula φ).vars.count v ≤ 3 := - CNF.count_vars_compact_le (rawFormula φ) (count_vars_rawFormula_le_three hw hv) - -end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PolyTime.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PolyTime.lean deleted file mode 100644 index 48178aa3a..000000000 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PolyTime.lean +++ /dev/null @@ -1,502 +0,0 @@ -/- -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.PathPolyTime -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile -public import Complexity.Computability.Complexity.Problems.SAT -public import Complexity.Computability.Geometry.Orthogonal.Subdivision -public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Finite -public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option -public import Complexity.Logics.Propositional.CNF.PolyTime -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Finite -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Int.Binary -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Fin -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain - -/-! -# Native computation of the finite planarization compiler - -Input variable names and all coordinates use binary encodings. Syntactic indices, ranks and -the subdivision budget use unary counters. The fixed template has 53 names independently of -the runtime input, so its finite encoding introduces no growing enumeration. - -## Main definitions - -* `Cslib.Complexity.SAT.PlanarCompile.encVariable`: binary coordinates and a fixed optional tag. -* `Cslib.Complexity.SAT.PlanarCompile.encPlacedClause`: a clause with its finite geometric data. - -## Main results - -* `computableInPolyTime_formula`: the complete formula compiler under binary CNF encodings. -* `computableInPolyTime_positions`, `computableInPolyTime_routes`: its actual geometric output. -* `computableInPolyTime_paths`, `computableInPolyTime_crossingSites`: bounded unit paths and - finite crossing-site selection, with no geometric validity assumption on the input. - -## References - -The compiler is the finite construction defined in `Compile`. --/ - -@[expose] public section - -namespace Cslib.Complexity.SAT.PlanarCompile - -open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal Turing.MultiTapeTM - -/-- Structured names retain binary coordinates and a fixed finite crossover tag. -/ -noncomputable def encVariable : Variable ↪ List Bool := - encPair encPoint (encOption (encFinite Crossover.SplitVariable)) - -/-- Framed literal, position and route data of one emitted clause. -/ -noncomputable def encPlacedClause : PlacedClause ↪ List Bool := - encPair (encList (encPair encVariable encBool)) (encPair encPoint (encList encRoute)) - -private theorem computable_natCast : - ComputableInPolyTime (fun n : ℕ => (n : ℤ)) encUnary encIntBin := - .of_tidy (ComputableTidilyInPolyTime.intBin_natCast.comp - ComputableTidilyInPolyTime.unary_to_binary) - -private theorem computable_finVal : - ComputableInPolyTime (fun s : Fin 3 => s.val) (encFinite (Fin 3)) encNat := - .of_tidy (ComputableTidilyInPolyTime.of_finite _) - -attribute [local fun_prop] computable_natCast computable_finVal ComputableInPolyTime.tidy - -private theorem computable_incidencePort : - ComputableInPolyTime (fun p : Graph × ℕ => p.1.incidencePort p.2) - (encPair encGraph encUnary) (encFinite (Fin 3)) := by - have hc : ComputableTidilyInPolyTime (fun p : Graph × ℕ => - (p.1.incidenceVertices.take p.2).count (p.1.incidenceVertices.getD p.2 0)) - (encPair encGraph encUnary) encUnary := by - unfold Graph.incidenceVertices encGraph - fun_prop - exact .of_tidy ((ComputableTidilyInPolyTime.unary_finMod (by decide) - (encFinite (Fin 3))).comp hc) - -attribute [local fun_prop] computable_incidencePort - -private theorem computable_canonicalPorts : - ComputableInPolyTime Graph.canonicalPorts encGraph - (encList (encPair (encFinite (Fin 3)) (encFinite (Fin 3)))) := by - refine .of_tidy ?_ - unfold Graph.canonicalPorts encGraph - fun_prop - -attribute [local fun_prop] computable_canonicalPorts - -private theorem computable_layoutCenter : - ComputableInPolyTime Layout.center encUnary encPoint := by - refine .of_tidy ?_ - unfold Layout.center encPoint - fun_prop - -private theorem computable_layoutColumn : - ComputableInPolyTime (fun p : ℕ × Fin 3 => Layout.column p.1 p.2) - (encPair encUnary (encFinite (Fin 3))) encIntBin := by - refine .of_tidy ?_ - unfold Layout.column - fun_prop - -private theorem computable_layoutTrack : - ComputableInPolyTime (fun p : ℕ × ℕ => Layout.track p.1 p.2) - (encPair encUnary encUnary) encIntBin := by - refine .of_tidy ?_ - unfold Layout.track - fun_prop - -attribute [local fun_prop] computable_layoutCenter computable_layoutColumn computable_layoutTrack - -private theorem computable_layoutElbow : - ComputableInPolyTime (fun p : ℕ × Fin 3 => Layout.elbow p.1 p.2) - (encPair encUnary (encFinite (Fin 3))) encPoint := by - refine .of_tidy ?_ - unfold Layout.elbow encPoint - fun_prop - -attribute [local fun_prop] computable_layoutElbow - -private theorem computable_layoutRoute : - ComputableInPolyTime (fun p : ℕ × ℕ × ℕ × ℕ × Fin 3 × Fin 3 => - Layout.route p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2.1 p.2.2.2.2.2) - (encPair encUnary (encPair encUnary (encPair encUnary - (encPair encUnary (encPair (encFinite (Fin 3)) (encFinite (Fin 3))))))) encRoute := by - refine .of_tidy ?_ - unfold Layout.route encRoute - fun_prop - -attribute [local fun_prop] computable_layoutRoute - -private theorem computable_orthogonalRoutes : - ComputableInPolyTime (fun G : Graph => G.orthogonalRoutes G.canonicalPorts) - encGraph (encList encRoute) := by - let edgeEncoding := encPair (encPair encNat encNat) encUnary - let routeInput := encPair encUnary (encPair encUnary (encPair encUnary - (encPair encUnary (encPair (encFinite (Fin 3)) (encFinite (Fin 3)))))) - have hcan := computable_canonicalPorts.tidy - have hp : ComputableTidilyInPolyTime (fun p : Graph × ((ℕ × ℕ) × ℕ) => - p.1.canonicalPorts.getD p.2.2 (0, 0)) - (encPair encGraph edgeEncoding) (encPair (encFinite (Fin 3)) (encFinite (Fin 3))) := by - unfold edgeEncoding encGraph - fun_prop - have hargs : ComputableInPolyTime (fun p : Graph × ((ℕ × ℕ) × ℕ) => - (p.1.1.length, p.2.2, p.1.1.idxOf p.2.1.1, p.1.1.idxOf p.2.1.2, - (p.1.canonicalPorts.getD p.2.2 (0, 0)).1, - (p.1.canonicalPorts.getD p.2.2 (0, 0)).2)) - (encPair encGraph edgeEncoding) routeInput := by - refine .of_tidy ?_ - unfold routeInput edgeEncoding encGraph at * - fun_prop - have hbody := computable_layoutRoute.comp hargs - have hlist : ComputableInPolyTime (fun G : Graph => G.2.zipIdx) encGraph - (encList edgeEncoding) := by - refine .of_tidy ?_ - unfold encGraph edgeEncoding - fun_prop - simpa only [Graph.orthogonalRoutes, Function.comp_def] using - ComputableInPolyTime.mapWithInput hlist hbody - -attribute [local fun_prop] computable_orthogonalRoutes - -private def endpointColumns (p : Graph × ℕ) : Point := - (Layout.column (p.1.1.idxOf (p.1.edgeEndpoint p.2 false)) - (Graph.portAt p.1.canonicalPorts p.2 false), - Layout.column (p.1.1.idxOf (p.1.edgeEndpoint p.2 true)) - (Graph.portAt p.1.canonicalPorts p.2 true)) - -private theorem computable_endpointColumns : - ComputableInPolyTime endpointColumns (encPair encGraph encUnary) encPoint := by - unfold endpointColumns - have hcan := computable_canonicalPorts.tidy - have hp : ComputableTidilyInPolyTime (fun p : Graph × ℕ => - p.1.canonicalPorts.getD p.2 (0, 0)) - (encPair encGraph encUnary) (encPair (encFinite (Fin 3)) (encFinite (Fin 3))) := by - unfold encGraph - fun_prop - have he : ComputableTidilyInPolyTime (fun p : Graph × ℕ => p.1.2.getD p.2 (0, 0)) - (encPair encGraph encUnary) (encPair encNat encNat) := by - unfold encGraph - fun_prop - refine .of_tidy ?_ - unfold Graph.edgeEndpoint Graph.portAt encPoint encGraph at * - simp only [Bool.false_eq_true, ↓reduceIte] - fun_prop - -attribute [local fun_prop] computable_endpointColumns - -private def candidatePair (p : Graph × (ℕ × ℕ)) : List Point := - [((endpointColumns (p.1, p.2.2)).1, Layout.track p.1.1.length p.2.1), - ((endpointColumns (p.1, p.2.2)).2, Layout.track p.1.1.length p.2.1)] - -private theorem computable_candidatePair : - ComputableInPolyTime candidatePair (encPair encGraph (encPair encUnary encUnary)) - (encList encPoint) := by - have hselect : ComputableTidilyInPolyTime - (fun p : Graph × (ℕ × ℕ) => (p.1, p.2.2)) - (encPair encGraph (encPair encUnary encUnary)) (encPair encGraph encUnary) := by fun_prop - have hcols := computable_endpointColumns.tidy.comp hselect - have hleft := hcols.fst' - have hright := hcols.snd' - have htrack : ComputableTidilyInPolyTime (fun p : Graph × (ℕ × ℕ) => - Layout.track p.1.1.length p.2.1) - (encPair encGraph (encPair encUnary encUnary)) encIntBin := by - unfold encGraph - fun_prop - refine .of_tidy ?_ - unfold candidatePair encPoint at * - fun_prop - -private def candidateRow (p : Graph × ℕ) : List Point := - (List.range p.1.2.length).flatMap fun j => candidatePair (p.1, p.2, j) - -private theorem computable_edgeRange : - ComputableInPolyTime (fun G : Graph => List.range G.2.length) encGraph - (encList encUnary) := by - refine .of_tidy ?_ - unfold encGraph - fun_prop - -private theorem computable_candidateRow : - ComputableInPolyTime candidateRow (encPair encGraph encUnary) (encList encPoint) := by - have hlist := computable_edgeRange.comp (ComputableInPolyTime.fst encGraph encUnary) - have harg : ComputableInPolyTime (fun p : (Graph × ℕ) × ℕ => (p.1.1, p.1.2, p.2)) - (encPair (encPair encGraph encUnary) encUnary) - (encPair encGraph (encPair encUnary encUnary)) := by fun_prop - have hbody := computable_candidatePair.comp harg - change ComputableInPolyTime (fun p : Graph × ℕ => - (List.range p.1.2.length).flatMap fun j => candidatePair (p.1, p.2, j)) _ _ - simpa only [Function.comp_def] using ComputableInPolyTime.flatMapWithInput hlist hbody - -private theorem computable_crossingCandidates : - ComputableInPolyTime (fun G : Graph => G.crossingCandidates G.canonicalPorts) - encGraph (encList encPoint) := by - have h := ComputableInPolyTime.flatMapWithInput - (f := fun G i => candidateRow (G, i)) (encB := encPoint) - computable_edgeRange computable_candidateRow - simpa only [candidateRow, candidatePair, endpointColumns, Graph.crossingCandidates] using h - -attribute [local fun_prop] computable_crossingCandidates - -private theorem computable_orthogonalPositions : - ComputableInPolyTime Graph.orthogonalPositions encGraph encRoute := by - refine .of_tidy ?_ - unfold Graph.orthogonalPositions encRoute encGraph - fun_prop - -attribute [local fun_prop] computable_orthogonalPositions - -private theorem computable_distinctPoints : - ComputableInPolyTime (fun l : Route => selectDistinct l (List.replicate l.length true)) - encRoute encRoute := by - have hrep : ComputableTidilyInPolyTime (fun n => List.replicate n true) encUnary encBits := - ComputableTidilyInPolyTime.of_linear (.of_eq fun _ => rfl) - refine .of_tidy ?_ - unfold selectDistinct encRoute - fun_prop - -private theorem computable_crossingPredicate : - ComputableInPolyTime (fun p : CNF ℕ × Point => - !((SAT.incidenceGraph p.1).orthogonalPositions.contains p.2) && - decide (2 ≤ ((paths p.1).filter fun r => r.contains p.2).length)) - (encPair encCNF encPoint) encBool := by - have hg := SAT.computableInPolyTime_incidenceGraph encNat - have hv : ComputableTidilyInPolyTime (fun p : CNF ℕ × Point => - (SAT.incidenceGraph p.1).orthogonalPositions) (encPair encCNF encPoint) encRoute := - (computable_orthogonalPositions.comp hg).tidy.comp (ComputableTidilyInPolyTime.fst _ _) - have hp : ComputableTidilyInPolyTime (fun p : CNF ℕ × Point => paths p.1) - (encPair encCNF encPoint) (encList encRoute) := - computableInPolyTime_paths.tidy.comp (ComputableTidilyInPolyTime.fst _ _) - refine .of_tidy ?_ - unfold encRoute at * - simp only [List.contains_eq_mem] - fun_prop - -private theorem computable_side : - ComputableInPolyTime (fun p : Point × Point => side p.1 p.2) - (encPair encPoint encPoint) (encFinite (Fin 4)) := by - refine .of_tidy ?_ - unfold side encPoint - fun_prop - -private theorem computable_cellOrigin : - ComputableInPolyTime (cellOrigin 120) encPoint encPoint := by - refine .of_tidy ?_ - unfold cellOrigin encPoint - fun_prop - -private theorem computable_center : ComputableInPolyTime center encPoint encPoint := by - refine .of_tidy ?_ - change ComputableTidilyInPolyTime (fun p : Point => - (240 * p.1 + 120, 240 * p.2 + 120)) encPoint encPoint - unfold encPoint - fun_prop - -private theorem computable_translate : - ComputableInPolyTime (fun p : Point × Route => translate p.1 p.2) - (encPair encPoint encRoute) encRoute := by - refine .of_tidy ?_ - change ComputableTidilyInPolyTime (fun p : Point × Route => - p.2.map fun q => (q.1 + p.1.1, q.2 + p.1.2)) _ _ - unfold encPoint encRoute - fun_prop - -private theorem computable_pointAdd : - ComputableInPolyTime (fun p : Point × Point => p.1 + p.2) - (encPair encPoint encPoint) encPoint := by - refine .of_tidy ?_ - change ComputableTidilyInPolyTime (fun p : Point × Point => - (p.1.1 + p.2.1, p.1.2 + p.2.2)) _ _ - unfold encPoint - fun_prop - -attribute [local fun_prop] computable_side computable_cellOrigin computable_center - computable_translate computable_pointAdd - -private theorem computable_signal : - ComputableInPolyTime (fun p : List Point × Point × Point => signal p.1 p.2.1 p.2.2) - (encPair encRoute (encPair encPoint encPoint)) encVariable := by - have ht : ComputableTidilyInPolyTime Crossover.splitTerminal (encFinite (Fin 4)) - (encFinite Crossover.SplitVariable) := ComputableTidilyInPolyTime.of_finite _ - refine .of_tidy ?_ - unfold signal encVariable encRoute - fun_prop - -private theorem computable_cellPort : - ComputableInPolyTime (fun p : Point × Fin 4 => cellPort 120 p.1 p.2) - (encPair encPoint (encFinite (Fin 4))) encPoint := by - refine .of_tidy ?_ - have hlocal : ComputableTidilyInPolyTime (cellPort 120 (0, 0)) (encFinite (Fin 4)) - encPoint := ComputableTidilyInPolyTime.of_finite _ - have heq : (fun p : Point × Fin 4 => cellPort 120 p.1 p.2) = - fun p => cellOrigin 120 p.1 + cellPort 120 (0, 0) p.2 := by - funext p - simp [cellPort, cellOrigin] - rw [heq] - fun_prop - -attribute [local fun_prop] computable_cellPort - -private theorem computable_access : - ComputableInPolyTime (fun p : List Point × Point × Point => access p.1 p.2.1 p.2.2) - (encPair encRoute (encPair encPoint encPoint)) encRoute := by - have ha : ComputableTidilyInPolyTime Crossover.accessRoute (encFinite (Fin 4)) encRoute := - ComputableTidilyInPolyTime.of_finite _ - refine .of_tidy ?_ - unfold access encRoute - fun_prop - -attribute [local fun_prop] computable_signal computable_access - -private theorem computable_variablePosition : - ComputableInPolyTime variablePosition encVariable encPoint := by - have hl : ComputableTidilyInPolyTime (fun v : Option Crossover.SplitVariable => - v.elim (120, 120) Crossover.variablePosition) - (encOption (encFinite Crossover.SplitVariable)) encPoint := - ComputableTidilyInPolyTime.of_finite _ - refine .of_tidy ?_ - unfold variablePosition encVariable - fun_prop - -private theorem computable_link : - ComputableInPolyTime (fun p : List Point × Bool × Point × Point => - link p.1 p.2.1 p.2.2.1 p.2.2.2) - (encPair encRoute (encPair encBool (encPair encPoint encPoint))) encPlacedClause := by - refine .of_tidy ?_ - dsimp only [link] - unfold encPlacedClause - fun_prop - -private theorem computable_dropLast : - ComputableInPolyTime (List.dropLast (α := Point)) encRoute encRoute := by - refine .of_tidy ?_ - change ComputableTidilyInPolyTime (fun r : Route => r.dropLast) encRoute encRoute - simp only [List.dropLast_eq_take] - unfold encRoute - fun_prop - -attribute [local fun_prop] computable_variablePosition computable_link computable_dropLast - -private theorem computable_links : - ComputableInPolyTime (fun p : List Point × Bool × Route => links p.1 p.2.1 p.2.2) - (encPair encRoute (encPair encBool encRoute)) (encList encPlacedClause) := by - refine .of_tidy ?_ - unfold links List.consecutivePairs - fun_prop - -private theorem computable_lastLiteral : - ComputableInPolyTime (fun p : List Point × Route × Bool => lastLiteral p.1 p.2.1 p.2.2) - (encPair encRoute (encPair encRoute encBool)) - (encPair (encPair encVariable encBool) encRoute) := by - refine .of_tidy ?_ - dsimp only [lastLiteral] - simp only [List.getLastD_eq_getLast?, List.getLast?_eq_head?_reverse] - unfold encRoute - fun_prop - -attribute [local fun_prop] computable_links computable_lastLiteral - -private theorem computable_originalClauses : - ComputableInPolyTime (fun p : CNF ℕ × List Point => originalClauses p.1 p.2) - (encPair encCNF encRoute) (encList encPlacedClause) := by - refine .of_tidy ?_ - dsimp only [originalClauses] - unfold encPlacedClause encCNF - fun_prop - -private theorem computable_crossingClauses : - ComputableInPolyTime crossingClauses encPoint (encList encPlacedClause) := by - let rowEncoding := encPair - (encList (encPair (encFinite Crossover.SplitVariable) encBool)) encUnary - have hbody : ComputableInPolyTime (fun p : Point × (Clause Crossover.SplitVariable × ℕ) => - (p.2.1.relabel (fun v => (p.1, some v)), - cellOrigin 120 p.1 + Crossover.clausePositions.getD p.2.2 (0, 0), - (Crossover.incidenceRoutes.filter fun e => e.1 == p.2.2).map fun e => - translate (cellOrigin 120 p.1) e.2.2)) - (encPair encPoint rowEncoding) encPlacedClause := by - have horigin := computable_cellOrigin.tidy.comp - (ComputableTidilyInPolyTime.fst encPoint rowEncoding) - have hpositions : ComputableTidilyInPolyTime - (fun _ : Point × (Clause Crossover.SplitVariable × ℕ) => Crossover.clausePositions) - (encPair encPoint rowEncoding) encRoute := ComputableTidilyInPolyTime.const _ - have hposition : ComputableTidilyInPolyTime - (fun p : Point × (Clause Crossover.SplitVariable × ℕ) => - Crossover.clausePositions.getD p.2.2 (0, 0)) - (encPair encPoint rowEncoding) encPoint := by - unfold rowEncoding encRoute at * - fun_prop - refine .of_tidy ?_ - unfold rowEncoding encPlacedClause Clause.relabel encVariable Prod.map at * - fun_prop - have hlist : ComputableInPolyTime (fun _ : Point => Crossover.splitFormula.zipIdx) - encPoint (encList rowEncoding) := .of_tidy (ComputableTidilyInPolyTime.const _) - change ComputableInPolyTime (fun p => crossingClauses p) _ _ - simpa only [crossingClauses] using ComputableInPolyTime.mapWithInput hlist hbody - -attribute [local fun_prop] computable_originalClauses computable_crossingClauses - -/-- The actual clause and incidence-route records are produced in native polynomial time. -/ -@[fun_prop] -theorem computableInPolyTime_placedClauses : - ComputableInPolyTime placedClauses encCNF (encList encPlacedClause) := by - have hs := computableInPolyTime_crossingSites.tidy - have ho := (Cslib.Logic.PL.computableInPolyTime_occurrences encNat).tidy - refine .of_tidy ?_ - change ComputableTidilyInPolyTime (fun φ => placedClauses φ) _ _ - dsimp only [placedClauses] - unfold encCNF Cslib.Logic.PL.encOccurrence at * - fun_prop - -/-- Structured formula output is computed by projecting the actual emitted clause records. -/ -@[fun_prop] -theorem computableInPolyTime_rawFormula : - ComputableInPolyTime rawFormula encCNF (encList (encList (encPair encVariable encBool))) := by - have hp := computableInPolyTime_placedClauses.tidy - refine .of_tidy ?_ - change ComputableTidilyInPolyTime (fun φ => rawFormula φ) _ _ - unfold rawFormula encPlacedClause at * - fun_prop - -/-- The complete formula compiler is native polynomial-time under the usual binary CNF -encoding. Compact indices are computed in unary and then encoded in binary. -/ -@[fun_prop] -theorem computableInPolyTime_formula : ComputableInPolyTime formula encCNF encCNF := by - have hu := (CNF.isPolyTime_compact encVariable).comp computableInPolyTime_rawFormula - have hi : ComputableInPolyTime (fun n : ℕ => n) encUnary encNat := - .of_tidy ComputableTidilyInPolyTime.unary_to_binary - have hr := (CNF.computableInPolyTime_relabel hi).comp hu - have he (ψ : CNF ℕ) : ψ.relabel (fun n : ℕ => n) = ψ := CNF.relabel_id ψ - change ComputableInPolyTime (fun φ => (rawFormula φ).compact) _ _ - simpa only [Function.comp_def, he, encCNF] using hr - -/-- All output vertex positions are computed in native polynomial time. -/ -@[fun_prop] -theorem computableInPolyTime_positions : ComputableInPolyTime positions encCNF encRoute := by - have hv := (CNF.computableInPolyTime_distinctVars encVariable).comp - computableInPolyTime_rawFormula - have hp := computableInPolyTime_placedClauses.tidy - refine .of_tidy ?_ - change ComputableTidilyInPolyTime (fun φ => positions φ) _ _ - dsimp only [positions] - unfold encPlacedClause encRoute at * - fun_prop - -/-- All output incidence routes are computed in native polynomial time. -/ -@[fun_prop] -theorem computableInPolyTime_routes : - ComputableInPolyTime routes encCNF (encList encRoute) := by - have hp := computableInPolyTime_placedClauses.tidy - refine .of_tidy ?_ - change ComputableTidilyInPolyTime (fun φ => routes φ) _ _ - unfold routes encPlacedClause at * - fun_prop - -end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Semantics.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Semantics.lean deleted file mode 100644 index 30f5ee086..000000000 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Semantics.lean +++ /dev/null @@ -1,235 +0,0 @@ -/- -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.PathAssignments -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile -public import Complexity.Logics.Propositional.CNF.Planar.DirectedWire -import Mathlib.Data.List.GetD -import Mathlib.Tactic.SplitIfs - -/-! -# Logical semantics of the actual finite planar SAT compiler - -This module connects the executable placed clauses to ordinary CNF evaluation and the generic -polarity-directed wire rules. Logical conditions are kept explicit until discharged for the -actual incidence paths. No geometric planarity or machine-time claim is made here. - -## Main definitions - -The compiler data are defined in `PlanarCompile`; this module introduces no second compiler. - -## Main results - -* `Cslib.Complexity.SAT.PlanarCompile.eval_rawFormula_iff`: actual output block semantics. -* `Cslib.Complexity.SAT.PlanarCompile.crossing_boundary_eq`: opposite ports of selected sites agree. - -## References - -The finite assembly and its logical composition proofs are original. --/ - -@[expose] public section - -namespace Cslib.Complexity.SAT.PlanarCompile - -open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal - -/-- Forgetting geometric data gives exactly the renamed fixed crossover clauses. -/ -theorem map_fst_crossingClauses (p : Point) : - (crossingClauses p).map Prod.fst = - Crossover.splitFormula.relabel (fun v => (p, some v)) := by - change (Crossover.splitFormula.zipIdx.map fun c => - c.1.relabel (fun v => (p, some v))) = _ - calc - _ = (Crossover.splitFormula.zipIdx.map Prod.fst).map - (Clause.relabel (fun v => (p, some v))) := by rw [List.map_map]; rfl - _ = _ := by rw [List.zipIdx_map_fst]; rfl - -/-- The structured output is the original-clause, crossover, and directed-link blocks. -/ -theorem rawFormula_eq (φ : CNF ℕ) : - rawFormula φ = - ((originalClauses φ (crossingSites φ)).map Prod.fst) ++ - ((crossingSites φ).flatMap fun p => - Crossover.splitFormula.relabel (fun v => (p, some v))) ++ - ((Cslib.Logic.PL.occurrences φ).flatMap fun o => - (links (crossingSites φ) o.2.2.2 (occurrencePath φ o)).map Prod.fst) := by - simp only [rawFormula, placedClauses, List.map_append, List.map_flatMap] - simp_rw [map_fst_crossingClauses] - -/-- Evaluating the actual output checks exactly its three clause blocks. -/ -theorem eval_rawFormula_iff (φ : CNF ℕ) (σ : Variable → Bool) : - (rawFormula φ).eval σ = true ↔ - CNF.eval σ ((originalClauses φ (crossingSites φ)).map Prod.fst) = true ∧ - (∀ p ∈ crossingSites φ, Crossover.splitFormula.eval (fun v => σ (p, some v)) = true) ∧ - ∀ o ∈ Cslib.Logic.PL.occurrences φ, - CNF.eval σ - ((links (crossingSites φ) o.2.2.2 (occurrencePath φ o)).map Prod.fst) = true := by - rw [rawFormula_eq] - simp only [eval_append, Bool.and_eq_true, eval_flatMap_eq_true_iff, eval_relabel, and_assoc, - Function.comp_def] - -/-- Every selected site's actual crossover clauses force its opposite terminal values to agree. -/ -theorem crossing_boundary_eq {φ : CNF ℕ} {σ : Variable → Bool} - (h : (rawFormula φ).eval σ = true) {p : Point} (hp : p ∈ crossingSites φ) : - σ (p, some .aLeft) = σ (p, some .aRight) ∧ - σ (p, some .bTop) = σ (p, some .bBottom) := - Crossover.split_boundary_eq_of_holds (((eval_rawFormula_iff φ σ).1 h).2.1 p hp) - -/-- The placed intercell clauses are exactly the generic polarity-directed wire clauses. -/ -theorem map_fst_links (sites : List Point) (b : Bool) (r : Route) : - (links sites b r).map Prod.fst = CNF.DirectedWire.links b (wire sites r) := by - apply List.ext_getElem - · simp [links, CNF.DirectedWire.links, wire, List.consecutivePairs] - · intro i hi hj - have hi' : i + 2 < r.length := by - simp only [links, List.length_map, List.consecutivePairs, List.length_zip, - List.length_tail, List.length_dropLast] at hi - omega - simp only [links, CNF.DirectedWire.links, List.getElem_map, List.consecutivePairs, - List.getElem_zip, List.getElem_tail] - rw [getElem_wire sites r i (by omega), getElem_wire sites r (i + 1) (by omega)] - simp only [List.getElem_dropLast] - have hn : r.getD (i + 1) r[i] = r[i + 1] := List.getD_eq_getElem _ _ (by omega) - have hp : r.getD (i + 1 - 1) r[i + 1] = r[i] := by - rw [Nat.add_sub_cancel, List.getD_eq_getElem _ _ (by omega)] - simp only [hn, hp] - cases b <;> rfl - -private theorem lastD_eq_getElem {α : Type*} (xs : List α) (d : α) (hne : xs ≠ []) : - xs.getLastD d = xs[xs.length - 1]'(by cases xs <;> simp_all) := by - induction xs generalizing d with - | nil => exact False.elim (hne rfl) - | cons a xs ih => - cases xs with - | nil => rfl - | cons b xs => - rw [List.getLastD_cons, ih a (List.cons_ne_nil _ _)] - simp only [List.length_cons, Nat.add_sub_cancel, List.getElem_cons_succ] - -/-- The final exit of the executable cell list is the variable used by its original literal. -/ -theorem last_exit_eq_lastLiteral (sites : List Point) (r : Route) (b : Bool) - (fallback : Variable) (hlen : 2 ≤ r.length) : - ((wire sites r).getLastD (fallback, fallback)).2 = (lastLiteral sites r b).1.1 := by - rw [lastD_eq_getElem _ _ (wire_ne_nil sites r hlen)] - have hi : (wire sites r).length - 1 < r.length - 1 := by rw [length_wire]; omega - rw [getElem_wire sites r _ hi] - simp only [length_wire] - unfold lastLiteral - have hp : r.getD (r.length - 2) (0, 0) = r[r.length - 1 - 1] := by - rw [List.getD_eq_getElem _ _ (by omega)] - congr 1 - have hn : r.getLastD (0, 0) = r[r.length - 1] := by - rw [lastD_eq_getElem] - intro h - simp [h] at hlen - simp only [hp, hn] - congr 1 - rw [List.getD_eq_getElem _ _ (by omega)] - congr 1 - omega - -/-- Opposite horizontal ports of a selected cell carry the same signal. -/ -theorem horizontal_signal_eq {φ : CNF ℕ} {σ : Variable → Bool} - (h : (rawFormula φ).eval σ = true) {p : Point} (hp : p ∈ crossingSites φ) : - σ (signal (crossingSites φ) p (p - (1, 0))) = - σ (signal (crossingSites φ) p (p + (1, 0))) := by - have hleft : side p (p - (1, 0)) = 0 := by - rcases p with ⟨x, y⟩ - simp only [side, Prod.fst_sub, Prod.snd_sub] - split_ifs <;> first | rfl | omega - have hright : side p (p + (1, 0)) = 1 := by - rcases p with ⟨x, y⟩ - simp only [side, Prod.fst_add, Prod.snd_add] - split_ifs <;> first | rfl | omega - simpa only [signal, hp, ite_true, hleft, hright, Crossover.splitTerminal] using - (crossing_boundary_eq h hp).1 - -/-- Opposite vertical ports of a selected cell carry the same signal. -/ -theorem vertical_signal_eq {φ : CNF ℕ} {σ : Variable → Bool} - (h : (rawFormula φ).eval σ = true) {p : Point} (hp : p ∈ crossingSites φ) : - σ (signal (crossingSites φ) p (p - (0, 1))) = - σ (signal (crossingSites φ) p (p + (0, 1))) := by - have hbottom : side p (p - (0, 1)) = 2 := by - rcases p with ⟨x, y⟩ - simp only [side, Prod.fst_sub, Prod.snd_sub] - split_ifs <;> first | rfl | omega - have htop : side p (p + (0, 1)) = 3 := by - rcases p with ⟨x, y⟩ - simp only [side, Prod.fst_add, Prod.snd_add] - split_ifs <;> first | rfl | omega - simpa only [signal, hp, ite_true, hbottom, htop, Crossover.splitTerminal] using - (crossing_boundary_eq h hp).2 - -/-- The original placed clauses use exactly the endpoint variables of the generic wires. -/ -theorem map_fst_originalClauses (φ : CNF ℕ) (sites : List Point) (fallback : Variable) - (hpaths : ∀ o ∈ Cslib.Logic.PL.occurrences φ, 2 ≤ (occurrencePath φ o).length) : - (originalClauses φ sites).map Prod.fst = - DirectedWire.replacementClauses φ (fun o => wire sites (occurrencePath φ o)) fallback := by - simp only [originalClauses, DirectedWire.replacementClauses, List.map_map, Function.comp_def] - apply List.map_congr_left - intro c hc - apply List.map_congr_left - intro l hl - have ho : (c.2, l.2, l.1) ∈ Cslib.Logic.PL.occurrences φ := - List.mem_flatMap.mpr ⟨c, hc, List.mem_map.mpr ⟨l, hl, rfl⟩⟩ - apply Prod.ext - · exact (last_exit_eq_lastLiteral sites _ l.1.2 fallback (hpaths _ ho)).symm - · rfl - -/-- Actual raw output satisfaction projects to the source once the actual path endpoint and -cell-value conditions are proved. These are logical obligations, not assumed planarity. -/ -theorem eval_rawFormula_sound_of_cells (φ : CNF ℕ) (τ : ℕ → Bool) (σ : Variable → Bool) - (hpaths : ∀ o ∈ Cslib.Logic.PL.occurrences φ, 2 ≤ (occurrencePath φ o).length) - (hcells : ∀ o ∈ Cslib.Logic.PL.occurrences φ, - ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), σ c.1 = σ c.2) - (hfirst : ∀ o ∈ Cslib.Logic.PL.occurrences φ, - σ ((wire (crossingSites φ) (occurrencePath φ o)).headD - (((0, 0), none), ((0, 0), none))).1 = τ o.2.2.1) - (h : (rawFormula φ).eval σ = true) : φ.eval τ = true := by - have he := (eval_rawFormula_iff φ σ).1 h - apply DirectedWire.eval_assemble_sound φ - (fun o => wire (crossingSites φ) (occurrencePath φ o)) ((0, 0), none) τ σ - · intro o ho - exact wire_ne_nil _ _ (hpaths o ho) - · exact hcells - · exact hfirst - · rw [DirectedWire.assemble, eval_append, Bool.and_eq_true] - constructor - · rw [← map_fst_originalClauses φ (crossingSites φ) ((0, 0), none) hpaths] - exact he.1 - · apply (DirectedWire.eval_allLinks_iff φ _ σ).2 - intro o ho - rw [← map_fst_links] - exact he.2.2 o ho - -/-- A compatible assignment satisfying the actual selected crossover blocks satisfies the -actual raw output whenever the source formula holds. Existence and compatibility of this -assignment are separate obligations. -/ -theorem eval_rawFormula_complete_of_compatible (φ : CNF ℕ) (τ : ℕ → Bool) - (σ : Variable → Bool) - (hpaths : ∀ o ∈ Cslib.Logic.PL.occurrences φ, 2 ≤ (occurrencePath φ o).length) - (hcompat : ∀ o ∈ Cslib.Logic.PL.occurrences φ, - ∀ c ∈ wire (crossingSites φ) (occurrencePath φ o), - σ c.1 = τ o.2.2.1 ∧ σ c.2 = τ o.2.2.1) - (hcross : ∀ p ∈ crossingSites φ, - Crossover.splitFormula.eval (fun v => σ (p, some v)) = true) - (h : φ.eval τ = true) : (rawFormula φ).eval σ = true := by - have he := DirectedWire.eval_assemble_complete φ - (fun o => wire (crossingSites φ) (occurrencePath φ o)) ((0, 0), none) τ σ - (fun o ho => wire_ne_nil _ _ (hpaths o ho)) hcompat h - rw [DirectedWire.assemble, eval_append, Bool.and_eq_true] at he - apply (eval_rawFormula_iff φ σ).2 - refine ⟨?_, hcross, ?_⟩ - · rw [map_fst_originalClauses φ (crossingSites φ) ((0, 0), none) hpaths] - exact he.1 - · intro o ho - rw [map_fst_links] - exact (DirectedWire.eval_allLinks_iff φ _ σ).1 he.2 o ho - -end Cslib.Complexity.SAT.PlanarCompile diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/Size.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/Size.lean deleted file mode 100644 index 078a60735..000000000 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/Size.lean +++ /dev/null @@ -1,193 +0,0 @@ -/- -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.PathBounds -public import Complexity.Computability.Complexity.Problems.SAT.Planar.Compile -import Mathlib.Algebra.BigOperators.Ring.List -import Mathlib.Data.List.GetD -import Mathlib.Tactic.Linarith - -/-! -# Size accounting for the finite planarization compiler - -These bounds concern the actual output lists. In particular, crossing sites are selected from -the canonical quadratic cover, rather than supplied as an unbounded certificate. - -## Main definitions - -* `Cslib.Complexity.SAT.PlanarCompile.linkCount`: the number of emitted binary implications. - -## Main results - -* `Cslib.Complexity.SAT.PlanarCompile.crossingSites_length_le`: at most twice the squared - number of input literal incidences. -* `Cslib.Complexity.SAT.PlanarCompile.length_formula`: exact clause accounting. -* `Cslib.Complexity.SAT.PlanarCompile.width_formula`: clause widths are preserved up to three. - -## References - -The accounting is for the original finite construction in `Compile`. --/ - -@[expose] public section - -namespace Cslib.Complexity.SAT.PlanarCompile - -open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal - -/-- Original clauses keep their count. -/ -theorem length_originalClauses (φ : CNF ℕ) (sites : List Point) : - (originalClauses φ sites).length = φ.length := by simp [originalClauses] - -/-- One crossing contributes the fixed 74 clauses. -/ -theorem length_crossingClauses (p : Point) : (crossingClauses p).length = 74 := by - simp [crossingClauses, Crossover.length_splitFormula] - -/-- Every external gap contributes exactly one binary clause. -/ -theorem length_links (sites : List Point) (positive : Bool) (r : Route) : - (links sites positive r).length = r.length - 2 := by - simp only [links, List.length_map, List.consecutivePairs, List.length_zip, - List.length_tail, List.length_dropLast] - omega - -/-- Exact clause count: original clauses, fixed templates, and external links. -/ -theorem length_rawFormula (φ : CNF ℕ) : - (rawFormula φ).length = φ.length + 74 * (crossingSites φ).length + linkCount φ := by - simp [rawFormula, placedClauses, List.length_flatMap, length_originalClauses, - length_crossingClauses, length_links, linkCount, Nat.mul_comm, Nat.add_assoc] - -/-- Compaction keeps the exact output clause count. -/ -theorem length_formula (φ : CNF ℕ) : - (formula φ).length = φ.length + 74 * (crossingSites φ).length + linkCount φ := by - simpa only [formula, CNF.length_compact] using length_rawFormula φ - -/-- The original clause records keep their individual widths. -/ -theorem width_originalClauses {φ : CNF ℕ} {k : ℕ} - (h : ∀ c ∈ φ, c.length ≤ k) (sites : List Point) : - ∀ c ∈ originalClauses φ sites, c.1.length ≤ k := by - intro c hc - obtain ⟨⟨d, i⟩, hd, rfl⟩ := List.mem_map.mp hc - have hd' : d ∈ φ := List.fst_mem_of_mem_zipIdx hd - simpa using h d hd' - -/-- The fixed crossing clauses have width at most three. -/ -theorem width_crossingClauses (p : Point) : - ∀ c ∈ crossingClauses p, c.1.length ≤ 3 := by - intro c hc - obtain ⟨⟨d, i⟩, hd, rfl⟩ := List.mem_map.mp hc - have hd' : d ∈ Crossover.splitFormula := List.fst_mem_of_mem_zipIdx hd - simpa [Clause.relabel] using Crossover.width_splitFormula d hd' - -/-- Every link clause is binary, independent of input validity. -/ -theorem width_links (sites : List Point) (positive : Bool) (r : Route) : - ∀ c ∈ links sites positive r, c.1.length = 2 := by - intro c hc - obtain ⟨e, _, rfl⟩ := List.mem_map.mp hc - cases positive <;> rfl - -/-- Width-three inputs produce width-three output formulas. -/ -theorem width_rawFormula {φ : CNF ℕ} (h : ∀ c ∈ φ, c.length ≤ 3) : - ∀ c ∈ rawFormula φ, c.length ≤ 3 := by - intro c hc - obtain ⟨d, hd, rfl⟩ := List.mem_map.mp hc - rcases List.mem_append.mp hd with hd | hd - · rcases List.mem_append.mp hd with hd | hd - · exact width_originalClauses h _ d hd - · obtain ⟨p, _, hd⟩ := List.mem_flatMap.mp hd - exact width_crossingClauses p d hd - · obtain ⟨o, _, hd⟩ := List.mem_flatMap.mp hd - exact (width_links _ _ _ d hd).le.trans (by decide) - -/-- Compaction preserves the width-three guarantee. -/ -theorem width_formula {φ : CNF ℕ} (h : ∀ c ∈ φ, c.length ≤ 3) : - ∀ c ∈ formula φ, c.length ≤ 3 := by - intro c hc - have hm : c.length ∈ (formula φ).map List.length := List.mem_map_of_mem hc - rw [formula, CNF.map_length_compact] at hm - obtain ⟨d, hd, he⟩ := List.mem_map.mp hm - rw [← he] - exact width_rawFormula h d hd - -/-- An explicit quadratic clause bound in the source incidence graph's combinatorial size. -/ -theorem length_formula_le (φ : CNF ℕ) : - (formula φ).length ≤ 600 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by - have hc := crossingSites_length_le φ - have hl := linkCount_le φ - rw [length_formula] - have hb : budget φ = 80 * (φ.numVars + φ.length) + 10 * φ.vars.length := by - simp [budget, SAT.length_vertices_incidenceGraph, SAT.length_edges_incidenceGraph] - rw [hb] at hl - nlinarith [sq_nonneg (φ.numVars : ℤ), sq_nonneg (φ.length : ℤ), - sq_nonneg (φ.vars.length : ℤ)] - -private theorem original_literal_count (φ : CNF ℕ) (sites : List Point) : - ((originalClauses φ sites).map fun c => c.1.length).sum = φ.vars.length := by - rw [CNF.length_vars] - simp only [originalClauses, List.map_map, Function.comp_def, List.length_map, - List.length_zipIdx] - change ((φ.zipIdx).map (List.length ∘ Prod.fst)).sum = (φ.map List.length).sum - rw [← List.map_map, List.zipIdx_map_fst] - -private theorem crossing_literal_count (p : Point) : - ((crossingClauses p).map fun c => c.1.length).sum = 154 := by - simp only [crossingClauses, List.map_map, Function.comp_def, Clause.relabel, List.length_map] - change ((Crossover.splitFormula.zipIdx.map Prod.fst).map List.length).sum = 154 - decide +kernel - -private theorem links_literal_count (sites : List Point) (positive : Bool) (r : Route) : - ((links sites positive r).map fun c => c.1.length).sum = 2 * (r.length - 2) := by - have hmap : (links sites positive r).map (fun c => c.1.length) = - (links sites positive r).map (fun _ => 2) := - List.map_congr_left fun c hc => width_links sites positive r c hc - rw [hmap] - simp [length_links, Nat.mul_comm] - -/-- Exact literal count, counting repetitions: one original literal, 154 per crossover, -and two per external implication. -/ -theorem length_vars_rawFormula (φ : CNF ℕ) : - (rawFormula φ).vars.length = - φ.vars.length + 154 * (crossingSites φ).length + 2 * linkCount φ := by - rw [CNF.length_vars] - simp only [rawFormula, List.map_map] - change ((placedClauses φ).map fun c => c.1.length).sum = _ - simp only [placedClauses, List.map_append, List.sum_append, List.map_flatMap] - rw [original_literal_count] - have hc : (((crossingSites φ).flatMap fun p => - (crossingClauses p).map fun c => c.1.length)).sum = 154 * (crossingSites φ).length := by - induction crossingSites φ with - | nil => simp - | cons p ps ih => simp [crossing_literal_count, ih, Nat.mul_add, Nat.add_comm] - rw [hc] - have hl : (((Cslib.Logic.PL.occurrences φ).flatMap fun o => - (links (crossingSites φ) o.2.2.2 (occurrencePath φ o)).map fun c => c.1.length)).sum = - 2 * linkCount φ := by - unfold linkCount - induction Cslib.Logic.PL.occurrences φ with - | nil => simp - | cons o os ih => simp [links_literal_count, ih, Nat.mul_add] - rw [hl] - -/-- Compaction keeps the exact literal count. -/ -theorem length_vars_formula (φ : CNF ℕ) : - (formula φ).vars.length = - φ.vars.length + 154 * (crossingSites φ).length + 2 * linkCount φ := by - simpa only [formula, CNF.length_vars, CNF.map_length_compact] using length_vars_rawFormula φ - -/-- An explicit quadratic bound on the number of output literal incidences. -/ -theorem length_vars_formula_le (φ : CNF ℕ) : - (formula φ).vars.length ≤ 1210 * (φ.numVars + φ.length + φ.vars.length + 1) ^ 2 := by - have hc := crossingSites_length_le φ - have hl := linkCount_le φ - rw [length_vars_formula] - have hb : budget φ = 80 * (φ.numVars + φ.length) + 10 * φ.vars.length := by - simp [budget, SAT.length_vertices_incidenceGraph, SAT.length_edges_incidenceGraph] - rw [hb] at hl - nlinarith - -end Cslib.Complexity.SAT.PlanarCompile diff --git a/ComplexityTests/PlanarThreeSATThree.lean b/ComplexityTests/PlanarThreeSATThree.lean index 60a6c6aa2..780409104 100644 --- a/ComplexityTests/PlanarThreeSATThree.lean +++ b/ComplexityTests/PlanarThreeSATThree.lean @@ -33,8 +33,11 @@ example : toDrawnPlanarThreeSATThree [[(0, true), (1, true), (2, true), (3, true example : toDrawnPlanarThreeSATThree [[(0, true)], [(0, false)], [(0, true)], [(0, false)]] = ([[]], [(0, 0)], []) := by decide +kernel --- A valid succinct label takes the actual 32-clause compilation branch. -example : (toPlanarThreeSATThree [[(2 ^ 100, true)]]).length = 32 := by decide +kernel +-- A succinct binary label takes the actual paired compilation branch. +example : (toPlanarThreeSATThree [[(2 ^ 100, true)]]).length = 319 := by + change (SAT.ParsimoniousPlanar.formula [[(2 ^ 100, true)]]).length = 319 + rw [SAT.ParsimoniousPlanar.length_formula] + decide +kernel -- Original 3SAT inputs use the occurrence splitter before the geometric compiler. example : (toPlanarThreeSAT [[(7, true)]]).Satisfiable := by diff --git a/guide/ComplexityGuide/NPCompleteness.lean b/guide/ComplexityGuide/NPCompleteness.lean index cd829fd84..447e7f4b9 100644 --- a/guide/ComplexityGuide/NPCompleteness.lean +++ b/guide/ComplexityGuide/NPCompleteness.lean @@ -242,13 +242,17 @@ Here is the tree, with the reduction for each edge and the completeness theorem count separately. {name}`Cslib.Logic.PL.CNF.toThreeOccurrence` gives each occurrence a fresh copy and connects copies by binary implication cycles. For `m` clauses and `ℓ` literal occurrences it produces exactly `m + ℓ` clauses, `3ℓ` literal occurrences, and `ℓ` distinct - variables. No planarity condition is imposed. + variables. The implication cycles force each copy's value, so the reduction also preserves + the exact number of satisfying assignments ({name}`modelCount_toThreeSATThree`). No planarity + condition is imposed. * Orthogonal planar 3SAT-3 is NP-hard, both when a drawing must exist ({name}`PlanarThreeSATThree_npHard`) and when it is supplied ({name}`DrawnPlanarThreeSATThree_npHard`). Clauses have width at most three, binary clauses are allowed, and each variable has at most three literal occurrences. Routes are simple integer orthogonal paths whose full real supports meet only at common graph endpoints. The native polynomial-time compiler {name}`toDrawnPlanarThreeSAT` starts from ordinary 3SAT. + Its paired implications and local templates have unique extensions, preserving the exact + model count ({name}`modelCount_toPlanarThreeSAT`); only occurring variables are counted. For original size `S = clauses + literal occurrences + 1`, its grid sides are at most `13440*S`; formula size, route count, segment count and Manhattan wire length are quadratic in `S` ({name}`toDrawnPlanarThreeSAT_fits`, {name}`toDrawnPlanarThreeSAT_costs`).