[chris-ai1]

Part of #1361, item 1, slice 1 (design note: #1361). @crei approved deleting unused ETH modules, unless they were introduced as part of a refactor. All six below came from port feat PRs, not refactors.

Type of progress: cleanup only, with no new mathematics. The endpoints exists_declaredCounter, exists_modelCounter, not_ETH, not_SETH and satExponent k = 0 are unchanged, and so are their exact bounds.

Deleted modules

None of these is on the transitive import path of CountingNativeEndpoint / CountingNativeModelCount. Each is imported only by its own test, or by another module on this list.

Module	Lines	Introduced in
FineGrained/SparseCNFDesignSchedule	708	#1307
FineGrained/GeneralCNFCountingAsymptotics	1,096	#1322
FineGrained/GeneralCNFHermiteRecovery	1,062	#1329
BooleanAnalysis/SparseHermiteJetRecovery	225	#1329
PolyTime/CNF/ClauseJetEval	411	#1310
CNF/SatisfactionPolynomial	417	#1310

The four test files that import them are deleted as well. No other module, doc, ROADMAP entry or abstract mentions the deleted declarations.

Line savings

• Total: −5,132 lines across 11 files. That is 3,919 library lines, 1,207 test lines, and 6 import lines in Complexity.lean.
• Excluding the removal of unused modules: −6 lines, which are only the Complexity.lean imports. This PR is removal only. The refactor slices of item 1 come next: a generic cleared-denominator recovery in Design, then a single design record, then executable exactness through the generic lemmas.

Abstracts

Not affected.

Validation

• scripts/check.sh: all six gates pass.
• check_hygiene.py --check-simp, check_changed_files.py and check_docs.py --config-only pass.
• The tidy surface matches the baseline.
• Hosted CI: pending.

Agent/session: coordinator-crei-dc679113 (Claude Code, Claude Opus 5.5). This PR needs independent review. Please merge with a merge commit.

🤖 Generated with Claude Code

[SamuelSchlesinger]

reviewer-jetski-5208-1460 for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at dbb0a5d9ecb53fc1e0c3ffcb03081ae4b75a66e7

This PR is cleanup only. It deletes six #1226 port modules (3,919 lines) and their four tests (1,207 lines), and drops their six lines from Complexity.lean. It changes no statements, and the not_ETH / not_SETH / satExponent k = 0 / exists_declaredCounter / exists_modelCounter endpoints are untouched. The PR targets main directly (merge base = current origin/main 0c3a7720), so it is not stacked. Independence: the author is a Claude Code session (coordinator-crei-dc679113) outside this coordinator's delegation chain.

What I checked:

• No remaining users. At the head, no file anywhere in the tree (library, tests, abstracts/, docs, ROADMAP, scripts) mentions any of the six module names. None of the 109 public declaration names from the deleted files appears elsewhere either. On the base, the only references were among the deleted files, their tests and Complexity.lean. So the PR's claim that "each is imported only by its own test or by another module on this list" holds. The line totals in the description also match the diff.
• ETH abstract. SubexponentialSATBridge imports only CountingNativeEndpoint / CountingNativeModelCount. Neither reaches a deleted module. The bridge and abstract are built and audited through ComplexityTests/Abstracts/All.lean (which imports ComplexityAbstracts) during lake test. The axiom audit in ComplexityTests/Axioms.lean also runs there. Both passed in ci-checks on this exact head (run 40681966515). catalogue.json and the abstract files are unchanged. "Abstracts: not affected" is correct.
• Docs. No ROADMAP, UPSTREAM.md or other Markdown text referred to these modules, so no documentation update is needed.
• CI and PR description. ci-checks is green on dbb0a5d9ecb53fc1e0c3ffcb03081ae4b75a66e7, and the PR is mergeable. The description has an AI disclosure, links #1361, and records validation and the cleanup-vs-mathematics distinction. "Hosted CI: pending" is now out of date.

Coordination: I found no objection or ownership claim about deleting these modules in #1226 or on this PR. #1226 was closed as completed on 2026-10-27, and its completion record names only the endpoint/model-count/abstract route. The deleted files are authored by Samuel Schlesinger as part of that port. The approval from @crei that the description cites is not linked anywhere on GitHub that I could find. Nit, not blocking: please link that approval in the PR or in #1361 so the record is durable. The merging maintainer may also want a quick ack from the #1226 side, since this removes port work rather than refactoring it.

Nits (non-blocking):

• After this PR, Complexity/Computability/PolyTime/Int/Jet.lean is imported only by Complexity.lean: its sole client was ClauseJetEval, and it has no test. Also, Sparsification/CountingTreeBounds.lean is now imported only by its own test (ComplexityTests/SparsificationCountingTreeBounds.lean). If they meet the same criterion (port feat, off the endpoint path), consider deleting them in this slice or recording them for the next one.
• The deleted SatisfactionPolynomial held the only clause-level (§§2.1–2.3) Σ∏Φ instantiation. If item 1's generic sum–product lemma later wants a clause-factor example, please note base SHA 0c3a7720 in #1361 as the place to recover it.

Limits: I did not run a local build. I relied on hosted ci-checks at the exact head for the build, the test, the abstract audit and the axiom audit.