[karnseth]

Part of #894 (M4 of the PPSZ track; design): PPSZ for every satisfiable k-CNF, k ≥ 3, for the same unmodified PPSZ.round with w-implication as #1453–#1500.

Headlines (FineGrained/PPSZ/General.lean, namespace Cslib.Complexity.PPSZ):

theorem round_success_ge_of_guess_le (hp : 1 - 1 / (2 * Real.log 2) ≤ p) (hsat : φ.Satisfiable)
    (herr : ∀ T σ x, φ.eval σ = true → Frozen φ (restrict σ T) x → guessProb φ w T σ x ≤ p) :
    (2 : ℝ) ^ (-(p * n)) ≤ ∑ σ ∈ univ.filter (fun σ => φ.eval σ = true), ((round φ w) fun x => some (σ x)).toReal
theorem round_success_of_satisfiable (hk : 3 ≤ k) (hsat : φ.Satisfiable) (hlen : ∀ c ∈ φ, c.length ≤ k)
    (hw : ∑ i ∈ range h, (k - 1) ^ i ≤ w) : (2 : ℝ) ^ (-((1 - qbar k h) * n)) ≤ ∑ σ ∈ …, …
theorem round_success_of_satisfiable_three (hw : 3 ≤ w) … : (2 : ℝ) ^ (-(39 / 70 * n : ℝ)) ≤ …
theorem round_success_limit (hk : 3 ≤ k) : ∀ ε > 0, ∃ w : ℕ, ∀ n (φ : CNF (Fin n)), φ.Satisfiable →
    (∀ c ∈ φ, c.length ≤ k) → (2 : ℝ) ^ (-((1 - mu k / ((k : ℝ) - 1) + ε) * n)) ≤ ∑ σ ∈ …, …

These match the unique-SAT exponents of #1466/#1500 for all satisfiable formulas. Hypotheses beyond k ≥ 3, satisfiability, clause width and the bound on w: none.

Sources and mapping ([Hertli2011] = arXiv:1103.2165v2; [SchederSteinberger2017] = CCC 2017, LIPIcs 79):

• round_success_ge_of_guess_le is SS17 Thm 6 (p. 9:5), attributed to Hertli.
  • Its herr is SS17 Def 2's error condition E_π[J_x] ≤ p (p. 9:4), restricted to frozen variables over all restrictions φ|σ_T.
  • Every satisfiable restriction has that form, and herr drops Def 2's liquid-variable part.
  • So the theorem is at least as strong as Thm 6 for restriction-closed classes, the setting of SS17 Def 8 / Lemma 15 and of Hertli.
• Proof route. It follows Hertli's cost-function induction (Thm 15, p. 7), adapted to the unmodified algorithm (original).
  • Hertli analyses a modified PPSZ that eagerly sets implied literals, and notes his approach does not work with the original algorithm (p. 4).
  • The adaptation keeps the exact first-step weights 2^{-(guessBit)} instead of his uniform recursion (Obs 9), and charges frozen guesses in the success step.
  • Before implementation, a separate non-author agent independently checked the adaptation on paper and found it sound.
• Ingredients:
  • Hertli's AssignSL R(τ) (Def 12, p. 6), with Obs 13 (p. 7) and Lemma 16 (p. 7, first statement; the induction proof is original).
  • Frozen variables and the guess probability guessProb, which equals SS17's E_π[J_x] for frozen x. This is the unmodified analogue of Hertli's p_guessed (Def 4).
  • Lemma 10 (monotonicity) and the unmodified analogue of Lemma 11 (card_compl_mul_guessProb, by marginalising permutations to Bernoulli placements).
  • The frozen guess bound guessProb ≤ 1 − qbar k h, via critical trees on the restricted formula rooted at x (IsCriticalTreeAt). The unmodified statement is SS17 Thm 4 (p. 9:4).
  • Threshold: qbar k h ≤ qbar 3 h ≤ 2 − 2 ln 2 ≤ 1/(2 ln 2). qbar is antitone in k; the idea is from Hertli p. 8 that S_k increases with k, and the finite form is original. k ≥ 3 is the condition used, which is sufficient but not necessary.
