[chris-ai1]

Follow-up to #1338 (tracking: #1226; abstract catalogue: #587), which merged before the last four offered commits were picked up (comment). These are readability changes to the ETH abstract requested by @crei. No theorem statement changes meaning.

1. vars is the set of occurring variables. def vars (φ : Formula) : Finset ℕ, so numVars φ = (vars φ).card and modelCount ranges over vars φ → Bool. Every former use went through .toFinset.
2. New supporting theorem length_encCNF, the exact encoding length, shown in a new Input size section and listed in the catalogue's supporting_theorems: (encCNF φ).length = φ.length + (φ.flatten.map fun l => 10 + 8 * Nat.size l.var).sum. That is one bit per clause plus 10 + 8 · (binary length of the variable) per literal occurrence. It shows that the polynomial factor in exact_count is honest. The proof is in the bridge, by induction, in about 20 lines.
3. open ComplexityTests.Abstracts.Encoding, so encCNF := encList (encList (encPair encNat encBool)) and exact_count reads ComputableInO count encCNF encNat ….
4. ComputableInO is displayed locally over upstream ComputableInTimeAndSpace, like DecidableInTimeO. The abstract no longer imports or allowlists MultiTape.ResourceBounds; its only allowlisted module is Encoding.

The audit now reports 27 roots and 143 dependencies. New tests check:

• vars = (CNF.vars ·).toFinset by rfl;
• ComputableInO ↔ the library predicate by Iff.rfl;
• concrete encoding lengths of 27 and 12 bits.

Validation.

• Locally on main 6789daf6, all six scripts/check.sh gates pass, together with check_hygiene.py and check_docs.py --config-only.
• Hosted CI: Lean Action CI run 40556777159 on 0e9292b7 passed. The review follow-up 7e600f54 passed Lean Action CI run 40600078340 and the Formal abstract PDFs run 40600078353.

Agent/session: worker-crei-dc679113 (Claude Code, Claude Opus 5.5). Please merge with a merge commit.

🤖 Generated with Claude Code

[SamuelSchlesinger]

reviewer-jetski-5208-1352 for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at 0e9292b78edd58ef06f6d9e84b6e74dda558e5a7

Thanks for picking up these readability changes. The edits to the existing statements keep their meaning, and the abstract reads better for them.

What changed. vars is now Finset ℕ. numVars and modelCount stay definitionally equal to the library, and the tests check this by rfl. modelCount still ranges over assignments of the occurring variables only, with every other variable set to false. The local ComputableInO matches Turing.MultiTapeTM.ComputableInO in ResourceBounds.lean exactly: one constant c, time c(T+1), work space c(S+1), and the encoded output also bounded by c(S+1). The test checks this by Iff.rfl. The prose for upstream ComputableInTimeAndSpace matches Deterministic.lean: there is one finite-state binary machine, and on each input it halts with encOut (f x) within t x steps and s x work cells. exact_count, not_eth, not_seth and satExponent_eq_zero are unchanged up to notation. The #check_abstract audit is still present. It now allowlists only Encoding (27 roots, 143 dependencies), so the statement boundary is tighter than before.

New statement length_encCNF. Against the Encoding foundation, frame w has length 2|w| + 1 and a literal's encPair has length 2·size v + 2. So a literal costs 2(2·size v + 2) + 1 bits inside its clause, and the clause frame doubles that and adds 1, giving 10 + 8·size v per occurrence plus one bit per clause, as stated. Checked instance: [[(2, true)]] gives 1 + 10 + 8·2 = 27, which matches the decide test. Empty clauses each contribute one bit, which the [[(0,false)],[]] ↦ 12 test covers.

Blocking

• length_encCNF does not appear in the curated abstract that readers see (see the inline comment). It sits under ## Representation details and is not listed in catalogue.json, so build_abstracts.py omits both its statement and its docstring. In the PDF built by this PR's "Formal abstract PDFs" run, subexponential-sat.pdf says "A fifth theorem, length_encCNF, gives the exact length of the input encoding", but the theorem appears nowhere. Please either display it or drop the sentence; the inline comment gives the details. The catalogue summary and scope are otherwise still accurate.

Nits

• Please cite Garey and Johnson by key (inline comment).
• The PR body could link the tracking issue (#1226, or #587 for the abstract catalogue), as #1338 did.

CI: ci-checks is green on 0e9292b78edd58ef06f6d9e84b6e74dda558e5a7, and the PR is mergeable. Limits: I did not build locally. I relied on CI for the proofs and on the downloaded PDF artifact for the rendering point.

[SamuelSchlesinger]

Blocking: this theorem never reaches the rendered abstract. build_abstracts.py shows only the headline and supporting_theorems entries listed in catalogue.json, and it drops an unselected theorem's docstring too. ## Representation details also moves to the appendix, and selected statements are not allowed there. The rendered subexponential-sat.pdf from this PR's run mentions length_encCNF in the intro (line 20) but never shows it.

Suggested fix: move length_encCNF out of ## Representation details, for example to the start of ## Deterministic machine and resource conventions or into a short "Input size" section before exact_count. Then add

"supporting_theorems": ["ComplexityAbstracts.SubexponentialSATAbstract.length_encCNF"]

to the subexponential-sat catalogue entry. Alternatively, if you want to keep it only in the source, drop the "A fifth theorem" sentence from the intro.

[chris-ai1]

Fixed in 7e600f54. length_encCNF now sits in a new ## Input size section just before exact_count, outside the appendix, and the subexponential-sat catalogue entry lists it under supporting_theorems. build_abstracts.py --check passes (20 abstracts, 33 headlines).

[SamuelSchlesinger]

nit: please cite by key, as [Garey and Johnson][GareyJohnson1979] (already in references.bib), and add it to the module's References list.

[chris-ai1]

Done in 7e600f54: it is now cited as [Garey and Johnson][GareyJohnson1979] and added to the References list.

[SamuelSchlesinger]

reviewer-jetski-5208-1352b for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at 7e600f5487eece294abd34a50c39027e13565306

This re-review covers the delta since 0e9292b7, where the previous review asked for changes. Thank you for the quick fixes.

The blocking finding is resolved. length_encCNF has moved out of the ## Representation details appendix into a new ## Input size section just before exact_count. The subexponential-sat catalogue entry now lists it under supporting_theorems, a field build_abstracts.py already reads. I downloaded subexponential-sat.pdf from this head's "Formal abstract PDFs" run (run 40600078353, head 7e600f54). It now shows the section, the docstring and the statement (encCNF φ).length = φ.length + (φ.flatten.map fun l => 10 + 8 * Nat.size l.var).sum, so the intro's "A fifth theorem, length_encCNF…" sentence is now accurate. The new section's lead sentence is also correct: in exact_count, the polynomial factors are in (encCNF φ).length.

No statement changes meaning. The theorem and its proof term are moved verbatim. The only edits are in docstrings, a section comment, a References entry and the catalogue. exact_count, not_eth, not_seth and satExponent_eq_zero are byte-identical to the previously reviewed revision. The #check_abstract audit still reports 27 roots and 143 dependencies, with Encoding as the only allowlisted module. The catalogue summary and scope remain accurate.

Both nits are addressed. Garey and Johnson are now cited as [Garey and Johnson][GareyJohnson1979], a key present in references.bib, and the entry is in the module's References list. The PR body now links #1226 and #587.

CI: ci-checks and the abstract PDF build are green on 7e600f54, and the PR is mergeable. Limits: I reviewed only the delta and did not build locally. I relied on CI for the build and on the PDF artifact for the rendering.