#SAT of unbounded clause width in time 2^O(N/√log N) for N literal occurrences, by tensor contraction #2061

Goal. One machine counts the satisfying assignments of every CNF formula, with no bound on clause width. Let N be the number of literal occurrences (φ.vars.length). The time is 2^(A(N+1)/√⌊log₂(N+2)⌋) times a polynomial in the encoding length, and the space is polynomial. When N ≤ D·n for n variables, this is 2^O_D(n/√log n), which is 2^o(n) for sparse formulas with long clauses.

Claimed by worker-claude-e6cf7b0d-wide-sat (Claude Code, Opus), branch claude/wide-clause-count. This is a follow-up to #2029 and is linked from #1538.

Why the fixed-width counter (#2029) doesn't apply directly. Its clause vertices have explicit tables of size 2^width. Its exponent A(m+1)/√⌊log₂(n+2)⌋ divides by the log of the variable count. So it fails for wide clauses, and also for many short clauses over few variables.

Route: no entry procedures needed.

1. Split. Apply §2.8's count-preserving OR-gate split (p. 18 of the pinned manuscript), which is already on main as toSharpThreeSAT = toExact3CNF renumbered:
   • every clause gets width ≤ 3;
   • modelCount is unchanged;
   • it runs in polynomial time;
   • N ≤ N' ≤ 7N.
2. Contract. Run feat(FineGrained): fixed-density #k-SAT counting by tensor contraction (Theorem 1.1, D.2) #2029's width-3 contraction counter. Its network has s = 3N' edges, so Theorem D.1 (p. 53) gives exponent K s/√⌊log₂ s⌋ = O(N/√log N). This is the occurrence-count form of the D.2 bound (p. 54), with no divisor in n.

Splitting into constant width keeps every table explicit and of bounded size. So E1's EntryAdmissible/EntryContractionAlgorithm (#2042, #2045, #2047, E1.3) is not needed for this theorem, and this lane does not depend on them. E1 is still needed for Lemma D.2. Splitting only the clauses wider than ⌈s^{9/10}⌉ and using entry procedures for the rest would give the same bound with more machinery.

Exact statements (namespace Cslib.Complexity.ContractionCounting; N := φ.vars.length):

/-- Fixed width, exponent in the occurrences. `exists_modelCounter k` becomes a corollary
(`N ≤ k m`, `n ≤ N`); its statement is unchanged. -/
theorem exists_modelCounter_occurrences (k : ℕ) :
    ∃ (count : CNF ℕ → ℕ) (A e b : ℕ),
      (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) → count φ = φ.modelCount) ∧
      ComputableInO count encCNF encNat
        (fun φ => 2 ^ (A * (φ.vars.length + 1) / Nat.sqrt (Nat.log 2 (φ.vars.length + 2))) *
          ((encCNF φ).length + 1) ^ e)
        (fun φ => ((encCNF φ).length + 1) ^ b)

/-- Every formula, any clause width. -/
theorem exists_modelCounter_unboundedWidth :
    ∃ (count : CNF ℕ → ℕ) (A e b : ℕ),
      (∀ φ : CNF ℕ, count φ = φ.modelCount) ∧
      ComputableInO count encCNF encNat
        (fun φ => 2 ^ (A * (φ.vars.length + 1) / Nat.sqrt (Nat.log 2 (φ.vars.length + 2))) *
          ((encCNF φ).length + 1) ^ e)
        (fun φ => ((encCNF φ).length + 1) ^ b)

/-- Linearly many occurrences: machine, `T`, `S`, `e`, `b` fixed before `D`; only `A` depends on `D`. -/
theorem exists_modelCounter_unboundedWidth_linearLength :
    ∃ (count : CNF ℕ → ℕ) (T S : CNF ℕ → ℕ) (e b : ℕ),
      (∀ φ : CNF ℕ, count φ = φ.modelCount) ∧
      ComputableInO count encCNF encNat T S ∧
      (∀ φ, S φ = ((encCNF φ).length + 1) ^ b) ∧
      ∀ D : ℕ, ∃ A : ℕ, ∀ φ : CNF ℕ, φ.vars.length ≤ D * φ.numVars →
        T φ ≤ 2 ^ (A * (φ.numVars + 1) / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) *
          ((encCNF φ).length + 1) ^ e

Existential-constant check. A, e and b in the first two are absolute (in the first, they depend on k only). The √⌊log₂⌋ divisor is explicit, so no constant can absorb it. The +1/+2 shifts avoid Lean's division by zero for N ≤ 1.

Source relation. The paper states Theorem 1.1 for fixed k in terms of n and m. The occurrence-count bound for unbounded width combines §2.8's split with D.2. That combination is a library extension, labelled as such; it is not a claim of the paper. Locators are checked against the pinned PDF (openai/math@7ef5c0cc).

Plan. One PR of about 4 files:

• FineGrained/ContractionCounting.lean: add the occurrence form and re-derive exists_modelCounter.
• New FineGrained/WideClauseCounting.lean.
• Tests: concrete wide formulas, counts by decide, plus a nonvacuity check of the linear-length hypothesis.

Completion. The three theorems are on main, with no sorry. The arbitrary-density bound (Theorem 1.1's first claim, #1538) is not part of this.