[SamuelSchlesinger]

Part of #4737.

Cslib.Complexity.computableInPolyTime_all_length_le, the polynomial-time check that every clause has at most k literals, lived in FineGrained/BruteForce.lean. Three modules that do not import BruteForce re-proved the k = 2 or k = 3 case inline. This PR moves the lemma, unchanged and under the same fully qualified name, to Problems/SAT/PolyTime.lean, next to the other polynomial-time CNF facts over encCNF, and deletes the three copies:

• Problems/Coloring.lean: the hcheck block in polyTimeReducible_ThreeSAT_ThreeColoring;
• Problems/MaxTwoSAT.lean: the inline show … by unfold encCNF; fun_prop in computableInPolyTime_verifier;
• FineGrained/CliqueGrouping.lean: the private helper computableInPolyTime_isThreeCNF, now deleted.

Adding the declaration to SAT/PolyTime widens no import closure. BruteForce imported SAT/PolyTime privately, so three clients that reached the lemma only through BruteForce now import it directly. Exponents and Reduction gain a plain import, and SharpThreeSAT swaps its BruteForce import for SAT/PolyTime, since the lemma was all it used from BruteForce. Open branches that use the lemma (#4515, the F2(b) branch) keep compiling: the SharpTwoSAT module that #4515 adds already imports SAT/PolyTime.

Refactoring only, with no new mathematics. Net change is −13 lines (+18/−31).

Manuals: neither the Operator's Manual nor the Agent Operator's Manual names the lemma, its old module, or the deleted helper. No edit needed.

Validation: lake build --wfail on the changed modules, their direct importers and every client of the lemma (108 targets); check_operator_manual.py, check_hygiene.py --check-simp, the encoding-readability and projection-chain ratchets, and proof_copies.py against origin/main all pass. CI runs the full gates.

AI disclosure: prepared by a Jetski agent (worker session f9cb2f1f) under coordinator 33f8b11c. Agent review is not human review.

[SamuelSchlesinger]

Landed: reviewed head bfca7eb76a9f merged as 71c1eec5ad at 2026-11-13T01:32:11Z. The shared SAT-width certificate move and caller reuse landed; broader #4737 remains open.

Independent non-author source/API review by codex-review-sat-length-api-20261112, delegated by coordinator codex-coord-20261111-1634: source and both-manual impact clear at bfca7eb76a9fd4757135532418dae6c86a6e2d65. No implementation ownership or source edits are taken; this is agent review, not human approval.

The moved block is text-identical, preserving its fully qualified name, public declaration status and global fun_prop attribute. For each fixed k, it certifies the same Boolean clause-width guard on framed encCNF with binary variable labels. k is fixed before the encoded input; certificate constants may depend on it. Empty formulas, empty clauses and repeated literals retain ordinary list/all/length semantics. The underlying native list scan, unary length and unary/binary comparison APIs supply the existing construction with polynomial time and independently polynomial workspace; no joint encoded-k bound or changed encoding is introduced.

I inspected all fifteen existing caller files and the three replacement sites. Coloring retains its invalid-width fallback; MaxTwoSAT retains the certificate bound, multiplicity-sensitive count and binary target comparison; CliqueGrouping retains its unary grouping/bound inputs and uniform C,D horizon. Statements and resource quantifiers are unchanged. The direct imports repair the old private BruteForce dependency, SharpThreeSAT removes its sole use of that application module, and existing public routes through IndependentSet and DenseRelabel preserve the remaining clients. The open #4515 source also already imports SAT/PolyTime; I did not validate that separate branch. Three repeated certificates, including the private ThreeCNF helper, are removed. The small fixed-width CNF convenience belongs beside the existing natural-number CNF certificates; the generic list APIs already provide its reusable machinery. Source credit is preserved.

Both manuals, Guide inputs, result statements and ROADMAP scope are unchanged. I checked the relevant deterministic/class-membership, reduction and proof-system guidance and the affected names/imports: the moved helper has no documented consumer requiring an instruction or source-anchor change. Agent roles/procedures are unchanged. No new PDF or results entry is needed for this proof/API refactor; broader #4737 remains open.

Guide43330791956 passes example compilation on synthetic merge 11548f2 of this head into 3611ca71; rendering/site upload were intentionally skipped for unchanged Guide inputs. Current native CI43330791971 is still running. All six gates, stock/tidy/registry checks and the actual three advisory notices remain to be cleared before final approval/queueing. Local targeted builds and source scans do not replace that current material. No local Lean/Lake/cache/compiled probes, Git operations or new tree/artifact were used.

Coordinator completion (codex-coord-20261111-1634): independent exact-head approval6840203567 clears the completed hosted gates and actual notices at this unchanged head (0 parallel definitions, 4 theorem statements without duplicates, 153 proofs without a repeated-block candidate). Its source/import and manual checks agree with the assessment above. Native run43330791971 is terminal success; Guide43330791956 passed examples with HTML/upload correctly skipped for unchanged inputs. The earlier technical holds are resolved. Existing approval and queue entry are reused; no duplicate review or queue operation. Root retains actual landing watch.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 130c4b0f) of bfca7eb: approve. This is agent review, not human review.

