diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/CrossoverLayoutChecks.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/CrossoverLayoutChecks.lean index 087ce5b134..80c671451f 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/CrossoverLayoutChecks.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/CrossoverLayoutChecks.lean @@ -94,9 +94,6 @@ def commonEndpoints (e f : ℕ × SplitVariable × Route) : List Point := def consecutiveContact (a b : Point × Point) : List Point := if a.2 = b.1 then [a.2] else if b.2 = a.1 then [a.1] else [] -private instance (r : Route) : Decidable (IsOrthogonal r) := - inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2)) - private def LocalSpec (e : ℕ × SplitVariable × Route) : Prop := (e.1 < 74 ∧ e.2.2.head? = some (clausePosition e.1) ∧ e.2.2.getLast? = some (variablePosition e.2.1)) ∧ diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean index 7a496be62d..5c45cb0a8b 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/OrdinaryRing.lean @@ -114,9 +114,6 @@ theorem formula_sizes : formula.length = 8 ∧ ∀ c ∈ formula, c.length = 2 : /-- 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)) = diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean index 1f584ab938..8ca4ac420c 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedCrossoverLayoutChecks.lean @@ -90,9 +90,6 @@ def commonEndpoints (e f : ℕ × Variable × Route) : List Point := def consecutiveContact (a b : Point × Point) : List Point := if a.2 = b.1 then [a.2] else if b.2 = a.1 then [a.1] else [] -private instance (r : Route) : Decidable (IsOrthogonal r) := - inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2)) - private def LocalSpec (e : ℕ × Variable × Route) : Prop := (e.1 < 78 ∧ e.2.2.head? = some (clausePosition e.1) ∧ e.2.2.getLast? = some (variablePosition e.2.1)) ∧ diff --git a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedGeometry.lean b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedGeometry.lean index f721724da8..5e0f8036db 100644 --- a/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedGeometry.lean +++ b/Complexity/Computability/Complexity/Problems/SAT/Planar/PairedGeometry.lean @@ -32,7 +32,6 @@ All geometric assertions concern entire real supports. ## Main results -* `boundary_eq_cases`: matching boundaries identify opposite adjacent sides and the lane. * `access_eq_translate`: every actual access uses the common fixed paired-port interface. * `route_contacts`, `routes_contacts`: continuous endpoint-only contacts of the actual routes. * `isPlanarOrthogonalDrawing`: the actual compact formula's continuous drawing certificate. @@ -48,12 +47,6 @@ namespace Cslib.Complexity.SAT.ParsimoniousPlanar open Cslib.Logic.PL Cslib.Logic.PL.CNF Orthogonal -/-- Equal paired boundary points in different cells identify both the side and the lane. -/ -theorem boundary_eq_cases {c d : Point} {s t : Fin 4} {l k : Fin 2} - (hcd : c ≠ d) (h : boundary c s l = boundary d t k) : - l = k ∧ d = c + PairedPorts.neighbor s ∧ t = PairedPorts.oppositeSide s := - PairedPorts.boundary_eq_cases hcd h - /-- Within one cell, boundary positions identify both the side and the lane. -/ theorem boundary_injective (c : Point) : Function.Injective (fun p : PairedPorts.Port => boundary c p.1 p.2) := by @@ -248,9 +241,6 @@ theorem clause_cell_not_ordinary {φ : CNF ℕ} {i : ℕ} (hi : i < φ.length) : obtain ⟨o, ho, rfl⟩ := List.mem_map.mp hr exact PlanarCompile.clause_cell_not_mem_path_dropLast ho hi hp -private instance (r : Route) : Decidable (IsOrthogonal r) := - inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2)) - private def finalLocalRoute (s : Fin 4) : Route := [(120, 120), PairedPorts.spokeElbow s, PairedPorts.boundaryPort s (PairedPorts.spokeLane s), cellOrigin 120 (PairedPorts.neighbor s) + diff --git a/Complexity/Foundations/Geometry/Orthogonal.lean b/Complexity/Foundations/Geometry/Orthogonal.lean index 59ac0abf21..6170e20d5a 100644 --- a/Complexity/Foundations/Geometry/Orthogonal.lean +++ b/Complexity/Foundations/Geometry/Orthogonal.lean @@ -81,6 +81,10 @@ instance (a b : Point) : Decidable (AxisAligned a b) := inferInstanceAs (Decidab /-- Every consecutive segment is proper and axis aligned. -/ def IsOrthogonal (r : Route) : Prop := ∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2 +/-- Orthogonality is decidable by checking the finitely many consecutive segments. -/ +instance : DecidablePred IsOrthogonal := + fun r => inferInstanceAs (Decidable (∀ e ∈ r.consecutivePairs, AxisAligned e.1 e.2)) + /-- Removing the initial listed point preserves proper orthogonality. -/ theorem IsOrthogonal.of_cons {a : Point} {r : Route} (h : IsOrthogonal (a :: r)) : IsOrthogonal r := by diff --git a/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean b/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean index b311f95a1d..50a34d3722 100644 --- a/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean +++ b/Complexity/Foundations/Geometry/Orthogonal/PairedPorts.lean @@ -94,9 +94,6 @@ 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) ∧ diff --git a/Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean b/Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean index f80b2dc0f6..ebe423000f 100644 --- a/Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean +++ b/Complexity/Foundations/Geometry/Orthogonal/PairedSpokes.lean @@ -50,9 +50,6 @@ def spokeElbow (s : Fin 4) : Point := 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) ∧ diff --git a/Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean b/Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean index b0371b7ae9..deb7fe1cff 100644 --- a/Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean +++ b/Complexity/Logics/Propositional/CNF/Planar/CrossoverCounting.lean @@ -29,6 +29,9 @@ rings. Construction and source credit are documented in `Crossover` and `Crossov ## References The construction adapts [Lichtenstein1982, Figs. 4–5] and [Tromino2025, Fig. 8(b)]. +Unique extension is the parsimony condition of +[HuntMaratheRadhakrishnanStearns1998, Definition 3.1]. Their Theorem 3.2 proves that property for +Lichtenstein's crossover; kernel evaluation checks the adapted 13-variable table here. -/ @[expose] public section diff --git a/Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean b/Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean index 05994f7e53..8c8c5a51c4 100644 --- a/Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean +++ b/Complexity/Logics/Propositional/CNF/Planar/PairedCrossover.lean @@ -26,6 +26,8 @@ Lichtenstein's crossover [Lichtenstein1982, Figs. 4–5], as drawn in [Tromino20 ## Main results +* `PairedCrossover.existsUnique_holds`: a unique full satisfying assignment for each input pair. +* `PairedCrossover.eval_formula_iff`: split-formula semantics with paired-terminal agreement. * `PairedCrossover.eq_canonicalExtension_of_holds`: uniqueness of the full extension. * `PairedCrossover.terminal_occurrences`: two internal incidences at each of the eight ports.