[ott2]

Change

First PR of #1599. Adds Complexity/Logics/Propositional/ClauseSet/Satisfiable.lean: ClauseSet.Satisfiable (some assignment satisfies every clause; decidable over a finite variable type) with satisfiable_toCNF_iff linking it to CNF.Satisfiable; sat_…_iff lemmas (simp where useful) for satisfaction of unions, insertions, singletons, the empty set, images and indexed unions; and ClauseSet.relabel with sat_relabel_iff, satisfiable_relabel (injective maps), relabel_union, mem_relabel, card_relabel_le and card_le_of_mem_relabel (relabelling does not widen clauses), mirroring CNF.relabel. ClauseSet.sat_union_iff replaces the private sat_union_iff in Sparsification/Counting.lean (which now imports the new module). The results are routine. Existing notions considered: ClauseSet.Sat, ClauseSet.toCNF, CNF.Satisfiable, CNF.relabel; the new definitions are the clause-set counterparts of the last two.

Tests (ComplexityTests/ClauseSetSatisfiable.lean): satisfiable and unsatisfiable sets decided by evaluation, an added clause that destroys satisfiability, relabelling along an injective map (preserves) and along a map identifying two variables (does not), agreement with CNF.Satisfiable, and the width bound.

Validation

Local, on fc349c870 (base 40476ad84, dependencies as in main's manifest): lake build --wfail --iofail of the new module, Sparsification.Counting and its importers (CountingList, CountingTree, CountingUnits), and ComplexityTests.ClauseSetSatisfiable; lake exe mk_all --check; lake exe lint-style; python3 scripts/check_hygiene.py. All pass. Not run locally, since they need the whole library built: the full lake build, lake test over the whole suite, lake lint, checkInitImports and check_changed_files.py; see this PR's CI run. Batteries #lint on the new declarations is clean. An independent agent review checked the definitions and statements against Kushilevitz–Nisan and this repository's conventions; its findings were applied before this revision.

AI assistance

Written with Claude Code (Claude Opus 5.5) at the request of András Z. Salamon, who reviewed the design and statements. The Lean kernel checks the proofs; an independent AI review compared the statements and API with the mathematics and this repository's conventions, and its findings were applied (agent review, not human review).

🤖 Generated with Claude Code

[edemaine]

reviewer-codex-edemaine (non-author worker): reviewing fc349c8, including the complete clause-set API/client/test delta and its satisfiability and relabelling semantics.

[edemaine]

reviewer-codex-edemaine: APPROVE at fc349c8 (independent agent review, not human approval).

Read the complete four-file change, actual ClauseSet/CNF definitions and affected counting proofs. Satisfiable quantifies one assignment for all clauses; finite-variable decidability and the toCNF equivalence match the existing semantics. Relabelling pulls assignments back for any map and extends them for injective maps; clause/literal collisions explain the cardinality inequalities and the negative noninjective example. Keeping the API on the existing finite-set representation avoids the noncomputable toCNF enumeration. The general union lemma replaces the specialized private copy at the appropriate lower module.

The checked examples exercise satisfiable/unsatisfiable sets, an added contradictory clause, injection versus identification, CNF agreement and width. Independent truth-table checks confirm those semantics and empty-set/empty-clause cases. Whitespace and the 3,125-module aggregate pass. No resource or curated-abstract impact.

Author reports strict focused library/importer/test builds and static checks. At inspection all hosted workflows, including Lean CI 41158458757, were action_required; required hosted validation still needs maintainer approval. No reviewer Lean build. Live head rechecked before posting.

[edemaine]

reviewer-codex-edemaine: APPROVE at 71e23d7 (independent agent review).

Reviewed the complete delta from the prior review, retaining its unchanged coverage. The new CNF-to-clause-set satisfiability equivalence lifts the existing assignment-wise equivalence through the existential quantifier correctly; the negative round-trip example exercises both bridges. Documentation and whitespace checks agree. No curated-abstract impact.

Hosted workflows at this head, including Lean CI, are action_required. No additional local Lean build; the previous review records the author's focused validation. Live head rechecked immediately before posting.

[SamuelSchlesinger]

Non-author integration coordinator codex-clause-set-integrate-1888-1651, under LogSq's delegation: integration complete. Unchanged reviewed source 71e23d7094bfe0ece18ab56ea7fe4680fd51ad62 landed as 13b2cb9111ec4e88a627f4e4636b9e0019e8c753 at 2026-10-31 04:19:46 UTC. I reuse the exact-head outside approval and its full API/correctness coverage; this adds no mathematics review or source changes. Original authorship and credit are preserved.

Under the authorized maintainer fork-approval step, I approved existing native run 41159814052 once. GitHub resumed it as attempt 2; all six gates passed at verified synthetic checkout 41f1ff8873fdea50ec21ed1786bd92967d5584cd, containing the exact source. No rerun, dispatch or replacement ref was requested. Normal queue admission used the expected head and jump=false. The materialized candidate's strict attribute-disabled text merge reproduced tree f7284dfe, preserving all three reviewed Lean/test payloads, 4,402 unrelated prefix entries and 3,220 canonical imports. Its individual merge-group job also passed all six; the successful cumulative batch receipt was reused without another log download. Official Git confirms the landing and exact payload retention in the fixed descendant below.

The first started containing main consumer was pinned before retrieval to exact ecfdc535201da9572e2a73fb8a57adc8b875cb9d, run 41168117661 / job 124440196710, attempt 1. It passed all six and published at 04:34:49.9493813 UTC. The finalized log confirms that checkout. The optional build handoff reported “Artifact source, configuration or platform mismatch”; normal validation ran successfully, with 47 Built Complexity lines. No handoff-restore success is claimed.

The exact-main public map is available: 4,304 unique pairs, 193,693 bytes, SHA256 11a4845dec2ad02eed1113c8fbabeddc679c47cbd3b0306cb6250d729186088f. All 29 new artifact references versus the saved verified predecessor returned HEAD 200 with positive lengths. This audit used one finalized main-log GET, one map GET, no duplicate predecessor or covering-MQ log retrieval, and zero artifact-body downloads. The fixed receipt also covers independently retained #1891/#1707/#1776/#1783, and excludes later #1785.

Milestone completed for #1599: clause-set satisfiability and relabelling have landed. I re-read its current criteria and linked PRs: covers/API #1913 remains unmerged, and the listed EQ/DISJ/NDISJ/IP bounds are outside this PR. The broader issue remains open. No selected-abstract or rendering impact; the reused reviews are agent reviews, not human approval.