From bd448eb1260bf2dabdc9527f393dd3a17dd5968a Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Tue, 27 Oct 2026 05:25:52 +0000 Subject: [PATCH 1/2] feat(FineGrained): counting-sparsification step with a captured runtime context Add CountingSparsify.stepWith, which reads its thresholds from a runtime context and passes the context to the leaf counter, keeping the existing state, initialization and occurring-support weighting (convention of #1226 comment 6434391211: an externally declared count lives in the context and is handled by the outer wrapper). For counting thresholds of a base read from the context every iterate agrees with the existing step, so its correctness theorems apply pointwise. Certify one context step as a plain ComputableInO within a polynomial in the encoded context and state plus the leaf counter's separate time and space. Part of #1226. --- Complexity.lean | 1 + .../FineGrained/CountingSparsifyContext.lean | 275 ++++++++++++++++++ ComplexityTests/CountingSparsifyContext.lean | 67 +++++ 3 files changed, 343 insertions(+) create mode 100644 Complexity/Computability/Complexity/FineGrained/CountingSparsifyContext.lean create mode 100644 ComplexityTests/CountingSparsifyContext.lean diff --git a/Complexity.lean b/Complexity.lean index 494891200..c5739d9cf 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -766,6 +766,7 @@ public import Complexity.Computability.Complexity.FineGrained.CountingEndpoint public import Complexity.Computability.Complexity.FineGrained.CountingParameterBounds public import Complexity.Computability.Complexity.FineGrained.CountingScale public import Complexity.Computability.Complexity.FineGrained.CountingSparsification +public import Complexity.Computability.Complexity.FineGrained.CountingSparsifyContext public import Complexity.Computability.Complexity.FineGrained.CountingTreeBound public import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch public import Complexity.Computability.Complexity.FineGrained.Exponents diff --git a/Complexity/Computability/Complexity/FineGrained/CountingSparsifyContext.lean b/Complexity/Computability/Complexity/FineGrained/CountingSparsifyContext.lean new file mode 100644 index 000000000..6b49bce9b --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/CountingSparsifyContext.lean @@ -0,0 +1,275 @@ +/- +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.CountingSparsification +import Complexity.Computability.Complexity.Problems.SAT.PolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain + +/-! +# The counting-sparsification step with a captured runtime context + +The counting-sparsification search (`Cslib.Complexity.CountingSparsify.step`) fixes its threshold +base `M` and its leaf counter `g` before the input. A single machine for Proposition 6.4 +[OpenAI2026ETH] instead computes its parameters from the input: the threshold base from the +sparsification parameter, and the leaf counter's own parameters from the declared number of +variables (Section 6.4, printed pp. 43–44). This module carries a runtime context `c : C` beside +the search state: `Cslib.Complexity.CountingSparsify.stepWith θ K g` reads its thresholds `θ c` and +passes `c` to the leaf counter `g`, and never changes `c`. + +The search state, its initialization `init` and its weighting and cap are those of the existing +search: the state records the number of variables occurring in the input, and the leaf counter's +contract is the occurring-support count `ψ.modelCount`. An externally declared number of variables +`N` lives in the context; accounting for the `N - φ.numVars` unused declared variables, and +normalizing any declared-`N` leaf count before it reaches the weighting, are left to the outer +wrapper. + +For the thresholds `countingThreshold (Mof c)`, the context step is the existing step at base +`Mof c` with leaf counter `g (c, ·)`, at every iterate +(`Cslib.Complexity.CountingSparsify.iterate_stepWith_countingThreshold`), so the existing +correctness theorems apply pointwise. One step is computable within a polynomial in the encoded +context and state, plus the time and space of the leaf counter on a sparse head formula +(`Cslib.Complexity.CountingSparsify.exists_computableInO_stepWith`); the context is charged in +full, and the leaf counter's time and space are kept separate. + +This module provides the step interface only. The resource bound for a whole uniform search, the +outer wrapper for an externally declared count, and the assembly of Proposition 6.4 are separate. + +## Main definitions + +* `Cslib.Complexity.CountingSparsify.stepWith`: one step with a captured runtime context. + +## Main results + +* `Cslib.Complexity.CountingSparsify.iterate_stepWith_fst`: the context is never changed. +* `Cslib.Complexity.CountingSparsify.iterate_stepWith_countingThreshold`: agreement with the + fixed-parameter step at the context's own base. +* `Cslib.Complexity.CountingSparsify.exists_computableInO_stepWith`: the time and space of one + step. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Section 6.4, + Proposition 6.4 (pp. 43–44) and Appendix A (pp. 44–47). +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification Turing.MultiTapeTM + +namespace CountingSparsify + +variable {C : Type} + +/-- One step of the counting-sparsification search with a captured runtime context `c`: the +thresholds are `θ c`, the leaf counter receives `c` with the sparse head formula, and `c` is kept. +-/ +def stepWith (θ : C → ℕ → ℕ) (K : ℕ) (g : C × CNF ℕ → ℕ) (x : C × State) : C × State := + (x.1, if x.2.2.1.isEmpty then x.2 + else if isSparse (θ x.1) K (x.2.2.1.headD []) then + leafUpdate x.2 (g (x.1, x.2.2.1.headD [])) + else + (x.2.1, (countingNext (θ x.1) K (x.2.2.1.headD []) false :: + countingNext (θ x.1) K (x.2.2.1.headD []) true :: x.2.2.1.tail, x.2.2.2))) + +/-- A step keeps the context. -/ +@[simp] theorem stepWith_fst (θ : C → ℕ → ℕ) (K : ℕ) (g : C × CNF ℕ → ℕ) (x : C × State) : + (stepWith θ K g x).1 = x.1 := + rfl + +/-- The search keeps the context. -/ +theorem iterate_stepWith_fst (θ : C → ℕ → ℕ) (K : ℕ) (g : C × CNF ℕ → ℕ) (i : ℕ) + (x : C × State) : ((stepWith θ K g)^[i] x).1 = x.1 := by + induction i generalizing x with + | zero => rfl + | succ i ih => rw [Function.iterate_succ_apply, ih, stepWith_fst] + +/-- For the counting thresholds of a base read from the context, a context step is the existing +step at that base, with the leaf counter applied to the context. -/ +theorem stepWith_countingThreshold (Mof : C → ℕ) (K : ℕ) (g : C × CNF ℕ → ℕ) (c : C) + (s : State) : + stepWith (fun c => countingThreshold (Mof c)) K g (c, s) = + (c, step (Mof c) K (fun ψ => g (c, ψ)) s) := + rfl + +/-- **Agreement with the fixed-parameter search.** Every iterate of the context step, for the +counting thresholds of a base read from the context, is the iterate of the existing step at that +base. -/ +theorem iterate_stepWith_countingThreshold (Mof : C → ℕ) (K : ℕ) (g : C × CNF ℕ → ℕ) (c : C) + (i : ℕ) (s : State) : + (stepWith (fun c => countingThreshold (Mof c)) K g)^[i] (c, s) = + (c, (step (Mof c) K (fun ψ => g (c, ψ)))^[i] s) := by + induction i generalizing s with + | zero => rfl + | succ i ih => + rw [Function.iterate_succ_apply, stepWith_countingThreshold, ih, + ← Function.iterate_succ_apply] + +section PolyTime + +open ComputableTidilyInPolyTime + +/-- Search states with a context, encoded as framed tuples: the context, the weighting count in +unary, the stack of formulas, and the accumulator in binary. -/ +local notation "encX" encC => + encPair encC (encPair encUnary (encPair (encList encCNF) encNat)) + +variable {encC : C ↪ List Bool} {θ : C → ℕ → ℕ} + +/-- Popping a sparse leaf and adding its weighted count is polynomial-time, keeping the context. -/ +private theorem computableTidilyInPolyTime_leafUpdateWith : + ComputableTidilyInPolyTime (fun p : (C × State) × ℕ => (p.1.1, leafUpdate p.1.2 p.2)) + (encPair (encX encC) encNat) (encX encC) := by + have hvars := SAT.computableInPolyTime_distinctVars.tidy + have heq : (fun p : (C × State) × ℕ => (p.1.1, leafUpdate p.1.2 p.2)) = fun p => + (p.1.1, (p.1.2.1, (p.1.2.2.1.tail, + if decide (2 ^ p.1.2.1 ≤ p.1.2.2.2 + + 2 ^ (p.1.2.1 - (p.1.2.2.1.headD []).distinctVars.length) * p.2) then + 2 ^ p.1.2.1 + else + p.1.2.2.2 + 2 ^ (p.1.2.1 - (p.1.2.2.1.headD []).distinctVars.length) * p.2))) := by + funext p + simp [leafUpdate, leafWeight, min_def] + rw [heq] + unfold encCNF + fun_prop + +/-- Branching on the head formula is polynomial-time for runtime thresholds, keeping the context. +-/ +private theorem computableTidilyInPolyTime_innerWith + (hθ : ComputableInPolyTime (fun x : C × ℕ × ℕ => decide (θ x.1 x.2.1 ≤ x.2.2)) + (encPair encC (encPair encUnary encUnary)) encBool) (K : ℕ) : + ComputableTidilyInPolyTime (fun x : C × State => + (x.1, (x.2.1, (countingNext (θ x.1) K (x.2.2.1.headD []) false :: + countingNext (θ x.1) K (x.2.2.1.headD []) true :: x.2.2.1.tail, x.2.2.2)))) + (encX encC) (encX encC) := by + have h := (computableInPolyTime_countingNextWith encNat hθ K).tidy + have hH : ComputableTidilyInPolyTime (fun x : C × State => x.2.2.1.headD []) + (encX encC) encCNF := by + unfold encCNF + fun_prop + have hb (b : Bool) : ComputableTidilyInPolyTime + (fun x : C × State => countingNext (θ x.1) K (x.2.2.1.headD []) b) (encX encC) + (encList (encList (encPair encNat encBool))) := by + simpa only [Function.comp_def] using + h.comp ((fst encC _).prod (hH.prod (const (encMid := encBool) b))) + have h₀ := hb false + have h₁ := hb true + unfold encCNF + fun_prop + +private theorem exists_computableTidilyInO_stepWith + (hθ : ComputableInPolyTime (fun x : C × ℕ × ℕ => decide (θ x.1 x.2.1 ≤ x.2.2)) + (encPair encC (encPair encUnary encUnary)) encBool) (K : ℕ) + {g : C × CNF ℕ → ℕ} {t s : C × CNF ℕ → ℕ} + (hg : ComputableTidilyInO g (encPair encC encCNF) encNat t s) : + ∃ d, ComputableTidilyInO (stepWith θ K g) (encX encC) (encX encC) + (fun x => (((encX encC) x).length + 1) ^ d + + if x.2.2.1.isEmpty = false ∧ isSparse (θ x.1) K (x.2.2.1.headD []) = true then + t (x.1, x.2.2.1.headD []) + + (((encX encC) x).length + (encNat (g (x.1, x.2.2.1.headD []))).length + 1) ^ d + else 0) + (fun x => (((encX encC) x).length + 1) ^ d + + if x.2.2.1.isEmpty = false ∧ isSparse (θ x.1) K (x.2.2.1.headD []) = true then + s (x.1, x.2.2.1.headD []) + + (((encX encC) x).length + (encNat (g (x.1, x.2.2.1.headD []))).length + 1) ^ d + else 0) := by + have hH0 : ComputableTidilyInPolyTime (fun x : C × State => x.2.2.1.headD []) + (encX encC) encCNF := by + unfold encCNF + fun_prop + obtain ⟨dE, eE, hE⟩ := (show ComputableTidilyInPolyTime (fun x : C × State => x.2.2.1.isEmpty) + (encX encC) encBool by unfold encCNF; fun_prop).exists_degree + obtain ⟨dI, eI, hI⟩ := (id' (encIn := encX encC)).exists_degree + have hS0 : ComputableTidilyInPolyTime + (fun x : C × State => isSparse (θ x.1) K (x.2.2.1.headD [])) (encX encC) encBool := by + simpa only [Function.comp_def] using + (computableInPolyTime_isSparseWith encNat hθ K).tidy.comp ((fst encC _).prod hH0) + obtain ⟨dS, eS, hS⟩ := hS0.exists_degree + obtain ⟨dH, eH, hH⟩ := (show ComputableTidilyInPolyTime + (fun x : C × State => (x.1, x.2.2.1.headD [])) (encX encC) (encPair encC encCNF) from + (fst encC _).prod hH0).exists_degree + obtain ⟨dN, eN, hN⟩ := (computableTidilyInPolyTime_innerWith hθ K).exists_degree + obtain ⟨dU, eU, hU⟩ := (computableTidilyInPolyTime_leafUpdateWith (encC := encC)).exists_degree + set D := dE + dI + dS + dH + dN + dU + 1 + have hE' := (hE.mono (d' := D) (e' := eE) (by omega) le_rfl).inO + have hI' := (hI.mono (d' := D) (e' := eI) (by omega) le_rfl).inO + have hS' := (hS.mono (d' := D) (e' := eS) (by omega) le_rfl).inO + have hH' := (hH.mono (d' := D) (e' := eH) (by omega) le_rfl).inO + have hN' := (hN.mono (d' := D) (e' := eN) (by omega) le_rfl).inO + have hU' := (hU.mono (d' := D) (e' := eU) (by omega) le_rfl).inO + have hleaf := hU'.comp (hI'.prod (hg.comp hH')) + have h := hE'.ite hI' (hS'.ite hleaf hN') + have heq : stepWith θ K g = fun x => + if x.2.2.1.isEmpty then x + else if isSparse (θ x.1) K (x.2.2.1.headD []) then + (x.1, leafUpdate x.2 (g (x.1, x.2.2.1.headD []))) + else + (x.1, (x.2.1, (countingNext (θ x.1) K (x.2.2.1.headD []) false :: + countingNext (θ x.1) K (x.2.2.1.headD []) true :: x.2.2.1.tail, x.2.2.2))) := by + funext x + unfold stepWith + split_ifs <;> rfl + have hpair_le (x : C × State) (c : ℕ) : + ((encPair (encX encC) encNat (x, c)).length + 1) ^ D ≤ + 4 ^ D * (((encX encC) x).length + (encNat c).length + 1) ^ D := by + rw [← mul_pow] + refine Nat.pow_le_pow_left ?_ D + simp only [length_encPair] + omega + rw [heq] + refine ⟨D, h.mono (4 ^ D + 5) (fun x => ?_) (fun x => ?_)⟩ <;> + · simp only [Function.comp_apply] + have hp := hpair_le x (g (x.1, x.2.2.1.headD [])) + have h4D : 1 ≤ 4 ^ D := Nat.one_le_pow _ _ (by norm_num) + generalize 4 ^ D = F at hp h4D ⊢ + generalize (((encX encC) x).length + 1) ^ D = P + generalize t (x.1, x.2.2.1.headD []) = T + generalize s (x.1, x.2.2.1.headD []) = S + generalize (((encX encC) x).length + (encNat (g (x.1, x.2.2.1.headD []))).length + 1) ^ D = Q + at hp ⊢ + generalize ((encPair (encX encC) encNat (x, g (x.1, x.2.2.1.headD []))).length + 1) ^ D = R + at hp ⊢ + cases x.2.2.1.isEmpty <;> + cases isSparse (θ x.1) K (x.2.2.1.headD []) <;> + simp only [Bool.false_eq_true, ite_false, ite_true, and_true, and_false, + Bool.true_eq_false] <;> nlinarith + +/-- **The time and space of a context step**: a polynomial in the length of the encoded context +and state, plus the time (respectively space) of the leaf counter and a polynomial in the state and +counter output lengths when the head formula is sparse. -/ +theorem exists_computableInO_stepWith + (hθ : ComputableInPolyTime (fun x : C × ℕ × ℕ => decide (θ x.1 x.2.1 ≤ x.2.2)) + (encPair encC (encPair encUnary encUnary)) encBool) (K : ℕ) + {g : C × CNF ℕ → ℕ} {t s : C × CNF ℕ → ℕ} + (hg : ComputableInO g (encPair encC encCNF) encNat t s) : + ∃ d, ComputableInO (stepWith θ K g) (encX encC) (encX encC) + (fun x => (((encX encC) x).length + 1) ^ d + + if x.2.2.1.isEmpty = false ∧ isSparse (θ x.1) K (x.2.2.1.headD []) = true then + t (x.1, x.2.2.1.headD []) + + (((encX encC) x).length + (encNat (g (x.1, x.2.2.1.headD []))).length + 1) ^ d + else 0) + (fun x => (((encX encC) x).length + 1) ^ d + + if x.2.2.1.isEmpty = false ∧ isSparse (θ x.1) K (x.2.2.1.headD []) = true then + s (x.1, x.2.2.1.headD []) + + (((encX encC) x).length + (encNat (g (x.1, x.2.2.1.headD []))).length + 1) ^ d + else 0) := + let ⟨d, h⟩ := exists_computableTidilyInO_stepWith hθ K (ComputableInO.tidy hg) + ⟨d, ComputableInO.of_tidy h⟩ + +end PolyTime + +end CountingSparsify + +end Cslib.Complexity diff --git a/ComplexityTests/CountingSparsifyContext.lean b/ComplexityTests/CountingSparsifyContext.lean new file mode 100644 index 000000000..bdbf0ded2 --- /dev/null +++ b/ComplexityTests/CountingSparsifyContext.lean @@ -0,0 +1,67 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.FineGrained.CountingSparsifyContext + +/-! +# Tests for the counting-sparsification step with a captured runtime context +-/ + +namespace ComplexityTests.CountingSparsifyContext + +open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification Cslib.Complexity +open Cslib.Complexity.CountingSparsify Turing.MultiTapeTM + +/-- With the threshold base as the context, the context search is the existing search at that base, +so the existing correctness theorems apply to each input. -/ +example (K k B M : ℕ) (g : ℕ × CNF ℕ → ℕ) (φ : CNF ℕ) : + ((stepWith (fun c => countingThreshold c) K g)^[rounds B φ] (M, init k φ)).2.2.2 = + search M K k B (fun ψ => g (M, ψ)) φ := by + rw [iterate_stepWith_countingThreshold (Mof := fun c => c)] + rfl + +/-- The context is retained by the whole search. -/ +example (θ : ℕ → ℕ → ℕ) (K : ℕ) (g : ℕ × CNF ℕ → ℕ) (i : ℕ) (x : ℕ × State) : + ((stepWith θ K g)^[i] x).1 = x.1 := + iterate_stepWith_fst θ K g i x + +/-- The context can hold an externally declared count `N` without changing the search: here the +context `(M, N)` supplies the base `M`, and `N` is only retained, for the outer wrapper. -/ +example (K k B : ℕ) (g : (ℕ × ℕ) × CNF ℕ → ℕ) (M N : ℕ) (φ : CNF ℕ) : + (stepWith (fun c => countingThreshold c.1) K g)^[rounds B φ] ((M, N), init k φ) = + ((M, N), (step M K (fun ψ => g ((M, N), ψ)))^[rounds B φ] (init k φ)) := + iterate_stepWith_countingThreshold (fun c => c.1) K g (M, N) _ _ + +/-- On the empty formula the existing search counts one assignment, with any context. -/ +example (N : ℕ) : ((stepWith (fun _ : ℕ => countingThreshold 2) 2 (fun x => x.2.modelCount)) + (N, init 2 [])).2.2.2 = 1 := by + rw [stepWith_countingThreshold (Mof := fun _ => 2)] + change (step 2 2 (fun ψ => ψ.modelCount) (init 2 [])).2.2 = 1 + decide + +/-- One step for a runtime base `M` given in binary, with any leaf counter certificate. -/ +example {g : ℕ × CNF ℕ → ℕ} {t s : ℕ × CNF ℕ → ℕ} + (hg : ComputableInO g (encPair encNat encCNF) encNat t s) (K : ℕ) : + ∃ d, ComputableInO (stepWith (fun c => countingThreshold c) K g) + (encPair encNat (encPair encUnary (encPair (encList encCNF) encNat))) + (encPair encNat (encPair encUnary (encPair (encList encCNF) encNat))) + (fun x => ((encPair encNat (encPair encUnary (encPair (encList encCNF) encNat)) x).length + + 1) ^ d + + if x.2.2.1.isEmpty = false ∧ isSparse (countingThreshold x.1) K (x.2.2.1.headD []) = true + then t (x.1, x.2.2.1.headD []) + + ((encPair encNat (encPair encUnary (encPair (encList encCNF) encNat)) x).length + + (encNat (g (x.1, x.2.2.1.headD []))).length + 1) ^ d + else 0) + (fun x => ((encPair encNat (encPair encUnary (encPair (encList encCNF) encNat)) x).length + + 1) ^ d + + if x.2.2.1.isEmpty = false ∧ isSparse (countingThreshold x.1) K (x.2.2.1.headD []) = true + then s (x.1, x.2.2.1.headD []) + + ((encPair encNat (encPair encUnary (encPair (encList encCNF) encNat)) x).length + + (encNat (g (x.1, x.2.2.1.headD []))).length + 1) ^ d + else 0) := + exists_computableInO_stepWith computableInPolyTime_countingThreshold_le_binary K hg + +end ComplexityTests.CountingSparsifyContext From 047ee04653bc144c9586389c362013e6d9365a44 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Tue, 27 Oct 2026 07:37:38 +0000 Subject: [PATCH 2/2] refactor(FineGrained): share stepWith with the declared-count wrapper; concrete context tests Move the five context-step declarations into CountingSparsification.lean with the exact signatures, argument order and simp attributes of the reviewed wrapper 0f58c8a9 (#1321), as agreed in #1320, so the resource module and the wrapper consume one copy. Replace the two signature-mirror tests by concrete branch and leaf steps under a pair context. --- .../FineGrained/CountingSparsification.lean | 51 ++++++++++++++++ .../FineGrained/CountingSparsifyContext.lean | 59 ++----------------- ComplexityTests/CountingSparsifyContext.lean | 32 ++++++---- 3 files changed, 77 insertions(+), 65 deletions(-) diff --git a/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean b/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean index bc712e30a..86ffc1adb 100644 --- a/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean +++ b/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean @@ -83,6 +83,10 @@ bound includes `leafTime`, no separate polynomial leaf-workspace certificate is on formulas of width `≤ k` (and `0` otherwise). * `Cslib.Complexity.CountingSparsify.exists_computableInO_search`: native `ComputableInO ... T T` time-and-space transfer certificate for `CountingSparsify.search`. +* `Cslib.Complexity.CountingSparsify.stepWith`, + `Cslib.Complexity.CountingSparsify.iterate_stepWith_fst`, + `Cslib.Complexity.CountingSparsify.iterate_stepWith_countingThreshold`: the step with a captured + runtime context, which keeps the context and agrees with `step` at the context's base. ## References @@ -935,6 +939,53 @@ theorem exists_computableInO_search (hM2 : 2 ≤ M) {k B L_coeff : ℕ} (hkK : k exact mul_le_mul_of_nonneg_right (Nat.le_ceil C₀) (by positivity) linarith [h_prod, (Nat.cast_nonneg ⌈C₀⌉₊ : (0 : ℝ) ≤ ⌈C₀⌉₊)] +/-! ### Captured runtime context -/ + +section ContextWrapper + +variable {P : Type*} + +/-- One step of the depth-first search of the counting-sparsification tree carrying an unchanged +runtime context `p : P`, using threshold family `θ p` and context-aware leaf counter `g` +(returning the occurring-variable count `ψ.modelCount` on sparse leaves). -/ +def stepWith (θ : P → ℕ → ℕ) (K : ℕ) (g : P × CNF ℕ → ℕ) (ps : P × State) : P × State := + (ps.1, + if ps.2.2.1.isEmpty then ps.2 + else if isSparse (θ ps.1) K (ps.2.2.1.headD []) then + leafUpdate ps.2 (g (ps.1, ps.2.2.1.headD [])) + else + (ps.2.1, (countingNext (θ ps.1) K (ps.2.2.1.headD []) false :: + countingNext (θ ps.1) K (ps.2.2.1.headD []) true :: ps.2.2.1.tail, ps.2.2.2))) + +@[simp] +theorem stepWith_fst (θ : P → ℕ → ℕ) (K : ℕ) (g : P × CNF ℕ → ℕ) (ps : P × State) : + (stepWith θ K g ps).1 = ps.1 := rfl + +@[simp] +theorem iterate_stepWith_fst (θ : P → ℕ → ℕ) (K : ℕ) (g : P × CNF ℕ → ℕ) (r : ℕ) + (ps : P × State) : ((stepWith θ K g)^[r] ps).1 = ps.1 := by + induction r generalizing ps with + | zero => rfl + | succ r ih => rw [Function.iterate_succ_apply, ih, stepWith_fst] + +@[simp] +theorem stepWith_countingThreshold (MOf : P → ℕ) (K : ℕ) (g : P × CNF ℕ → ℕ) + (p : P) (s : State) : + stepWith (fun q => countingThreshold (MOf q)) K g (p, s) = + (p, step (MOf p) K (fun ψ => g (p, ψ)) s) := rfl + +@[simp] +theorem iterate_stepWith_countingThreshold (MOf : P → ℕ) (K : ℕ) (g : P × CNF ℕ → ℕ) + (r : ℕ) (p : P) (s : State) : + (stepWith (fun q => countingThreshold (MOf q)) K g)^[r] (p, s) = + (p, (step (MOf p) K (fun ψ => g (p, ψ)))^[r] s) := by + induction r generalizing s with + | zero => rfl + | succ r ih => rw [Function.iterate_succ_apply, stepWith_countingThreshold, ih, + Function.iterate_succ_apply] + +end ContextWrapper + end CountingSparsify end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/FineGrained/CountingSparsifyContext.lean b/Complexity/Computability/Complexity/FineGrained/CountingSparsifyContext.lean index 6b49bce9b..c5cf5e56e 100644 --- a/Complexity/Computability/Complexity/FineGrained/CountingSparsifyContext.lean +++ b/Complexity/Computability/Complexity/FineGrained/CountingSparsifyContext.lean @@ -33,26 +33,23 @@ contract is the occurring-support count `ψ.modelCount`. An externally declared normalizing any declared-`N` leaf count before it reaches the weighting, are left to the outer wrapper. -For the thresholds `countingThreshold (Mof c)`, the context step is the existing step at base -`Mof c` with leaf counter `g (c, ·)`, at every iterate +For the thresholds `countingThreshold (MOf c)`, the context step is the existing step at base +`MOf c` with leaf counter `g (c, ·)`, at every iterate (`Cslib.Complexity.CountingSparsify.iterate_stepWith_countingThreshold`), so the existing correctness theorems apply pointwise. One step is computable within a polynomial in the encoded context and state, plus the time and space of the leaf counter on a sparse head formula (`Cslib.Complexity.CountingSparsify.exists_computableInO_stepWith`); the context is charged in full, and the leaf counter's time and space are kept separate. -This module provides the step interface only. The resource bound for a whole uniform search, the +This module certifies one step only. The resource bound for a whole uniform search, the outer wrapper for an externally declared count, and the assembly of Proposition 6.4 are separate. -## Main definitions - -* `Cslib.Complexity.CountingSparsify.stepWith`: one step with a captured runtime context. +The context step `Cslib.Complexity.CountingSparsify.stepWith` and its agreement lemmas live with +the search in `Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean`; this +module certifies its resources. ## Main results -* `Cslib.Complexity.CountingSparsify.iterate_stepWith_fst`: the context is never changed. -* `Cslib.Complexity.CountingSparsify.iterate_stepWith_countingThreshold`: agreement with the - fixed-parameter step at the context's own base. * `Cslib.Complexity.CountingSparsify.exists_computableInO_stepWith`: the time and space of one step. @@ -72,50 +69,6 @@ namespace CountingSparsify variable {C : Type} -/-- One step of the counting-sparsification search with a captured runtime context `c`: the -thresholds are `θ c`, the leaf counter receives `c` with the sparse head formula, and `c` is kept. --/ -def stepWith (θ : C → ℕ → ℕ) (K : ℕ) (g : C × CNF ℕ → ℕ) (x : C × State) : C × State := - (x.1, if x.2.2.1.isEmpty then x.2 - else if isSparse (θ x.1) K (x.2.2.1.headD []) then - leafUpdate x.2 (g (x.1, x.2.2.1.headD [])) - else - (x.2.1, (countingNext (θ x.1) K (x.2.2.1.headD []) false :: - countingNext (θ x.1) K (x.2.2.1.headD []) true :: x.2.2.1.tail, x.2.2.2))) - -/-- A step keeps the context. -/ -@[simp] theorem stepWith_fst (θ : C → ℕ → ℕ) (K : ℕ) (g : C × CNF ℕ → ℕ) (x : C × State) : - (stepWith θ K g x).1 = x.1 := - rfl - -/-- The search keeps the context. -/ -theorem iterate_stepWith_fst (θ : C → ℕ → ℕ) (K : ℕ) (g : C × CNF ℕ → ℕ) (i : ℕ) - (x : C × State) : ((stepWith θ K g)^[i] x).1 = x.1 := by - induction i generalizing x with - | zero => rfl - | succ i ih => rw [Function.iterate_succ_apply, ih, stepWith_fst] - -/-- For the counting thresholds of a base read from the context, a context step is the existing -step at that base, with the leaf counter applied to the context. -/ -theorem stepWith_countingThreshold (Mof : C → ℕ) (K : ℕ) (g : C × CNF ℕ → ℕ) (c : C) - (s : State) : - stepWith (fun c => countingThreshold (Mof c)) K g (c, s) = - (c, step (Mof c) K (fun ψ => g (c, ψ)) s) := - rfl - -/-- **Agreement with the fixed-parameter search.** Every iterate of the context step, for the -counting thresholds of a base read from the context, is the iterate of the existing step at that -base. -/ -theorem iterate_stepWith_countingThreshold (Mof : C → ℕ) (K : ℕ) (g : C × CNF ℕ → ℕ) (c : C) - (i : ℕ) (s : State) : - (stepWith (fun c => countingThreshold (Mof c)) K g)^[i] (c, s) = - (c, (step (Mof c) K (fun ψ => g (c, ψ)))^[i] s) := by - induction i generalizing s with - | zero => rfl - | succ i ih => - rw [Function.iterate_succ_apply, stepWith_countingThreshold, ih, - ← Function.iterate_succ_apply] - section PolyTime open ComputableTidilyInPolyTime diff --git a/ComplexityTests/CountingSparsifyContext.lean b/ComplexityTests/CountingSparsifyContext.lean index bdbf0ded2..c763c0272 100644 --- a/ComplexityTests/CountingSparsifyContext.lean +++ b/ComplexityTests/CountingSparsifyContext.lean @@ -20,25 +20,33 @@ so the existing correctness theorems apply to each input. -/ example (K k B M : ℕ) (g : ℕ × CNF ℕ → ℕ) (φ : CNF ℕ) : ((stepWith (fun c => countingThreshold c) K g)^[rounds B φ] (M, init k φ)).2.2.2 = search M K k B (fun ψ => g (M, ψ)) φ := by - rw [iterate_stepWith_countingThreshold (Mof := fun c => c)] + rw [iterate_stepWith_countingThreshold (MOf := fun c => c)] rfl -/-- The context is retained by the whole search. -/ -example (θ : ℕ → ℕ → ℕ) (K : ℕ) (g : ℕ × CNF ℕ → ℕ) (i : ℕ) (x : ℕ × State) : - ((stepWith θ K g)^[i] x).1 = x.1 := - iterate_stepWith_fst θ K g i x +/-- Two clauses sharing the heart `x₁`, on three occurring variables, with five models. -/ +abbrev ψ : CNF ℕ := [[(1, true), (2, true)], [(1, true), (3, true)]] -/-- The context can hold an externally declared count `N` without changing the search: here the -context `(M, N)` supplies the base `M`, and `N` is only retained, for the outer wrapper. -/ -example (K k B : ℕ) (g : (ℕ × ℕ) × CNF ℕ → ℕ) (M N : ℕ) (φ : CNF ℕ) : - (stepWith (fun c => countingThreshold c.1) K g)^[rounds B φ] ((M, N), init k φ) = - ((M, N), (step M K (fun ψ => g ((M, N), ψ)))^[rounds B φ] (init k φ)) := - iterate_stepWith_countingThreshold (fun c => c.1) K g (M, N) _ _ +/-- With context `(1, 7)` the base is `1`, the heart `x₁` is heavy, and one step replaces the +formula on the stack by its two counting children, keeping the context and the accumulator. -/ +example : (stepWith (fun c : ℕ × ℕ => countingThreshold c.1) 2 (fun x => x.2.modelCount) + ((1, 7), init 2 ψ)).1 = (1, 7) ∧ + (stepWith (fun c : ℕ × ℕ => countingThreshold c.1) 2 (fun x => x.2.modelCount) + ((1, 7), init 2 ψ)).2.2.1.length = 2 ∧ + (stepWith (fun c : ℕ × ℕ => countingThreshold c.1) 2 (fun x => x.2.modelCount) + ((1, 7), init 2 ψ)).2.2.2 = 0 := by + decide + +/-- With context `(100, 7)` the formula is sparse, so one step pops it and adds its five models. -/ +example : (stepWith (fun c : ℕ × ℕ => countingThreshold c.1) 2 (fun x => x.2.modelCount) + ((100, 7), init 2 ψ)).2.2.1 = [] ∧ + (stepWith (fun c : ℕ × ℕ => countingThreshold c.1) 2 (fun x => x.2.modelCount) + ((100, 7), init 2 ψ)).2.2.2 = 5 := by + decide /-- On the empty formula the existing search counts one assignment, with any context. -/ example (N : ℕ) : ((stepWith (fun _ : ℕ => countingThreshold 2) 2 (fun x => x.2.modelCount)) (N, init 2 [])).2.2.2 = 1 := by - rw [stepWith_countingThreshold (Mof := fun _ => 2)] + rw [stepWith_countingThreshold (MOf := fun _ => 2)] change (step 2 2 (fun ψ => ψ.modelCount) (init 2 [])).2.2 = 1 decide