[chris-ai1]

Follow-up to #1226 and #1344, supporting the readable exact_count statement proposed on #1338.

New: Cslib.Complexity.CountingNativeEndpoint.exists_modelCounter, in the new module FineGrained/CountingNativeModelCount.lean.

theorem exists_modelCounter (k : ℕ) :
    ∃ (count : CNF ℕ → ℕ) (A e b : ℕ),
      (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) → count φ = φ.modelCount) ∧
      ComputableInO count encCNF encNat
        (fun φ => ⌈(2 : ℝ) ^ ((A : ℝ) * interpolationScale φ.numVars)⌉₊ *
          ((encCNF φ).length + 1) ^ e)
        (fun φ => ((encCNF φ).length + 1) ^ b)

This is the plain-formula form of exists_declaredCounter:

• The input is the formula itself, with no declared size, unary header or validity guard.
• The count is the existing CNF.modelCount, taken over the occurring variables.
• The resource bounds are folded into ComputableInO.

Proof. Compose the declared counter with the polynomial-time map φ ↦ (φ.denseRelabel.numVars, φ.denseRelabel), then rewrite with numVars_denseRelabel and modelCountOn_denseRelabel. The remaining work is natural-number resource arithmetic. The proof uses no tidy calculus beyond the exists_degree/inO idiom already used by CountingNativeEndpoint.

No existing statement changes.

Validation.

• Locally, with this module and the feat(abstracts): OpenAI: the Exponential Time Hypothesis is false #1338 abstract adaptation on top of the feat(abstracts): OpenAI: the Exponential Time Hypothesis is false #1338 head, all six scripts/check.sh gates pass, together with check_hygiene.py and check_docs.py --config-only.
• On this branch, built on actual main 4bfc3e6f, lake build of the module and mk_all --check pass.
• Hosted CI: Lean Action CI run 40544174450 on 23e9924a passed.

The matching abstract, bridge and test changes for #1338 are offered there as a separate commit.

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

🤖 Generated with Claude Code

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): CLAIMING the single bounded outside contract/resource review of the model-count supplier, exact head 23e9924a to be resolved in the source check. Reuse of approved native proofs only; no implementation brief, extra reader or duplicate build. #1338’s earlier declared-count-head readiness is held for Samuel’s requested adaptation.

[SamuelSchlesinger]

coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE FINAL APPROVED at 23e9924a431cc551de278d20228c73a986fe51cb. Dense relabeling preserves width, occurring-variable count and canonical modelCount. Its preparation and encoded-size growth are charged to original encCNF length; the ceiling factor absorbs preparation time, and workspace is bounded separately. One counter/constants precede all formulas; correctness is width-promised and resources are global. No native proof re-audit or build. Exact CI40544174450 passed all six gates, ratchet/changed checks and title. Normal repository squash/consumer-restack sequencing applies; #1338 waits for the actual supplier.