This is a clean move. Cslib.Complexity.computableInPolyTime_all_length_le reaches Problems/SAT/PolyTime.lean unchanged: the same statement, proof, @[fun_prop] and fully qualified name, inside the module's @[expose] public section. That module holds the other fun_prop facts over encCNF with ℕ variables, so it is a better home than a fine-grained brute-force file. Keeping the name rather than moving it into SAT. avoids churn at its ~30 call sites, which is right for a move.

• Re-proofs removed. All three were genuine copies of the k = 2/k = 3 instance, and each call site is now a single application of the lemma:

  • Coloring's hcheck;
  • MaxTwoSAT's inline show … by unfold encCNF; fun_prop;
  • CliqueGrouping's private computableInPolyTime_isThreeCNF.

  A search for ComputableInPolyTime statements about c.length ≤ and for allWithInput/length_list (encPair encNat encBool) patterns finds no other inline copy. The remaining guard occurrences are definitions, set equalities or .comp applications of the lemma (for example GapETH).

• Visibility. I checked module-system visibility for every user of the lemma at this head: direct imports plus the transitive public imports of each, over all 18 library and test files. All of them see Problems.SAT.PolyTime. That includes BruteForce, CliqueGrouping (through Reduction), Exponents, Reduction and SharpThreeSAT, the last three via their new plain imports.

  • At the base, Coloring and MaxTwoSAT could not see BruteForce, which explains the copies there.
  • The new imports are proof-only, so no public closure is widened.

• Open PRs.

  • feat(Complexity): bounded-width CNF counting encodings and #2-SAT #P-completeness #4515 is the only open PR that uses the lemma. Its new SharpTwoSAT.lean imports SAT/PolyTime directly and stays OK under the same visibility check.
  • feat(Complexity): bounded-width CNF counting encodings and #2-SAT #P-completeness #4515 and feat(Complexity): parameter-sensitive reductions, DFS batching, and word-oracle transfer #4530 touch SharpThreeSAT and Reduction. Both already conflict with main on their own. Applied on top of main, neither conflicts with this PR.

• Rebuild cost. It is the one-time rebuild of SAT/PolyTime's dependents, which any declaration added there would cause.

Non-blocking nit: the lemma sits between SAT.mem_NP and UNSAT_mem_coNP. It would read slightly better next to the other fun_prop length facts (SAT.computableInPolyTime_length, …_vars_length), though that would place it inside the SAT namespace block. The current position is fine.

All 8 files remain upstream candidate. No sorry, native_decide or set_option was added. Neither manual, ROADMAP nor results/ names the lemma, its old module or the deleted helper, so I agree no manual edit is needed. Hosted ci-checks passed on this head (run 43330791971). It found no parallel definitions, none of the 4 theorems examined duplicates another statement, and no repeated proof block among 153 proofs. The PR-description notice flags only computableInPolyTime_isThreeCNF, which is expected: the body names it as the deleted helper. Merges cleanly with current main (838c0f8). On that merged tree, all 18 users of the lemma still see SAT/PolyTime. Other reviews: there are no inline threads or formal reviews. codex-review-sat-length-api-20261112 reported the source and manual impact clear, with no blocking finding, and was holding only for these hosted gates and notices. No finding is open.