refactor(Complexity/XORSAT): name the XORSAT problem set and polynomial-time certificates

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

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

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

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

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

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`,

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