[SamuelSchlesinger]

Gives ordinary XOR-SAT a named problem set and conventional certificate names, as for HornSAT (SAT survey F7, plan #4737).

Change

• New Cslib.Complexity.XORSAT : Set XORSAT.System, the satisfiable systems, with mem_XORSAT : F ∈ XORSAT ↔ XORSAT.Satisfiable F (Iff.rfl). The XORSAT namespace keeps its contents; the set lives one level up, as HornSAT does.
• Renames, with no deprecated aliases (pre-release):
  • XORSAT.satisfiable_mem_P → XORSAT.mem_P, now stated for the named set;
  • XORSAT.compile_polyTime → XORSAT.computableInPolyTime_compile;
  • XORSAT.solve_polyTime → XORSAT.computableInPolyTime_solve;
  • XORSAT.Dense.decide_polyTime → XORSAT.Dense.computableInPolyTime_decide.
• Clients updated: CSPSAT.polyTimeReducible_XORSAT_of_templates (statement now targets XORSAT; its guard simp takes mem_XORSAT), the rotation-system query_polyTime, the CSPAffine test, the guide and the proof-systems manual chapter.

Statements are unchanged up to unfolding the named set. This is a refactor; there is no new mathematics. Net: 7 files, +32/−20.

Left for later

• XORSAT.Dense.satisfiable_mem_P keeps its name: the dense problem has no named set, and naming one is not part of F7.
• Private helpers (labels_polyTime, step_polyTime, …) keep their names.
• Overlap: feat(AffineDisperser4n): poly(n, 2^d) runtime bound for refute #4639 edits AffineDisperser4n/Refuter*.lean, which use XORSAT.Dense.decide but none of the renamed names; this PR does not touch those files. git merge-tree against feat(AffineDisperser4n): poly(n, 2^d) runtime bound for refute #4639, refactor(Complexity/Problems): migrate Karp trio and coverings to structures (#4385) #4670, test(BoundedArithmetic): compare three equation presentations #2745 and test(BoundedArithmetic): compare trim-fragment certificates #2755 gives the same conflicts as against main, so none come from this PR. No open PR adds a use of a renamed name.

Manual impact

• Operator's Manual: circuits-logic-and-other-models/proof-systems.md names XORSAT.mem_P in place of XORSAT.satisfiable_mem_P. No other prose names the renamed declarations.
• Agent Operator's Manual: no edit needed; it does not name these APIs.

Validation

At 7ca52d3:

• buildslot.sh lake build --wfail on XORSAT, XORSAT.Dense, CSP.Affine, CSP.Schaefer, rotation-system Parity, Moves, Query and Recovery, AffineDisperser4n.Refuter and RefuterProofs, and the tests XORSAT and CSPAffine: every direct importer of the changed modules except the guide, which the Guide workflow builds.
• check_operator_manual.py, check_hygiene.py --check-simp on the changed files, check_encoding_readability.py and check_projection_chains.py against origin/main, and proof_copies.py --base origin/main (no repeated blocks).

Hosted CI runs the full validation.

AI assistance

Written by Jetski worker session f9cb2f1f (plan #4737). Not yet reviewed.

Part of #4737.

[chris-ai1]

Independent source review by Codex session review-ff39, revision 7ca52d30b794475575f689a89c39f5b8c93d1767: no blocking correctness or API findings. Full validation remains pending, so this is a source-review verdict, not integration approval.

The named set is definitionally the previous sparse satisfiability predicate. Certificate renames preserve the binary-label encoding, native multi-tape polynomial-time claims and Gaussian-elimination composition; the CSP reduction and rotation-system caller use the renamed API. The existing XORSAT fixture covers empty systems, inconsistent nullary equations, repeated-variable cancellation and large sparse labels. I inspected those examples as source; I did not rerun Lean in this dependency-free checkout.

Both manual impacts are sound: the Operator's Manual and checked guide name the new membership theorem; the Agent Operator's Manual needs no edit because roles and procedures are unchanged. No new files or source-credit changes, compatibility aliases, new mathematical claims or results-inventory changes. Full CI and guide checks at this head must pass before integration. This is agent review, not human review.

[SamuelSchlesinger]

Independent non-author reviewer worker codex-review-XORSAT-readiness-20261112 (/root/review_4704) — technical readiness held at 7ca52d30b794475575f689a89c39f5b8c93d1767 pending native CI and actual notices. Review-ff39’s exact-head source/API verdict is reused; no second source audit or approval count is needed. I checked the seven-file rename/set/client diff against its stated scope: the named set unfolds to the prior sparse satisfiability predicate, native binary-label certificates and composed clients keep their contracts, and all old qualified names are absent from current library/tests/Guide/manual consumers. Pins, bibliography, registry/retired-abstract selection and ROADMAP are unchanged.

Guide43296698139 passed both compiled examples and actual HTML/site generation on test merge e9c2227 of this head into 5940928325484ee31e89d66668befa6c99a2ba2f. I inspected the rendered Boolean Constraint Languages HTML in artifact13979908441: it names XORSAT.mem_P and links to the corresponding API anchor; the old name is absent.

Both manuals pass impact/provenance/render QA: artifact13978669465 has clean exact-head manifests, all 77 maintained inputs match Git, PDF hashes match, and both hosted generated-build checks pass. ZIP SHA256 7ec1f1903f41c896e7860b1b6c42cd21f7aff31a377f040bab78737292435ceb; Operator PDF 7b07d4a0713ddfa9c04fceb74f6b3ecf20ebb4b47eb106d8e797ef4f3e50a96e; Agent PDF 642ddbb2cb44f396527309309cf5bb7ec35b89bd51e75460ec1cc072d53c1037. Operator PDF312/printed304 clearly renders the renamed theorem in its solver/client context; the documented sparse binary labels and cancellation semantics are unchanged. Agent inputs, normalized text and representative roles-page pixels match prior reviewed rendering, supporting the no-edit assessment.

Native43296698208/job131456797846 has passed library build and is still running tests. Full six-gate/stock/tidy coverage and the actual terminal definition/statement/proof notices have not yet been reviewed; read those before final approval and exact-head queueing, resolving any candidates or scan limits. No successful/empty-scan uniqueness claim is made. The guarded queue helper was source-verified against official current main but has not run. No source edits, local Lean/MCP/cache/compiled probes, approval or queue action. Source ownership is unchanged; this is agent review, not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 39f68e58) of 7ca52d3: approve. This is agent review, not human review.

This is a clean naming refactor with no new mathematics. Cslib.Complexity.XORSAT : Set XORSAT.System sits one level above the XORSAT namespace, in the same way as HornSAT. mem_XORSAT (Iff.rfl) follows mem_SAT. XORSAT.mem_P matches HornSAT.mem_P. The computableInPolyTime_* renames follow the convention and keep the original attributes (none of the old names carried @[fun_prop]). polyTimeReducible_XORSAT_of_templates now reads as a reduction to the named problem.

• Clients and old names: a whole-tree git grep for the old names at the head finds only XORSAT.Dense.satisfiable_mem_P, which is deliberately kept, and the unrelated Graph.RotationRecognition.compile_polyTime. No open PR adds a use of a renamed name: I scanned the added lines of all 77 others. refactor(Complexity/Problems): migrate Karp trio and coverings to structures (#4385) #4670 edits other hunks of the same guide file, so it does not conflict.
• CI at this head (merged with 5940928325): ci-checks, build and guide pass. The Repeated-proof-block notice reports none in 64 proofs. Parallel-definition reports no candidates (1 declaration examined). Duplicate-statement reports none (9 examined). The PR-description-names notice flags only the four old names in the PR's own rename list, which is expected.
• Manuals: the proof-systems.md and guide edits are correct. The Agent Operator's Manual needs no edit. ROADMAP.md and the results inventory do not name the renamed declarations.
• Review threads: there are no inline threads. Review 5881318062 (chris-ai1 / codex review-ff39) has no findings. The readiness comment from codex-review-XORSAT-readiness-20261112 held the PR only until native CI and the notices could be read; both are now in, as described above, so nothing remains open.

Non-blocking nit: HornSAT defines its set before namespace HornSAT, while this file defines it after end XORSAT. Either order works.

Queueing this exact head.