From 209dd3ccc7be1f309c171f01ecb2e3e9321952d1 Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Mon, 26 Oct 2026 07:26:47 -0400 Subject: [PATCH 1/5] doc(roadmap): record ASP framework follow-up --- ROADMAP.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ROADMAP.md b/ROADMAP.md index e8aa6b0e1..2bdc7c2a8 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -187,6 +187,8 @@ index links to canonical definitions rather than keeping a second set. ### Counting and modular classes +- The Another Solution Problem (ASP) framework: solution-preserving reductions with explicit + polynomial-time solution bijections, and applications to SAT and planar SAT. - Counting reductions and further oracle results preserving exact multiplicities; permanent #P-completeness; modular and counting hierarchies; the oracle-algorithm form of Stockmeyer's approximate counting. From 5b65c48394bf529138806b0cfe2d571b797998e8 Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Mon, 26 Oct 2026 07:26:47 -0400 Subject: [PATCH 2/5] feat(CNF): preserve model counts under occurrence splitting 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 | 5 + .../Complexity/Problems/ThreeSATThree.lean | 9 ++ .../Problems/ThreeSATThree/Counting.lean | 75 ++++++++++ Complexity/Foundations/Data/List/Filter.lean | 136 ++++++++++++++++++ Complexity/Foundations/Data/List/Last.lean | 40 ++++++ Complexity/Foundations/Data/List/Range.lean | 36 +++++ .../Propositional/CNF/Compact/ModelCount.lean | 58 ++++++++ .../Logics/Propositional/CNF/Occurrence.lean | 6 + .../Propositional/CNF/ThreeOccurrence.lean | 91 ++++++++++-- ComplexityTests/ThreeSATThreeCounting.lean | 64 +++++++++ 10 files changed, 507 insertions(+), 13 deletions(-) create mode 100644 Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean create mode 100644 Complexity/Foundations/Data/List/Filter.lean create mode 100644 Complexity/Foundations/Data/List/Last.lean create mode 100644 Complexity/Foundations/Data/List/Range.lean create mode 100644 Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean create mode 100644 ComplexityTests/ThreeSATThreeCounting.lean diff --git a/Complexity.lean b/Complexity.lean index e6c16467f..55ff7de36 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -828,6 +828,7 @@ public import Complexity.Computability.Complexity.Problems.TQBF.Closed public import Complexity.Computability.Complexity.Problems.TSP public import Complexity.Computability.Complexity.Problems.ThreeSAT public import Complexity.Computability.Complexity.Problems.ThreeSATThree +public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Counting public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Size public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax public import Complexity.Computability.Complexity.Problems.TwoSAT @@ -1886,10 +1887,13 @@ public import Complexity.Foundations.Data.List.BalancedFold public import Complexity.Foundations.Data.List.Basic public import Complexity.Foundations.Data.List.Counting public import Complexity.Foundations.Data.List.Equiv +public import Complexity.Foundations.Data.List.Filter public import Complexity.Foundations.Data.List.Fold +public import Complexity.Foundations.Data.List.Last public import Complexity.Foundations.Data.List.Lex public import Complexity.Foundations.Data.List.Lookup public import Complexity.Foundations.Data.List.OfFn +public import Complexity.Foundations.Data.List.Range public import Complexity.Foundations.Data.List.SelectDistinct public import Complexity.Foundations.Data.Matrix.Binary public import Complexity.Foundations.Data.Matrix.Permanent @@ -2080,6 +2084,7 @@ public import Complexity.Logics.FirstOrder.Tuple public import Complexity.Logics.Propositional.CNF public import Complexity.Logics.Propositional.CNF.Coding public import Complexity.Logics.Propositional.CNF.Compact +public import Complexity.Logics.Propositional.CNF.Compact.ModelCount public import Complexity.Logics.Propositional.CNF.Compact.Relabel public import Complexity.Logics.Propositional.CNF.ExactlyOne public import Complexity.Logics.Propositional.CNF.Gadgets diff --git a/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean b/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean index bfa06d5a0..b2cbc9f37 100644 --- a/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean +++ b/Complexity/Computability/Complexity/Problems/ThreeSATThree.lean @@ -42,6 +42,7 @@ This endpoint imposes no planarity condition. ## Main results * `Cslib.Complexity.mem_ThreeSATThree_toThreeSATThree_iff`: correctness of the reduction. +* `Cslib.Complexity.modelCount_toThreeSATThree`: preservation of counts for width-three inputs. * `Cslib.Complexity.computableInPolyTime_toThreeSATThree`: native polynomial time under `encCNF`. * `Cslib.Complexity.ThreeSATThree_npComplete`: 3SAT-3 is NP-complete. @@ -149,6 +150,14 @@ theorem length_vars_toThreeSATThree (φ : CNF ℕ) (hφ : ∀ c ∈ φ, c.length have hg : φ.all (fun c => decide (c.length ≤ 3)) = true := by simpa using hφ simp [toThreeSATThree, hg, CNF.vars_relabel, CNF.length_vars_toThreeOccurrence] +/-- For a width-three input, occurrence splitting and injective numbering preserve the number of +satisfying assignments on occurring variables. -/ +theorem modelCount_toThreeSATThree (φ : CNF ℕ) (hφ : ∀ c ∈ φ, c.length ≤ 3) : + (toThreeSATThree φ).modelCount = φ.modelCount := by + have hg : φ.all (fun c => decide (c.length ≤ 3)) = true := by simpa using hφ + simp only [toThreeSATThree, hg, ↓reduceIte] + rw [CNF.modelCount_relabel ThreeSATThree.numberCopy_injective, CNF.modelCount_toThreeOccurrence] + /-- The total splitter is polynomial-time under binary `encCNF`. -/ @[fun_prop] theorem computableInPolyTime_toThreeSATThree : diff --git a/Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean b/Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean new file mode 100644 index 000000000..b6e9f2dbe --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/ThreeSATThree/Counting.lean @@ -0,0 +1,75 @@ +/- +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.Classes.SharpP.Completeness +public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Size +public import Complexity.Computability.Complexity.Problems.ThreeSATThree.Syntax + +/-! +# Parsimonious occurrence reduction for 3SAT + +The existing occurrence splitter preserves the number of satisfying assignments. Each source +variable has one value on every copy in its implication cycle, and numbering copies is injective. +The counting problems below count only occurring variables and return zero outside their syntax. +They reuse `CNF.modelCount` and the existing syntax guards rather than introducing new assignment +or satisfiability semantics. + +## Main definitions + +* `Cslib.Complexity.SharpThreeSAT`: model count for width-at-most-three CNF, zero otherwise. +* `Cslib.Complexity.SharpThreeSATThree`: model count with the additional three-occurrence bound. + +## Main results + +* `Cslib.Complexity.sharpThreeSATThree_toThreeSATThree`: exact counts for the total compiler. +* `Cslib.Complexity.parsimoniousReducible_SharpThreeSAT_SharpThreeSATThree`: the existing + polynomial-time compiler is a parsimonious reduction. + +## References + +The occurrence construction and its source credit are documented in `ThreeSATThree`. +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Cslib.Logic.PL + +/-- Count satisfying assignments of width-at-most-three CNF; reject other syntax with count zero. +Only variables occurring in the formula are counted. -/ +def SharpThreeSAT (φ : CNF ℕ) : ℕ := + if φ.all (fun c => decide (c.length ≤ 3)) then φ.modelCount else 0 + +/-- Count satisfying assignments of width-three, occurrence-three CNF; reject other syntax with +count zero. Repetitions are literal positions, as in `ThreeSATThree.syntaxCheck`. -/ +def SharpThreeSATThree (φ : CNF ℕ) : ℕ := + if ThreeSATThree.syntaxCheck φ then φ.modelCount else 0 + +/-- The total occurrence compiler preserves the count, including rejected inputs. -/ +theorem sharpThreeSATThree_toThreeSATThree (φ : CNF ℕ) : + SharpThreeSATThree (toThreeSATThree φ) = SharpThreeSAT φ := by + have hout := (ThreeSATThree.syntaxCheck_iff (toThreeSATThree φ)).2 + ⟨width_toThreeSATThree φ, count_vars_toThreeSATThree_le φ⟩ + simp only [SharpThreeSATThree, hout, ↓reduceIte] + by_cases hw : φ.all (fun c => decide (c.length ≤ 3)) = true + · have hwidth : ∀ c ∈ φ, c.length ≤ 3 := by + simpa only [List.all_eq_true, decide_eq_true_eq] using hw + rw [modelCount_toThreeSATThree φ hwidth] + simp only [SharpThreeSAT, hw, ↓reduceIte] + · simp only [SharpThreeSAT, toThreeSATThree, hw, Bool.false_eq_true, ite_false] + decide + +/-- The already-certified polynomial-time 3SAT-to-3SAT-3 compiler is parsimonious. -/ +theorem parsimoniousReducible_SharpThreeSAT_SharpThreeSATThree : + ParsimoniousReducible encCNF encCNF SharpThreeSAT SharpThreeSATThree := + ⟨toThreeSATThree, computableInPolyTime_toThreeSATThree, + fun φ => (sharpThreeSATThree_toThreeSATThree φ).symm⟩ + +end Cslib.Complexity diff --git a/Complexity/Foundations/Data/List/Filter.lean b/Complexity/Foundations/Data/List/Filter.lean new file mode 100644 index 000000000..1af02195a --- /dev/null +++ b/Complexity/Foundations/Data/List/Filter.lean @@ -0,0 +1,136 @@ +/- +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.Init +import Mathlib.Data.List.GetD + +/-! +# Indexed multiplicity under list membership filtering + +These statements count positions, so repeated equal lists still contribute separately. +They are generalized from the canonical incidence-path occupancy proofs. + +## Main results + +* `List.exists_pair_indices_of_two_le_filter_contains`. +* `List.two_le_filter_contains_of_indices`. +* `List.exists_other_index_of_two_le_filter_contains`. +-/ + +@[expose] public section + +namespace List + +/-- Two filtered memberships occur at distinct indices, even for repeated lists. -/ +theorem exists_pair_indices_of_two_le_filter_contains {α : Type*} [DecidableEq α] + (rs : List (List α)) (p : α) + (hlen : 2 ≤ (rs.filter fun r => r.contains p).length) : + ∃ (i j : ℕ) (hi : i < rs.length) (hj : j < rs.length), + i ≠ j ∧ p ∈ rs[i] ∧ p ∈ rs[j] := by + induction rs with + | nil => simp at hlen + | cons r rs ih => + by_cases hp : p ∈ r + · have hne : (rs.filter fun r => r.contains p) ≠ [] := by + intro h + have hf : ((r :: rs).filter fun r => r.contains p) = [r] := by + have hpred : r.contains p = true := by simpa using hp + simp only [List.filter_cons, hpred, ↓reduceIte, h] + rw [hf] at hlen + simp at hlen + cases hf : rs.filter (fun r => r.contains p) with + | nil => exact False.elim (hne hf) + | cons t ts => + have ht : t ∈ rs.filter (fun r => r.contains p) := by rw [hf]; simp + obtain ⟨htmem, htp⟩ := List.mem_filter.mp ht + obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp htmem + exact ⟨0, j + 1, by simp, by simpa using hj, by omega, hp, by simpa using htp⟩ + · have hf : ((r :: rs).filter fun r => r.contains p) = rs.filter (fun r => r.contains p) := by + simp [hp] + rw [hf] at hlen + obtain ⟨i, j, hi, hj, hij, hpi, hpj⟩ := ih hlen + exact ⟨i + 1, j + 1, by simpa using hi, by simpa using hj, by omega, hpi, hpj⟩ + +/-- Two distinct indices witnessing membership give at least two filtered entries. -/ +theorem two_le_filter_contains_of_indices {α : Type*} [DecidableEq α] + (rs : List (List α)) (p : α) {i j : ℕ} + (hi : i < rs.length) (hj : j < rs.length) (hij : i ≠ j) + (hpi : p ∈ rs[i]) (hpj : p ∈ rs[j]) : + 2 ≤ (rs.filter fun r => r.contains p).length := by + induction rs generalizing i j with + | nil => simp at hi + | cons r rs ih => + cases i with + | zero => + cases j with + | zero => exact False.elim (hij rfl) + | succ j => + have hj' : j < rs.length := by simpa using hj + have hm : rs[j] ∈ rs.filter (fun r => r.contains p) := + List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hj), + List.contains_iff_mem.mpr hpj⟩ + obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm + have hphead : p ∈ r := hpi + simp only [List.filter_cons, List.contains_iff_mem.mpr hphead, + ite_true, List.length_cons] + omega + | succ i => + cases j with + | zero => + have hi' : i < rs.length := by simpa using hi + have hm : rs[i] ∈ rs.filter (fun r => r.contains p) := + List.mem_filter.mpr ⟨List.getElem_mem (by simpa using hi), + List.contains_iff_mem.mpr hpi⟩ + obtain ⟨k, hk, _⟩ := List.mem_iff_getElem.mp hm + have hphead : p ∈ r := hpj + simp only [List.filter_cons, List.contains_iff_mem.mpr hphead, + ite_true, List.length_cons] + omega + | succ j => + have ht := ih (by simpa using hi) (by simpa using hj) (by omega) hpi hpj + rw [List.filter_cons] + split_ifs + · simp only [List.length_cons] + omega + · exact ht + +/-- At least two filtered memberships give an index different from any given index. -/ +theorem exists_other_index_of_two_le_filter_contains {α : Type*} [DecidableEq α] + (rs : List (List α)) (p : α) (i : ℕ) (hi : i < rs.length) + (hcount : 2 ≤ (rs.filter fun r => r.contains p).length) : + ∃ j, ∃ hj : j < rs.length, j ≠ i ∧ p ∈ rs[j] := by + induction rs generalizing i with + | nil => simp at hi + | cons r rs ih => + cases i with + | zero => + have hpos : 0 < (rs.filter fun r => r.contains p).length := by + rw [List.filter_cons] at hcount + split_ifs at hcount + · simp only [List.length_cons] at hcount + omega + · omega + obtain ⟨s, hs⟩ := List.exists_mem_of_length_pos hpos + have hm := List.mem_filter.mp hs + obtain ⟨j, hj, hsj⟩ := List.mem_iff_getElem.mp hm.1 + refine ⟨j + 1, by simp only [List.length_cons]; omega, by omega, ?_⟩ + simp only [List.getElem_cons_succ] + rw [hsj] + exact List.contains_iff_mem.mp hm.2 + | succ i => + by_cases hmem : r.contains p = true + · exact ⟨0, by simp, by omega, by simpa using List.contains_iff_mem.mp hmem⟩ + · have ht : 2 ≤ (rs.filter fun r => r.contains p).length := by + have hp : p ∉ r := fun hp => hmem (List.contains_iff_mem.mpr hp) + simpa [List.filter_cons, hp] using hcount + obtain ⟨j, hj, hji, hp⟩ := ih i (by simp only [List.length_cons] at hi; omega) ht + exact ⟨j + 1, by simp only [List.length_cons]; omega, by omega, by simpa using hp⟩ + + +end List diff --git a/Complexity/Foundations/Data/List/Last.lean b/Complexity/Foundations/Data/List/Last.lean new file mode 100644 index 000000000..b0781335c --- /dev/null +++ b/Complexity/Foundations/Data/List/Last.lean @@ -0,0 +1,40 @@ +/- +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.Init +import Mathlib.Data.List.GetD + +/-! +# Defaulted last-element lookup + +The default is unused for a nonempty list. The proof is moved from the path semantics. + +## Main results + +* `List.getLastD_eq_getElem`. +-/ + +@[expose] public section + +namespace List + +/-- A nonempty list's defaulted last lookup is its final indexed element. -/ +theorem getLastD_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] + + +end List diff --git a/Complexity/Foundations/Data/List/Range.lean b/Complexity/Foundations/Data/List/Range.lean new file mode 100644 index 000000000..d2770bd73 --- /dev/null +++ b/Complexity/Foundations/Data/List/Range.lean @@ -0,0 +1,36 @@ +/- +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.Init +import Mathlib.Data.List.GetD +import Mathlib.Data.List.Nodup + +/-! +# First indices in natural-number ranges + +This index identity is shared by source endpoint and path geometry certificates. + +## Main results + +* `List.idxOf_range_of_lt`. +-/ + +@[expose] public section + +namespace List + +/-- An in-range natural number occurs at its own position in `range`. -/ +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 + + +end List diff --git a/Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean b/Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean new file mode 100644 index 000000000..83e40eca3 --- /dev/null +++ b/Complexity/Logics/Propositional/CNF/Compact/ModelCount.lean @@ -0,0 +1,58 @@ +/- +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.Logics.Propositional.CNF.Compact +public import Complexity.Logics.Propositional.CNF.ModelCount +import Mathlib.Data.List.GetD + +/-! +# Model counts under compact variable numbering + +First-occurrence numbering preserves the number of satisfying assignments on the variables +occurring in a formula. The variable type may be infinite or empty. + +## Main results + +* `Cslib.Logic.PL.CNF.modelCount_compact`: compaction preserves the model count. + +## References + +This is an elementary counting property of the existing compaction construction. +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF + +variable {V : Type*} [DecidableEq V] + +/-- First-occurrence numbering preserves the number of satisfying assignments, including for +empty formulas, empty clauses, and repeated literal occurrences. -/ +theorem modelCount_compact (φ : CNF V) : φ.compact.modelCount = φ.modelCount := by + refine modelCount_eq_card_filter (fun σ (v : φ.vars.toFinset) => σ (φ.vars.idxOf (v : V))) + (fun τ => φ.eval (φ.extendAssignment τ) = true) (fun σ τ _ _ => ?_) fun τ => ?_ + · rw [compact, vars_relabel, List.forall_mem_map, funext_iff, Subtype.forall] + simp only [List.mem_toFinset] + · constructor + · intro hτ + let σ : ℕ → Bool := fun i => φ.vars[i]?.elim false (φ.extendAssignment τ) + have he : ∀ v ∈ φ.vars, σ (φ.vars.idxOf v) = φ.extendAssignment τ v := by + intro v hv + simp [σ, List.getElem?_idxOf hv] + refine ⟨σ, ?_, funext fun v => ?_⟩ + · rw [compact, eval_relabel] + exact (eval_congr he).trans hτ + · exact (he v (List.mem_toFinset.1 v.2)).trans + (extendAssignment_of_mem _ (List.mem_toFinset.1 v.2)) + · rintro ⟨σ, hσ, rfl⟩ + rw [compact, eval_relabel] at hσ + rw [← hσ] + exact eval_extendAssignment_restrict φ (σ ∘ φ.vars.idxOf) + +end Cslib.Logic.PL.CNF diff --git a/Complexity/Logics/Propositional/CNF/Occurrence.lean b/Complexity/Logics/Propositional/CNF/Occurrence.lean index 8d299e11d..17ba7e0ba 100644 --- a/Complexity/Logics/Propositional/CNF/Occurrence.lean +++ b/Complexity/Logics/Propositional/CNF/Occurrence.lean @@ -24,6 +24,12 @@ The proof follows the indexed-copy uniqueness argument in `CNF.ThreeOccurrence`. namespace Cslib.Logic.PL +/-- The variable named by an indexed literal occurrence occurs in the formula. -/ +theorem variable_mem_of_mem_occurrences {V : Type*} {φ : CNF V} {o : Occurrence V} + (ho : o ∈ occurrences φ) : o.2.2.1 ∈ φ.vars := by + rw [← map_occurrences] + exact List.mem_map_of_mem ho + /-- Clause and literal indices distinguish every source occurrence, including repeated literals. -/ theorem occurrences_nodup {V : Type*} (φ : CNF V) : (occurrences φ).Nodup := by rw [occurrences, List.nodup_flatMap] diff --git a/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean b/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean index edd3bb974..9c714a4f0 100644 --- a/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean +++ b/Complexity/Logics/Propositional/CNF/ThreeOccurrence.lean @@ -35,7 +35,9 @@ This construction uses ordinary CNF formulas and Boolean assignments. ## Main results +* `Cslib.Logic.PL.CNF.eval_toThreeOccurrence_iff`: correspondence of satisfying assignments. * `Cslib.Logic.PL.CNF.satisfiable_toThreeOccurrence`: equisatisfiability. +* `Cslib.Logic.PL.CNF.modelCount_toThreeOccurrence`: preservation of satisfying-assignment counts. * `Cslib.Logic.PL.CNF.width_toThreeOccurrence`: preservation of width bounds of at least two. * `Cslib.Logic.PL.CNF.count_vars_toThreeOccurrence_le`: at most three literal occurrences. * `Cslib.Logic.PL.CNF.length_toThreeOccurrence`, @@ -114,11 +116,14 @@ theorem copies_agree [DecidableEq V] {φ : CNF V} {τ : V × ℕ × ℕ → Bool · simp [occurrenceCopies, hx] · simp [occurrenceCopies, hy, he] -/-- Occurrence splitting preserves satisfiability, including empty clauses and formulas. -/ -theorem satisfiable_toThreeOccurrence [DecidableEq V] (φ : CNF V) : - φ.toThreeOccurrence.Satisfiable ↔ φ.Satisfiable := by +/-- An assignment satisfies the split formula exactly when its occurring copies agree with a +satisfying assignment of the original formula. Together with `copies_agree`, this retains the +assignment correspondence, rather than just equisatisfiability. -/ +theorem eval_toThreeOccurrence_iff [DecidableEq V] (φ : CNF V) (τ : V × ℕ × ℕ → Bool) : + φ.toThreeOccurrence.eval τ = true ↔ + ∃ σ : V → Bool, φ.eval σ = true ∧ ∀ x ∈ φ.occurrenceClauses.vars, σ x.1 = τ x := by constructor - · rintro ⟨τ, hτ⟩ + · intro hτ classical let σ : V → Bool := fun v => if h : ∃ x ∈ φ.occurrenceClauses.vars, x.1 = v then τ (Classical.choose h) else false @@ -127,21 +132,33 @@ theorem satisfiable_toThreeOccurrence [DecidableEq V] (φ : CNF V) : have hex : ∃ y ∈ φ.occurrenceClauses.vars, y.1 = x.1 := ⟨x, hx, rfl⟩ simp only [σ, dite_eq_left hex] exact copies_agree hτ (Classical.choose_spec hex).1 hx (Classical.choose_spec hex).2 - refine ⟨σ, ?_⟩ + refine ⟨σ, ?_, he⟩ rw [← eval_occurrenceClauses] have ht := hτ simp only [toThreeOccurrence, eval_append, Bool.and_eq_true] at ht exact (eval_congr he).trans ht.1 - · rintro ⟨σ, hσ⟩ - refine ⟨σ ∘ Prod.fst, ?_⟩ - rw [toThreeOccurrence, eval_append, Bool.and_eq_true, eval_occurrenceClauses] - refine ⟨hσ, (eval_flatMap_eq_true_iff _ _ _).2 fun v _ => ?_⟩ + · rintro ⟨σ, hσ, he⟩ + rw [toThreeOccurrence, eval_append, Bool.and_eq_true] + refine ⟨(eval_congr he).symm.trans ((eval_occurrenceClauses φ σ).trans hσ), + (eval_flatMap_eq_true_iff _ _ _).2 fun v _ => ?_⟩ rw [eval_implicationCycle] intro x hx y hy - have hx := (List.mem_filter.1 hx).2 - have hy := (List.mem_filter.1 hy).2 - simp only [beq_iff_eq] at hx hy - simp [hx, hy] + obtain ⟨hx, hxv⟩ := List.mem_filter.1 hx + obtain ⟨hy, hyv⟩ := List.mem_filter.1 hy + simp only [beq_iff_eq] at hxv hyv + calc τ x = σ x.1 := (he x hx).symm + _ = σ y.1 := congrArg σ (hxv.trans hyv.symm) + _ = τ y := he y hy + +/-- Occurrence splitting preserves satisfiability, including empty clauses and formulas. -/ +theorem satisfiable_toThreeOccurrence [DecidableEq V] (φ : CNF V) : + φ.toThreeOccurrence.Satisfiable ↔ φ.Satisfiable := by + constructor + · rintro ⟨τ, hτ⟩ + obtain ⟨σ, hσ, _⟩ := (eval_toThreeOccurrence_iff φ τ).1 hτ + exact ⟨σ, hσ⟩ + · rintro ⟨σ, hσ⟩ + exact ⟨σ ∘ Prod.fst, (eval_toThreeOccurrence_iff φ _).2 ⟨σ, hσ, fun _ _ => rfl⟩⟩ /-- Cycles are binary, so a width bound of at least two is preserved. -/ theorem width_toThreeOccurrence [DecidableEq V] {φ : CNF V} {k : ℕ} (hk : 2 ≤ k) @@ -271,4 +288,52 @@ theorem numVars_toThreeOccurrence [DecidableEq V] (φ : CNF V) : rw [numVars, he, List.toFinset_card_of_nodup (nodup_vars_occurrenceClauses φ)] simpa using congrArg List.length (map_fst_vars_occurrenceClauses φ) +/-- Occurrence splitting preserves the number of satisfying assignments on occurring variables, +including empty formulas, empty clauses, and repeated literals. -/ +theorem modelCount_toThreeOccurrence [DecidableEq V] (φ : CNF V) : + φ.toThreeOccurrence.modelCount = φ.modelCount := by + classical + have hmem (x : V × ℕ × ℕ) : + x ∈ φ.toThreeOccurrence.vars ↔ x ∈ φ.occurrenceClauses.vars := by + simp only [← List.count_pos_iff, count_vars_toThreeOccurrence] + omega + have hfst {x : V × ℕ × ℕ} (hx : x ∈ φ.occurrenceClauses.vars) : x.1 ∈ φ.vars := by + rw [← map_fst_vars_occurrenceClauses] + exact List.mem_map.2 ⟨x, hx, rfl⟩ + have hex (v : φ.vars.toFinset) : ∃ x ∈ φ.occurrenceClauses.vars, x.1 = v := by + apply List.mem_map.1 + simpa only [map_fst_vars_occurrenceClauses] using List.mem_toFinset.1 v.2 + let copy (v : φ.vars.toFinset) : V × ℕ × ℕ := Classical.choose (hex v) + have hcopy (v : φ.vars.toFinset) : copy v ∈ φ.occurrenceClauses.vars ∧ (copy v).1 = v := + Classical.choose_spec (hex v) + let f (τ : V × ℕ × ℕ → Bool) (v : φ.vars.toFinset) : Bool := τ (copy v) + refine modelCount_eq_card_filter f (fun τ => φ.eval (φ.extendAssignment τ) = true) + (fun σ τ hσ hτ => ?_) fun τ => ?_ + · constructor + · intro he x hx + have hx := (hmem x).1 hx + let v : φ.vars.toFinset := ⟨x.1, List.mem_toFinset.2 (hfst hx)⟩ + calc σ x = σ (copy v) := copies_agree hσ hx (hcopy v).1 (hcopy v).2.symm + _ = τ (copy v) := congrFun he v + _ = τ x := copies_agree hτ (hcopy v).1 hx (hcopy v).2 + · intro he + exact funext fun v => he (copy v) ((hmem _).2 (hcopy v).1) + · constructor + · intro hτ + refine ⟨φ.extendAssignment τ ∘ Prod.fst, ?_, funext fun v => ?_⟩ + · exact (eval_toThreeOccurrence_iff φ _).2 ⟨φ.extendAssignment τ, hτ, fun _ _ => rfl⟩ + · change φ.extendAssignment τ (copy v).1 = τ v + rw [(hcopy v).2, extendAssignment_of_mem _ (List.mem_toFinset.1 v.2)] + · rintro ⟨σ, hσ, rfl⟩ + rw [← eval_occurrenceClauses] + have he : ∀ x ∈ φ.occurrenceClauses.vars, + (φ.extendAssignment (f σ) ∘ Prod.fst) x = σ x := by + intro x hx + change φ.extendAssignment (f σ) x.1 = σ x + rw [extendAssignment_of_mem _ (hfst hx)] + exact copies_agree hσ (hcopy _).1 hx (hcopy _).2 + have ht := hσ + simp only [toThreeOccurrence, eval_append, Bool.and_eq_true] at ht + exact (eval_congr he).trans ht.1 + end Cslib.Logic.PL.CNF diff --git a/ComplexityTests/ThreeSATThreeCounting.lean b/ComplexityTests/ThreeSATThreeCounting.lean new file mode 100644 index 000000000..270dafc50 --- /dev/null +++ b/ComplexityTests/ThreeSATThreeCounting.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +import Complexity.Computability.Complexity.Problems.ThreeSATThree +import Complexity.Computability.Complexity.Problems.ThreeSATThree.Counting + +/-! # Exact counts under occurrence splitting and numbering -/ + +open Cslib.Logic.PL Cslib.Complexity + +/-- The empty formula has one assignment on its empty variable set. -/ +example : (toThreeSATThree []).modelCount = 1 := by + rw [modelCount_toThreeSATThree _ (by simp)] + decide + +/-- An empty clause has no satisfying assignment. -/ +example : (toThreeSATThree [[]]).modelCount = 0 := by + rw [modelCount_toThreeSATThree _ (by simp)] + decide + +/-- Repeated literals within a clause do not multiply the satisfying-assignment count. -/ +example : (toThreeSATThree [[(0, true), (0, true), (0, true)]]).modelCount = 1 := by + rw [modelCount_toThreeSATThree _ (by simp)] + decide + +/-- A singleton cycle introduces no additional choice for a forced variable. -/ +example : (toThreeSATThree [[(7, true)]]).modelCount = 1 := by + rw [modelCount_toThreeSATThree _ (by simp)] + decide + +/-- Several occurrences per variable preserve all three satisfying assignments of a disjunction. -/ +example : (toThreeSATThree + [[(0, true), (1, true)], [(0, true), (1, true)]]).modelCount = 3 := by + rw [modelCount_toThreeSATThree _ (by simp)] + decide + +/-- The unnumbered splitter preserves counts even beyond width three. -/ +example : (CNF.toThreeOccurrence + [[(0, true), (0, false), (0, true), (0, false)]]).modelCount = 2 := by + rw [CNF.modelCount_toThreeOccurrence] + decide + +/-- The numbered reduction rejects a width-four input, so its width hypothesis is necessary. -/ +example : (toThreeSATThree + [[(0, true), (0, false), (0, true), (0, false)]]).modelCount = 0 := by + decide + +/-- A satisfiable width-four formula has raw models but is rejected by the 3SAT count. -/ +example : SharpThreeSAT [[(0, true), (0, false), (0, true), (0, false)]] = 0 := by decide + +/-- The source count accepts width three even when the occurrence bound fails. -/ +example : SharpThreeSAT [[(0, true), (0, true), (0, true)], [(0, true)]] = 1 := by decide + +/-- The target count rejects the same formula for its fourth literal occurrence. -/ +example : SharpThreeSATThree [[(0, true), (0, true), (0, true)], [(0, true)]] = 0 := by decide + +/-- The actual compiler preserves that source count after repairing the occurrence bound. -/ +example : SharpThreeSATThree + (toThreeSATThree [[(0, true), (0, true), (0, true)], [(0, true)]]) = 1 := by + rw [sharpThreeSATThree_toThreeSATThree] + decide From 2ef95572326f53e35e84cae23f45f7db1f2bf726 Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Mon, 26 Oct 2026 07:29:46 -0400 Subject: [PATCH 3/5] doc(references): cite parsimonious planar SAT --- references.bib | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/references.bib b/references.bib index 422c12241..98a7ca2bd 100644 --- a/references.bib +++ b/references.bib @@ -2029,6 +2029,17 @@ @article{Huang2019 doi = {10.4007/annals.2019.190.3.6} } +@article{HuntMaratheRadhakrishnanStearns1998, + author = {Hunt III, Harry B. and Marathe, Madhav V. and Radhakrishnan, Venkatesh and Stearns, Richard E.}, + title = {The Complexity of Planar Counting Problems}, + journal = {SIAM Journal on Computing}, + volume = {27}, + number = {4}, + pages = {1142--1167}, + year = {1998}, + doi = {10.1137/S0097539793304601} +} + @inproceedings{Ilango2020, author = {Ilango, Rahul}, title = {Approaching {MCSP} from Above and Below: Hardness for a Conditional Variant and {$\mathsf{AC}^0[p]$}}, From 82860094aa1363005e1674471d2a342dc429dbca Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Mon, 26 Oct 2026 07:29:46 -0400 Subject: [PATCH 4/5] feat(planar-SAT): certify paired wires and unique gadget extensions 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 | 7 + .../Problems/SAT/Planar/OrdinaryRing.lean | 269 +++++++++++++++++ .../Geometry/Orthogonal/PairedBoundary.lean | 59 ++++ .../Geometry/Orthogonal/PairedPorts.lean | 153 ++++++++++ .../Geometry/Orthogonal/PairedSpokes.lean | 96 ++++++ .../CNF/Planar/CrossoverCounting.lean | 131 ++++++++ .../CNF/Planar/PairedCrossover.lean | 283 ++++++++++++++++++ .../Propositional/CNF/Planar/PairedWire.lean | 188 ++++++++++++ ComplexityTests/PairedCrossover.lean | 39 +++ ComplexityTests/PairedWire.lean | 56 ++++ ComplexityTests/PlanarCrossoverCounting.lean | 50 ++++ 11 files changed, 1331 insertions(+) create mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean create mode 100644 Complexity/Foundations/Geometry/Orthogonal/PairedBoundary.lean create mode 100644 Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean create mode 100644 Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean create mode 100644 Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean create mode 100644 Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean create mode 100644 Complexity/Logics/Propositional/CNF/Planar/PairedWire.lean create mode 100644 ComplexityTests/PairedCrossover.lean create mode 100644 ComplexityTests/PairedWire.lean create mode 100644 ComplexityTests/PlanarCrossoverCounting.lean diff --git a/Complexity.lean b/Complexity.lean index 55ff7de36..719aee534 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -808,6 +808,7 @@ public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverL 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.Paths public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths.Occupancy public import Complexity.Computability.Complexity.Problems.SAT.Planar.PolyTime @@ -1951,6 +1952,9 @@ public import Complexity.Foundations.Geometry.Orthogonal.Endpoint public import Complexity.Foundations.Geometry.Orthogonal.Layout public import Complexity.Foundations.Geometry.Orthogonal.Macrocell public import Complexity.Foundations.Geometry.Orthogonal.Neighborhood +public import Complexity.Foundations.Geometry.Orthogonal.PairedBoundary +public import Complexity.Foundations.Geometry.Orthogonal.PairedPorts +public import Complexity.Foundations.Geometry.Orthogonal.PairedSpokes public import Complexity.Foundations.Geometry.Orthogonal.Separation public import Complexity.Foundations.Geometry.Orthogonal.Simple public import Complexity.Foundations.Geometry.Orthogonal.Subdivision @@ -2094,8 +2098,11 @@ public import Complexity.Logics.Propositional.CNF.ModelCount public import Complexity.Logics.Propositional.CNF.Occurrence public import Complexity.Logics.Propositional.CNF.Parity public import Complexity.Logics.Propositional.CNF.Planar.Crossover +public import Complexity.Logics.Propositional.CNF.Planar.CrossoverCounting public import Complexity.Logics.Propositional.CNF.Planar.CrossoverSplit public import Complexity.Logics.Propositional.CNF.Planar.DirectedWire +public import Complexity.Logics.Propositional.CNF.Planar.PairedCrossover +public import Complexity.Logics.Propositional.CNF.Planar.PairedWire public import Complexity.Logics.Propositional.CNF.PolyTime public import Complexity.Logics.Propositional.CNF.ThreeCNF public import Complexity.Logics.Propositional.CNF.ThreeCNF.PolyTime diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean new file mode 100644 index 000000000..7a496be62 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean @@ -0,0 +1,269 @@ +/- +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.Foundations.Geometry.Orthogonal.PairedPorts +public import Complexity.Logics.Propositional.CNF.ImplicationCycle +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.SplitIfs + +/-! +# An eight-port ordinary signal ring + +Eight binary implications follow the perimeter of `[20,220]²`, forcing all eight +variables to agree. Every variable has two internal literal occurrences, leaving +one external occurrence for its paired access. Unused accesses introduce no freedom. +The sixteen incidence routes are straight and have total Manhattan length 800. + +## Main definitions + +* `Variable`, `cyclicOrder`, `formula`: the fixed implication ring. +* `variablePosition`, `clausePositions`, `incidenceRoutes`: its explicit drawing. + +## Main results + +* `eval_formula_iff`, `eval_constant`: all ports carry one freely chosen bit. +* `internal_occurrences`: exactly two internal literal occurrences per port. + +## References + +This fixed template is original and reuses `CNF.implicationCycle`. +-/ + +@[expose] public section + +namespace Cslib.Complexity.SAT.OrdinaryRing + +open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal + +/-- One variable for each side and lane of the common paired-port interface. -/ +abbrev Variable := Fin 4 × Fin 2 + +/-- Cyclic geometric order, traversing the inner square clockwise. -/ +def cyclicOrder : List Variable := + [(0, 0), (0, 1), (3, 0), (3, 1), (1, 1), (1, 0), (2, 1), (2, 0)] + +/-- The eight directed implications closing the signal ring. -/ +def formula : CNF Variable := implicationCycle cyclicOrder + +/-- The eight common inner access positions. -/ +def variablePosition (v : Variable) : Point := PairedPorts.variablePosition v.1 v.2 + +/-- Clause positions in precisely the order of the eight implications. -/ +def clausePositions : List Point := + [(20, 120), (20, 220), (120, 220), (220, 220), + (220, 120), (220, 20), (120, 20), (20, 20)] + +/-- Indexed clause position, with an irrelevant out-of-range default. -/ +def clausePosition (i : ℕ) : Point := clausePositions.getD i (0, 0) + +/-- The sixteen clause-to-variable incidences, in clause and literal order. -/ +def incidenceRoutes : List (ℕ × Variable × Route) := + [(0, (0, 0), [(20, 120), (20, 110)]), + (0, (0, 1), [(20, 120), (20, 130)]), + (1, (0, 1), [(20, 220), (20, 130)]), + (1, (3, 0), [(20, 220), (110, 220)]), + (2, (3, 0), [(120, 220), (110, 220)]), + (2, (3, 1), [(120, 220), (130, 220)]), + (3, (3, 1), [(220, 220), (130, 220)]), + (3, (1, 1), [(220, 220), (220, 130)]), + (4, (1, 1), [(220, 120), (220, 130)]), + (4, (1, 0), [(220, 120), (220, 110)]), + (5, (1, 0), [(220, 20), (220, 110)]), + (5, (2, 1), [(220, 20), (130, 20)]), + (6, (2, 1), [(120, 20), (130, 20)]), + (6, (2, 0), [(120, 20), (110, 20)]), + (7, (2, 0), [(20, 20), (110, 20)]), + (7, (0, 0), [(20, 20), (20, 110)])] + +/-- Common graph endpoints are the only permitted contacts between distinct incidences. -/ +def commonEndpoints (e f : ℕ × Variable × Route) : List Point := + (if e.1 = f.1 then [clausePosition e.1] else []) ++ + (if e.2.1 = f.2.1 then [variablePosition e.2.1] else []) + +/-- All eight port variables occur in the cycle. -/ +theorem mem_cyclicOrder : ∀ v : Variable, v ∈ cyclicOrder := by decide +kernel + +/-- The ring holds exactly when every port carries the value of the first port. -/ +theorem eval_formula_iff (σ : Variable → Bool) : + formula.eval σ = true ↔ ∀ v, σ v = σ (0, 0) := by + rw [formula, eval_implicationCycle] + constructor + · intro h v + exact h v (mem_cyclicOrder v) (0, 0) (mem_cyclicOrder (0, 0)) + · intro h x _ y _ + exact (h x).trans (h y).symm + +/-- Either constant assignment satisfies the ring. -/ +theorem eval_constant (b : Bool) : formula.eval (fun _ => b) = true := + (eval_formula_iff _).2 fun _ => rfl + +/-- Every port has exactly two internal literal occurrences. -/ +theorem internal_occurrences : ∀ v : Variable, formula.vars.count v = 2 := by decide +kernel + +/-- The formula has eight clauses, each of width two. -/ +theorem formula_sizes : formula.length = 8 ∧ ∀ c ∈ formula, c.length = 2 := by decide +kernel + +/-- Every variable is actually used, including variables with no external access in a client. -/ +theorem variables_used : ∀ v : Variable, v ∈ formula.vars := by decide +kernel + +private instance (r : Route) : Decidable (IsOrthogonal r) := + inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2)) + +/-- All literal incidences occur exactly once, in formula order. -/ +theorem incidenceRoutes_cover : + incidenceRoutes.map (fun e => (e.1, e.2.1)) = + formula.zipIdx.flatMap (fun ci => ci.1.map fun l => (ci.2, l.1)) := by decide +kernel + +/-- There are eight clause positions and sixteen incidence routes. -/ +theorem drawing_sizes : clausePositions.length = 8 ∧ incidenceRoutes.length = 16 := by + decide +kernel + +/-- Inner positions identify the eight variables. -/ +theorem variablePosition_injective : Function.Injective variablePosition := + PairedPorts.variablePosition_injective + +/-- Clause positions are distinct. -/ +theorem clausePositions_nodup : clausePositions.Nodup := by decide +kernel + +/-- Variables and clauses have different positions. -/ +theorem variablePosition_not_mem_clauses : + ∀ v : Variable, variablePosition v ∉ clausePositions := by decide +kernel + +/-- The sixteen labeled incidences are distinct. -/ +theorem incidenceEndpoints_nodup : + (incidenceRoutes.map fun e => (e.1, e.2.1)).Nodup := by decide +kernel + +/-- Every incidence has its prescribed clause and variable endpoints. -/ +theorem incidence_endpoints : ∀ e ∈ incidenceRoutes, + e.1 < 8 ∧ e.2.2.head? = some (clausePosition e.1) ∧ + e.2.2.getLast? = some (variablePosition e.2.1) := by decide +kernel + +/-- All sixteen incidence routes are straight segments. -/ +theorem incidence_pair : ∀ e ∈ incidenceRoutes, + e.2.2 = [clausePosition e.1, variablePosition e.2.1] := by decide +kernel + +/-- Every incidence is properly orthogonal. -/ +theorem incidence_orthogonal : ∀ e ∈ incidenceRoutes, IsOrthogonal e.2.2 := by decide +kernel + +/-- Listed incidence vertices are distinct within each route. -/ +theorem incidence_points_nodup : ∀ e ∈ incidenceRoutes, e.2.2.Nodup := by decide +kernel + +/-- Every incidence is continuously simple. -/ +theorem incidence_isSimple {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes) : + IsSimple e.2.2 := by + refine ⟨incidence_points_nodup e he, ?_⟩ + intro a ha b hb hne + rw [incidence_pair e he] at ha hb + have ha' : a = (clausePosition e.1, variablePosition e.2.1) := by + simpa only [List.consecutivePairs, List.tail_cons, List.tail_nil, List.zip_cons_cons, + List.zip_nil_right, List.mem_singleton] using ha + have hb' : b = (clausePosition e.1, variablePosition e.2.1) := by + simpa only [List.consecutivePairs, List.tail_cons, List.tail_nil, List.zip_cons_cons, + List.zip_nil_right, List.mem_singleton] using hb + exact False.elim (hne (ha'.trans hb'.symm)) + +/-- All listed core points lie in `[20,220]²`. -/ +theorem core_bounds : ∀ e ∈ incidenceRoutes, ∀ p ∈ e.2.2, + 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by decide +kernel + +/-- Every variable lies in the inner core square. -/ +theorem variable_bounds : ∀ v : Variable, + 20 ≤ (variablePosition v).1 ∧ (variablePosition v).1 ≤ 220 ∧ + 20 ≤ (variablePosition v).2 ∧ (variablePosition v).2 ≤ 220 := by decide +kernel + +/-- Every clause lies in the inner core square. -/ +theorem clause_bounds : ∀ p ∈ clausePositions, + 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by decide +kernel + +/-- The full continuous core support lies strictly inside the outer cell. -/ +theorem core_support_interior {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes) + {p : ℝ × ℝ} (hp : p ∈ support e.2.2) : + 0 < p.1 ∧ p.1 < 240 ∧ 0 < p.2 ∧ p.2 < 240 := by + have hsub : support e.2.2 ⊆ openCell 120 (0, 0) := by + apply support_subset_openCell + intro q hq + have hb := core_bounds e he q hq + have hq' : 0 < q.1 ∧ q.1 < 240 ∧ 0 < q.2 ∧ q.2 < 240 := by omega + have hreal : (0 : ℝ) < q.1 ∧ (q.1 : ℝ) < 240 ∧ + (0 : ℝ) < q.2 ∧ (q.2 : ℝ) < 240 := by exact_mod_cast hq' + simpa [openCell, realPoint] using hreal + simpa [openCell] using hsub hp + +/-- Finite certificate of all permitted contacts between distinct incidences. -/ +theorem routes_contact_check : ∀ e ∈ incidenceRoutes, ∀ f ∈ incidenceRoutes, e ≠ f → + routeContactCheck (commonEndpoints e f) e.2.2 f.2.2 = true := by decide +kernel + +/-- Continuous contacts between distinct incidences are shared graph endpoints. -/ +theorem routes_contact {e f : ℕ × Variable × Route} + (he : e ∈ incidenceRoutes) (hf : f ∈ incidenceRoutes) (hne : e ≠ f) + {p : ℝ × ℝ} (hp : p ∈ support e.2.2) (hq : p ∈ support f.2.2) : + ∃ q ∈ commonEndpoints e f, p = realPoint q := + routeContactCheck_sound (routes_contact_check e he f hf hne) hp hq + +/-- Finite certificate excluding nonincident variable vertices. -/ +theorem variable_avoidance_check : ∀ e ∈ incidenceRoutes, ∀ v : Variable, v ≠ e.2.1 → + routeContactCheck [] e.2.2 [variablePosition v] = true := by decide +kernel + +/-- Finite certificate excluding nonincident clause vertices. -/ +theorem clause_avoidance_check : ∀ e ∈ incidenceRoutes, ∀ i : Fin 8, i.val ≠ e.1 → + routeContactCheck [] e.2.2 [clausePosition i] = true := by decide +kernel + +/-- Incidences avoid every nonincident variable over their full real support. -/ +theorem variable_not_mem_support {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes) + {v : Variable} (hv : v ≠ e.2.1) : realPoint (variablePosition v) ∉ support e.2.2 := + not_mem_support_of_routeContactCheck (variable_avoidance_check e he v hv) + +/-- Incidences avoid every nonincident clause over their full real support. -/ +theorem clause_not_mem_support {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes) + {i : Fin 8} (hi : i.val ≠ e.1) : realPoint (clausePosition i) ∉ support e.2.2 := + not_mem_support_of_routeContactCheck (clause_avoidance_check e he i hi) + +/-- Finite certificate that access touches the core only at its own variable. -/ +theorem access_contact_check : ∀ s l, ∀ e ∈ incidenceRoutes, + routeContactCheck (if e.2.1 = (s, l) then [variablePosition (s, l)] else []) + (PairedPorts.accessRoute s l) e.2.2 = true := by decide +kernel + +/-- Every access/core contact is its designated variable endpoint. -/ +theorem access_contact {s : Fin 4} {l : Fin 2} {e : ℕ × Variable × Route} + (he : e ∈ incidenceRoutes) {p : ℝ × ℝ} + (hp : p ∈ support (PairedPorts.accessRoute s l)) (hq : p ∈ support e.2.2) : + e.2.1 = (s, l) ∧ p = realPoint (variablePosition (s, l)) := by + obtain ⟨q, hq, hpq⟩ := routeContactCheck_sound (access_contact_check s l e he) hp hq + split_ifs at hq with h + · have hq' : q = variablePosition (s, l) := List.mem_singleton.mp hq + exact ⟨h, hq' ▸ hpq⟩ + · exact False.elim (List.not_mem_nil hq) + +/-- Finite certificate excluding every other variable from an access. -/ +theorem access_variable_avoidance_check : ∀ s l, ∀ v : Variable, v ≠ (s, l) → + routeContactCheck [] (PairedPorts.accessRoute s l) [variablePosition v] = true := by + decide +kernel + +/-- Finite certificate excluding every clause from every access. -/ +theorem access_clause_avoidance_check : ∀ s l, ∀ p ∈ clausePositions, + routeContactCheck [] (PairedPorts.accessRoute s l) [p] = true := by decide +kernel + +/-- Access avoids every other variable over its full real support. -/ +theorem access_variable_not_mem {s : Fin 4} {l : Fin 2} {v : Variable} (hv : v ≠ (s, l)) : + realPoint (variablePosition v) ∉ support (PairedPorts.accessRoute s l) := + not_mem_support_of_routeContactCheck (access_variable_avoidance_check s l v hv) + +/-- Access avoids every clause over its full real support. -/ +theorem access_clause_not_mem {s : Fin 4} {l : Fin 2} {p : Point} (hp : p ∈ clausePositions) : + realPoint p ∉ support (PairedPorts.accessRoute s l) := + not_mem_support_of_routeContactCheck (access_clause_avoidance_check s l p hp) + +/-- The sixteen incidence segments have total Manhattan length 800. -/ +theorem route_sizes : + (incidenceRoutes.map fun e => e.2.2.consecutivePairs.length).sum = 16 ∧ + (incidenceRoutes.map fun e => wireLength e.2.2).sum = 800 := by decide +kernel + +end Cslib.Complexity.SAT.OrdinaryRing diff --git a/Complexity/Foundations/Geometry/Orthogonal/PairedBoundary.lean b/Complexity/Foundations/Geometry/Orthogonal/PairedBoundary.lean new file mode 100644 index 000000000..35b761b72 --- /dev/null +++ b/Complexity/Foundations/Geometry/Orthogonal/PairedBoundary.lean @@ -0,0 +1,59 @@ +/- +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.Foundations.Geometry.Orthogonal.PairedPorts +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Matching paired boundaries of grid cells + +## Main results + +* `boundary_eq_cases`: equal boundary points in distinct cells determine adjacent opposite + sides and the same lane. +* `boundary_not_mem_openCell`: a paired boundary belongs to no open grid cell. + +## References + +These are original integer-coordinate facts about the fixed paired-port interface. +-/ + +@[expose] public section + +namespace Cslib.Orthogonal.PairedPorts + +/-- Equal boundary points in distinct cells identify the lane and opposite adjacent sides. -/ +theorem boundary_eq_cases {c d : Point} {s t : Fin 4} {l k : Fin 2} + (hcd : c ≠ d) + (h : cellOrigin 120 c + boundaryPort s l = cellOrigin 120 d + boundaryPort t k) : + l = k ∧ d = c + neighbor s ∧ t = oppositeSide s := by + rcases c with ⟨cx, cy⟩ + rcases d with ⟨dx, dy⟩ + have hcd' : ¬ (cx = dx ∧ cy = dy) := fun h => hcd (Prod.ext h.1 h.2) + fin_cases s <;> fin_cases t <;> fin_cases l <;> fin_cases k <;> + norm_num [cellOrigin, boundaryPort, offset, neighbor, oppositeSide, Prod.ext_iff] at h ⊢ <;> + omega + +/-- Each translated paired boundary belongs to its own closed cell. -/ +theorem boundary_mem_closedCell (c : Point) (s : Fin 4) (l : Fin 2) : + realPoint (cellOrigin 120 c + boundaryPort s l) ∈ closedCell 120 c := by + rw [realPoint_add, add_comm, mem_closedCell_add_origin_iff] + fin_cases s <;> fin_cases l <;> norm_num [boundaryPort, offset, realPoint] + +/-- A translated paired boundary lies outside every open grid cell. -/ +theorem boundary_not_mem_openCell (c d : Point) (s : Fin 4) (l : Fin 2) : + realPoint (cellOrigin 120 c + boundaryPort s l) ∉ openCell 120 d := by + intro hp + have hdc := cell_eq_of_mem_open_closed (by decide) hp (boundary_mem_closedCell c s l) + subst d + rw [realPoint_add, add_comm, mem_openCell_add_origin_iff] at hp + fin_cases s <;> fin_cases l <;> norm_num [boundaryPort, offset, realPoint] at hp + +end Cslib.Orthogonal.PairedPorts diff --git a/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean b/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean new file mode 100644 index 000000000..b311f95a1 --- /dev/null +++ b/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean @@ -0,0 +1,153 @@ +/- +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.Foundations.Geometry.Orthogonal.Macrocell +public import Complexity.Foundations.Geometry.Orthogonal.Separation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.Ring + +/-! +# Paired ports of a fixed square cell + +Each side of `[0,240]²` has two ports, at offsets 110 and 130. Sides are ordered +left, right, bottom, top. Lane zero always has the smaller coordinate; translation +to an adjacent cell preserves the lane. Straight access routes end 20 units inside. + +## Main definitions + +* `boundaryPort`, `variablePosition`, `accessRoute`: the eight paired accesses. +* `oppositeSide`, `neighbor`: matching sides and adjacent cell displacements. + +## Main results + +* `boundaryPort_shared`: adjacent cells share the same port in the same lane. +* `access_disjoint`, `access_boundary_isolation`: continuous access separation. + +## References + +This fixed geometric interface is original. +-/ + +@[expose] public section + +namespace Cslib.Orthogonal.PairedPorts + +/-- A side and its lower- or higher-coordinate lane. -/ +abbrev Port := Fin 4 × Fin 2 + +/-- The two lane coordinates. -/ +def offset (l : Fin 2) : ℤ := 110 + 20 * (l : ℕ) + +/-- Paired boundary ports, in left/right/bottom/top side order. -/ +def boundaryPort (s : Fin 4) (l : Fin 2) : Point := + if s = 0 then (0, offset l) else if s = 1 then (240, offset l) + else if s = 2 then (offset l, 0) else (offset l, 240) + +/-- The corresponding inner positions on the perimeter of `[20,220]²`. -/ +def variablePosition (s : Fin 4) (l : Fin 2) : Point := + if s = 0 then (20, offset l) else if s = 1 then (220, offset l) + else if s = 2 then (offset l, 20) else (offset l, 220) + +/-- Straight access from one boundary port to its corresponding inner position. -/ +def accessRoute (s : Fin 4) (l : Fin 2) : Route := + [boundaryPort s l, variablePosition s l] + +/-- Opposite sides of neighboring cells. -/ +def oppositeSide (s : Fin 4) : Fin 4 := + if s = 0 then 1 else if s = 1 then 0 else if s = 2 then 3 else 2 + +/-- Displacement to the neighboring cell on the indicated side. -/ +def neighbor (s : Fin 4) : Point := + if s = 0 then (-1, 0) else if s = 1 then (1, 0) + else if s = 2 then (0, -1) else (0, 1) + +/-- Taking the opposite side twice recovers the original side. -/ +theorem oppositeSide_involutive : Function.Involutive oppositeSide := by + change ∀ s, oppositeSide (oppositeSide s) = s + decide +kernel + +/-- Adjacent cells match ports without reversing the lane. -/ +theorem boundaryPort_shared (p : Point) (s : Fin 4) (l : Fin 2) : + cellOrigin 120 p + boundaryPort s l = + cellOrigin 120 (p + neighbor s) + boundaryPort (oppositeSide s) l := by + fin_cases s <;> fin_cases l <;> ext <;> + simp [cellOrigin, boundaryPort, oppositeSide, neighbor, offset] <;> ring + +/-- All eight boundary positions are distinct. -/ +theorem boundaryPort_injective : Function.Injective (fun p : Port => boundaryPort p.1 p.2) := by + decide +kernel + +/-- All eight inner positions are distinct. -/ +theorem variablePosition_injective : + Function.Injective (fun p : Port => variablePosition p.1 p.2) := by decide +kernel + +/-- Every inner position lies in the smaller core square. -/ +theorem variable_bounds : ∀ s l, + 20 ≤ (variablePosition s l).1 ∧ (variablePosition s l).1 ≤ 220 ∧ + 20 ≤ (variablePosition s l).2 ∧ (variablePosition s l).2 ≤ 220 := by decide +kernel + +private instance (r : Route) : Decidable (IsOrthogonal r) := + inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2)) + +/-- Every access is orthogonal, with its prescribed boundary and inner endpoints. -/ +theorem access_endpoints : ∀ s l, IsOrthogonal (accessRoute s l) ∧ + (accessRoute s l).head? = some (boundaryPort s l) ∧ + (accessRoute s l).getLast? = some (variablePosition s l) := by decide +kernel + +/-- Every access is simple over its full real support. -/ +theorem access_isSimple (s : Fin 4) (l : Fin 2) : IsSimple (accessRoute s l) := by + constructor + · fin_cases s <;> fin_cases l <;> decide + · intro a ha b hb hne + have ht : (accessRoute s l).consecutivePairs = + [(boundaryPort s l, variablePosition s l)] := rfl + rw [ht, List.mem_singleton] at ha hb + exact False.elim (hne (ha.trans hb.symm)) + +/-- Each access has one segment and 20 units of Manhattan length. -/ +theorem access_route_sizes : ∀ s l, (accessRoute s l).consecutivePairs.length = 1 ∧ + wireLength (accessRoute s l) = 20 := by decide +kernel + +/-- Finite certificate separating every pair of distinct accesses. -/ +theorem access_disjoint_check : ∀ p q : Port, p ≠ q → + routeContactCheck [] (accessRoute p.1 p.2) (accessRoute q.1 q.2) = true := by decide +kernel + +/-- Distinct accesses have disjoint full real supports. -/ +theorem access_disjoint {p q : Port} (h : p ≠ q) : + Disjoint (support (accessRoute p.1 p.2)) (support (accessRoute q.1 q.2)) := + disjoint_support_of_routeContactCheck (access_disjoint_check p q h) + +private theorem mem_support_pair {a b : Point} {p : ℝ × ℝ} : + p ∈ support [a, b] ↔ p ∈ segment a b := by + rw [support_cons_cons] + change (p ∈ segment a b ∨ p ∈ support [b]) ↔ _ + have hright : realPoint b ∈ segment a b := _root_.right_mem_segment ℝ _ _ + have hs : p ∈ support [b] ↔ p = realPoint b := by simp [support, List.consecutivePairs] + rw [hs] + exact ⟨fun h => h.elim id (fun h => h ▸ hright), Or.inl⟩ + +/-- An access stays in the cell and touches its boundary only at the designated port. -/ +theorem access_boundary_isolation {s : Fin 4} {l : Fin 2} {p : ℝ × ℝ} + (hp : p ∈ support (accessRoute s l)) : + 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 (boundaryPort s l)) := by + unfold accessRoute at hp + rw [mem_support_pair] at hp + fin_cases s <;> fin_cases l <;> + simp only [boundaryPort, variablePosition, offset, Orthogonal.segment, realPoint] at hp ⊢ + all_goals + norm_num [mem_horizontal, mem_vertical, Set.mem_uIcc] at hp ⊢ + 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 + +end Cslib.Orthogonal.PairedPorts diff --git a/Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean b/Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean new file mode 100644 index 000000000..f80b2dc0f --- /dev/null +++ b/Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean @@ -0,0 +1,96 @@ +/- +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.Foundations.Geometry.Orthogonal.PairedPorts +import Mathlib.Tactic.FinCases + +/-! +# Four disjoint offset spokes + +A rotational choice of one of the paired ports on each side gives four proper orthogonal +spokes from the center of the square. Distinct spokes meet only at that center. These are +finite certificates about entire real route supports. + +## Main definitions + +* `Cslib.Orthogonal.PairedPorts.spokeLane`, `.spokeRoute`: selected ports and two-segment spokes. + +## Main results + +* `Cslib.Orthogonal.PairedPorts.spoke_isSimple`, `.spokes_contact`: simplicity and center-only + contacts. + +## References + +The finite offset star is original. +-/ + +@[expose] public section + +namespace Cslib.Orthogonal.PairedPorts + +/-- One selected lane on each side, in rotational order around the center. -/ +def spokeLane (s : Fin 4) : Fin 2 := if s = 1 ∨ s = 2 then 1 else 0 + +/-- A spoke first travels toward its bend and then toward its selected boundary point. -/ +def spokeElbow (s : Fin 4) : Point := + match s with + | 0 => (120, 110) + | 1 => (120, 130) + | 2 => (130, 120) + | _ => (110, 120) + +/-- A two-segment route from the center to the selected side port. -/ +def spokeRoute (s : Fin 4) : Route := + [(120, 120), spokeElbow s, boundaryPort s (spokeLane s)] + +private instance (r : Route) : Decidable (IsOrthogonal r) := + inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2)) + +/-- Every spoke is proper and orthogonal with its prescribed endpoints. -/ +theorem spoke_endpoints : ∀ s, IsOrthogonal (spokeRoute s) ∧ + (spokeRoute s).head? = some (120, 120) ∧ + (spokeRoute s).getLast? = some (boundaryPort s (spokeLane s)) := by decide +kernel + +/-- The two segments of a spoke meet only at their shared bend. -/ +theorem spoke_bend_check : ∀ s, + segmentContactCheck [spokeElbow s] (120, 120) (spokeElbow s) + (spokeElbow s) (boundaryPort s (spokeLane s)) = true := by decide +kernel + +/-- Each spoke is simple over its full real support. -/ +theorem spoke_isSimple (s : Fin 4) : IsSimple (spokeRoute s) := by + have hcontact : EndpointContacts (120, 120) (spokeElbow s) (spokeElbow s) + (boundaryPort s (spokeLane s)) := by + intro p hp hq + obtain ⟨q, hq, heq⟩ := segmentContactCheck_sound (spoke_bend_check s) hp hq + have hqb := List.mem_singleton.mp hq + exact ⟨Or.inr (hqb ▸ heq), Or.inl (hqb ▸ heq)⟩ + refine ⟨?_, ?_⟩ + · fin_cases s <;> decide + · intro e he f hf hne + simp only [spokeRoute, 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) + +/-- Distinct spokes have only the center as an allowed continuous contact. -/ +theorem spokes_contact_check : ∀ s t : Fin 4, s ≠ t → + routeContactCheck [(120, 120)] (spokeRoute s) (spokeRoute t) = true := by decide +kernel + +/-- Every real intersection of distinct spokes is their common center. -/ +theorem spokes_contact {s t : Fin 4} (hst : s ≠ t) {p : ℝ × ℝ} + (hp : p ∈ support (spokeRoute s)) (hq : p ∈ support (spokeRoute t)) : + p = realPoint (120, 120) := by + obtain ⟨q, hq, hpq⟩ := routeContactCheck_sound (spokes_contact_check s t hst) hp hq + exact (List.mem_singleton.mp hq) ▸ hpq + +end Cslib.Orthogonal.PairedPorts diff --git a/Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean b/Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean new file mode 100644 index 000000000..b0371b7ae --- /dev/null +++ b/Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean @@ -0,0 +1,131 @@ +/- +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.Logics.Propositional.CNF.Planar.CrossoverSplit + +/-! +# Unique extensions through the fixed crossover + +The fixed clause tables have exactly one satisfying full assignment for each pair of incoming +bits. The explicit Boolean extension and its uniqueness are preserved by the internal splitting +rings. Construction and source credit are documented in `Crossover` and `CrossoverSplit`. + +## Main definitions + +* `Cslib.Logic.PL.CNF.Crossover.canonicalExtension`: the original full assignment from two bits. +* `Cslib.Logic.PL.CNF.Crossover.canonicalSplitExtension`: its lift to all internal copies. + +## Main results + +* `Cslib.Logic.PL.CNF.Crossover.existsUnique_holds`: uniqueness before splitting. +* `Cslib.Logic.PL.CNF.Crossover.existsUnique_split_holds`: uniqueness after splitting. + +## References + +The construction adapts [Lichtenstein1982, Figs. 4–5] and [Tromino2025, Fig. 8(b)]. +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF.Crossover + +/-- The full satisfying assignment determined by the left and top input values. +The explicit Boolean expressions describe all nine internal values as well as the outputs. -/ +def canonicalExtension (a b : Bool) : Variable → Bool := + assignment a a b b a (!a || b) (!a || !b) b a b (a || b) (a || !b) a + +/-- The explicit extension satisfies all 26 clauses for every pair of inputs. -/ +theorem eval_canonicalExtension (a b : Bool) : + formula.eval (canonicalExtension a b) = true := by + cases a <;> cases b <;> decide +kernel + +-- Only the nine internal values are enumerated after the two inputs are fixed; the existing +-- boundary theorem has already identified the outputs with those inputs. +private theorem assignment_eq_canonicalExtension (a b : Bool) : + ∀ aInnerLeft upperLeft lowerLeft bInnerTop center bInnerBottom + upperRight lowerRight aInnerRight : Bool, + formula.eval (assignment a a b b aInnerLeft upperLeft lowerLeft bInnerTop center + bInnerBottom upperRight lowerRight aInnerRight) = true → + ∀ v, assignment a a b b aInnerLeft upperLeft lowerLeft bInnerTop center + bInnerBottom upperRight lowerRight aInnerRight v = canonicalExtension a b v := by + cases a <;> cases b <;> decide +kernel + +/-- Every satisfying full assignment is the explicit extension of its two incoming values. -/ +theorem eq_canonicalExtension_of_holds {σ : Variable → Bool} + (h : formula.eval σ = true) : + σ = canonicalExtension (σ .aLeft) (σ .bTop) := by + obtain ⟨horizontal, vertical⟩ := boundary_eq_of_holds h + have heq : assignment (σ .aLeft) (σ .aLeft) (σ .bTop) (σ .bTop) + (σ .aInnerLeft) (σ .upperLeft) (σ .lowerLeft) (σ .bInnerTop) (σ .center) + (σ .bInnerBottom) (σ .upperRight) (σ .lowerRight) (σ .aInnerRight) = σ := by + funext v + cases v <;> first | rfl | exact horizontal | exact vertical + have hfull := assignment_eq_canonicalExtension (σ .aLeft) (σ .bTop) + (σ .aInnerLeft) (σ .upperLeft) (σ .lowerLeft) (σ .bInnerTop) (σ .center) + (σ .bInnerBottom) (σ .upperRight) (σ .lowerRight) (σ .aInnerRight) + rw [heq] at hfull + exact funext (hfull h) + +/-- Satisfying assignments agreeing on the incoming ports agree on every variable. -/ +theorem ext_of_holds {σ τ : Variable → Bool} + (hσ : formula.eval σ = true) (hτ : formula.eval τ = true) + (ha : σ .aLeft = τ .aLeft) (hb : σ .bTop = τ .bTop) : σ = τ := by + rw [eq_canonicalExtension_of_holds hσ, eq_canonicalExtension_of_holds hτ, ha, hb] + +/-- Each pair of incoming values extends uniquely to a satisfying full assignment. -/ +theorem existsUnique_holds (a b : Bool) : + ∃! σ : Variable → Bool, + formula.eval σ = true ∧ σ .aLeft = a ∧ σ .bTop = b := by + refine ⟨canonicalExtension a b, ⟨eval_canonicalExtension a b, rfl, rfl⟩, ?_⟩ + rintro σ ⟨hσ, ha, hb⟩ + rw [eq_canonicalExtension_of_holds hσ, ha, hb] + +/-- The explicit full split assignment: every local copy receives its original variable's +canonical value, determined by the left and top inputs. -/ +def canonicalSplitExtension (a b : Bool) : SplitVariable → Bool := + canonicalExtension a b ∘ SplitVariable.origin + +/-- The canonical split extension satisfies all 74 clauses. -/ +theorem eval_canonicalSplitExtension (a b : Bool) : + splitFormula.eval (canonicalSplitExtension a b) = true := + eval_splitFormula_lift _ (eval_canonicalExtension a b) + +/-- Every satisfying split assignment is the explicit extension of its incoming values. +The implication rings identify the six copies before applying the original uniqueness result; +no enumeration of assignments to the 53 split variables is needed. -/ +theorem eq_canonicalSplitExtension_of_holds {σ : SplitVariable → Bool} + (h : splitFormula.eval σ = true) : + σ = canonicalSplitExtension (σ .aLeft) (σ .bTop) := by + obtain ⟨hbase, hagree⟩ := (eval_splitFormula_iff σ).1 h + have heq := eq_canonicalExtension_of_holds hbase + funext v + have hv := congrFun heq v.origin + cases v with + | aLeft | aRight | bTop | bBottom | center => exact hv + | copy v i => + have hzero : σ (.copy v 0) = canonicalSplitExtension (σ .aLeft) (σ .bTop) + (.copy v i) := by + cases v <;> exact hv + exact (hagree v i).trans hzero + +/-- Satisfying split assignments agreeing on the two incoming ports agree everywhere. -/ +theorem split_ext_of_holds {σ τ : SplitVariable → Bool} + (hσ : splitFormula.eval σ = true) (hτ : splitFormula.eval τ = true) + (ha : σ .aLeft = τ .aLeft) (hb : σ .bTop = τ .bTop) : σ = τ := by + rw [eq_canonicalSplitExtension_of_holds hσ, eq_canonicalSplitExtension_of_holds hτ, ha, hb] + +/-- Each pair of incoming values extends uniquely to a satisfying full split assignment. -/ +theorem existsUnique_split_holds (a b : Bool) : + ∃! σ : SplitVariable → Bool, + splitFormula.eval σ = true ∧ σ .aLeft = a ∧ σ .bTop = b := by + refine ⟨canonicalSplitExtension a b, ⟨eval_canonicalSplitExtension a b, rfl, rfl⟩, ?_⟩ + rintro σ ⟨hσ, ha, hb⟩ + rw [eq_canonicalSplitExtension_of_holds hσ, ha, hb] + +end Cslib.Logic.PL.CNF.Crossover diff --git a/Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean b/Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean new file mode 100644 index 000000000..05994f7e5 --- /dev/null +++ b/Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean @@ -0,0 +1,283 @@ +/- +Copyright (c) 2026 lean-trominoes contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine, Stefan Langerman, GPT 5.6 +-/ + +module +-- upstream: candidate + +public import Complexity.Logics.Propositional.CNF.Planar.CrossoverCounting +import Mathlib.Tactic.FinCases + +/-! +# A crossover with two attachment ports per side + +Each old terminal is replaced by two ports and one implication between them. Together with +its two old incidences this forms an implication chain between two equal internal copies. +Consequently both ports have the old terminal's uniquely determined value. Each port has two +internal incidences and room for one external incidence. The unchanged internal core comes from +Lichtenstein's crossover [Lichtenstein1982, Figs. 4–5], as drawn in [Tromino2025, Fig. 8(b)]. + +## Main definitions + +* `PairedCrossover.formula`: the 57-variable, 78-clause paired-port template. +* `PairedCrossover.canonicalExtension`: its full assignment from two input bits. + +## Main results + +* `PairedCrossover.eq_canonicalExtension_of_holds`: uniqueness of the full extension. +* `PairedCrossover.terminal_occurrences`: two internal incidences at each of the eight ports. + +## References + +* David Lichtenstein, *Planar Formulae and Their Uses*, Figs. 4–5 [Lichtenstein1982]. +* MIT–ULB CompGeom Group, *Undecidability of Tiling with a Tromino*, Fig. 8(b) [Tromino2025]. + +The paired-terminal replacement and its uniqueness proof are original. +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF.PairedCrossover + +/-- Eight boundary ports, the unsplit center, and the old 48 internal copies. -/ +inductive Variable + | port (side : Fin 4) (lane : Fin 2) + | center + | copy (v : Crossover.Internal) (i : Fin 6) + deriving DecidableEq, Repr + +instance : Fintype Variable where + elems := { .center } ∪ + Finset.univ.biUnion (fun s => Finset.univ.image (Variable.port s)) ∪ + Finset.univ.biUnion (fun v => Finset.univ.image (Variable.copy v)) + complete v := by cases v <;> simp + +/-- The eight attachment ports in left/right/bottom/top geometric order, with two lanes per +side. The source variables `.bTop` and `.bBottom` retain their historical names. -/ +def terminal : Fin 4 → Fin 2 → Variable := Variable.port + +/-- Forget the lane of a boundary port. -/ +def Variable.origin : Variable → Crossover.SplitVariable + | .port 0 _ => .aLeft + | .port 1 _ => .aRight + | .port 2 _ => .bTop + | .port 3 _ => .bBottom + | .center => .center + | .copy v i => .copy v i + +/-- Choose lane zero as the representative of each old terminal. -/ +def representative : Crossover.SplitVariable → Variable + | .aLeft => .port 0 0 + | .aRight => .port 1 0 + | .bTop => .port 2 0 + | .bBottom => .port 3 0 + | .center => .center + | .copy v i => .copy v i + +/-- Replace each old boundary literal by the port at that incidence's geometric lane. -/ +def mapLiteral : Literal Crossover.SplitVariable → Literal Variable + | (.aLeft, true) => (.port 0 0, true) + | (.aLeft, false) => (.port 0 1, false) + | (.aRight, false) => (.port 1 0, false) + | (.aRight, true) => (.port 1 1, true) + | (.bTop, false) => (.port 2 0, false) + | (.bTop, true) => (.port 2 1, true) + | (.bBottom, true) => (.port 3 0, true) + | (.bBottom, false) => (.port 3 1, false) + | (.center, b) => (.center, b) + | (.copy v i, b) => (.copy v i, b) + +/-- One directed implication joins the paired ports on each side. -/ +def bridges : CNF Variable := + [[(.port 0 0, false), (.port 0 1, true)], + [(.port 1 1, false), (.port 1 0, true)], + [(.port 2 1, false), (.port 2 0, true)], + [(.port 3 0, false), (.port 3 1, true)]] + +/-- Preserve the old 74 clauses with their terminal incidences separated, then add four bridges. -/ +def formula : CNF Variable := + Crossover.splitFormula.map (List.map mapLiteral) ++ bridges + +/-- The internal copy at the start of each terminal's implication chain. -/ +def chainStart : Fin 4 → Variable + | 0 => .copy .aInnerLeft 5 + | 1 => .copy .aInnerRight 3 + | 2 => .copy .bInnerTop 1 + | 3 => .copy .bInnerBottom 4 + +/-- The internal copy at the end of each terminal's implication chain. -/ +def chainEnd : Fin 4 → Variable + | 0 => .copy .aInnerLeft 4 + | 1 => .copy .aInnerRight 2 + | 2 => .copy .bInnerTop 0 + | 3 => .copy .bInnerBottom 3 + +/-- The first lane in each directed chain. -/ +def firstLane : Fin 4 → Fin 2 + | 0 => 0 + | 1 => 1 + | 2 => 1 + | 3 => 0 + +/-- Three existing clauses form a chain between two equal internal copies. -/ +def chain : Fin 4 → CNF Variable + | 0 => [[(.port 0 0, true), (.copy .aInnerLeft 5, false)], + [(.port 0 0, false), (.port 0 1, true)], + [(.port 0 1, false), (.copy .aInnerLeft 4, true)]] + | 1 => [[(.copy .aInnerRight 3, false), (.port 1 1, true)], + [(.port 1 1, false), (.port 1 0, true)], + [(.copy .aInnerRight 2, true), (.port 1 0, false)]] + | 2 => [[(.port 2 1, true), (.copy .bInnerTop 1, false)], + [(.port 2 1, false), (.port 2 0, true)], + [(.port 2 0, false), (.copy .bInnerTop 0, true)]] + | 3 => [[(.copy .bInnerBottom 4, false), (.port 3 0, true)], + [(.port 3 0, false), (.port 3 1, true)], + [(.copy .bInnerBottom 3, true), (.port 3 1, false)]] + +private theorem chain_mem : ∀ s, ∀ c ∈ chain s, c ∈ formula := by decide +kernel + +private theorem ring_mem : ∀ v, ∀ c ∈ (Crossover.ring v).relabel representative, + c ∈ formula := by decide +kernel + +private theorem eval_chain {σ : Variable → Bool} {s : Fin 4} + (h : (chain s).eval σ = true) (heq : σ (chainStart s) = σ (chainEnd s)) : + σ (terminal s 0) = σ (chainStart s) ∧ + σ (terminal s 1) = σ (chainStart s) := by + have cert : ∀ a p q : Bool, + ((!a || p) && (!p || q) && (!q || a)) = true → p = a ∧ q = a := by + decide +kernel + have h' : ((!σ (chainStart s) || σ (terminal s (firstLane s))) && + (!σ (terminal s (firstLane s)) || σ (terminal s (1 - firstLane s))) && + (!σ (terminal s (1 - firstLane s)) || σ (chainEnd s))) = true := by + fin_cases s <;> + simpa [chain, chainStart, chainEnd, terminal, firstLane, CNF.eval, Clause.eval, + Literal.eval, Bool.and_assoc, Bool.or_comm] using h + rw [← heq] at h' + have hp := cert _ _ _ h' + fin_cases s <;> simpa [firstLane, and_comm] using hp + +private theorem eval_mapped (σ : Variable → Bool) + (ha : ∀ s, σ (terminal s 0) = σ (terminal s 1)) : + CNF.eval σ (Crossover.splitFormula.map (List.map mapLiteral)) = + Crossover.splitFormula.eval (σ ∘ representative) := by + have hl : ∀ l, Literal.eval σ (mapLiteral l) = Literal.eval (σ ∘ representative) l := by + simp only [terminal] at ha + rintro ⟨v, b⟩ + cases v <;> cases b <;> + simp [mapLiteral, Literal.eval, representative, ← ha] + simp only [CNF.eval, List.all_map, Function.comp_def, Clause.eval, List.any_map, hl] + rfl + +/-- Exact semantics: the old split formula together with agreement of each paired terminal. -/ +theorem eval_formula_iff (σ : Variable → Bool) : + formula.eval σ = true ↔ + Crossover.splitFormula.eval (σ ∘ representative) = true ∧ + ∀ s, σ (terminal s 0) = σ (terminal s 1) := by + constructor + · intro h + have hc := CNF.eval_eq_true_iff σ formula |>.1 h + have hr : ∀ v i, σ (.copy v i) = σ (.copy v 0) := by + intro v + apply (Crossover.eval_ring_iff (σ ∘ representative) v).1 + rw [← CNF.eval_relabel] + exact (CNF.eval_eq_true_iff _ _).2 fun c hc' => hc c (ring_mem v c hc') + have hp : ∀ s, σ (terminal s 0) = σ (terminal s 1) := by + intro s + have hchain := (CNF.eval_eq_true_iff σ (chain s)).2 fun c hc' => hc c (chain_mem s c hc') + have heq : σ (chainStart s) = σ (chainEnd s) := by + fin_cases s <;> exact (hr _ _).trans (hr _ _).symm + exact (eval_chain hchain heq).1.trans (eval_chain hchain heq).2.symm + refine ⟨?_, hp⟩ + rw [formula, CNF.eval_append, Bool.and_eq_true] at h + rw [eval_mapped σ hp] at h + exact h.1 + · rintro ⟨h, hp⟩ + rw [formula, CNF.eval_append, Bool.and_eq_true, eval_mapped σ hp] + refine ⟨h, ?_⟩ + simp only [terminal] at hp + simp [bridges, CNF.eval, Clause.eval, Literal.eval, ← hp] + +/-- The explicit unique full assignment, including both lanes on every side. -/ +def canonicalExtension (a b : Bool) : Variable → Bool := + Crossover.canonicalSplitExtension a b ∘ Variable.origin + +/-- The explicit full assignment satisfies the paired-port formula. -/ +theorem eval_canonicalExtension (a b : Bool) : formula.eval (canonicalExtension a b) = true := by + apply (eval_formula_iff _).2 + constructor + · have heq : canonicalExtension a b ∘ representative = Crossover.canonicalSplitExtension a b := by + funext v + cases v <;> rfl + rw [heq] + exact Crossover.eval_canonicalSplitExtension a b + · intro s + fin_cases s <;> rfl + +/-- Both lanes on the left and right carry `a`; both lanes on the top and bottom carry `b`. -/ +theorem terminal_values_canonicalExtension (a b : Bool) : + ∀ s l, canonicalExtension a b (terminal s l) = if s.val < 2 then a else b := by + intro s l + fin_cases s <;> rfl + +/-- Every satisfying full assignment is determined by the left and top lane-zero inputs. -/ +theorem eq_canonicalExtension_of_holds {σ : Variable → Bool} (h : formula.eval σ = true) : + σ = canonicalExtension (σ (terminal 0 0)) (σ (terminal 2 0)) := by + obtain ⟨hb, hp⟩ := (eval_formula_iff σ).1 h + have heq := Crossover.eq_canonicalSplitExtension_of_holds hb + funext v + cases v with + | center => exact congrFun heq .center + | copy v i => exact congrFun heq (.copy v i) + | port s l => + have hs : σ (terminal s 0) = canonicalExtension (σ (terminal 0 0)) + (σ (terminal 2 0)) (terminal s l) := by + fin_cases s + · exact congrFun heq .aLeft + · exact congrFun heq .aRight + · exact congrFun heq .bTop + · exact congrFun heq .bBottom + fin_cases l + · exact hs + · exact (hp s).symm.trans hs + +/-- All satisfying terminal values are the horizontal or vertical input value. -/ +theorem terminal_value_of_holds {σ : Variable → Bool} (h : formula.eval σ = true) + (s : Fin 4) (l : Fin 2) : + σ (terminal s l) = if s.val < 2 then σ (terminal 0 0) else σ (terminal 2 0) := + (congrFun (eq_canonicalExtension_of_holds h) (terminal s l)).trans + (terminal_values_canonicalExtension _ _ s l) + +/-- Projecting a satisfying paired assignment recovers a satisfying old split assignment. -/ +theorem eval_representative_of_holds {σ : Variable → Bool} (h : formula.eval σ = true) : + Crossover.splitFormula.eval (σ ∘ representative) = true := + ((eval_formula_iff σ).1 h).1 + +/-- Every two-bit input has exactly one satisfying full assignment. -/ +theorem existsUnique_holds (a b : Bool) : + ∃! σ : Variable → Bool, + formula.eval σ = true ∧ σ (terminal 0 0) = a ∧ σ (terminal 2 0) = b := by + refine ⟨canonicalExtension a b, ⟨eval_canonicalExtension a b, rfl, rfl⟩, ?_⟩ + rintro σ ⟨h, ha, hb⟩ + rw [eq_canonicalExtension_of_holds h, ha, hb] + +/-- The template uses exactly 57 variables. -/ +theorem card_variable : Fintype.card Variable = 57 := by decide +kernel + +/-- The template has exactly 78 clauses. -/ +theorem length_formula : formula.length = 78 := by decide +kernel + +/-- All clauses have width at most three. -/ +theorem width_formula : ∀ c ∈ formula, c.length ≤ 3 := by decide +kernel + +/-- No clause repeats a variable. -/ +theorem distinct_variables : ∀ c ∈ formula, (c.map Prod.fst).Nodup := by decide +kernel + +/-- Every variable has at most three internal incidences. -/ +theorem occurrences_le_three : ∀ v, formula.occurrences v ≤ 3 := by decide +kernel + +/-- Each of the eight ports has exactly two internal incidences. -/ +theorem terminal_occurrences : ∀ s l, formula.occurrences (terminal s l) = 2 := by decide +kernel + +end Cslib.Logic.PL.CNF.PairedCrossover diff --git a/Complexity/Logics/Propositional/CNF/Planar/PairedWire.lean b/Complexity/Logics/Propositional/CNF/Planar/PairedWire.lean new file mode 100644 index 000000000..022d1f5e8 --- /dev/null +++ b/Complexity/Logics/Propositional/CNF/Planar/PairedWire.lean @@ -0,0 +1,188 @@ +/- +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.Logics.Propositional.CNF +public import Mathlib.Data.List.Defs +import Mathlib.Data.List.Basic +import Mathlib.Data.Bool.Basic + +/-! +# Paired implication wires + +Each cell has two lanes, each with an entry and an exit. Local constraints must equate all +four port values. Across a gap, lane zero implies the next entry from the previous exit; +lane one implies the previous exit from the next entry. These implications use separate +ports. Under the local equalities, they force the representative values of consecutive cells +to agree. Thus every port of a nonempty wire has the value of its first lane-zero entry. + +This module uses ordinary CNF semantics. It supplies no local cell constraints or geometry. +The two clauses and four literal positions per gap are counted with multiplicity, without +distinctness assumptions on the port variables. + +## Main definitions + +* `Cell`, `Cell.Agree`: two entry/exit pairs and equality of all four values. +* `gapClauses`, `links`: opposite implications across one gap and all consecutive gaps. + +## Main results + +* `eval_links_iff`: under local agreement, the links equate consecutive representatives. +* `agree_head`, `agree_head_of_ne_nil`: every entry and exit has the first entry's value. +* `eval_links_of_constant`: constant port values satisfy every link. +* `length_links`, `length_vars_links`, `length_of_mem_links`: exact sizes and binary width. + +## References + +The paired-port composition and equality argument are original. +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF.PairedWire + +variable {V : Type*} + +/-- Two lanes of entry/exit variables. Lane zero's entry represents the cell's value. -/ +abbrev Cell (V : Type*) := Fin 2 → V × V + +/-- All four port values agree with the lane-zero entry. Local cell constraints must provide +this property; the wire clauses alone do not impose it. -/ +def Cell.Agree (cell : Cell V) (σ : V → Bool) : Prop := + ∀ lane, σ (cell lane).1 = σ (cell 0).1 ∧ σ (cell lane).2 = σ (cell 0).1 + +/-- Across one gap, lane zero points forward and lane one points backward. -/ +def gapClauses (previous next : Cell V) : CNF V := + [Clause.imp [(previous 0).2] (next 0).1, + Clause.imp [(next 1).1] (previous 1).2] + +/-- Two opposite implications across every consecutive pair of cells. -/ +def links (cells : List (Cell V)) : CNF V := + cells.consecutivePairs.flatMap fun p => gapClauses p.1 p.2 + +/-- With local agreement, the two implications equate the neighboring cell values. -/ +theorem eval_gapClauses_iff (σ : V → Bool) (previous next : Cell V) + (hp : previous.Agree σ) (hn : next.Agree σ) : + (gapClauses previous next).eval σ = true ↔ σ (previous 0).1 = σ (next 0).1 := by + simp only [gapClauses, eval_cons, eval_nil, Bool.and_true, Bool.and_eq_true, + Clause.eval_imp, List.forall_mem_singleton, (hp 0).2, (hp 1).2, (hn 1).1] + cases σ (previous 0).1 <;> cases σ (next 0).1 <;> simp + +/-- Under local agreement in every cell, the links hold exactly when consecutive lane-zero +entries agree. -/ +theorem eval_links_iff (σ : V → Bool) (cells : List (Cell V)) + (hcells : ∀ c ∈ cells, c.Agree σ) : + (links cells).eval σ = true ↔ + ∀ p ∈ cells.consecutivePairs, σ (p.1 0).1 = σ (p.2 0).1 := by + rw [links, eval_flatMap_eq_true_iff] + apply forall₂_congr fun p hp => ?_ + have hm := List.of_mem_zip hp + exact eval_gapClauses_iff σ p.1 p.2 (hcells _ hm.1) + (hcells _ (List.mem_of_mem_tail hm.2)) + +/-- Empty wires have no gap clauses. -/ +@[simp] theorem links_nil : links ([] : List (Cell V)) = [] := rfl + +/-- A single cell has no gap clauses. -/ +@[simp] theorem links_singleton (cell : Cell V) : links [cell] = [] := rfl + +/-- Remove the first gap, leaving the links of the nonempty tail. -/ +theorem links_cons_cons (first next : Cell V) (rest : List (Cell V)) : + links (first :: next :: rest) = gapClauses first next ++ links (next :: rest) := rfl + +/-- Under local agreement and satisfied links, all entries and exits have the value of the +first lane-zero entry, including for a singleton wire. -/ +theorem agree_head (σ : V → Bool) (first : Cell V) (rest : List (Cell V)) + (hcells : ∀ c ∈ first :: rest, c.Agree σ) + (hlinks : (links (first :: rest)).eval σ = true) : + ∀ c ∈ first :: rest, ∀ lane, + σ (c lane).1 = σ (first 0).1 ∧ σ (c lane).2 = σ (first 0).1 := by + induction rest generalizing first with + | nil => + intro c hc lane + rw [List.mem_singleton.1 hc] + exact hcells first List.mem_cons_self lane + | cons next rest ih => + rw [links_cons_cons, eval_append, Bool.and_eq_true] at hlinks + have he := (eval_gapClauses_iff σ first next (hcells _ List.mem_cons_self) + (hcells _ (List.mem_cons_of_mem _ List.mem_cons_self))).1 hlinks.1 + intro c hc lane + rcases List.mem_cons.1 hc with he | hc + · rw [he] + exact hcells first List.mem_cons_self lane + · have h := ih next (fun c hc => hcells c (List.mem_cons_of_mem _ hc)) hlinks.2 c hc lane + exact ⟨h.1.trans he.symm, h.2.trans he.symm⟩ + +/-- The head-agreement rule for a list with an explicit nonemptiness hypothesis. The fallback +only makes `headD` total and does not affect the result. -/ +theorem agree_head_of_ne_nil (σ : V → Bool) (fallback : Cell V) (cells : List (Cell V)) + (hne : cells ≠ []) (hcells : ∀ c ∈ cells, c.Agree σ) + (hlinks : (links cells).eval σ = true) : + ∀ c ∈ cells, ∀ lane, + σ (c lane).1 = σ (cells.headD fallback 0).1 ∧ + σ (c lane).2 = σ (cells.headD fallback 0).1 := by + cases cells with + | nil => exact False.elim (hne rfl) + | cons first rest => exact agree_head σ first rest hcells hlinks + +/-- A common value on every entry and exit satisfies all paired links. -/ +theorem eval_links_of_constant (σ : V → Bool) (value : Bool) (cells : List (Cell V)) + (h : ∀ c ∈ cells, ∀ lane, σ (c lane).1 = value ∧ σ (c lane).2 = value) : + (links cells).eval σ = true := by + have hcells : ∀ c ∈ cells, c.Agree σ := fun c hc lane => + ⟨(h c hc lane).1.trans (h c hc 0).1.symm, (h c hc lane).2.trans (h c hc 0).1.symm⟩ + apply (eval_links_iff σ cells hcells).2 + intro p hp + have hm := List.of_mem_zip hp + exact (h p.1 hm.1 0).1.trans (h p.2 (List.mem_of_mem_tail hm.2) 0).1.symm + +/-- There are exactly two clauses per gap. -/ +theorem length_gapClauses (previous next : Cell V) : + (gapClauses previous next).length = 2 := rfl + +/-- Each gap clause is binary, even if some port variables coincide. -/ +theorem length_of_mem_gapClauses (previous next : Cell V) {c : Clause V} + (hc : c ∈ gapClauses previous next) : c.length = 2 := by + simp only [gapClauses, List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with rfl | rfl <;> rfl + +/-- A gap contributes four literal positions, counted with multiplicity. -/ +theorem length_vars_gapClauses (previous next : Cell V) : + (gapClauses previous next).vars.length = 4 := rfl + +/-- There are exactly two clauses for each consecutive pair of cells. -/ +theorem length_links_eq_gaps (cells : List (Cell V)) : + (links cells).length = 2 * cells.consecutivePairs.length := by + simp [links, List.length_flatMap, length_gapClauses, Nat.mul_comm] + +/-- A wire with `n` cells has `2 (n - 1)` clauses, with truncated subtraction for `n = 0`. -/ +theorem length_links (cells : List (Cell V)) : + (links cells).length = 2 * (cells.length - 1) := by + rw [length_links_eq_gaps] + simp [List.consecutivePairs] + +/-- Every clause of a paired wire has exactly two literal positions. -/ +theorem length_of_mem_links (cells : List (Cell V)) {c : Clause V} + (hc : c ∈ links cells) : c.length = 2 := by + obtain ⟨p, _, hc⟩ := List.mem_flatMap.1 hc + exact length_of_mem_gapClauses p.1 p.2 hc + +/-- Paired links have width at most two. -/ +theorem width_links (cells : List (Cell V)) : ∀ c ∈ links cells, c.length ≤ 2 := + fun _ hc => Nat.le_of_eq (length_of_mem_links cells hc) + +/-- There are exactly four literal positions per gap. -/ +theorem length_vars_links (cells : List (Cell V)) : + (links cells).vars.length = 4 * (cells.length - 1) := by + have h : (links cells).map List.length = List.replicate (links cells).length 2 := by + apply List.map_eq_replicate_iff.2 + exact fun c hc => length_of_mem_links cells hc + rw [CNF.length_vars, h] + simp [length_links, Nat.mul_right_comm] + +end Cslib.Logic.PL.CNF.PairedWire diff --git a/ComplexityTests/PairedCrossover.lean b/ComplexityTests/PairedCrossover.lean new file mode 100644 index 000000000..05277fd48 --- /dev/null +++ b/ComplexityTests/PairedCrossover.lean @@ -0,0 +1,39 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +import Complexity.Logics.Propositional.CNF.Planar.PairedCrossover +import Mathlib.Data.Fintype.Pi +import Mathlib.Data.Fintype.Prod + +/-! The paired template has exactly four full models, including every internal copy and all +eight ports. Counting uses the canonical-extension bijection instead of enumerating 57 bits. -/ + +open Cslib.Logic.PL Cslib.Logic.PL.CNF.PairedCrossover + +private def modelsEquivInputs : + {σ : Variable → Bool // formula.eval σ = true} ≃ Bool × Bool where + toFun σ := (σ.val (terminal 0 0), σ.val (terminal 2 0)) + invFun ab := ⟨canonicalExtension ab.1 ab.2, eval_canonicalExtension ab.1 ab.2⟩ + left_inv σ := Subtype.ext (eq_canonicalExtension_of_holds σ.property).symm + right_inv _ := rfl + +example : Fintype.card {σ : Variable → Bool // formula.eval σ = true} = 4 := by + rw [Fintype.card_congr modelsEquivInputs] + decide + +-- Incoming and outgoing values on distinct lanes still agree across the same wire. +example {σ : Variable → Bool} (h : formula.eval σ = true) : + σ (terminal 0 1) = σ (terminal 1 0) ∧ + σ (terminal 2 1) = σ (terminal 3 0) := by + constructor + · exact (terminal_value_of_holds h 0 1).trans (terminal_value_of_holds h 1 0).symm + · exact (terminal_value_of_holds h 2 1).trans (terminal_value_of_holds h 3 0).symm + +-- The two signals are independent, with all ports populated in this concrete model. +example : formula.eval (canonicalExtension true false) = true ∧ + canonicalExtension true false (terminal 1 1) = true ∧ + canonicalExtension true false (terminal 3 1) = false := + ⟨eval_canonicalExtension true false, rfl, rfl⟩ diff --git a/ComplexityTests/PairedWire.lean b/ComplexityTests/PairedWire.lean new file mode 100644 index 000000000..b72c10171 --- /dev/null +++ b/ComplexityTests/PairedWire.lean @@ -0,0 +1,56 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +import Complexity.Logics.Propositional.CNF.Planar.PairedWire + +/-! # Paired-wire directions, propagation, and exact sizes -/ + +open Cslib.Logic.PL Cslib.Logic.PL.CNF.PairedWire + +/-- Four distinct variables per cell, with two consecutive variables per lane. -/ +private def cell (index : ℕ) : Cell ℕ := + fun lane => (4 * index + 2 * lane.val, 4 * index + 2 * lane.val + 1) + +/-- The opposite clauses use separate lanes, with the prescribed entry/exit directions. -/ +example : gapClauses (cell 0) (cell 1) = + [[(1, false), (4, true)], [(6, false), (3, true)]] := rfl + +example : (links ([] : List (Cell ℕ))).length = 0 ∧ + (links ([] : List (Cell ℕ))).vars.length = 0 := by decide + +example : (links [cell 0]).length = 0 ∧ (links [cell 0]).vars.length = 0 := by decide + +example : (links [cell 0, cell 1, cell 2]).length = 4 ∧ + (links [cell 0, cell 1, cell 2]).vars.length = 8 := by decide + +/-- Counts retain multiplicity even when all port variables coincide. -/ +example : (links [fun _ => (0, 0), fun _ => (0, 0)]).length = 2 ∧ + (links [fun _ => (0, 0), fun _ => (0, 0)]).vars.length = 4 := by decide + +example (value : Bool) : (links [cell 0, cell 1, cell 2]).eval (fun _ => value) = true := + eval_links_of_constant _ value _ (fun _ _ _ => ⟨rfl, rfl⟩) + +/-- Local agreement is satisfiable when the two cells have different representative values. -/ +example : ∀ c ∈ [cell 0, cell 1], c.Agree (fun v => decide (v < 4)) := by + intro c hc + simp only [List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with rfl | rfl <;> unfold Cell.Agree <;> decide + +/-- The forward implication excludes a drop from true to false between cells. -/ +example : (links [cell 0, cell 1]).eval (fun v => decide (v < 4)) = false := by decide + +/-- The backward implication excludes a rise from false to true between cells. -/ +example : (links [cell 0, cell 1]).eval (fun v => decide (4 ≤ v)) = false := by decide + +/-- Links alone allow different representatives when local agreement is absent. -/ +example : (links [cell 0, cell 1]).eval (fun v => v == 4) = true ∧ + ((cell 0 0).1 == 4) ≠ ((cell 1 0).1 == 4) := by decide + +/-- A compiler can recover any terminal port from local cell guarantees and satisfied links. -/ +example (σ : ℕ → Bool) (hcells : ∀ c ∈ [cell 0, cell 1, cell 2], c.Agree σ) + (hlinks : (links [cell 0, cell 1, cell 2]).eval σ = true) : + σ (cell 2 1).2 = σ (cell 0 0).1 := + (agree_head σ (cell 0) [cell 1, cell 2] hcells hlinks (cell 2) (by simp) 1).2 diff --git a/ComplexityTests/PlanarCrossoverCounting.lean b/ComplexityTests/PlanarCrossoverCounting.lean new file mode 100644 index 000000000..17167cb9a --- /dev/null +++ b/ComplexityTests/PlanarCrossoverCounting.lean @@ -0,0 +1,50 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +import Complexity.Logics.Propositional.CNF.Planar.CrossoverCounting +import Mathlib.Data.Fintype.Pi +import Mathlib.Data.Fintype.Prod + +/-! Full satisfying assignments correspond bijectively to the two incoming bits, including +after splitting. The model counts below use these structural equivalences, not enumeration. -/ + +open Cslib.Logic.PL Cslib.Logic.PL.CNF.Crossover + +private def modelsEquivInputs : + {σ : Variable → Bool // formula.eval σ = true} ≃ Bool × Bool where + toFun σ := (σ.val .aLeft, σ.val .bTop) + invFun ab := ⟨canonicalExtension ab.1 ab.2, eval_canonicalExtension ab.1 ab.2⟩ + left_inv σ := Subtype.ext (eq_canonicalExtension_of_holds σ.property).symm + right_inv _ := rfl + +private def splitModelsEquivInputs : + {σ : SplitVariable → Bool // splitFormula.eval σ = true} ≃ Bool × Bool where + toFun σ := (σ.val .aLeft, σ.val .bTop) + invFun ab := ⟨canonicalSplitExtension ab.1 ab.2, eval_canonicalSplitExtension ab.1 ab.2⟩ + left_inv σ := Subtype.ext (eq_canonicalSplitExtension_of_holds σ.property).symm + right_inv _ := rfl + +example : Fintype.card {σ : Variable → Bool // formula.eval σ = true} = 4 := by + rw [Fintype.card_congr modelsEquivInputs] + decide + +example : Fintype.card {σ : SplitVariable → Bool // splitFormula.eval σ = true} = 4 := by + rw [Fintype.card_congr splitModelsEquivInputs] + decide + +-- The mixed input has a concrete internal value, common to all six copies. +example (i : Fin 6) : canonicalSplitExtension false true (.copy .upperLeft i) = true := rfl + +-- Changing a free-looking internal value cannot produce another satisfying full assignment. +example : splitFormula.eval (Function.update (canonicalSplitExtension false true) .center true) = + false := by + cases h : splitFormula.eval + (Function.update (canonicalSplitExtension false true) .center true) with + | false => rfl + | true => + have heq := eq_canonicalSplitExtension_of_holds h + have hcenter := congrFun heq .center + simp [canonicalSplitExtension, canonicalExtension, assignment, SplitVariable.origin] at hcenter From 55e49e5a9516a978ab2d33bdbb9537fd29fe8acd Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Mon, 26 Oct 2026 07:32:59 -0400 Subject: [PATCH 5/5] feat(planar-SAT): certify the paired crossover drawing 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 | 3 + .../SAT/Planar/PairedCrossoverLayout.lean | 203 +++++ .../Planar/PairedCrossoverLayoutChecks.lean | 841 ++++++++++++++++++ .../SAT/Planar/PairedCrossoverLayoutData.lean | 253 ++++++ 4 files changed, 1300 insertions(+) create mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean create mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean create mode 100644 Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutData.lean diff --git a/Complexity.lean b/Complexity.lean index 719aee534..cfc6defa2 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -809,6 +809,9 @@ public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverL public import Complexity.Computability.Complexity.Problems.SAT.Planar.Geometry public import Complexity.Computability.Complexity.Problems.SAT.Planar.Occurrence public import Complexity.Computability.Complexity.Problems.SAT.Planar.OrdinaryRing +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayout +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutChecks +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutData public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths public import Complexity.Computability.Complexity.Problems.SAT.Planar.Paths.Occupancy public import Complexity.Computability.Complexity.Problems.SAT.Planar.PolyTime diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean new file mode 100644 index 000000000..2b111bc70 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayout.lean @@ -0,0 +1,203 @@ +/- +Copyright (c) 2026 lean-trominoes contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine, Stefan Langerman, GPT 5.6 +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutChecks +public import Complexity.Foundations.Geometry.Orthogonal.Simple +import Mathlib.Data.List.Zip +import Mathlib.Tactic.Linarith + +/-! +# Certified continuous orthogonal paired-port crossover + +The finite checks for the fixed degree-three CNF template certify entire real supports. +Its 57 variable vertices and 78 clause vertices are distinct. Its 162 incidence routes are simple, +orthogonal, avoid nonincident vertices, and meet only at common graph endpoints. Their total +wire length is 2192. Eight mutually disjoint access routes connect degree-two terminals to the +boundary of `[0,240]²`, and meet the core only at the corresponding terminal. Each terminal +therefore accommodates exactly one external clause occurrence. + +## Main definitions + +This module uses the fixed table from `PairedCrossoverLayoutData` and the shared `Orthogonal` route +and continuous support semantics. + +## Main results + +* `Cslib.Logic.PL.CNF.PairedCrossover.incidence_simple`: continuous segment simplicity. +* `Cslib.Logic.PL.CNF.PairedCrossover.routes_contact`: intersections are common endpoints. +* `Cslib.Logic.PL.CNF.PairedCrossover.access_contact`: access meets the core only at its terminal. +* `Cslib.Logic.PL.CNF.PairedCrossover.access_boundary_isolation`: only ports touch the boundary. + +## References + +* David Lichtenstein, *Planar Formulae and Their Uses*, Figs. 4–5 [Lichtenstein1982]. +* MIT–ULB CompGeom Group, *Undecidability of Tiling with a Tromino*, Fig. 8(b) [Tromino2025]. + +The paired-terminal modification and its continuous orthogonal certificates are original. +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF.PairedCrossover + +open Orthogonal + +private theorem support_bounds_of_points {r : Route} + (h : ∀ q ∈ r, 20 ≤ q.1 ∧ q.1 ≤ 220 ∧ 20 ≤ q.2 ∧ q.2 ≤ 220) + {p : ℝ × ℝ} (hp : p ∈ support r) : + 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by + have cast_bounds (q : Point) (hq : q ∈ r) : + (20 : ℝ) ≤ q.1 ∧ (q.1 : ℝ) ≤ 220 ∧ 20 ≤ (q.2 : ℝ) ∧ (q.2 : ℝ) ≤ 220 := by + exact_mod_cast h q hq + rcases hp with ⟨q, hq, rfl⟩ | ⟨e, he, hp⟩ + · exact cast_bounds q hq + · have he' := List.of_mem_zip he + have ha := cast_bounds e.1 he'.1 + have hb := cast_bounds e.2 (List.mem_of_mem_tail he'.2) + obtain ⟨hx, hy⟩ := mem_segment_bounds hp + rw [Set.mem_uIcc] at hx hy + have hx' : 20 ≤ p.1 ∧ p.1 ≤ 220 := by + rcases hx with hx | hx <;> constructor <;> linarith [ha.1, ha.2.1, hb.1, hb.2.1] + have hy' : 20 ≤ p.2 ∧ p.2 ≤ 220 := by + rcases hy with hy | hy <;> constructor <;> + linarith [ha.2.2.1, ha.2.2.2, hb.2.2.1, hb.2.2.2] + exact ⟨hx'.1, hx'.2, hy'.1, hy'.2⟩ + +/-- Every real point of the core drawing is strictly inside the outer 240-by-240 box. -/ +theorem core_support_interior {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes) + {p : ℝ × ℝ} (hp : p ∈ support e.2.2) : + 0 < p.1 ∧ p.1 < 240 ∧ 0 < p.2 ∧ p.2 < 240 := by + have h := support_bounds_of_points (core_bounds e he) hp + constructor + · linarith [h.1] + constructor + · linarith [h.2.1] + constructor <;> linarith [h.2.2.1, h.2.2.2] + +/-- Distinct segments of a route intersect only at their consecutive shared bend. -/ +theorem incidence_simple {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes) + {a b : Point × Point} (ha : a ∈ e.2.2.consecutivePairs) + (hb : b ∈ e.2.2.consecutivePairs) (hne : a ≠ b) + {p : ℝ × ℝ} (hp : p ∈ segment a.1 a.2) (hq : p ∈ segment b.1 b.2) : + ∃ q ∈ consecutiveContact a b, p = realPoint q := + segmentContactCheck_sound (incidence_simple_check e he a ha b hb hne) hp hq + +/-- Every incidence route is simple in the shared continuous polygonal-route semantics. -/ +theorem incidence_isSimple {e : ℕ × Variable × Route} (he : e ∈ incidenceRoutes) : + IsSimple e.2.2 := by + refine ⟨incidence_points_nodup e he, ?_⟩ + intro a ha b hb hne p hp hq + obtain ⟨q, hq, hpq⟩ := incidence_simple he ha hb hne hp hq + unfold consecutiveContact at hq + split_ifs at hq with h h' + · have hqa : q = a.2 := List.mem_singleton.mp hq + subst q + exact ⟨Or.inr hpq, Or.inl (hpq.trans (congrArg realPoint h))⟩ + · have hqa : q = a.1 := List.mem_singleton.mp hq + subst q + exact ⟨Or.inl hpq, Or.inr (hpq.trans (congrArg realPoint h'.symm))⟩ + · exact False.elim (List.not_mem_nil hq) + +/-- Every continuous intersection of distinct incidence routes is a shared graph endpoint. -/ +theorem routes_contact {e f : ℕ × Variable × Route} + (he : e ∈ incidenceRoutes) (hf : f ∈ incidenceRoutes) (hne : e ≠ f) + {p : ℝ × ℝ} (hp : p ∈ support e.2.2) (hq : p ∈ support f.2.2) : + ∃ q ∈ commonEndpoints e f, p = realPoint q := + routeContactCheck_sound (routes_contact_check e he f hf hne) hp hq + +/-- Continuous incidence routes avoid every nonincident variable vertex. -/ +theorem variable_not_mem_support {e : ℕ × Variable × Route} + (he : e ∈ incidenceRoutes) {v : Variable} (hv : v ≠ e.2.1) : + realPoint (variablePosition v) ∉ support e.2.2 := + not_mem_support_of_routeContactCheck (variable_avoidance_check e he v hv) + +/-- Continuous incidence routes avoid every nonincident clause vertex. -/ +theorem clause_not_mem_support {e : ℕ × Variable × Route} + (he : e ∈ incidenceRoutes) {i : Fin 78} (hi : i.val ≠ e.1) : + realPoint (clausePosition i) ∉ support e.2.2 := + not_mem_support_of_routeContactCheck (clause_avoidance_check e he i hi) + +/-- Every literal incidence appears exactly once in the route list. -/ +theorem incidenceEndpoints_nodup : + (incidenceRoutes.map fun e => (e.1, e.2.1)).Nodup := by decide +kernel + +/-- Every variable vertex lies in the core rectangle. -/ +theorem variable_bounds : ∀ v, 20 ≤ (variablePosition v).1 ∧ (variablePosition v).1 ≤ 220 ∧ + 20 ≤ (variablePosition v).2 ∧ (variablePosition v).2 ≤ 220 := by decide +kernel + +/-- Every clause vertex lies in the core rectangle. -/ +theorem clause_bounds : ∀ p ∈ clausePositions, + 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := by decide +kernel + +/-- Each of the 57 variable names is genuinely used by the fixed formula. -/ +theorem variables_used : ∀ v, v ∈ formula.vars := by decide +kernel + +/-- No access route visits any other variable vertex. -/ +theorem access_variable_avoidance_check : ∀ s l v, v ≠ terminal s l → + routeContactCheck [] (accessRoute s l) [variablePosition v] = true := by decide +kernel + +/-- No access route visits a clause vertex. -/ +theorem access_clause_avoidance_check : ∀ s l, ∀ p ∈ clausePositions, + routeContactCheck [] (accessRoute s l) [p] = true := by decide +kernel + +/-- The full real access route avoids every other variable vertex. -/ +theorem access_variable_not_mem {s : Fin 4} {l : Fin 2} {v : Variable} + (hv : v ≠ terminal s l) : + realPoint (variablePosition v) ∉ support (accessRoute s l) := + not_mem_support_of_routeContactCheck (access_variable_avoidance_check s l v hv) + +/-- The full real access route avoids every clause vertex. -/ +theorem access_clause_not_mem {s : Fin 4} {l : Fin 2} {p : Point} + (hp : p ∈ clausePositions) : + realPoint p ∉ support (accessRoute s l) := + not_mem_support_of_routeContactCheck (access_clause_avoidance_check s l p hp) + +/-- Each access route has one segment and 20 units of wire length. -/ +theorem access_route_sizes : ∀ s l, (accessRoute s l).consecutivePairs.length = 1 ∧ + wireLength (accessRoute s l) = 20 := PairedPorts.access_route_sizes + +/-- Including all eight accesses gives 415 segments and total wire length 2352. -/ +theorem full_route_sizes : + (incidenceRoutes.map fun e => e.2.2.consecutivePairs.length).sum + + ((List.finRange 4).flatMap fun s => (List.finRange 2).map fun l => + (accessRoute s l).consecutivePairs.length).sum = 415 ∧ + (incidenceRoutes.map fun e => wireLength e.2.2).sum + + ((List.finRange 4).flatMap fun s => (List.finRange 2).map fun l => + wireLength (accessRoute s l)).sum = 2352 := by + rw [route_sizes.1, route_sizes.2] + decide +kernel + +/-- Each straight access is simple over its full real support. -/ +theorem access_isSimple (s : Fin 4) (l : Fin 2) : IsSimple (accessRoute s l) := + PairedPorts.access_isSimple s l + +/-- Distinct accesses have disjoint full real support. -/ +theorem access_disjoint {p q : PairedPorts.Port} (h : p ≠ q) : + Disjoint (support (accessRoute p.1 p.2)) (support (accessRoute q.1 q.2)) := + PairedPorts.access_disjoint h + +/-- Every continuous contact between an access and the core is its associated port. -/ +theorem access_contact {s : Fin 4} {l : Fin 2} {e : ℕ × Variable × Route} + (he : e ∈ incidenceRoutes) {p : ℝ × ℝ} + (hp : p ∈ support (accessRoute s l)) (hq : p ∈ support e.2.2) : + e.2.1 = terminal s l ∧ p = realPoint (variablePosition (terminal s l)) := by + obtain ⟨q, hq, hpq⟩ := routeContactCheck_sound (access_contact_check s l e he) hp hq + split_ifs at hq with h + · have hq' : q = variablePosition (terminal s l) := List.mem_singleton.mp hq + exact ⟨h, hq' ▸ hpq⟩ + · exact False.elim (List.not_mem_nil hq) + +/-- Only the designated boundary point of an access lies on the outer box boundary. -/ +theorem access_boundary_isolation {s : Fin 4} {l : Fin 2} {p : ℝ × ℝ} + (hp : p ∈ support (accessRoute s l)) : + 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 (boundaryPort s l)) := + PairedPorts.access_boundary_isolation hp + +end Cslib.Logic.PL.CNF.PairedCrossover diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean new file mode 100644 index 000000000..1f584ab93 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean @@ -0,0 +1,841 @@ +/- +Copyright (c) 2026 lean-trominoes contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine, Stefan Langerman, GPT 5.6 +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Problems.SAT.Planar.PairedCrossoverLayoutData +public import Complexity.Foundations.Geometry.Orthogonal.Separation +import Mathlib.Data.List.GetD +import Mathlib.Data.List.Nodup +import Mathlib.Data.List.Zip +import Mathlib.Tactic.FinCases + +/-! +# Finite certificates for the paired-port orthogonal crossover + +Finite arithmetic certificates control the full real support of every route. The core has +57 variable vertices, 78 clause vertices and 162 incidences. Eight mutually disjoint access routes +connect the signal terminals to the boundary of `[0,240]²`; only the associated terminal may meet +an access route. An external clause uses this access and the terminal's remaining occurrence. + +## Main definitions + +* `Cslib.Logic.PL.CNF.PairedCrossover.clausePosition`: indexed positions of clause vertices. +* `Cslib.Logic.PL.CNF.PairedCrossover.commonEndpoints`: permitted contacts of incidence routes. + +## Main results + +* `Cslib.Logic.PL.CNF.PairedCrossover.incidenceRoutes_cover`: exact ordinary CNF literal incidences. +* `Cslib.Logic.PL.CNF.PairedCrossover.routes_contact_check`: finite permitted-contact certificate. +* `Cslib.Logic.PL.CNF.PairedCrossover.access_contact_check`: finite access isolation certificate. + +## References + +* David Lichtenstein, *Planar Formulae and Their Uses*, Figs. 4–5 [Lichtenstein1982]. +* MIT–ULB CompGeom Group, *Undecidability of Tiling with a Tromino*, Fig. 8(b) [Tromino2025]. + +The paired modification and its finite orthogonal certificates are original. +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF.PairedCrossover + +open Orthogonal + +/-- The clause position at an index. All indices in `incidenceRoutes` are certified in range. -/ +def clausePosition (i : ℕ) : Point := clausePositions.getD i (0, 0) + +/-- Every variable, including both lanes on each side. -/ +def variableList : List Variable := + [.center] ++ (List.finRange 4).flatMap (fun s => + (List.finRange 2).map (Variable.port s)) ++ + Crossover.internalList.flatMap fun v => List.ofFn fun i : Fin 6 => Variable.copy v i + +/-- Every variable is included in the finite drawing vertex list. -/ +theorem mem_variableList : ∀ v, v ∈ variableList := by decide +kernel + +/-- The exact literal-incidence list of the ordinary CNF formula. -/ +theorem incidenceRoutes_cover : + incidenceRoutes.map (fun e => (e.1, e.2.1)) = + formula.zipIdx.flatMap (fun ci => ci.1.map fun l => (ci.2, l.1)) := by + decide +kernel + +/-- The fixed formula and drawing have 78 clauses and 162 incidences. -/ +theorem drawing_sizes : clausePositions.length = 78 ∧ incidenceRoutes.length = 162 := by + decide +kernel + +/-- Variable vertices have distinct positions. -/ +theorem variablePosition_injective : Function.Injective variablePosition := by + have h : (variableList.map variablePosition).Nodup := by decide +kernel + exact fun v w => List.inj_on_of_nodup_map h (mem_variableList v) (mem_variableList w) + +/-- Clause vertices are pairwise distinct. -/ +theorem clausePositions_nodup : clausePositions.Nodup := by decide +kernel + +/-- No clause vertex is a variable vertex. -/ +theorem variablePosition_not_mem_clauses : + ∀ v, variablePosition v ∉ clausePositions := by decide +kernel + +/-- The only allowed contacts between two distinct incidence routes are shared graph endpoints. -/ +def commonEndpoints (e f : ℕ × Variable × Route) : List Point := + (if e.1 = f.1 then [clausePosition e.1] else []) ++ + (if e.2.1 = f.2.1 then [variablePosition e.2.1] else []) + +/-- A pair of different segments may meet only at a consecutive shared bend. -/ +def consecutiveContact (a b : Point × Point) : List Point := + if a.2 = b.1 then [a.2] else if b.2 = a.1 then [a.1] else [] + +private instance (r : Route) : Decidable (IsOrthogonal r) := + inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2)) + +private def LocalSpec (e : ℕ × Variable × Route) : Prop := + (e.1 < 78 ∧ e.2.2.head? = some (clausePosition e.1) ∧ + e.2.2.getLast? = some (variablePosition e.2.1)) ∧ + IsOrthogonal e.2.2 ∧ + (∀ p ∈ e.2.2, 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220) ∧ + e.2.2.Nodup ∧ + ∀ a ∈ e.2.2.consecutivePairs, ∀ b ∈ e.2.2.consecutivePairs, a ≠ b → + segmentContactCheck (consecutiveContact a b) a.1 a.2 b.1 b.2 = true + +private instance (e : ℕ × Variable × Route) : Decidable (LocalSpec e) := + inferInstanceAs (Decidable (_ ∧ _)) + +private def rowCheck (e : ℕ × Variable × Route) : Bool := + decide (LocalSpec e) && + ((incidenceRoutes.all fun f => e == f || + routeContactCheck (commonEndpoints e f) e.2.2 f.2.2) && + ((variableList.all fun v => v == e.2.1 || + routeContactCheck [] e.2.2 [variablePosition v]) && + ((List.finRange 78).all fun i => i.val == e.1 || + routeContactCheck [] e.2.2 [clausePosition i]))) + +private def routeAt (i : Fin 162) : ℕ × Variable × Route := + incidenceRoutes.getD i (0, .center, []) + +-- Separate closed certificates keep kernel reduction memory bounded per incidence row. + +private theorem row_0 : rowCheck (routeAt 0) = true := by decide +kernel + +private theorem row_1 : rowCheck (routeAt 1) = true := by decide +kernel +private theorem row_2 : rowCheck (routeAt 2) = true := by decide +kernel +private theorem row_3 : rowCheck (routeAt 3) = true := by decide +kernel +private theorem row_4 : rowCheck (routeAt 4) = true := by decide +kernel +private theorem row_5 : rowCheck (routeAt 5) = true := by decide +kernel +private theorem row_6 : rowCheck (routeAt 6) = true := by decide +kernel +private theorem row_7 : rowCheck (routeAt 7) = true := by decide +kernel +private theorem row_8 : rowCheck (routeAt 8) = true := by decide +kernel +private theorem row_9 : rowCheck (routeAt 9) = true := by decide +kernel +private theorem row_10 : rowCheck (routeAt 10) = true := by decide +kernel + +private theorem row_11 : rowCheck (routeAt 11) = true := by decide +kernel +private theorem row_12 : rowCheck (routeAt 12) = true := by decide +kernel +private theorem row_13 : rowCheck (routeAt 13) = true := by decide +kernel +private theorem row_14 : rowCheck (routeAt 14) = true := by decide +kernel +private theorem row_15 : rowCheck (routeAt 15) = true := by decide +kernel +private theorem row_16 : rowCheck (routeAt 16) = true := by decide +kernel +private theorem row_17 : rowCheck (routeAt 17) = true := by decide +kernel +private theorem row_18 : rowCheck (routeAt 18) = true := by decide +kernel +private theorem row_19 : rowCheck (routeAt 19) = true := by decide +kernel +private theorem row_20 : rowCheck (routeAt 20) = true := by decide +kernel + +private theorem row_21 : rowCheck (routeAt 21) = true := by decide +kernel +private theorem row_22 : rowCheck (routeAt 22) = true := by decide +kernel +private theorem row_23 : rowCheck (routeAt 23) = true := by decide +kernel +private theorem row_24 : rowCheck (routeAt 24) = true := by decide +kernel +private theorem row_25 : rowCheck (routeAt 25) = true := by decide +kernel +private theorem row_26 : rowCheck (routeAt 26) = true := by decide +kernel +private theorem row_27 : rowCheck (routeAt 27) = true := by decide +kernel +private theorem row_28 : rowCheck (routeAt 28) = true := by decide +kernel +private theorem row_29 : rowCheck (routeAt 29) = true := by decide +kernel +private theorem row_30 : rowCheck (routeAt 30) = true := by decide +kernel + +private theorem row_31 : rowCheck (routeAt 31) = true := by decide +kernel +private theorem row_32 : rowCheck (routeAt 32) = true := by decide +kernel +private theorem row_33 : rowCheck (routeAt 33) = true := by decide +kernel +private theorem row_34 : rowCheck (routeAt 34) = true := by decide +kernel +private theorem row_35 : rowCheck (routeAt 35) = true := by decide +kernel +private theorem row_36 : rowCheck (routeAt 36) = true := by decide +kernel +private theorem row_37 : rowCheck (routeAt 37) = true := by decide +kernel +private theorem row_38 : rowCheck (routeAt 38) = true := by decide +kernel +private theorem row_39 : rowCheck (routeAt 39) = true := by decide +kernel +private theorem row_40 : rowCheck (routeAt 40) = true := by decide +kernel + +private theorem row_41 : rowCheck (routeAt 41) = true := by decide +kernel +private theorem row_42 : rowCheck (routeAt 42) = true := by decide +kernel +private theorem row_43 : rowCheck (routeAt 43) = true := by decide +kernel +private theorem row_44 : rowCheck (routeAt 44) = true := by decide +kernel +private theorem row_45 : rowCheck (routeAt 45) = true := by decide +kernel +private theorem row_46 : rowCheck (routeAt 46) = true := by decide +kernel +private theorem row_47 : rowCheck (routeAt 47) = true := by decide +kernel +private theorem row_48 : rowCheck (routeAt 48) = true := by decide +kernel +private theorem row_49 : rowCheck (routeAt 49) = true := by decide +kernel +private theorem row_50 : rowCheck (routeAt 50) = true := by decide +kernel + +private theorem row_51 : rowCheck (routeAt 51) = true := by decide +kernel +private theorem row_52 : rowCheck (routeAt 52) = true := by decide +kernel +private theorem row_53 : rowCheck (routeAt 53) = true := by decide +kernel +private theorem row_54 : rowCheck (routeAt 54) = true := by decide +kernel +private theorem row_55 : rowCheck (routeAt 55) = true := by decide +kernel +private theorem row_56 : rowCheck (routeAt 56) = true := by decide +kernel +private theorem row_57 : rowCheck (routeAt 57) = true := by decide +kernel +private theorem row_58 : rowCheck (routeAt 58) = true := by decide +kernel +private theorem row_59 : rowCheck (routeAt 59) = true := by decide +kernel +private theorem row_60 : rowCheck (routeAt 60) = true := by decide +kernel + +private theorem row_61 : rowCheck (routeAt 61) = true := by decide +kernel +private theorem row_62 : rowCheck (routeAt 62) = true := by decide +kernel +private theorem row_63 : rowCheck (routeAt 63) = true := by decide +kernel +private theorem row_64 : rowCheck (routeAt 64) = true := by decide +kernel +private theorem row_65 : rowCheck (routeAt 65) = true := by decide +kernel +private theorem row_66 : rowCheck (routeAt 66) = true := by decide +kernel +private theorem row_67 : rowCheck (routeAt 67) = true := by decide +kernel +private theorem row_68 : rowCheck (routeAt 68) = true := by decide +kernel +private theorem row_69 : rowCheck (routeAt 69) = true := by decide +kernel +private theorem row_70 : rowCheck (routeAt 70) = true := by decide +kernel + +private theorem row_71 : rowCheck (routeAt 71) = true := by decide +kernel +private theorem row_72 : rowCheck (routeAt 72) = true := by decide +kernel +private theorem row_73 : rowCheck (routeAt 73) = true := by decide +kernel +private theorem row_74 : rowCheck (routeAt 74) = true := by decide +kernel +private theorem row_75 : rowCheck (routeAt 75) = true := by decide +kernel +private theorem row_76 : rowCheck (routeAt 76) = true := by decide +kernel +private theorem row_77 : rowCheck (routeAt 77) = true := by decide +kernel +private theorem row_78 : rowCheck (routeAt 78) = true := by decide +kernel +private theorem row_79 : rowCheck (routeAt 79) = true := by decide +kernel +private theorem row_80 : rowCheck (routeAt 80) = true := by decide +kernel + +private theorem row_81 : rowCheck (routeAt 81) = true := by decide +kernel +private theorem row_82 : rowCheck (routeAt 82) = true := by decide +kernel +private theorem row_83 : rowCheck (routeAt 83) = true := by decide +kernel +private theorem row_84 : rowCheck (routeAt 84) = true := by decide +kernel +private theorem row_85 : rowCheck (routeAt 85) = true := by decide +kernel +private theorem row_86 : rowCheck (routeAt 86) = true := by decide +kernel +private theorem row_87 : rowCheck (routeAt 87) = true := by decide +kernel +private theorem row_88 : rowCheck (routeAt 88) = true := by decide +kernel +private theorem row_89 : rowCheck (routeAt 89) = true := by decide +kernel +private theorem row_90 : rowCheck (routeAt 90) = true := by decide +kernel + +private theorem row_91 : rowCheck (routeAt 91) = true := by decide +kernel +private theorem row_92 : rowCheck (routeAt 92) = true := by decide +kernel +private theorem row_93 : rowCheck (routeAt 93) = true := by decide +kernel +private theorem row_94 : rowCheck (routeAt 94) = true := by decide +kernel +private theorem row_95 : rowCheck (routeAt 95) = true := by decide +kernel +private theorem row_96 : rowCheck (routeAt 96) = true := by decide +kernel +private theorem row_97 : rowCheck (routeAt 97) = true := by decide +kernel +private theorem row_98 : rowCheck (routeAt 98) = true := by decide +kernel +private theorem row_99 : rowCheck (routeAt 99) = true := by decide +kernel +private theorem row_100 : rowCheck (routeAt 100) = true := by decide +kernel + +private theorem row_101 : rowCheck (routeAt 101) = true := by decide +kernel +private theorem row_102 : rowCheck (routeAt 102) = true := by decide +kernel +private theorem row_103 : rowCheck (routeAt 103) = true := by decide +kernel +private theorem row_104 : rowCheck (routeAt 104) = true := by decide +kernel +private theorem row_105 : rowCheck (routeAt 105) = true := by decide +kernel +private theorem row_106 : rowCheck (routeAt 106) = true := by decide +kernel +private theorem row_107 : rowCheck (routeAt 107) = true := by decide +kernel +private theorem row_108 : rowCheck (routeAt 108) = true := by decide +kernel +private theorem row_109 : rowCheck (routeAt 109) = true := by decide +kernel +private theorem row_110 : rowCheck (routeAt 110) = true := by decide +kernel + +private theorem row_111 : rowCheck (routeAt 111) = true := by decide +kernel +private theorem row_112 : rowCheck (routeAt 112) = true := by decide +kernel +private theorem row_113 : rowCheck (routeAt 113) = true := by decide +kernel +private theorem row_114 : rowCheck (routeAt 114) = true := by decide +kernel +private theorem row_115 : rowCheck (routeAt 115) = true := by decide +kernel +private theorem row_116 : rowCheck (routeAt 116) = true := by decide +kernel +private theorem row_117 : rowCheck (routeAt 117) = true := by decide +kernel +private theorem row_118 : rowCheck (routeAt 118) = true := by decide +kernel +private theorem row_119 : rowCheck (routeAt 119) = true := by decide +kernel +private theorem row_120 : rowCheck (routeAt 120) = true := by decide +kernel + +private theorem row_121 : rowCheck (routeAt 121) = true := by decide +kernel +private theorem row_122 : rowCheck (routeAt 122) = true := by decide +kernel +private theorem row_123 : rowCheck (routeAt 123) = true := by decide +kernel +private theorem row_124 : rowCheck (routeAt 124) = true := by decide +kernel +private theorem row_125 : rowCheck (routeAt 125) = true := by decide +kernel +private theorem row_126 : rowCheck (routeAt 126) = true := by decide +kernel +private theorem row_127 : rowCheck (routeAt 127) = true := by decide +kernel +private theorem row_128 : rowCheck (routeAt 128) = true := by decide +kernel +private theorem row_129 : rowCheck (routeAt 129) = true := by decide +kernel +private theorem row_130 : rowCheck (routeAt 130) = true := by decide +kernel + +private theorem row_131 : rowCheck (routeAt 131) = true := by decide +kernel +private theorem row_132 : rowCheck (routeAt 132) = true := by decide +kernel +private theorem row_133 : rowCheck (routeAt 133) = true := by decide +kernel +private theorem row_134 : rowCheck (routeAt 134) = true := by decide +kernel +private theorem row_135 : rowCheck (routeAt 135) = true := by decide +kernel +private theorem row_136 : rowCheck (routeAt 136) = true := by decide +kernel +private theorem row_137 : rowCheck (routeAt 137) = true := by decide +kernel +private theorem row_138 : rowCheck (routeAt 138) = true := by decide +kernel +private theorem row_139 : rowCheck (routeAt 139) = true := by decide +kernel +private theorem row_140 : rowCheck (routeAt 140) = true := by decide +kernel + +private theorem row_141 : rowCheck (routeAt 141) = true := by decide +kernel +private theorem row_142 : rowCheck (routeAt 142) = true := by decide +kernel +private theorem row_143 : rowCheck (routeAt 143) = true := by decide +kernel +private theorem row_144 : rowCheck (routeAt 144) = true := by decide +kernel +private theorem row_145 : rowCheck (routeAt 145) = true := by decide +kernel +private theorem row_146 : rowCheck (routeAt 146) = true := by decide +kernel +private theorem row_147 : rowCheck (routeAt 147) = true := by decide +kernel +private theorem row_148 : rowCheck (routeAt 148) = true := by decide +kernel +private theorem row_149 : rowCheck (routeAt 149) = true := by decide +kernel +private theorem row_150 : rowCheck (routeAt 150) = true := by decide +kernel + +private theorem row_151 : rowCheck (routeAt 151) = true := by decide +kernel +private theorem row_152 : rowCheck (routeAt 152) = true := by decide +kernel +private theorem row_153 : rowCheck (routeAt 153) = true := by decide +kernel + +private theorem row_154 : rowCheck (routeAt 154) = true := by decide +kernel +private theorem row_155 : rowCheck (routeAt 155) = true := by decide +kernel +private theorem row_156 : rowCheck (routeAt 156) = true := by decide +kernel +private theorem row_157 : rowCheck (routeAt 157) = true := by decide +kernel +private theorem row_158 : rowCheck (routeAt 158) = true := by decide +kernel +private theorem row_159 : rowCheck (routeAt 159) = true := by decide +kernel +private theorem row_160 : rowCheck (routeAt 160) = true := by decide +kernel +private theorem row_161 : rowCheck (routeAt 161) = true := by decide +kernel + +-- Keep dispatch proofs small as well as the individual kernel certificates. In particular, +-- no theorem elaborates the full 162-case split: six rows form a block, then 27 blocks cover all. +private def blockIndex (q : Fin 27) (r : Fin 6) : Fin 162 := + ⟨q.val * 6 + r.val, by omega⟩ + +private theorem block_0 (r : Fin 6) : rowCheck (routeAt (blockIndex 0 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (0 : Fin 162) + exact row_0 + · conv_lhs => arg 1; arg 1; change (1 : Fin 162) + exact row_1 + · conv_lhs => arg 1; arg 1; change (2 : Fin 162) + exact row_2 + · conv_lhs => arg 1; arg 1; change (3 : Fin 162) + exact row_3 + · conv_lhs => arg 1; arg 1; change (4 : Fin 162) + exact row_4 + · conv_lhs => arg 1; arg 1; change (5 : Fin 162) + exact row_5 + +private theorem block_1 (r : Fin 6) : rowCheck (routeAt (blockIndex 1 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (6 : Fin 162) + exact row_6 + · conv_lhs => arg 1; arg 1; change (7 : Fin 162) + exact row_7 + · conv_lhs => arg 1; arg 1; change (8 : Fin 162) + exact row_8 + · conv_lhs => arg 1; arg 1; change (9 : Fin 162) + exact row_9 + · conv_lhs => arg 1; arg 1; change (10 : Fin 162) + exact row_10 + · conv_lhs => arg 1; arg 1; change (11 : Fin 162) + exact row_11 + +private theorem block_2 (r : Fin 6) : rowCheck (routeAt (blockIndex 2 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (12 : Fin 162) + exact row_12 + · conv_lhs => arg 1; arg 1; change (13 : Fin 162) + exact row_13 + · conv_lhs => arg 1; arg 1; change (14 : Fin 162) + exact row_14 + · conv_lhs => arg 1; arg 1; change (15 : Fin 162) + exact row_15 + · conv_lhs => arg 1; arg 1; change (16 : Fin 162) + exact row_16 + · conv_lhs => arg 1; arg 1; change (17 : Fin 162) + exact row_17 + +private theorem block_3 (r : Fin 6) : rowCheck (routeAt (blockIndex 3 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (18 : Fin 162) + exact row_18 + · conv_lhs => arg 1; arg 1; change (19 : Fin 162) + exact row_19 + · conv_lhs => arg 1; arg 1; change (20 : Fin 162) + exact row_20 + · conv_lhs => arg 1; arg 1; change (21 : Fin 162) + exact row_21 + · conv_lhs => arg 1; arg 1; change (22 : Fin 162) + exact row_22 + · conv_lhs => arg 1; arg 1; change (23 : Fin 162) + exact row_23 + +private theorem block_4 (r : Fin 6) : rowCheck (routeAt (blockIndex 4 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (24 : Fin 162) + exact row_24 + · conv_lhs => arg 1; arg 1; change (25 : Fin 162) + exact row_25 + · conv_lhs => arg 1; arg 1; change (26 : Fin 162) + exact row_26 + · conv_lhs => arg 1; arg 1; change (27 : Fin 162) + exact row_27 + · conv_lhs => arg 1; arg 1; change (28 : Fin 162) + exact row_28 + · conv_lhs => arg 1; arg 1; change (29 : Fin 162) + exact row_29 + +private theorem block_5 (r : Fin 6) : rowCheck (routeAt (blockIndex 5 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (30 : Fin 162) + exact row_30 + · conv_lhs => arg 1; arg 1; change (31 : Fin 162) + exact row_31 + · conv_lhs => arg 1; arg 1; change (32 : Fin 162) + exact row_32 + · conv_lhs => arg 1; arg 1; change (33 : Fin 162) + exact row_33 + · conv_lhs => arg 1; arg 1; change (34 : Fin 162) + exact row_34 + · conv_lhs => arg 1; arg 1; change (35 : Fin 162) + exact row_35 + +private theorem block_6 (r : Fin 6) : rowCheck (routeAt (blockIndex 6 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (36 : Fin 162) + exact row_36 + · conv_lhs => arg 1; arg 1; change (37 : Fin 162) + exact row_37 + · conv_lhs => arg 1; arg 1; change (38 : Fin 162) + exact row_38 + · conv_lhs => arg 1; arg 1; change (39 : Fin 162) + exact row_39 + · conv_lhs => arg 1; arg 1; change (40 : Fin 162) + exact row_40 + · conv_lhs => arg 1; arg 1; change (41 : Fin 162) + exact row_41 + +private theorem block_7 (r : Fin 6) : rowCheck (routeAt (blockIndex 7 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (42 : Fin 162) + exact row_42 + · conv_lhs => arg 1; arg 1; change (43 : Fin 162) + exact row_43 + · conv_lhs => arg 1; arg 1; change (44 : Fin 162) + exact row_44 + · conv_lhs => arg 1; arg 1; change (45 : Fin 162) + exact row_45 + · conv_lhs => arg 1; arg 1; change (46 : Fin 162) + exact row_46 + · conv_lhs => arg 1; arg 1; change (47 : Fin 162) + exact row_47 + +private theorem block_8 (r : Fin 6) : rowCheck (routeAt (blockIndex 8 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (48 : Fin 162) + exact row_48 + · conv_lhs => arg 1; arg 1; change (49 : Fin 162) + exact row_49 + · conv_lhs => arg 1; arg 1; change (50 : Fin 162) + exact row_50 + · conv_lhs => arg 1; arg 1; change (51 : Fin 162) + exact row_51 + · conv_lhs => arg 1; arg 1; change (52 : Fin 162) + exact row_52 + · conv_lhs => arg 1; arg 1; change (53 : Fin 162) + exact row_53 + +private theorem block_9 (r : Fin 6) : rowCheck (routeAt (blockIndex 9 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (54 : Fin 162) + exact row_54 + · conv_lhs => arg 1; arg 1; change (55 : Fin 162) + exact row_55 + · conv_lhs => arg 1; arg 1; change (56 : Fin 162) + exact row_56 + · conv_lhs => arg 1; arg 1; change (57 : Fin 162) + exact row_57 + · conv_lhs => arg 1; arg 1; change (58 : Fin 162) + exact row_58 + · conv_lhs => arg 1; arg 1; change (59 : Fin 162) + exact row_59 + +private theorem block_10 (r : Fin 6) : rowCheck (routeAt (blockIndex 10 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (60 : Fin 162) + exact row_60 + · conv_lhs => arg 1; arg 1; change (61 : Fin 162) + exact row_61 + · conv_lhs => arg 1; arg 1; change (62 : Fin 162) + exact row_62 + · conv_lhs => arg 1; arg 1; change (63 : Fin 162) + exact row_63 + · conv_lhs => arg 1; arg 1; change (64 : Fin 162) + exact row_64 + · conv_lhs => arg 1; arg 1; change (65 : Fin 162) + exact row_65 + +private theorem block_11 (r : Fin 6) : rowCheck (routeAt (blockIndex 11 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (66 : Fin 162) + exact row_66 + · conv_lhs => arg 1; arg 1; change (67 : Fin 162) + exact row_67 + · conv_lhs => arg 1; arg 1; change (68 : Fin 162) + exact row_68 + · conv_lhs => arg 1; arg 1; change (69 : Fin 162) + exact row_69 + · conv_lhs => arg 1; arg 1; change (70 : Fin 162) + exact row_70 + · conv_lhs => arg 1; arg 1; change (71 : Fin 162) + exact row_71 + +private theorem block_12 (r : Fin 6) : rowCheck (routeAt (blockIndex 12 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (72 : Fin 162) + exact row_72 + · conv_lhs => arg 1; arg 1; change (73 : Fin 162) + exact row_73 + · conv_lhs => arg 1; arg 1; change (74 : Fin 162) + exact row_74 + · conv_lhs => arg 1; arg 1; change (75 : Fin 162) + exact row_75 + · conv_lhs => arg 1; arg 1; change (76 : Fin 162) + exact row_76 + · conv_lhs => arg 1; arg 1; change (77 : Fin 162) + exact row_77 + +private theorem block_13 (r : Fin 6) : rowCheck (routeAt (blockIndex 13 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (78 : Fin 162) + exact row_78 + · conv_lhs => arg 1; arg 1; change (79 : Fin 162) + exact row_79 + · conv_lhs => arg 1; arg 1; change (80 : Fin 162) + exact row_80 + · conv_lhs => arg 1; arg 1; change (81 : Fin 162) + exact row_81 + · conv_lhs => arg 1; arg 1; change (82 : Fin 162) + exact row_82 + · conv_lhs => arg 1; arg 1; change (83 : Fin 162) + exact row_83 + +private theorem block_14 (r : Fin 6) : rowCheck (routeAt (blockIndex 14 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (84 : Fin 162) + exact row_84 + · conv_lhs => arg 1; arg 1; change (85 : Fin 162) + exact row_85 + · conv_lhs => arg 1; arg 1; change (86 : Fin 162) + exact row_86 + · conv_lhs => arg 1; arg 1; change (87 : Fin 162) + exact row_87 + · conv_lhs => arg 1; arg 1; change (88 : Fin 162) + exact row_88 + · conv_lhs => arg 1; arg 1; change (89 : Fin 162) + exact row_89 + +private theorem block_15 (r : Fin 6) : rowCheck (routeAt (blockIndex 15 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (90 : Fin 162) + exact row_90 + · conv_lhs => arg 1; arg 1; change (91 : Fin 162) + exact row_91 + · conv_lhs => arg 1; arg 1; change (92 : Fin 162) + exact row_92 + · conv_lhs => arg 1; arg 1; change (93 : Fin 162) + exact row_93 + · conv_lhs => arg 1; arg 1; change (94 : Fin 162) + exact row_94 + · conv_lhs => arg 1; arg 1; change (95 : Fin 162) + exact row_95 + +private theorem block_16 (r : Fin 6) : rowCheck (routeAt (blockIndex 16 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (96 : Fin 162) + exact row_96 + · conv_lhs => arg 1; arg 1; change (97 : Fin 162) + exact row_97 + · conv_lhs => arg 1; arg 1; change (98 : Fin 162) + exact row_98 + · conv_lhs => arg 1; arg 1; change (99 : Fin 162) + exact row_99 + · conv_lhs => arg 1; arg 1; change (100 : Fin 162) + exact row_100 + · conv_lhs => arg 1; arg 1; change (101 : Fin 162) + exact row_101 + +private theorem block_17 (r : Fin 6) : rowCheck (routeAt (blockIndex 17 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (102 : Fin 162) + exact row_102 + · conv_lhs => arg 1; arg 1; change (103 : Fin 162) + exact row_103 + · conv_lhs => arg 1; arg 1; change (104 : Fin 162) + exact row_104 + · conv_lhs => arg 1; arg 1; change (105 : Fin 162) + exact row_105 + · conv_lhs => arg 1; arg 1; change (106 : Fin 162) + exact row_106 + · conv_lhs => arg 1; arg 1; change (107 : Fin 162) + exact row_107 + +private theorem block_18 (r : Fin 6) : rowCheck (routeAt (blockIndex 18 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (108 : Fin 162) + exact row_108 + · conv_lhs => arg 1; arg 1; change (109 : Fin 162) + exact row_109 + · conv_lhs => arg 1; arg 1; change (110 : Fin 162) + exact row_110 + · conv_lhs => arg 1; arg 1; change (111 : Fin 162) + exact row_111 + · conv_lhs => arg 1; arg 1; change (112 : Fin 162) + exact row_112 + · conv_lhs => arg 1; arg 1; change (113 : Fin 162) + exact row_113 + +private theorem block_19 (r : Fin 6) : rowCheck (routeAt (blockIndex 19 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (114 : Fin 162) + exact row_114 + · conv_lhs => arg 1; arg 1; change (115 : Fin 162) + exact row_115 + · conv_lhs => arg 1; arg 1; change (116 : Fin 162) + exact row_116 + · conv_lhs => arg 1; arg 1; change (117 : Fin 162) + exact row_117 + · conv_lhs => arg 1; arg 1; change (118 : Fin 162) + exact row_118 + · conv_lhs => arg 1; arg 1; change (119 : Fin 162) + exact row_119 + +private theorem block_20 (r : Fin 6) : rowCheck (routeAt (blockIndex 20 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (120 : Fin 162) + exact row_120 + · conv_lhs => arg 1; arg 1; change (121 : Fin 162) + exact row_121 + · conv_lhs => arg 1; arg 1; change (122 : Fin 162) + exact row_122 + · conv_lhs => arg 1; arg 1; change (123 : Fin 162) + exact row_123 + · conv_lhs => arg 1; arg 1; change (124 : Fin 162) + exact row_124 + · conv_lhs => arg 1; arg 1; change (125 : Fin 162) + exact row_125 + +private theorem block_21 (r : Fin 6) : rowCheck (routeAt (blockIndex 21 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (126 : Fin 162) + exact row_126 + · conv_lhs => arg 1; arg 1; change (127 : Fin 162) + exact row_127 + · conv_lhs => arg 1; arg 1; change (128 : Fin 162) + exact row_128 + · conv_lhs => arg 1; arg 1; change (129 : Fin 162) + exact row_129 + · conv_lhs => arg 1; arg 1; change (130 : Fin 162) + exact row_130 + · conv_lhs => arg 1; arg 1; change (131 : Fin 162) + exact row_131 + +private theorem block_22 (r : Fin 6) : rowCheck (routeAt (blockIndex 22 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (132 : Fin 162) + exact row_132 + · conv_lhs => arg 1; arg 1; change (133 : Fin 162) + exact row_133 + · conv_lhs => arg 1; arg 1; change (134 : Fin 162) + exact row_134 + · conv_lhs => arg 1; arg 1; change (135 : Fin 162) + exact row_135 + · conv_lhs => arg 1; arg 1; change (136 : Fin 162) + exact row_136 + · conv_lhs => arg 1; arg 1; change (137 : Fin 162) + exact row_137 + +private theorem block_23 (r : Fin 6) : rowCheck (routeAt (blockIndex 23 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (138 : Fin 162) + exact row_138 + · conv_lhs => arg 1; arg 1; change (139 : Fin 162) + exact row_139 + · conv_lhs => arg 1; arg 1; change (140 : Fin 162) + exact row_140 + · conv_lhs => arg 1; arg 1; change (141 : Fin 162) + exact row_141 + · conv_lhs => arg 1; arg 1; change (142 : Fin 162) + exact row_142 + · conv_lhs => arg 1; arg 1; change (143 : Fin 162) + exact row_143 + +private theorem block_24 (r : Fin 6) : rowCheck (routeAt (blockIndex 24 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (144 : Fin 162) + exact row_144 + · conv_lhs => arg 1; arg 1; change (145 : Fin 162) + exact row_145 + · conv_lhs => arg 1; arg 1; change (146 : Fin 162) + exact row_146 + · conv_lhs => arg 1; arg 1; change (147 : Fin 162) + exact row_147 + · conv_lhs => arg 1; arg 1; change (148 : Fin 162) + exact row_148 + · conv_lhs => arg 1; arg 1; change (149 : Fin 162) + exact row_149 + +private theorem block_25 (r : Fin 6) : rowCheck (routeAt (blockIndex 25 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (150 : Fin 162) + exact row_150 + · conv_lhs => arg 1; arg 1; change (151 : Fin 162) + exact row_151 + · conv_lhs => arg 1; arg 1; change (152 : Fin 162) + exact row_152 + · conv_lhs => arg 1; arg 1; change (153 : Fin 162) + exact row_153 + · conv_lhs => arg 1; arg 1; change (154 : Fin 162) + exact row_154 + · conv_lhs => arg 1; arg 1; change (155 : Fin 162) + exact row_155 + +private theorem block_26 (r : Fin 6) : rowCheck (routeAt (blockIndex 26 r)) = true := by + fin_cases r + · conv_lhs => arg 1; arg 1; change (156 : Fin 162) + exact row_156 + · conv_lhs => arg 1; arg 1; change (157 : Fin 162) + exact row_157 + · conv_lhs => arg 1; arg 1; change (158 : Fin 162) + exact row_158 + · conv_lhs => arg 1; arg 1; change (159 : Fin 162) + exact row_159 + · conv_lhs => arg 1; arg 1; change (160 : Fin 162) + exact row_160 + · conv_lhs => arg 1; arg 1; change (161 : Fin 162) + exact row_161 + +private theorem blocks_checked (q : Fin 27) (r : Fin 6) : + rowCheck (routeAt (blockIndex q r)) = true := by + fin_cases q + · exact block_0 r + · exact block_1 r + · exact block_2 r + · exact block_3 r + · exact block_4 r + · exact block_5 r + · exact block_6 r + · exact block_7 r + · exact block_8 r + · exact block_9 r + · exact block_10 r + · exact block_11 r + · exact block_12 r + · exact block_13 r + · exact block_14 r + · exact block_15 r + · exact block_16 r + · exact block_17 r + · exact block_18 r + · exact block_19 r + · exact block_20 r + · exact block_21 r + · exact block_22 r + · exact block_23 r + · exact block_24 r + · exact block_25 r + · exact block_26 r + +private theorem rows_checked (i : Fin 162) : rowCheck (routeAt i) = true := by + let q : Fin 27 := ⟨i.val / 6, by omega⟩ + let r : Fin 6 := ⟨i.val % 6, by omega⟩ + have heq : blockIndex q r = i := by + apply Fin.ext + simp only [blockIndex, q, r] + omega + have h := blocks_checked q r + rwa [heq] at h + +private theorem row_checked (e : ℕ × Variable × Route) (he : e ∈ incidenceRoutes) : + rowCheck e = true := by + obtain ⟨i, rfl⟩ := List.mem_iff_get.mp he + have hi : i.val < 162 := by simpa only [drawing_sizes.2] using i.isLt + have h := rows_checked ⟨i.val, hi⟩ + have heq : routeAt ⟨i.val, hi⟩ = incidenceRoutes.get i := + List.getD_eq_get incidenceRoutes (0, .center, []) i + rwa [heq] at h + +private theorem local_checked (e : ℕ × Variable × Route) (he : e ∈ incidenceRoutes) : + LocalSpec e := by + have h := row_checked e he + simp only [rowCheck, Bool.and_eq_true, decide_eq_true_eq] at h + exact h.1 + +/-- Every route starts at its clause and ends at its variable, with a valid clause index. -/ +theorem incidence_endpoints : ∀ e ∈ incidenceRoutes, + e.1 < 78 ∧ e.2.2.head? = some (clausePosition e.1) ∧ + e.2.2.getLast? = some (variablePosition e.2.1) := + fun e he => (local_checked e he).1 + +/-- All incidence routes have proper axis-aligned segments. -/ +theorem incidence_orthogonal : + ∀ e ∈ incidenceRoutes, IsOrthogonal e.2.2 := + fun e he => (local_checked e he).2.1 + +/-- All listed core points are inside the smaller rectangle `[20,220]²`. -/ +theorem core_bounds : ∀ e ∈ incidenceRoutes, ∀ p ∈ e.2.2, + 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220 := + fun e he => (local_checked e he).2.2.1 + +/-- Exactly 407 proper segments and 2192 units of total Manhattan wire length. -/ +theorem route_sizes : + (incidenceRoutes.map fun e => e.2.2.consecutivePairs.length).sum = 407 ∧ + (incidenceRoutes.map fun e => wireLength e.2.2).sum = 2192 := by decide +kernel + +/-- Every incidence route lists each bend only once. -/ +theorem incidence_points_nodup : ∀ e ∈ incidenceRoutes, e.2.2.Nodup := + fun e he => (local_checked e he).2.2.2.1 + +/-- Finite simplicity certificate: distinct segments are disjoint except at a shared next bend. -/ +theorem incidence_simple_check : ∀ e ∈ incidenceRoutes, + ∀ a ∈ e.2.2.consecutivePairs, ∀ b ∈ e.2.2.consecutivePairs, a ≠ b → + segmentContactCheck (consecutiveContact a b) a.1 a.2 b.1 b.2 = true := + fun e he => (local_checked e he).2.2.2.2 + +/-- Exhaustive finite contact certificate for the fixed route table. -/ +theorem routes_contact_check : ∀ e ∈ incidenceRoutes, ∀ f ∈ incidenceRoutes, + e ≠ f → routeContactCheck (commonEndpoints e f) e.2.2 f.2.2 = true := by + intro e he f hf hne + have h := row_checked e he + simp only [rowCheck, Bool.and_eq_true] at h + have hf' := List.all_eq_true.mp h.2.1 f hf + simpa only [Bool.or_eq_true, beq_iff_eq, hne, false_or] using hf' + +/-- No route visits a nonincident variable vertex. -/ +theorem variable_avoidance_check : ∀ e ∈ incidenceRoutes, ∀ v, + v ≠ e.2.1 → routeContactCheck [] e.2.2 [variablePosition v] = true := by + intro e he v hv + have h := row_checked e he + simp only [rowCheck, Bool.and_eq_true] at h + have hv' := List.all_eq_true.mp h.2.2.1 v (mem_variableList v) + simpa only [Bool.or_eq_true, beq_iff_eq, hv, false_or] using hv' + +/-- No route visits a nonincident clause vertex. -/ +theorem clause_avoidance_check : ∀ e ∈ incidenceRoutes, ∀ i : Fin 78, + i.val ≠ e.1 → routeContactCheck [] e.2.2 [clausePosition i] = true := by + intro e he i hi + have h := row_checked e he + simp only [rowCheck, Bool.and_eq_true] at h + have hi' := List.all_eq_true.mp h.2.2.2 i (List.mem_finRange i) + simpa only [Bool.or_eq_true, beq_iff_eq, hi, false_or] using hi' + +/-- All eight access routes have their prescribed endpoints and proper orthogonal segments. -/ +theorem access_endpoints : ∀ s l, IsOrthogonal (accessRoute s l) ∧ + (accessRoute s l).head? = some (boundaryPort s l) ∧ + (accessRoute s l).getLast? = some (variablePosition (terminal s l)) := by decide +kernel + +/-- The eight access routes are mutually disjoint. -/ +theorem access_disjoint_check : ∀ p q : PairedPorts.Port, p ≠ q → + routeContactCheck [] (accessRoute p.1 p.2) (accessRoute q.1 q.2) = true := + PairedPorts.access_disjoint_check + +/-- Access to a port can meet an incidence route only at that port. -/ +theorem access_contact_check : ∀ s l, ∀ e ∈ incidenceRoutes, + routeContactCheck (if e.2.1 = terminal s l then [variablePosition (terminal s l)] else []) + (accessRoute s l) e.2.2 = true := by decide +kernel + +end Cslib.Logic.PL.CNF.PairedCrossover diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutData.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutData.lean new file mode 100644 index 000000000..f97d12560 --- /dev/null +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutData.lean @@ -0,0 +1,253 @@ +/- +Copyright (c) 2026 lean-trominoes contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine, Stefan Langerman, GPT 5.6 +-/ + +module +-- upstream: candidate + +public import Complexity.Logics.Propositional.CNF.Planar.PairedCrossover +public import Complexity.Foundations.Geometry.Orthogonal.PairedPorts +public import Complexity.Computability.Complexity.Problems.SAT.Planar.CrossoverLayoutData + +/-! +# Orthogonal drawing data for the paired-port crossover + +The old internal drawing is retained. Each old terminal is replaced by ports at offsets 110 +and 130, with the new implication clause at the old terminal position. Only the eight old +terminal incidence routes are rerouted. The shared paired accesses end at these eight ports. + +## Main definitions + +* `variablePosition`, `clausePositions`, `incidenceRoutes`: the 57-variable, 78-clause drawing. +* `accessRoute`: the eight accesses from `Orthogonal.PairedPorts`. + +## References + +The unchanged core comes from [Lichtenstein1982, Figs. 4–5] and [Tromino2025, Fig. 8(b)]. +The paired terminal modification is original. +Source credit for the core is in `CrossoverLayoutData`. +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF.PairedCrossover + +open Orthogonal + +/-- The eight new ports use the shared paired interface; other vertices keep their positions. -/ +def variablePosition : Variable → Point + | .port s l => PairedPorts.variablePosition s l + | .center => Crossover.variablePosition .center + | .copy v i => Crossover.variablePosition (.copy v i) + +/-- The old clause positions followed by the four old terminal positions. -/ +def clausePositions : List Point := + Crossover.clausePositions ++ [(20, 120), (220, 120), (120, 20), (120, 220)] + +/-- Exact clause-to-variable incidence routes in clause and literal order. -/ +def incidenceRoutes : List (ℕ × Variable × Route) := + [ + (0, .port 0 0, [(40, 120), (40, 119), (21, 119), (21, 110), (20, 110)]), + (0, .copy .aInnerLeft 5, [(40, 120), (56, 120)]), + (1, .port 0 1, [(40, 140), (37, 140), (37, 135), (33, 135), (33, 131), (29, 131), (29, 130), + (20, 130)]), + (1, .copy .aInnerLeft 4, [(40, 140), (40, 137), (45, 137), (45, 133), (49, 133), (49, 129), + (53, 129), (53, 125), (56, 125), (56, 124)]), + (2, .copy .aInnerLeft 0, [(60, 60), (59, 60), (59, 115), (60, 115), (60, 116)]), + (2, .copy .upperLeft 0, [(60, 60), (60, 63), (65, 63), (65, 67), (69, 67), (69, 71), (73, 71), + (73, 75), (77, 75), (77, 79), (81, 79), (81, 83), (85, 83), (85, 87), (89, 87), (89, 91), + (93, 91), (93, 95), (96, 95), (96, 96)]), + (2, .copy .bInnerTop 5, [(60, 60), (116, 60)]), + (3, .copy .aInnerLeft 3, [(60, 180), (59, 180), (59, 125), (60, 125), (60, 124)]), + (3, .copy .lowerLeft 4, [(60, 180), (60, 177), (65, 177), (65, 173), (69, 173), (69, 169), (73, + 169), (73, 165), (77, 165), (77, 161), (81, 161), (81, 157), (85, 157), (85, 153), (89, 153), + (89, 149), (93, 149), (93, 145), (96, 145), (96, 144)]), + (3, .copy .bInnerBottom 5, [(60, 180), (116, 180)]), + (4, .copy .aInnerLeft 1, [(80, 100), (77, 100), (77, 105), (73, 105), (73, 109), (69, 109), + (69, 113), (65, 113), (65, 116), (64, 116)]), + (4, .copy .upperLeft 5, [(80, 100), (96, 100)]), + (5, .copy .upperLeft 4, [(80, 120), (80, 117), (85, 117), (85, 113), (89, 113), (89, 109), (93, + 109), (93, 105), (96, 105), (96, 104)]), + (5, .copy .lowerLeft 0, [(80, 120), (80, 123), (85, 123), (85, 127), (89, 127), (89, 131), (93, + 131), (93, 135), (96, 135), (96, 136)]), + (6, .copy .aInnerLeft 2, [(80, 140), (77, 140), (77, 135), (73, 135), (73, 131), (69, 131), + (69, 127), (65, 127), (65, 124), (64, 124)]), + (6, .copy .lowerLeft 5, [(80, 140), (96, 140)]), + (7, .port 2 0, [(100, 40), (100, 37), (105, 37), (105, 33), (109, 33), (109, 20), (110, 20)]), + (7, .copy .bInnerTop 0, [(100, 40), (100, 43), (105, 43), (105, 47), (109, 47), (109, 51), + (113, 51), (113, 55), (116, 55), (116, 56)]), + (8, .copy .upperLeft 1, [(100, 80), (100, 96)]), + (8, .copy .bInnerTop 4, [(100, 80), (100, 77), (105, 77), (105, 73), (109, 73), (109, 69), + (113, 69), (113, 65), (116, 65), (116, 64)]), + (9, .copy .upperLeft 3, [(100, 120), (100, 104)]), + (9, .copy .lowerLeft 1, [(100, 120), (100, 136)]), + (9, .center, [(100, 120), (120, 120)]), + (10, .copy .lowerLeft 3, [(100, 160), (100, 144)]), + (10, .copy .bInnerBottom 0, [(100, 160), (100, 163), (105, 163), (105, 167), (109, 167), (109, + 171), (113, 171), (113, 175), (116, 175), (116, 176)]), + (11, .port 2 1, [(120, 40), (121, 40), (121, 21), (130, 21), (130, 20)]), + (11, .copy .bInnerTop 1, [(120, 40), (120, 56)]), + (12, .copy .upperLeft 2, [(120, 100), (104, 100)]), + (12, .copy .upperRight 5, [(120, 100), (136, 100)]), + (13, .copy .lowerLeft 2, [(120, 140), (104, 140)]), + (13, .copy .lowerRight 5, [(120, 140), (136, 140)]), + (14, .copy .bInnerBottom 4, [(120, 200), (120, 184)]), + (14, .port 3 0, [(120, 200), (120, 201), (110, 201), (110, 220)]), + (15, .copy .bInnerTop 3, [(140, 80), (137, 80), (137, 75), (133, 75), (133, 71), (129, 71), + (129, 67), (125, 67), (125, 64), (124, 64)]), + (15, .copy .upperRight 0, [(140, 80), (140, 96)]), + (16, .center, [(140, 120), (120, 120)]), + (16, .copy .upperRight 4, [(140, 120), (140, 104)]), + (16, .copy .lowerRight 0, [(140, 120), (140, 136)]), + (17, .copy .bInnerBottom 1, [(140, 160), (137, 160), (137, 165), (133, 165), (133, 169), (129, + 169), (129, 173), (125, 173), (125, 176), (124, 176)]), + (17, .copy .lowerRight 4, [(140, 160), (140, 144)]), + (18, .copy .bInnerBottom 3, [(140, 200), (140, 197), (135, 197), (135, 193), (131, 193), (131, + 189), (127, 189), (127, 185), (124, 185), (124, 184)]), + (18, .port 3 1, [(140, 200), (137, 200), (137, 205), (133, 205), (133, 209), (133, 213), (130, + 213), (130, 220)]), + (19, .copy .upperRight 2, [(160, 100), (144, 100)]), + (19, .copy .aInnerRight 0, [(160, 100), (160, 103), (165, 103), (165, 107), (169, 107), (169, + 111), (173, 111), (173, 115), (176, 115), (176, 116)]), + (20, .copy .upperRight 3, [(160, 120), (157, 120), (157, 115), (153, 115), (153, 111), (149, + 111), (149, 107), (145, 107), (145, 104), (144, 104)]), + (20, .copy .lowerRight 1, [(160, 120), (160, 123), (155, 123), (155, 127), (151, 127), (151, + 131), (147, 131), (147, 135), (144, 135), (144, 136)]), + (21, .copy .lowerRight 2, [(160, 140), (144, 140)]), + (21, .copy .aInnerRight 5, [(160, 140), (160, 137), (165, 137), (165, 133), (169, 133), (169, + 129), (173, 129), (173, 125), (176, 125), (176, 124)]), + (22, .copy .bInnerTop 2, [(180, 60), (180, 59), (125, 59), (125, 60), (124, 60)]), + (22, .copy .upperRight 1, [(180, 60), (177, 60), (177, 65), (173, 65), (173, 69), (169, 69), + (169, 73), (165, 73), (165, 77), (161, 77), (161, 81), (157, 81), (157, 85), (153, 85), (153, + 89), (149, 89), (149, 93), (145, 93), (145, 96), (144, 96)]), + (22, .copy .aInnerRight 1, [(180, 60), (180, 116)]), + (23, .copy .bInnerBottom 2, [(180, 180), (180, 181), (125, 181), (125, 180), (124, 180)]), + (23, .copy .lowerRight 3, [(180, 180), (177, 180), (177, 175), (173, 175), (173, 171), (169, + 171), (169, 167), (165, 167), (165, 163), (161, 163), (161, 159), (157, 159), (157, 155), + (153, 155), (153, 151), (149, 151), (149, 147), (145, 147), (145, 144), (144, 144)]), + (23, .copy .aInnerRight 4, [(180, 180), (180, 124)]), + (24, .copy .aInnerRight 2, [(200, 100), (197, 100), (197, 105), (193, 105), (193, 109), (189, + 109), (189, 113), (185, 113), (185, 116), (184, 116)]), + (24, .port 1 0, [(200, 100), (200, 103), (205, 103), (205, 107), (209, 107), (209, 110), (220, + 110)]), + (25, .copy .aInnerRight 3, [(200, 120), (184, 120)]), + (25, .port 1 1, [(200, 120), (200, 121), (219, 121), (219, 130), (220, 130)]), + (26, .copy .aInnerLeft 0, [(62, 116), (60, 116)]), + (26, .copy .aInnerLeft 1, [(62, 116), (64, 116)]), + (27, .copy .aInnerLeft 1, [(64, 120), (64, 116)]), + (27, .copy .aInnerLeft 2, [(64, 120), (64, 124)]), + (28, .copy .aInnerLeft 2, [(62, 124), (64, 124)]), + (28, .copy .aInnerLeft 3, [(62, 124), (60, 124)]), + (29, .copy .aInnerLeft 3, [(58, 124), (60, 124)]), + (29, .copy .aInnerLeft 4, [(58, 124), (56, 124)]), + (30, .copy .aInnerLeft 4, [(56, 122), (56, 124)]), + (30, .copy .aInnerLeft 5, [(56, 122), (56, 120)]), + (31, .copy .aInnerLeft 5, [(56, 116), (56, 120)]), + (31, .copy .aInnerLeft 0, [(56, 116), (60, 116)]), + (32, .copy .upperLeft 0, [(98, 96), (96, 96)]), + (32, .copy .upperLeft 1, [(98, 96), (100, 96)]), + (33, .copy .upperLeft 1, [(104, 96), (100, 96)]), + (33, .copy .upperLeft 2, [(104, 96), (104, 100)]), + (34, .copy .upperLeft 2, [(104, 104), (104, 100)]), + (34, .copy .upperLeft 3, [(104, 104), (100, 104)]), + (35, .copy .upperLeft 3, [(98, 104), (100, 104)]), + (35, .copy .upperLeft 4, [(98, 104), (96, 104)]), + (36, .copy .upperLeft 4, [(96, 102), (96, 104)]), + (36, .copy .upperLeft 5, [(96, 102), (96, 100)]), + (37, .copy .upperLeft 5, [(96, 98), (96, 100)]), + (37, .copy .upperLeft 0, [(96, 98), (96, 96)]), + (38, .copy .lowerLeft 0, [(98, 136), (96, 136)]), + (38, .copy .lowerLeft 1, [(98, 136), (100, 136)]), + (39, .copy .lowerLeft 1, [(104, 136), (100, 136)]), + (39, .copy .lowerLeft 2, [(104, 136), (104, 140)]), + (40, .copy .lowerLeft 2, [(104, 144), (104, 140)]), + (40, .copy .lowerLeft 3, [(104, 144), (100, 144)]), + (41, .copy .lowerLeft 3, [(98, 144), (100, 144)]), + (41, .copy .lowerLeft 4, [(98, 144), (96, 144)]), + (42, .copy .lowerLeft 4, [(96, 142), (96, 144)]), + (42, .copy .lowerLeft 5, [(96, 142), (96, 140)]), + (43, .copy .lowerLeft 5, [(96, 138), (96, 140)]), + (43, .copy .lowerLeft 0, [(96, 138), (96, 136)]), + (44, .copy .bInnerTop 0, [(118, 56), (116, 56)]), + (44, .copy .bInnerTop 1, [(118, 56), (120, 56)]), + (45, .copy .bInnerTop 1, [(124, 56), (120, 56)]), + (45, .copy .bInnerTop 2, [(124, 56), (124, 60)]), + (46, .copy .bInnerTop 2, [(124, 62), (124, 60)]), + (46, .copy .bInnerTop 3, [(124, 62), (124, 64)]), + (47, .copy .bInnerTop 3, [(120, 64), (124, 64)]), + (47, .copy .bInnerTop 4, [(120, 64), (116, 64)]), + (48, .copy .bInnerTop 4, [(116, 62), (116, 64)]), + (48, .copy .bInnerTop 5, [(116, 62), (116, 60)]), + (49, .copy .bInnerTop 5, [(116, 58), (116, 60)]), + (49, .copy .bInnerTop 0, [(116, 58), (116, 56)]), + (50, .copy .bInnerBottom 0, [(120, 176), (116, 176)]), + (50, .copy .bInnerBottom 1, [(120, 176), (124, 176)]), + (51, .copy .bInnerBottom 1, [(124, 178), (124, 176)]), + (51, .copy .bInnerBottom 2, [(124, 178), (124, 180)]), + (52, .copy .bInnerBottom 2, [(124, 182), (124, 180)]), + (52, .copy .bInnerBottom 3, [(124, 182), (124, 184)]), + (53, .copy .bInnerBottom 3, [(122, 184), (124, 184)]), + (53, .copy .bInnerBottom 4, [(122, 184), (120, 184)]), + (54, .copy .bInnerBottom 4, [(116, 184), (120, 184)]), + (54, .copy .bInnerBottom 5, [(116, 184), (116, 180)]), + (55, .copy .bInnerBottom 5, [(116, 178), (116, 180)]), + (55, .copy .bInnerBottom 0, [(116, 178), (116, 176)]), + (56, .copy .upperRight 0, [(142, 96), (140, 96)]), + (56, .copy .upperRight 1, [(142, 96), (144, 96)]), + (57, .copy .upperRight 1, [(144, 98), (144, 96)]), + (57, .copy .upperRight 2, [(144, 98), (144, 100)]), + (58, .copy .upperRight 2, [(144, 102), (144, 100)]), + (58, .copy .upperRight 3, [(144, 102), (144, 104)]), + (59, .copy .upperRight 3, [(142, 104), (144, 104)]), + (59, .copy .upperRight 4, [(142, 104), (140, 104)]), + (60, .copy .upperRight 4, [(136, 104), (140, 104)]), + (60, .copy .upperRight 5, [(136, 104), (136, 100)]), + (61, .copy .upperRight 5, [(136, 96), (136, 100)]), + (61, .copy .upperRight 0, [(136, 96), (140, 96)]), + (62, .copy .lowerRight 0, [(142, 136), (140, 136)]), + (62, .copy .lowerRight 1, [(142, 136), (144, 136)]), + (63, .copy .lowerRight 1, [(144, 138), (144, 136)]), + (63, .copy .lowerRight 2, [(144, 138), (144, 140)]), + (64, .copy .lowerRight 2, [(144, 142), (144, 140)]), + (64, .copy .lowerRight 3, [(144, 142), (144, 144)]), + (65, .copy .lowerRight 3, [(142, 144), (144, 144)]), + (65, .copy .lowerRight 4, [(142, 144), (140, 144)]), + (66, .copy .lowerRight 4, [(136, 144), (140, 144)]), + (66, .copy .lowerRight 5, [(136, 144), (136, 140)]), + (67, .copy .lowerRight 5, [(136, 136), (136, 140)]), + (67, .copy .lowerRight 0, [(136, 136), (140, 136)]), + (68, .copy .aInnerRight 0, [(178, 116), (176, 116)]), + (68, .copy .aInnerRight 1, [(178, 116), (180, 116)]), + (69, .copy .aInnerRight 1, [(182, 116), (180, 116)]), + (69, .copy .aInnerRight 2, [(182, 116), (184, 116)]), + (70, .copy .aInnerRight 2, [(184, 118), (184, 116)]), + (70, .copy .aInnerRight 3, [(184, 118), (184, 120)]), + (71, .copy .aInnerRight 3, [(184, 124), (184, 120)]), + (71, .copy .aInnerRight 4, [(184, 124), (180, 124)]), + (72, .copy .aInnerRight 4, [(178, 124), (180, 124)]), + (72, .copy .aInnerRight 5, [(178, 124), (176, 124)]), + (73, .copy .aInnerRight 5, [(176, 120), (176, 124)]), + (73, .copy .aInnerRight 0, [(176, 120), (176, 116)]), + (74, .port 0 0, [(20, 120), (20, 110)]), + (74, .port 0 1, [(20, 120), (20, 130)]), + (75, .port 1 1, [(220, 120), (220, 130)]), + (75, .port 1 0, [(220, 120), (220, 110)]), + (76, .port 2 1, [(120, 20), (130, 20)]), + (76, .port 2 0, [(120, 20), (110, 20)]), + (77, .port 3 0, [(120, 220), (110, 220)]), + (77, .port 3 1, [(120, 220), (130, 220)]) + ] + +/-- Boundary access points agree definitionally with the shared paired interface. -/ +def boundaryPort : Fin 4 → Fin 2 → Point := PairedPorts.boundaryPort + +/-- Straight shared accesses to the eight degree-two terminals. -/ +def accessRoute : Fin 4 → Fin 2 → Route := PairedPorts.accessRoute + +/-- The terminal coordinates are exactly the shared paired-port positions. -/ +theorem terminal_position (s : Fin 4) (l : Fin 2) : + variablePosition (terminal s l) = PairedPorts.variablePosition s l := rfl + +end Cslib.Logic.PL.CNF.PairedCrossover