[edemaine]

Addresses the nonblocking API suggestions from #1147’s review, after #1180. The approved lower heads are unchanged; this follow-up need not delay their integration. Closes #1190.

CNF.modelCount_relabel_of_injOn requires injectivity only on occurring variables. Global relabeling and compaction now share that proof. The existing global theorem keeps its name and statement in a dedicated relabel module, with all clients updated. Guarded 3SAT counts reuse SharpSAT, and new decision bridges characterize positive counts. Counts still range over occurring variables, including empty support; no finite ambient variable type is required.

The list cleanup combines multiplicity characterizations into one indexed iff, strengthens the other-index lemma, and reuses Lean’s core last-element API. Existing model counts, relabeling, compaction, SharpSAT and core list lemmas supply the underlying notions; no parallel counting definition is introduced. Documentation identifies the occurrence-splitting count proof as an original consequence of its assignment correspondence.

Validation at de1aecb: all six required local gates pass, using four Lean threads. Hygiene, changed-file, documentation configuration and catalogue checks pass. Tests cover collisions outside support, a count-changing collision inside support, empty/infinite ambient types, sparse compact labels, repeated entries and guarded rejection.

Independent agent count_polish_review found no blocking correctness or API issues in the final source delta; the reviewed source manifest was verified before commit. This was read-only source review, without independent builds, and is not coordinator or human approval. Outside-fleet coordinator review is requested for the new public statements. Selected formal abstracts, catalogue scope and rendering are unaffected.

AI assistance: implemented with Codex (gpt-6.1-sol), including a delegated counting worker and a separate non-authoring review context.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-87 (agent review) at de1aecb.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-87 — APPROVED at de1aecb

Agent review, not human approval.

I reviewed the single commit on top of #1180's head d7effb7e, which is this PR's base.

• No parallel counting notion. SharpThreeSAT and SharpThreeSATThree change their bodies from φ.modelCount to SharpSAT φ. That is definitionally the same, since SharpSAT φ := φ.modelCount (Problems/SharpSAT.lean:70), and their guards are unchanged. This is the 3a suggestion from the feat(CNF): preserve model counts under occurrence splitting #1147 review. The two new bridges, SharpThreeSAT.mem_ThreeSAT_iff and SharpThreeSATThree.mem_ThreeSATThree_iff, are faithful ↔s that follow the existing SharpSAT.mem_SAT_iff naming. Tests cover a positive case and a satisfiable formula with rejected syntax.
• Relabelling. The global CNF.modelCount_relabel moves to CNF/ModelCount/Relabel.lean with the same full name. Its statement is unchanged: [DecidableEq V] was already in scope at the old location. It is now a corollary of the new modelCount_relabel_of_injOn, whose Set.InjOn f {v | v ∈ φ.vars} hypothesis is strictly weaker. modelCount_compact now reuses it, and the duplicated proof is gone. All three main clients (CookLevin/Parsimonious, CountingSAT, ThreeSATThree) import the new module. Tests show a collision outside the support preserving the count and a collision inside it changing the count.
• Removed and changed public names, with all clients migrated and no aliases.
  • List.exists_pair_indices_of_two_le_filter_contains and List.two_le_filter_contains_of_indices become the single List.two_le_filter_contains_iff. Their former clients (PairedCorrectness, Occupancy, PathAssignments) are updated.
  • exists_other_index_of_two_le_filter_contains drops its hi hypothesis, a strict strengthening; its one client is updated.
  • git grep finds no remaining references to the old names at the head.
• Credit. The count preservation is now labelled original in both Counting.lean and ThreeOccurrence.lean, which addresses finding 1 of the feat(CNF): preserve model counts under occurrence splitting #1147 review.
• Hygiene. No sorry, native_decide or set_option.
• CI and merge. Hosted ci-checks and check-title pass at this exact head. GitHub reports the PR MERGEABLE/CLEAN into its stacked base.

Nonblocking: the stack as a whole (already at #1180) conflicts with current main in the planar-SAT block of the Complexity.lean import list. That conflict comes from lower layers, not this commit, and needs an ordinary restack when the stack lands.

[SamuelSchlesinger]

Coordinator restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix): the base merged, so I retargeted this PR to main and replayed its own linear commit range onto origin/main (the base was rewritten before landing, so a merge would conflict). New head: 306b34a05207859064f1333ed464627605231112. Outside Complexity.lean and references.bib, the PR's diff is byte-identical to its approved de1aecb4, and mk_all --check passes, so the approval carries over. I will enqueue once CI is green.