feat(FineGrained): restrict counting correctness to normalized bounded leaves

Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean

@@ -85,6 +85,13 @@ parameter uniformity and the native subexponential counting endpoint remain sepa
 * `Cslib.Complexity.CountingSparsify.search_eq_modelCount`,
   `Cslib.Complexity.CountingSparsify.search_eq_ite_modelCount`: the search computes `φ.modelCount`
   on formulas of width `≤ k` (and `0` otherwise).
+* `Cslib.Complexity.CountingSparsify.search_eq_ite_modelCount_of_normalized`: correctness only
+  requires the leaf counter to be exact on normalized sparse formulas within the search's
+  support and clause-count bounds.
+* `Cslib.Complexity.CountingSparsify.searchDeclaredWith_eq_ite_modelCountOn_of_normalized`:
+  the same invariant-restricted correctness contract for declared-variable counting, with either
+  occurring-variable or declared-variable leaf counts. These are semantic extensions; native
+  totality and resource certificates remain separate requirements.
 * `Cslib.Complexity.CountingSparsify.exists_computableInO_search`: native `ComputableInO ... T T`
   time-and-space transfer certificate for `CountingSparsify.search`.
 * `Cslib.Complexity.CountingSparsify.exists_computableInO_search_polySpace`: the same time envelope
@@ -420,15 +427,16 @@ theorem iterate_step (hM2 : 2 ≤ M) {k B L_coeff : ℕ} (hkK : k ≤ K)
       rfl
 
 include hM hK in
-/-- **The search computes the model count (occurring-variable support promise).** If `g` computes
-`ψ.modelCount` on sparse formulas `ψ` of width at most `k` whose occurring variables lie in
-`φ.vars.toFinset`, then `search M K k B g φ` returns `φ.modelCount` on formulas of width at most `k`
-and `0` otherwise. -/
-theorem search_eq_ite_modelCount_of_subset (hM2 : 2 ≤ M) {k B L_coeff : ℕ} (hkK : k ≤ K)
+/-- **Correctness from the invariants of sparse leaves.** The counter need only be exact on
+normalized sparse formulas of width at most `k`, supported on the input's variables, with at most
+`occBound K M * φ.numVars + 1` clauses. Its values outside this domain do not affect the result.
+The additive `1` includes the normalized contradiction `[[]]` when the input has no variables. -/
+theorem search_eq_ite_modelCount_of_normalized (hM2 : 2 ≤ M) {k B L_coeff : ℕ} (hkK : k ≤ K)
     (hTB : CountingTreeBound M K B L_coeff hM hK) {g : CNF ℕ → ℕ} {φ : CNF ℕ}
-    (hg : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ k) →
+    (hg : ∀ ψ : CNF ℕ, CountingNormalized K ψ → (∀ c ∈ ψ, c.length ≤ k) →
       isSparse (countingThreshold M) K ψ = true →
-      ψ.vars.toFinset ⊆ φ.vars.toFinset → g ψ = ψ.modelCount) :
+      ψ.vars.toFinset ⊆ φ.vars.toFinset →
+      ψ.length ≤ occBound K M * φ.numVars + 1 → g ψ = ψ.modelCount) :
     search M K k B g φ =
       if (φ.all fun c => decide (c.length ≤ k)) then φ.modelCount else 0 := by
   classical
