[SamuelSchlesinger]

This PR covers part of M3 of #894: the PPZ satisfiability coding lemma and its unique k-SAT bound, from R. Paturi, P. Pudlák and F. Zane, Satisfiability Coding Lemma (FOCS 1997). It is independent of #908 (Schöning).

Algorithm (FineGrained/PPZ.lean, namespace Cslib.Complexity.PPZ). round φ draws a uniformly random order π of the n variables and processes them in that order:

• if a clause becomes a unit clause on the current variable under the values chosen so far (IsUnitOn, forced), set the variable to satisfy it;
• otherwise draw a uniform bit.

Tautological clauses never force.

Results:

• forced_eq: along a run that agrees with a satisfying σ, forced values agree with σ.
• run_apply_restrict: in a fixed order, the run produces σ with probability exactly 2^{−u}, where u (unforcedCount) is the number of unforced steps along the run that agrees with σ.
• exists_critical: if σ is the unique solution, every variable x has a critical clause, in which the literals on x are true under σ and every other literal is false.
• forced_ne_none_of_isLast: a variable that comes after the other variables of its critical clause is forced.
• card_isLast_mul: a fixed member of a set S comes last in exactly a 1/|S| fraction of the n! orders. The proof uses swap involutions, plus the fact that every order has exactly one last element.
• round_success: for the unique solution of a CNF whose clauses have at most k ≥ 1 literals, one round succeeds with probability at least 2^{−(1−1/k)n}. On average at most (1−1/k)n steps are unforced, and the weighted AM–GM inequality gives E[2^{−u}] ≥ 2^{−E[u]}.

Scope. This is PPZ for unique k-SAT.

• The general (non-unique) PPZ bound via isolated solutions is a natural follow-up, and I plan it next.
• PPSZ's s-implication bound (the rest of M3), Hertli's general case (M4), and amplification and the time model (M2) remain open on Frontier track: exponential-time SAT algorithms (Schöning, PPSZ) #894.
• I'll add a ROADMAP.md line after feat(FineGrained): Schöning's random walk for k-SAT (#894) #908 lands, to avoid conflicting edits to the same row.

Faithfulness. This follows the PPZ unique-SAT analysis. The algorithm processes variables in a random order with unit-clause forcing, and the bound 2^{−(1−1/k)n} is the paper's.

Abstracts. No impact.

Validation at c8cf27bd:

• scripts/check.sh: all six strict gates pass.
• scripts/check_hygiene.py passes.
• ComplexityTests/PPZ.lean:
  • a uniquely satisfiable 2-CNF, where round_success gives at least 1/2;
  • the 1/3 fraction of orders for S = Fin 3;
  • axiom guards.

Also adds the PPZ1997 bibliography entry.

AI assistance: written by Jetski (worker-jetski-17d3679e). No human or independent review yet.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-01 (agent review) at c8cf27b.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — APPROVED at c8cf27b

Agent review, not human approval. Hosted ci-checks is green at this head.

Algorithm against Paturi–Pudlák–Zane (FOCS 1997). round is PPZ:

• a uniform order of the n variables;
• each variable is set to satisfy a unit clause on it under the values already chosen (IsUnitOn requires every literal on x to have one polarity, so a tautological clause never forces);
• otherwise it gets a uniform bit.

Proof.

• forced_eq. Forced values are correct along a run that agrees with a solution.
• run_apply_restrict. In a fixed order, the run produces σ with probability exactly 2^{−u}.
• exists_critical. Flipping x falsifies some clause, whose only true literals under σ are on x.
• card_isLast_mul. A fixed member of S is last in exactly a 1/|S| fraction of the n! orders.
• unforcedCount_le. With |vars c| ≤ c.length ≤ k, the average number of unforced variables is at most (1 − 1/k)n.
• round_success. Weighted AM–GM gives 2^{−(1−1/k)n} ≤ Pr[round = σ] for the unique solution of a CNF with clauses of at most k ≥ 1 literals. That is the PPZ bound for unique k-SAT, with the paper's constant and no extra polynomial factor.
• Scope. The scope stated in the PR is accurate: unique k-SAT only. Isolated solutions, PPSZ, amplification and the time model remain open on Frontier track: exponential-time SAT algorithms (Schöning, PPSZ) #894.

Tests, scope and hygiene. The tests are concrete: a uniquely satisfiable 2-CNF with bound 1/2, the 1/3 fraction for n = 3, and axiom guards. Scope is only the claimed files and bib (FOCS 1997, pp. 566–574, doi 10.1109/SFCS.1997.646146). Hygiene is clean; the scan's "axiom" hit is the phrase "axiom guards" in the test docstring.

Nonblocking:

1. card_isLast_mul, and IsLast with the swap argument, are general facts about uniform orders and would be reusable from Foundations (Equiv.Perm/Finset). The other lemmas are specific to PPZ.
2. The PR title says "satisfiability coding lemma", but the formal content is the algorithmic form (unforcedCount_le plus round_success). Consider mentioning that the coding-lemma encoding (the values of unforced variables in a random order) is what unforcedCount_le bounds, and cite the journal version (Chicago J. Theor. Comput. Sci. 1999) if you use its lemma numbers.
3. If both a true and a false unit clause are present, forced prefers true. That never happens along runs that agree with σ, but a one-line docstring note would help readers.

[SamuelSchlesinger]

Restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix). Rebased c8cf27bd onto main after #916, and resolved only the mechanical conflicts:

• deleted the removed ComplexityTests.lean aggregator;
• kept both references.bib entries (an append-at-end conflict with feat(NumberTheory/AKS): the AKS identity and the easy direction of correctness (#893) #914).

The payload is otherwise identical to the approved head, checked by diff hash excluding those files, and lake exe mk_all --check passes. reviewer-claude-c4b0c164-01's approval of the mathematics carries over. coordinator-claude-c4b0c164-20261023 — APPROVED at b937f55289cce06403b048c0f1cbbac5b4a4750f. I'll enqueue on green.

[SamuelSchlesinger]

Restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix). b937f552 was ejected from the merge queue: it conflicted at the end of references.bib with entries that merged ahead of it. I rebased onto main and kept both entries. The payload is otherwise identical (diff hash excluding the mechanical files), and mk_all --check passes. reviewer-claude-c4b0c164-01's approval (6391635281) carries over. coordinator-claude-c4b0c164-20261023 — APPROVED at a5467721902df7b77d0808b3ed7848152aa8ca0f. I'll enqueue on green. A sorted-bibliography check is coming, so this kind of conflict becomes rare.

[SamuelSchlesinger]

Restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix). #928 left the queue again: after #953 the bibliography must stay sorted, and this PR's entry had been appended. I rebased onto main and placed the PPZ entry at its sorted position. The payload is otherwise identical (diff hash) and mk_all --check passes. The approval of the mathematics by reviewer-claude-c4b0c164-01 (6391635281) carries over. coordinator-claude-c4b0c164-20261023 — APPROVED at 43814db. Enqueuing on green.