diff --git a/CslibFrontier/Computability/Complexity/Problems/CSP/Affine.lean b/CslibFrontier/Computability/Complexity/Problems/CSP/Affine.lean index 24218f52fc..8560238bfd 100644 --- a/CslibFrontier/Computability/Complexity/Problems/CSP/Affine.lean +++ b/CslibFrontier/Computability/Complexity/Problems/CSP/Affine.lean @@ -61,11 +61,11 @@ theorem exists_affine_templates (arity : Rel → ℕ) (sem : Rel → List Bool theorem polyTimeReducible_XORSAT_of_templates [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (template : Rel → AffineSystem ℕ) (ht : CSP.AffineTemplates arity sem template) : - PolyTimeReducible (encCSP encRel encNat) XORSAT.encoding (CSPSAT arity sem) - {F | XORSAT.Satisfiable F} := by + PolyTimeReducible (encCSP encRel encNat) XORSAT.encoding (CSPSAT arity sem) XORSAT := by refine polyTimeReducible_of_guard encRel arity sem [([], true)] (CSP.computableInPolyTime_instantiateAffine encRel template) (fun F hF => ?_) - (by simp [XORSAT.Satisfiable, AffineSystem.Holds, AffineEquation.Holds, Bool.zero_eq_false]) + (by simp [mem_XORSAT, XORSAT.Satisfiable, AffineSystem.Holds, AffineEquation.Holds, + Bool.zero_eq_false]) exact (CSP.satisfiable_instantiateAffine ht 0 hF).symm /-- **Native P membership for every fixed finite parity-preserved Boolean language.** The @@ -77,6 +77,6 @@ theorem mem_P_of_parity [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel CSPSAT arity sem ∈ P (encCSP encRel encNat) := by obtain ⟨template, ht⟩ := exists_affine_templates arity sem h exact (polyTimeReducible_XORSAT_of_templates encRel arity sem template ht).mem_P - XORSAT.satisfiable_mem_P + XORSAT.mem_P end Cslib.Complexity.CSPSAT diff --git a/CslibFrontier/Computability/Complexity/Problems/XORSAT.lean b/CslibFrontier/Computability/Complexity/Problems/XORSAT.lean index 1235af7e37..dae543db80 100644 --- a/CslibFrontier/Computability/Complexity/Problems/XORSAT.lean +++ b/CslibFrontier/Computability/Complexity/Problems/XORSAT.lean @@ -36,17 +36,21 @@ the chosen equations are fixed independently of the input. * `Cslib.Complexity.XORSAT.encoding`: lists of equations with binary variable labels. * `Cslib.Complexity.XORSAT.compile`: compress labels and cancel repeated occurrences. * `Cslib.Complexity.XORSAT.solve`: compile, then perform Gaussian elimination. +* `Cslib.Complexity.XORSAT`: the satisfiable systems. ## Main results * `Cslib.Complexity.XORSAT.solve_eq_true_iff`: correctness for ordinary parity systems. -* `Cslib.Complexity.XORSAT.solve_polyTime`: a native multi-tape polynomial-time certificate. -* `Cslib.Complexity.XORSAT.satisfiable_mem_P`: ordinary XOR-SAT is in `P`. +* `Cslib.Complexity.XORSAT.computableInPolyTime_solve`: a native multi-tape polynomial-time + certificate. +* `Cslib.Complexity.XORSAT.mem_P`: ordinary XOR-SAT is in `P`. -/ public section -namespace Cslib.Complexity.XORSAT +namespace Cslib.Complexity + +namespace XORSAT open Turing.MultiTapeTM Cslib.Logic.PL @@ -213,7 +217,7 @@ open scoped _root_.Cslib.Complexity.XORSAT.Dense /-- Label compression is itself a native polynomial-time computation. Binary labels are only compared, never expanded into a table indexed by their numerical value. -/ -theorem compile_polyTime : ComputableInPolyTime compile encoding Dense.encInput := by +theorem computableInPolyTime_compile : ComputableInPolyTime compile encoding Dense.encInput := by have hvars := labels_polyTime have hcoeff := coefficient_polyTime.computableInPolyTime unfold compile @@ -223,11 +227,18 @@ theorem compile_polyTime : ComputableInPolyTime compile encoding Dense.encInput end /-- Ordinary XOR-SAT is decided in polynomial time by native multi-tape machines. -/ -theorem solve_polyTime : ComputableInPolyTime solve encoding encBool := - Dense.decide_polyTime.comp compile_polyTime +theorem computableInPolyTime_solve : ComputableInPolyTime solve encoding encBool := + Dense.computableInPolyTime_decide.comp computableInPolyTime_compile + +end XORSAT + +/-- Ordinary XOR-SAT: the satisfiable systems of parity equations. -/ +@[expose] def XORSAT : Set XORSAT.System := {F | XORSAT.Satisfiable F} + +theorem mem_XORSAT {F : XORSAT.System} : F ∈ XORSAT ↔ XORSAT.Satisfiable F := Iff.rfl /-- Ordinary systems of affine parity equations, with sparse binary variable labels, are in P. -/ -theorem satisfiable_mem_P : {F : System | Satisfiable F} ∈ P encoding := - ⟨solve, solve_polyTime, fun F => (solve_eq_true_iff F).symm⟩ +theorem XORSAT.mem_P : XORSAT ∈ P XORSAT.encoding := + ⟨solve, computableInPolyTime_solve, fun F => (solve_eq_true_iff F).symm⟩ -end Cslib.Complexity.XORSAT +end Cslib.Complexity diff --git a/CslibFrontier/Computability/Complexity/Problems/XORSAT/Dense.lean b/CslibFrontier/Computability/Complexity/Problems/XORSAT/Dense.lean index b8a3b830fd..58b52cc97d 100644 --- a/CslibFrontier/Computability/Complexity/Problems/XORSAT/Dense.lean +++ b/CslibFrontier/Computability/Complexity/Problems/XORSAT/Dense.lean @@ -303,7 +303,7 @@ private theorem step_polyTime : ComputableTidilyInPolyTime step encSystem encSys /-- The actual Gaussian-elimination decider is computable in polynomial time on native multi-tape Turing machines, with unary width and raw binary coefficient words. -/ -theorem decide_polyTime : ComputableInPolyTime decide encInput encBool := by +theorem computableInPolyTime_decide : ComputableInPolyTime decide encInput encBool := by have hloop : ComputableTidilyInPolyTime (fun q : Input => step^[q.width] q.rows) encInput encSystem := .iterate_of_bounded_growth input_width_tidy input_rows_tidy @@ -322,6 +322,6 @@ theorem decide_polyTime : ComputableInPolyTime decide encInput encBool := by /-- Dense XOR-SAT is in the native Turing-machine class `P`. -/ theorem satisfiable_mem_P : {q : Input | Width q.width q.rows ∧ Satisfiable q.width q.rows} ∈ P encInput := - ⟨decide, decide_polyTime, fun q => (decide_eq_true_iff q).symm⟩ + ⟨decide, computableInPolyTime_decide, fun q => (decide_eq_true_iff q).symm⟩ end Cslib.Complexity.XORSAT.Dense diff --git a/CslibFrontier/Computability/PolyTime/Graph/RotationSystem/Recognition/Query.lean b/CslibFrontier/Computability/PolyTime/Graph/RotationSystem/Recognition/Query.lean index c548b22829..bf1be10a6e 100644 --- a/CslibFrontier/Computability/PolyTime/Graph/RotationSystem/Recognition/Query.lean +++ b/CslibFrontier/Computability/PolyTime/Graph/RotationSystem/Recognition/Query.lean @@ -21,7 +21,8 @@ import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime Every certificate covers all raw inputs. Unary ranges are funded only by actual vertex/edge list lengths. All supplied endpoint/dart labels use binary comparisons and saturating binary lookup, including malformed huge indices. The concrete query composes the sparse compiler with -`XORSAT.solve_polyTime`; there is no solver, recognizer, growth or encoding provider hypothesis. +`XORSAT.computableInPolyTime_solve`; there is no solver, recognizer, growth or encoding provider +hypothesis. ## Main results @@ -320,6 +321,6 @@ theorem compile_polyTime : ComputableInPolyTime compile encFixedRotationInput XO /-- Concrete all-raw native query. Invalid models reject, and every valid query actually calls existing certified sparse Gaussian elimination. No topological criterion is used. -/ theorem query_polyTime : ComputableInPolyTime query encFixedRotationInput encBool := - validate_polyTime.bool_and' (XORSAT.solve_polyTime.comp compile_polyTime) + validate_polyTime.bool_and' (XORSAT.computableInPolyTime_solve.comp compile_polyTime) end Cslib.Complexity.Graph.RotationRecognition diff --git a/CslibFrontierTests/CSPAffine.lean b/CslibFrontierTests/CSPAffine.lean index 8f055b79be..225e125cde 100644 --- a/CslibFrontierTests/CSPAffine.lean +++ b/CslibFrontierTests/CSPAffine.lean @@ -112,7 +112,7 @@ example : ([] : CSP (Fin 5) ℕ) ∈ CSPSAT arity sem := by -- Concrete templates exercise the native reduction certificate as well as its semantics. example : PolyTimeReducible (encCSP (encFinite (Fin 5)) encNat) XORSAT.encoding (CSPSAT arity sem) - {F | XORSAT.Satisfiable F} := + XORSAT := CSPSAT.polyTimeReducible_XORSAT_of_templates (encFinite (Fin 5)) arity sem template templates end CslibFrontierTests.CSPAffine diff --git a/guide/CslibFrontierGuide/NPCompleteness.lean b/guide/CslibFrontierGuide/NPCompleteness.lean index 4ec14032ec..79d5c308b5 100644 --- a/guide/CslibFrontierGuide/NPCompleteness.lean +++ b/guide/CslibFrontierGuide/NPCompleteness.lean @@ -552,7 +552,7 @@ so repeating a positive literal twice is rejected as non-Horn syntax. {name}`Cslib.Logic.PL.isPolymorphism_parity_iff_exists_affineSystem` characterizes ternary parity preservation by affine equations. -{name}`XORSAT.satisfiable_mem_P` certifies ordinary sparse XOR-SAT with binary +{name}`XORSAT.mem_P` certifies ordinary sparse XOR-SAT with binary variable names; repeated variables cancel modulo two. The dense Gaussian elimination algorithm and sparse compiler both have native certificates. Their fixed-language compilers give {name}`CSPSAT.mem_P_of_and`, diff --git a/manual/circuits-logic-and-other-models/proof-systems.md b/manual/circuits-logic-and-other-models/proof-systems.md index 19ac9e2f14..73778376cc 100644 --- a/manual/circuits-logic-and-other-models/proof-systems.md +++ b/manual/circuits-logic-and-other-models/proof-systems.md @@ -232,7 +232,7 @@ variables and include empty/nullary relations. See the [majority examples](../.. The ordinary solvers are also reusable: `TwoSAT.mem_P` ([TwoSAT/PolyTime.lean](../../CslibFrontier/Computability/Complexity/Problems/TwoSAT/PolyTime.lean)), -`HornSAT.mem_P`, `DualHornSAT.mem_P` and `XORSAT.satisfiable_mem_P`. For `TwoSAT`, +`HornSAT.mem_P`, `DualHornSAT.mem_P` and `XORSAT.mem_P`. For `TwoSAT`, `TwoSAT.assignment` constructs a satisfying assignment in polynomial time on binary CNF encodings (`TwoSAT.computableInPolyTime_assignment`, `TwoSAT.eval_assignment_of_mem`) by filtering occurrence-bounded implication-graph reachability lists (`TwoSAT.reach`). Horn syntax counts