@@ -447,7 +455,10 @@ theorem search_eq_ite_modelCount_of_subset (hM2 : 2 ≤ M) {k B L_coeff : ℕ} (
       fun c hc => length_le_of_mem_walk hM hK hkK hw.isNodeWord hc
     have hsub : ψ.1.vars.toFinset ⊆ φ.vars.toFinset :=
       vars_walk_subset hM hK hkK w
-    rw [leafWeight, hg ψ.1 hwidth hsparse hsub, CNF.length_distinctVars, CNF.length_distinctVars]
+    have hlength : ψ.1.length ≤ occBound K M * φ.numVars + 1 :=
+      length_walk_le_of_isSparse hM hK hkK hsparse
+    rw [leafWeight, hg ψ.1 ψ.2 hwidth hsparse hsub hlength,
+      CNF.length_distinctVars, CNF.length_distinctVars]
     exact (CNF.modelCountOn_eq_mul_modelCount ψ.1 φ.vars.toFinset hsub).symm
   have hsum : ∑ w ∈ W, leafWeight φ.distinctVars.length (R.walk s₀ w).1 (g (R.walk s₀ w).1) =
       (root k φ).modelCountOn φ.vars.toFinset :=
@@ -462,6 +473,21 @@ theorem search_eq_ite_modelCount_of_subset (hM2 : 2 ≤ M) {k B L_coeff : ℕ} (
   · rw [CNF.modelCountOn_eq_zero_of_nil_mem (List.mem_singleton_self [])]
     exact Nat.min_eq_right (Nat.zero_le _)
 
+include hM hK in
+/-- **The search computes the model count (occurring-variable support promise).** If `g` computes
+`ψ.modelCount` on sparse formulas `ψ` of width at most `k` whose occurring variables lie in
+`φ.vars.toFinset`, then `search M K k B g φ` returns `φ.modelCount` on formulas of width at most `k`
+and `0` otherwise. -/
+theorem search_eq_ite_modelCount_of_subset (hM2 : 2 ≤ M) {k B L_coeff : ℕ} (hkK : k ≤ K)
+    (hTB : CountingTreeBound M K B L_coeff hM hK) {g : CNF ℕ → ℕ} {φ : CNF ℕ}
+    (hg : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ k) →
+      isSparse (countingThreshold M) K ψ = true →
+      ψ.vars.toFinset ⊆ φ.vars.toFinset → g ψ = ψ.modelCount) :
+    search M K k B g φ =
+      if (φ.all fun c => decide (c.length ≤ k)) then φ.modelCount else 0 :=
+  search_eq_ite_modelCount_of_normalized hM hK hM2 hkK hTB
+    fun ψ _ hw hsp hsub _ => hg ψ hw hsp hsub
+
 include hM hK in
 /-- **The search computes the model count.** If `g` computes `ψ.modelCount` on sparse formulas `ψ`
 of width at most `k`, then `search M K k B g φ` returns `φ.modelCount` on formulas of width at most
@@ -1255,32 +1281,68 @@ theorem searchDeclaredWith_eq_ite_mul (NOf MOf BOf : P → ℕ) (K k : ℕ) (g :
   rw [searchDeclaredWith, searchWith_eq_search, Nat.shiftLeft_eq, CNF.length_distinctVars,
     Nat.mul_comm]
 
-/-- **Correctness of `searchDeclaredWith` under `CountingTreeBound`.**
-If `g (p, ψ) = ψ.modelCount` on sparse formulas `ψ` of width `≤ k` whose occurring variables lie in
-`Finset.range (NOf p)`, then `searchDeclaredWith` returns `φ.modelCountOn (Finset.range (NOf p))`
-when `validDeclaredInput k (NOf p) φ = true` and `0` otherwise. -/
-theorem searchDeclaredWith_eq_ite_modelCountOn {NOf MOf BOf : P → ℕ} {K k L_coeff : ℕ}
+/-- **Declared-variable correctness from normalized bounded leaves.** The occurring-variable
+counter need only be exact on normalized sparse width-`≤ k` formulas supported on the declared
+range and having at most `occBound K (MOf p) * NOf p + 1` clauses. -/
+theorem searchDeclaredWith_eq_ite_modelCountOn_of_normalized
+    {NOf MOf BOf : P → ℕ} {K k L_coeff : ℕ}
     {p : P} (hM : 1 ≤ MOf p) (hK : 1 ≤ K) (hM2 : 2 ≤ MOf p) (hkK : k ≤ K)
     (hTB : CountingTreeBound (MOf p) K (BOf p) L_coeff hM hK)
     {g : P × CNF ℕ → ℕ}
-    (hg : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ k) →
+    (hg : ∀ ψ : CNF ℕ, CountingNormalized K ψ → (∀ c ∈ ψ, c.length ≤ k) →
       isSparse (countingThreshold (MOf p)) K ψ = true →
-      ψ.vars.toFinset ⊆ Finset.range (NOf p) → g (p, ψ) = ψ.modelCount)
+      ψ.vars.toFinset ⊆ Finset.range (NOf p) →
+      ψ.length ≤ occBound K (MOf p) * NOf p + 1 → g (p, ψ) = ψ.modelCount)
     (φ : CNF ℕ) :
     searchDeclaredWith NOf MOf BOf K k g p φ =
       if validDeclaredInput k (NOf p) φ then φ.modelCountOn (Finset.range (NOf p)) else 0 := by
   rw [searchDeclaredWith_eq_ite_mul]
   split_ifs with hvalid
   · obtain ⟨hw, hsub⟩ := validDeclaredInput_eq_true_iff.mp hvalid
+    have hn : φ.numVars ≤ NOf p := by
+      simpa only [CNF.numVars, Finset.card_range] using Finset.card_le_card hsub
     have hsearch : search (MOf p) K k (BOf p) (fun ψ => g (p, ψ)) φ = φ.modelCount := by
-      rw [search_eq_ite_modelCount_of_subset hM hK hM2 hkK hTB
-        (fun ψ hψw hsp hψsub => hg ψ hψw hsp (hψsub.trans hsub)),
+      rw [search_eq_ite_modelCount_of_normalized hM hK hM2 hkK hTB
+        (fun ψ hnorm hψw hsp hψsub hlen => hg ψ hnorm hψw hsp (hψsub.trans hsub)
+          (hlen.trans (Nat.add_le_add_right (Nat.mul_le_mul_left _ hn) 1))),
         ite_eq_left_iff.mpr fun h =>
           absurd (List.all_eq_true.mpr fun c hc => decide_eq_true (hw c hc)) h]
     rw [hsearch, CNF.modelCountOn_eq_mul_modelCount φ (Finset.range (NOf p)) hsub,
       Finset.card_range]
   · rfl
 
+/-- Declared-variable correctness on valid inputs, from the invariants of sparse leaves. -/
+theorem searchDeclaredWith_eq_modelCountOn_of_normalized
+    {NOf MOf BOf : P → ℕ} {K k L_coeff : ℕ}
+    {p : P} (hM : 1 ≤ MOf p) (hK : 1 ≤ K) (hM2 : 2 ≤ MOf p) (hkK : k ≤ K)
+    (hTB : CountingTreeBound (MOf p) K (BOf p) L_coeff hM hK)
+    {g : P × CNF ℕ → ℕ}
+    (hg : ∀ ψ : CNF ℕ, CountingNormalized K ψ → (∀ c ∈ ψ, c.length ≤ k) →
+      isSparse (countingThreshold (MOf p)) K ψ = true →
+      ψ.vars.toFinset ⊆ Finset.range (NOf p) →
+      ψ.length ≤ occBound K (MOf p) * NOf p + 1 → g (p, ψ) = ψ.modelCount)
+    {φ : CNF ℕ} (hw : ∀ c ∈ φ, c.length ≤ k) (hsub : φ.vars.toFinset ⊆ Finset.range (NOf p)) :
+    searchDeclaredWith NOf MOf BOf K k g p φ = φ.modelCountOn (Finset.range (NOf p)) := by
+  rw [searchDeclaredWith_eq_ite_modelCountOn_of_normalized hM hK hM2 hkK hTB hg φ,
+    ite_eq_left_iff.mpr fun h => absurd (validDeclaredInput_eq_true_iff.mpr ⟨hw, hsub⟩) h]
+
+/-- **Correctness of `searchDeclaredWith` under `CountingTreeBound`.**
+If `g (p, ψ) = ψ.modelCount` on sparse formulas `ψ` of width `≤ k` whose occurring variables lie in
+`Finset.range (NOf p)`, then `searchDeclaredWith` returns `φ.modelCountOn (Finset.range (NOf p))`
+when `validDeclaredInput k (NOf p) φ = true` and `0` otherwise. -/
+theorem searchDeclaredWith_eq_ite_modelCountOn {NOf MOf BOf : P → ℕ} {K k L_coeff : ℕ}
+    {p : P} (hM : 1 ≤ MOf p) (hK : 1 ≤ K) (hM2 : 2 ≤ MOf p) (hkK : k ≤ K)
+    (hTB : CountingTreeBound (MOf p) K (BOf p) L_coeff hM hK)
+    {g : P × CNF ℕ → ℕ}
+    (hg : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ k) →
+      isSparse (countingThreshold (MOf p)) K ψ = true →
+      ψ.vars.toFinset ⊆ Finset.range (NOf p) → g (p, ψ) = ψ.modelCount)
+    (φ : CNF ℕ) :
+    searchDeclaredWith NOf MOf BOf K k g p φ =
+      if validDeclaredInput k (NOf p) φ then φ.modelCountOn (Finset.range (NOf p)) else 0 :=
+  searchDeclaredWith_eq_ite_modelCountOn_of_normalized hM hK hM2 hkK hTB
+    (fun ψ _ hw hsp hsub _ => hg ψ hw hsp hsub) φ
+
 /-- **Correctness of `searchDeclaredWith` on valid inputs under `CountingTreeBound`.** -/
 theorem searchDeclaredWith_eq_modelCountOn {NOf MOf BOf : P → ℕ} {K k L_coeff : ℕ}
     {p : P} (hM : 1 ≤ MOf p) (hK : 1 ≤ K) (hM2 : 2 ≤ MOf p) (hkK : k ≤ K)
@@ -1294,6 +1356,45 @@ theorem searchDeclaredWith_eq_modelCountOn {NOf MOf BOf : P → ℕ} {K k L_coef
   rw [searchDeclaredWith_eq_ite_modelCountOn hM hK hM2 hkK hTB hg φ,
     ite_eq_left_iff.mpr fun h => absurd (validDeclaredInput_eq_true_iff.mpr ⟨hw, hsub⟩) h]
 
+/-- Normalize a declared-variable leaf counter that is exact only on normalized bounded leaves,
+then recover the original declared-variable count. The input guard returns zero on invalid inputs.
+-/
+theorem searchDeclaredWith_normalizeDeclaredLeaf_eq_ite_modelCountOn_of_normalized
+    {NOf MOf BOf : P → ℕ} {K k L_coeff : ℕ}
+    {p : P} (hM : 1 ≤ MOf p) (hK : 1 ≤ K) (hM2 : 2 ≤ MOf p) (hkK : k ≤ K)
+    (hTB : CountingTreeBound (MOf p) K (BOf p) L_coeff hM hK)
+    {h : P × CNF ℕ → ℕ}
+    (hh : ∀ ψ : CNF ℕ, CountingNormalized K ψ → (∀ c ∈ ψ, c.length ≤ k) →
+      isSparse (countingThreshold (MOf p)) K ψ = true →
+      ψ.vars.toFinset ⊆ Finset.range (NOf p) →
+      ψ.length ≤ occBound K (MOf p) * NOf p + 1 →
+      h (p, ψ) = ψ.modelCountOn (Finset.range (NOf p)))
+    (φ : CNF ℕ) :
+    searchDeclaredWith NOf MOf BOf K k (normalizeDeclaredLeaf NOf h) p φ =
+      if validDeclaredInput k (NOf p) φ then φ.modelCountOn (Finset.range (NOf p)) else 0 :=
+  searchDeclaredWith_eq_ite_modelCountOn_of_normalized hM hK hM2 hkK hTB
+    (fun ψ hnorm hw hsp hsub hlen =>
+      normalizeDeclaredLeaf_eq_modelCount hsub (hh ψ hnorm hw hsp hsub hlen)) φ
+
+/-- Declared-variable correctness on valid inputs after normalizing a counter whose correctness
+is restricted to normalized bounded sparse leaves. -/
+theorem searchDeclaredWith_normalizeDeclaredLeaf_eq_modelCountOn_of_normalized
+    {NOf MOf BOf : P → ℕ} {K k L_coeff : ℕ}
+    {p : P} (hM : 1 ≤ MOf p) (hK : 1 ≤ K) (hM2 : 2 ≤ MOf p) (hkK : k ≤ K)
+    (hTB : CountingTreeBound (MOf p) K (BOf p) L_coeff hM hK)
+    {h : P × CNF ℕ → ℕ}
+    (hh : ∀ ψ : CNF ℕ, CountingNormalized K ψ → (∀ c ∈ ψ, c.length ≤ k) →
+      isSparse (countingThreshold (MOf p)) K ψ = true →
+      ψ.vars.toFinset ⊆ Finset.range (NOf p) →
+      ψ.length ≤ occBound K (MOf p) * NOf p + 1 →
+      h (p, ψ) = ψ.modelCountOn (Finset.range (NOf p)))
+    {φ : CNF ℕ} (hw : ∀ c ∈ φ, c.length ≤ k) (hsub : φ.vars.toFinset ⊆ Finset.range (NOf p)) :
+    searchDeclaredWith NOf MOf BOf K k (normalizeDeclaredLeaf NOf h) p φ =
+      φ.modelCountOn (Finset.range (NOf p)) :=
+  searchDeclaredWith_eq_modelCountOn_of_normalized hM hK hM2 hkK hTB
+    (fun ψ hnorm hψw hsp hψsub hlen =>
+      normalizeDeclaredLeaf_eq_modelCount hψsub (hh ψ hnorm hψw hsp hψsub hlen)) hw hsub
+
 /-- **Correctness of `searchDeclaredWith` composed with `normalizeDeclaredLeaf`.**
 When a leaf provider `h : P × CNF ℕ → ℕ` returns the declared-range count
 `ψ.modelCountOn (Finset.range (NOf p))` on sparse width-`≤ k` leaves with

ComplexityTests/Computability/Complexity/FineGrained/CountingNormalizedLeaves.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.FineGrained.CountingTreeBound
+
+/-!
+# Counting providers promised only on normalized sparse leaves
+
+The provider below deliberately returns a wrong, bounded result on long lists of duplicate
+clauses. The normalized-leaf correctness theorem still proves the search correct: duplicate
+clauses are removed before the provider is called. The zero-variable empty-clause control also
+requires the additive `+ 1` in the leaf-length bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Complexity.CountingNormalizedLeavesTests
+
+open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification
+open Cslib.Logic.PL.ClauseSet.Sparsification Cslib.Complexity.CountingSparsify
+
+/-- A bounded declared-variable provider that is exact only below the promised leaf-length cap. -/
+def boundedDeclared (K M : ℕ) (x : ℕ × CNF ℕ) : ℕ :=
+  if x.2.length ≤ occBound K M * x.1 + 1 then
+    x.2.modelCountOn (Finset.range x.1)
+  else 2 ^ x.1
+
+/-- Even on inputs outside its correctness promise, the provider respects the output bound. -/
+theorem boundedDeclared_le (K M : ℕ) (x : ℕ × CNF ℕ) :
+    boundedDeclared K M x ≤ 2 ^ x.1 := by
+  unfold boundedDeclared
+  split_ifs
+  · unfold CNF.modelCountOn
+    refine (Finset.card_filter_le _ _).trans ?_
+    simp only [Finset.card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_coe,
+      Finset.card_range, le_rfl]
+  · exact le_rfl
+
+/-- Long duplicate lists are sparse but violate the provider's size promise. In particular,
+the unrestricted sparse-leaf correctness premise is false for this bounded provider. -/
+example :
+    isSparse (countingThreshold 2) 1 (List.replicate 4 [(0, true)] : CNF ℕ) = true ∧
+    boundedDeclared 1 2 (1, List.replicate 4 [(0, true)]) = 2 ∧
+    CNF.modelCountOn (List.replicate 4 [(0, true)]) (Finset.range 1) = 1 := by
+  decide
+
+private theorem treeBound : CountingTreeBound 2 1 1 0 (by decide) (by decide) :=
+  countingTreeBound_of_budget (by decide) (by decide) (by decide) (by decide) (by decide)
+
+private theorem search_boundedDeclared (N : ℕ) {φ : CNF ℕ}
+    (hw : ∀ c ∈ φ, c.length ≤ 1) (hsub : φ.vars.toFinset ⊆ Finset.range N) :
+    searchDeclaredWith id (fun _ => 2) (fun _ => 1) 1 1
+      (normalizeDeclaredLeaf id (boundedDeclared 1 2)) N φ = φ.modelCountOn (Finset.range N) := by
+  refine searchDeclaredWith_normalizeDeclaredLeaf_eq_modelCountOn_of_normalized
+    (by decide) (by decide) (by decide) le_rfl treeBound ?_ hw hsub
+  intro ψ _ _ _ _ hlen
+  exact ite_eq_left hlen
+
+/-- The theorem, rather than evaluation of the search, establishes correctness despite the
+provider's wrong answer on the input itself. Two unused declared variables contribute a factor 4.
+-/
+example :
+    searchDeclaredWith id (fun _ => 2) (fun _ => 1) 1 1
+      (normalizeDeclaredLeaf id (boundedDeclared 1 2)) 3 (List.replicate 8 [(0, true)]) = 4 := by
+  have h := search_boundedDeclared 3
+    (φ := List.replicate 8 [(0, true)]) (by decide) (by decide)
+  exact h.trans (by decide)
+
+example : boundedDeclared 1 2 (3, List.replicate 8 [(0, true)]) = 8 := by decide
+
+/-- A tautological clause disappears during normalization. The theorem preserves its variable's
+contribution together with the two declared variables that never occurred in the formula. -/
+example :
+    searchDeclaredWith id (fun _ => 64) (fun _ => 1) 2 2
+      (normalizeDeclaredLeaf id (boundedDeclared 2 64)) 3 [[(0, true), (0, false)]] = 8 := by
+  have h :
+      searchDeclaredWith id (fun _ => 64) (fun _ => 1) 2 2
+        (normalizeDeclaredLeaf id (boundedDeclared 2 64)) 3 [[(0, true), (0, false)]] =
+        CNF.modelCountOn [[(0, true), (0, false)]] (Finset.range 3) := by
+    refine searchDeclaredWith_normalizeDeclaredLeaf_eq_modelCountOn_of_normalized
+      (NOf := id) (MOf := fun _ : ℕ => 64) (BOf := fun _ : ℕ => 1)
+      (K := 2) (k := 2) (p := 3) (φ := [[(0, true), (0, false)]])
+      (h := boundedDeclared 2 64) (L_coeff := countingDepthCoeff 2 64)
+      (by decide) (by decide) (by decide) le_rfl
+      (countingTreeBound_of_budget (M := 64) (K := 2) (B := 1)
+        (by decide) (by decide) (by decide) (by decide) (by decide))
+      ?_ (by decide) (by decide)
+    intro ψ _ _ _ _ hlen
+    exact ite_eq_left hlen
+  exact h.trans (by decide)
+
+/-- With zero declared variables, the empty formula has one assignment, whereas the single
+empty clause is an admissible one-clause leaf and has none. -/
+example :
+    searchDeclaredWith id (fun _ => 2) (fun _ => 1) 1 1
+      (normalizeDeclaredLeaf id (boundedDeclared 1 2)) 0 [] = 1 ∧
+    searchDeclaredWith id (fun _ => 2) (fun _ => 1) 1 1
+      (normalizeDeclaredLeaf id (boundedDeclared 1 2)) 0 [[]] = 0 ∧
+    boundedDeclared 1 2 (0, [[]]) = 0 := by
+  decide
+
+/-- The declared-input guard still rejects variable labels outside the declared range. -/
+example :
+    searchDeclaredWith id (fun _ => 2) (fun _ => 1) 1 1
+      (normalizeDeclaredLeaf id (boundedDeclared 1 2)) 1 [[(1, true)]] = 0 := by
+  decide
+
+end Cslib.Complexity.CountingNormalizedLeavesTests