From 209dd3ccc7be1f309c171f01ecb2e3e9321952d1 Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Mon, 26 Oct 2026 07:26:47 -0400 Subject: [PATCH 1/4] 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/4] 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/4] 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/4] 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