[SamuelSchlesinger]

This establishes the exact MAX-SAT and natural weighted-counting milestone from the counting roadmap, with ordinary native Turing-machine time and space certificates.

For an input of encoded length L, the new endpoints use polynomial space and time
poly(L) · 2^{O(N / sqrt(log(N + 2)))}:

• Exact MAX-SAT: computes threshold counts, the complete score histogram, and the optimum clause count. Here N is literal occurrences plus clauses. For fixed width k and at most c(n+1) clauses, the sparse endpoints give 2^{O_{k,c}(n / sqrt(log(n+2)))} poly(L). Counts range over all declared assignments, including unused variables, and preserve repeated and empty clauses. The declared variable count is unary, literal indices are binary, and output counts are binary.
• Natural weighted counting: computes Boolean CSP partition functions with fixed arity, nonempty constraint scopes, polynomial-time local weight evaluation, and input-dependent natural weights of polynomial bit length. Here N is the occurrence count; bounded occurrence gives the variable-count rate. The counter checks its scope and bit-budget promises, so the resource theorem holds on every encoded input.

The main entry points are MaxSAT.exists_histogram_algorithm, MaxSAT.exists_optimum_algorithm, their sparse variants, and BinaryWeightedCounting.exists_partitionFunctionCounter_of_weightBits / BinaryWeightedCounting.exists_partitionFunctionCounter_boundedDegree_of_weightBits.

Mathematics and native implementation

The weighted endpoint needs more than the previously stated linear precision and truncation ranges. This extends the contraction analysis to 1 ≤ P ≤ D·s·(log₂ s + 1) and 1 ≤ ℓ ≤ D·(s+1)^d, still with a linear vertex bound. The normalized-precision clock, polynomial interpolation overhead, and fixed small-size fallback preserve the contraction exponent. Resource constants are chosen before the input.

A natural weight is replaced by its binary-digit polynomial. Exact coefficient recovery followed by evaluation at 2 reconstructs the weighted count; the bit budget, degree, precision, entry evaluation, and output decoding are all proved and charged. MAX-SAT uses linear-size population-count/threshold circuits and a native polynomial-query/postprocessing closure.

These enlarged parameter ranges extend Theorem D.1 of the pinned OpenAI2026ETH manuscript. The module documentation distinguishes the paper's stated ranges from the extensions proved here and records the source mapping.

Scope and dependencies

This is a completed milestone for optimum values, score distributions, and natural weights. Native optimizing-assignment extraction, signed/rational weight interfaces, a variable-count bound for dense exact MAX-SAT, and the full D.2 application in #1538 remain open. ROADMAP.md preserves these gaps. No selected formal abstract or catalogue claim changes.

The branch includes the entry-procedure truncation interface from #2067 (head cfa776be) and preserves its author credit and ancestry. The general truncation assembly from #2044 is already on the base branch. The new result is separate from closing #1538 or superseding #2067's review.

Validation and independent review

Validated and reviewed source revision: 1e618125.

All six required project gates passed in Lean Action CI run 41242903927, which checked this head merged with current main:

• lake build --wfail --iofail
• lake exe mk_all --check
• lake test --wfail --iofail
• lake lint
• lake exe lint-style
• lake exe checkInitImports

The entire CI job, including source hygiene, changed-file documentation, registry references, and the tidy-statement checks, succeeded. The Guide build and PR-title check also passed.

Local strict build, aggregate check, hygiene, and focused endpoint tests passed. The duplicate local full-test run was stopped after hosted CI passed the full tests; that interrupted local run is not counted as a pass. Hosted CI supplies the complete validation record.

Independent, non-authoring reviewer /root/independent_review approves correctness and API for the revision above, with no open findings. The review covered the actual definitions, encodings, native reductions, quantitative bounds, parameter order, edge cases, and pinned-paper mapping. The public tuple-projection and stale-roadmap findings were fixed, and the general table-bit bound was moved beside its definition. The reviewer independently checked the successful CI metadata and logs.

The review covers this development and the relevant changed interfaces; it relies on the existing library for unchanged underlying theorems.

Ownership and AI assistance

Task owner: ChatGPT/Codex coordinator session, branch feat/maxsat-weighted-counting-20261031; this PR records the requested milestone and remaining scope. Parallel agents developed the MAX-SAT, precision, and weighted-counting components. ChatGPT/Codex generated and revised proofs, tests, and documentation; a separate non-authoring agent reviewed the source/API, source mapping, quantitative bounds, and edge cases. This is agent review, not human approval. The inherited #2067 implementation was written with Claude Code (Opus), as disclosed there. Handoff: awaiting maintainer review.