• Not formalized:
  • the uniform o(n) form with w = w(n);
  • Hertli's modified algorithm;
  • SS17's KL-divergence route and its improved 3-SAT bound;
  • repetition and running time.

Supporting changes:

• PPZ.lean gains the prefix-set API (prefixSet_succ, card_prefixSet, EqOnPrefix, prefixSet_swap, …), used by both PPZ and PPSZ.
• New Logics/Propositional/Resolution/Restrict.lean holds the CNF.restrictBy evaluation, width and preimage facts.
• IsSatExtension uses PartialAssignment.Agrees, and the unassigned variables are PartialAssignment.free (reuse).

PPSZ M4 (#894, branch feat/ppsz-894-hertli): PR notes

Signature changes in PPSZ/CriticalTree.lean (relative to feat/ppsz-894-general)

Four lemmas now take a critical clause tree rooted at x (IsCriticalTreeAt φ σ x h C) instead
of a full critical clause tree (IsCriticalTree φ σ h C), and the hypothesis on the root path
p ≠ [] becomes x ∈ p:

• card_children_le: (hC : IsCriticalTreeAt φ σ x h C) ... (hxp : x ∈ p) (was hC : IsCriticalTree φ σ h C, hp : p ≠ []).
• mem_of_mem_labels: (hC : IsCriticalTreeAt φ σ x h C) : ∀ {d p}, x ∈ p → ... (was
  IsCriticalTree, p ≠ []).
• card_labels_le: same change (IsCriticalTreeAt, x ∈ p).
• exists_mem_labels_eval_eq_false: same change (IsCriticalTreeAt, x ∈ p).

Callers with a full tree use IsCriticalTree.isCriticalTreeAt hC x. wImplied_of_cut keeps its
IsCriticalTree signature; the rooted form is IsCriticalTreeAt.wImplied_of_cut.

Review-fix renames and moves (M4 review)

• Deleted PPSZ.SatExt and PPSZ.satExt_iff_isSatExtension; Frozen is now stated with
  IsSatExtension (AssignSL.lean), whose agreement clause is now
  Cslib.BitString.PartialAssignment.Agrees τ σ.
• Deleted PPSZ.unassigned and PPSZ.mem_unassigned/PPSZ.unassigned_update; the unassigned
  variables are Cslib.BitString.PartialAssignment.free (mem_free, free_update). Renamed
  card_unassigned_update → card_free_update, card_unassigned_le_card_satLits →
  card_free_le_card_satLits, unassigned_induction → free_induction,
  assignProb_of_unassigned_eq_empty → assignProb_of_free_eq_empty.
• satExt_restrict → isSatExtension_restrict (Frozen.lean).
• satLit_iff_of_frozen moved from AssignSL.lean to Frozen.lean and restated with Frozen
  ((hσ : IsSatExtension φ τ σ) (hfr : Frozen φ τ y)).
• frozen_update → Frozen.update; exists_ne_of_not_frozen moved General.lean → Frozen.lean.
• implied_eq_none_iff moved General.lean → PPSZ/Basic.lean, now with hypotheses
  (hσ : φ.eval σ = true) (hτ : ∀ y b, τ y = some b → σ y = b) like implied_eq_some.
• instDecidableWImplied moved Frozen.lean → PPSZ/Defs.lean (global, after implied).
• Clause.eval_filter_of_extends, CNF.eval_restrictBy, CNF.length_le_of_mem_restrictBy,
  CNF.exists_preimage_restrictBy moved Frozen.lean → new module
  Complexity/Logics/Propositional/Resolution/Restrict.lean (beside restrictBy's module).
• Prefix facts moved General.lean → PPZ.lean (namespace PPZ): mem_prefixSet_iff →
  mem_prefixSet_iff_exists, prefixSet_zero, prefixSet_self, prefixSet_succ,
  card_prefixSet, PPSZ.Agrees → PPZ.EqOnPrefix (with its instance),
  prefixSet_eq_of_agrees → EqOnPrefix.prefixSet_eq, apply_notMem_prefixSet →
  EqOnPrefix.apply_notMem_prefixSet, agrees_swap_iff → eqOnPrefix_swap_iff,
  prefixSet_swap. New in PPZ: restrict_insert, apply_notMem_prefixSet_self;
  runWith_apply_restrict now uses them; unforcedCountWith_succ is public.
• guessCount is related to unforcedCount by the new public guessCount_add_unforcedCount;
  guessCount_zero, guessCount_self, guessCount_eq are private and derived from it.
• Private: card_mul_two_rpow_neg_le_sum, two_sub_two_mul_mul_le_mul_logb,
  restrict_compl_unassigned (now restrict_compl_free), the guessCount_* helpers above,
  Placement.sum_powerset_sum_eq_sum_sum_powerset_erase (no Mathlib equivalent found), and the
  new nonneg_of_one_sub_one_div_two_mul_log_two_le (the extracted hp0).
• one_sub_inv_two_mul_log_two_le_one_sub_qbar → one_sub_one_div_two_mul_log_two_le_one_sub_qbar.

Abstract impact. None. No abstracts/catalogue.json entry covers PPZ/PPSZ, and none is added here. A PPSZ headline abstract would be Samuel's decision (#894 decision 6).

Tests:

• PPSZGeneral: a 3-CNF with exactly two solutions (not uniquely satisfiable). It gets the 39/70 bound, the depth-1 k = 4 bound and the ε-form, plus a direct round_success_ge_of_guess_le with an explicit herr.
• PPSZFrozen:
  • a variable that becomes frozen only after a restriction;
  • the frozen guess bound attained exactly at 1/2;
  • Lemma 10.
• PPSZAssignSL: Hertli's p. 7 example (1/4, 3/8, 3/8), Obs 13 numerically, and a strict instance of Lemma 16.
• PPSZCriticalTree: an IsCriticalTreeAt where no IsCriticalTree exists.

Validation (local, this exact head on current main): scripts/check.sh (all six gates), check_hygiene.py --check-simp, check_changed_files.py --base origin/main. An independent read-only review (a non-author agent, which checked Hertli/SS17 locators, the herr–Def 2 mapping, duplicates and placement) found no blockers; its fixes are included.

Contributors / AI disclosure. worker-karn-claude-20261028, a Claude Code agent run by @karnseth, with implementation subagents in separate worktrees.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): FINAL at 019d685ed7b1a9e780e082f4ca6a79dc9835e33c

This is a full review of the single commit 019d685e on top of main at 07ffc17f. It touches 17 files with +2462/−65. The author is karnseth, so this verdict is not advisory. No blocking findings.

What is proved. Everything is in PPSZ/General.lean, for the unmodified PPSZ.round φ w. Each success probability is the total mass that one round puts on the satisfying assignments: ∑ σ ∈ univ.filter (φ.eval σ = true), (round φ w (some ∘ σ)).toReal.

• round_success_ge_of_guess_le.
  • Hypotheses: 1 - 1/(2 ln 2) ≤ p, φ.Satisfiable, and herr. herr says that for every T, every satisfying σ and every x frozen under restrict σ T, guessProb φ w T σ x ≤ p.
  • Conclusion: success probability ≥ 2^{-p n}.
• round_success_of_satisfiable: for 3 ≤ k, satisfiable φ, clause width ≤ k and ∑ i < h, (k-1)^i ≤ w, success probability ≥ 2^{-(1 - qbar k h) n}. It discharges herr with guessProb_le_of_frozen and the threshold with one_sub_one_div_two_mul_log_two_le_one_sub_qbar.
• round_success_of_satisfiable_three (3 ≤ w, width 3): the bound 2^{-(39/70) n}, through qbar_three_two = 31/70.
• round_success_limit: ∀ ε > 0, ∃ w, ∀ n φ, … with exponent 1 - μ_k/(k-1) + ε. w is uniform over n, and the o(n) form with w = w(n) is excluded, as stated.

None of these has hypotheses beyond the ones stated in the PR body. No uniqueness assumption is needed.

Definitions I checked.

• Frozen φ τ x := τ x = none ∧ all satisfying extensions agree on x (Hertli, Definition 5).
• IsSatExtension φ τ σ := Agrees τ σ ∧ φ.eval σ.
• guessProb φ w T σ x is the fraction of the n! permutations in which σ on T ∪ placedBefore π x does not w-imply x = σ x. That is SS17's E_π[J_x] for the restricted formula, as the docstring says.
• IsCriticalTreeAt φ σ x h C requires the labelling only on root paths that contain x. IsCriticalTree.isCriticalTreeAt is the one-line weakening.
• Mapping herr to SS17 Definition 2 restricted to frozen variables, and reading it as at least as strong as Theorem 6 for restriction-closed classes, is accurate.
• The citations are consistent:
  • Hertli: Definitions 5, 12 and 14, Observations 9 and 13, Lemmas 10, 11 and 16, Theorems 15 and 17, with pages.
  • SS17: Theorems 4 and 6, pp. 9:4–9:5.
  • Original steps are marked "(original)".
  • SchederSteinberger2017 is added to references.bib, and Hertli2011 was already there.

Instance checked. ComplexityTests/PPSZGeneral uses a 3-CNF on 3 variables whose two solutions are all-true and all-false, so it is not uniquely satisfiable.

• ψ_true and ψ_false hold by decide, and so does the explicit non-uniqueness example.
• No variable is frozen at the start, so totalCost = 3p.
• The 39/70 bound, the depth-one k = 4 bound (exponent 3/4), the ε-form, and herr with the trivial p = 1 all instantiate on it.
• PPSZCriticalTree exhibits an IsCriticalTreeAt where no IsCriticalTree exists. The Hertli p. 7 numbers (1/4, 3/8, 3/8) appear in PPSZAssignSL.

API changes against main. I extracted every public header in the 12 modified files at base and head.

• Exactly the four documented CriticalTree lemmas change signature: card_children_le, mem_of_mem_labels, card_labels_le and exists_mem_labels_eval_eq_false. Each now takes IsCriticalTreeAt … x and x ∈ p instead of IsCriticalTree and p ≠ []. That is a genuine generalization, and every caller in the repo is updated.
• No other public declaration changed or was removed.
• The "deleted/renamed" list in the PR body refers to the feature branch. None of those names (SatExt, unassigned, frozen_update, PPSZ.Agrees, …) occurs anywhere at the head.
• There is no @[fun_prop], sorry, native_decide, axiom or set_option in the added lines.

Nit. The PR body's "Review-fix renames and moves" section describes changes relative to feat/ppsz-894-general, not main. A reader comparing against main will not find most of those names there. A one-line note in the body would avoid that confusion.

Limits.

• I did not check the paper text beyond the locators that are internally consistent with the docstrings.
• I did not build locally.
• git merge-tree against current main merges cleanly.
• check-title passes. ci-checks was still in progress when I posted, so this verdict assumes it goes green.

[SamuelSchlesinger]

review-nw-codex-20261029 — API/model scope approved at 019d685ed7b1a9e780e082f4ca6a79dc9835e33c, conditional on CI (independent agent review, not human approval). Reusing the arriving exact-head full review.

The rooted-tree generalization and callers are consistent; full-tree forcing/cut-bound endpoints retain their signatures. Agreement/free-coordinate APIs and the shared CNF restriction module are reused coherently. Concrete tests distinguish rooted from full trees, freezing only after restriction, and multiple solutions. The aggregate exactly covers 2581 modules. No selected-abstract impact; #894 remains open with runtime, amplification and uniform o(n) gaps explicit.

One nonblocking reuse nit inline. I reviewed source/API preservation in independent Git storage; no local build. The cost/probability adaptation and pinned-paper verification are assigned separate reviews.

[SamuelSchlesinger]

Nit, nonblocking: the prefix-specific name and helper lemmas are useful, but this relation restates Set.EqOn π π₀ {j | (j : ℕ) < i}. Consider defining EqOnPrefix through Set.EqOn so it reuses the existing agreement relation; the current clients and meaning can remain the same.

[SamuelSchlesinger]

review_ot_sources — approve the source/model mapping at 019d685ed7b1a9e780e082f4ca6a79dc9835e33c (independent agent review, not human approval). This supplies the primary-paper check left outside the existing review.

I inspected Hertli's pinned v2, including Algorithms 1–2, the eager-implication warning, Definitions 12/14, Observations 9/13, Lemmas 10/11/16 and Theorems 15/17. His algorithm is modified; the PR correctly labels the weighted induction for the unmodified round as an original adaptation, rather than attributing that proof to him verbatim.

In the CCC paper, Algorithms 2–3 use the sequential round and the bounded-clause heuristic. Definition 2/Observation 1 (9:4), Theorem 6 (9:5), and Definition 8/Lemma 15 (9:6–9:7) support the stated mapping and exact threshold 1 − 1/(2 ln 2). For an already-frozen variable in a satisfiable restriction, J_x is precisely the guess indicator; uniform orders on all variables marginalize to uniform orders on the remaining variables. Thus Definition 2 on a restriction-closed class implies herr. The frozen-only hypothesis is an original strengthening, not an equivalence with the entire source error condition; the detailed docstring makes that distinction.

The finite-depth bound, 39/70 instance and ∀ ε > 0, ∃ w, ∀ n, φ conclusion are honestly scoped probability results. No runtime, amplification, uniform o(n), or improved CCC 3-SAT bound is claimed. Limits: source/statement review only, not a line-by-line audit of the new induction or a local build. Integration still requires the separate proof/API reviews and current-head CI.

[SamuelSchlesinger]

Agent review (review_remaining_math) at 019d685: approve the probability argument, conditional on required CI. This adds the original weighted-induction coverage to the outside exact-head review and primary-source audit.

The adaptation genuinely retains the unmodified PPSZ.round: succSum_eq keeps a factor 1/2 for every guessed step and 1 for every implied step; succSum_zero recovers the actual success mass with the n! normalization. For a frozen variable, the multiplied cost inequality follows from sP = w_x + Σw_y, Σ(u−u_y) = f−u, w_y ≥ P, and u_y ≤ u. This handles both f = 1 and an already-implied frozen variable (f = 0), without dropping its guessing cost. Liquid variables have two satisfying literals and contribute at most 2 + (s−2)p. Their count is s−m; the logarithmic inequality at p ≥ 1−1/(2 ln 2) and AM–GM then close the m! · 2^(−cost) induction. Every cost/critical-tree use of Frozen retains a satisfying-extension witness, so its vacuity on unsatisfiable restrictions introduces no loophole. No uniqueness assumption enters the result.

I inspected the nonunique three-variable example, the restriction that turns a liquid variable frozen, the exact frozen guess probability 1/2, and AssignSL’s nonuniform 1/4, 3/8, 3/8 example. An independent rational-arithmetic enumeration of all canonical CNFs on 0–2 variables with w = 0,1,2, across all satisfiable restrictions, also verified 1,548 first-step identities, 1,050 frozen cost inequalities (both implied and guessed cases), and 1,365 total cost inequalities. This is a small independent semantic check, not Lean validation.

The zero-variable case has one empty assignment and 0! = 1. The headline requires k ≥ 3; finite h,w obey the stated clause-count bound. The limit theorem chooses a fixed finite w for each ε > 0, uniformly in n and the formula. It establishes neither the uniform o(n) form with growing w(n) nor repetition/runtime bounds; those remain part of #894’s broader objective. No curated abstract changes. I did not build locally or repeat the unchanged placement/tree analysis; full CI is still running.