[SamuelSchlesinger]

Milestone M1 of #894: the random-walk analysis of Schöning's algorithm for k-SAT, following the M0 design in #894 (comment). The first commit covers k = 3. The second commit, made before any review began, generalizes the analysis to all k ≥ 3.

What is proved. FineGrained/Schoening.lean defines Schöning's local search and one trial:

• walk φ t σ: stop if σ satisfies φ; otherwise flip the variable of a uniformly chosen literal occurrence of the first unsatisfied clause.
• trial φ: a uniform start, then 3n steps.

The main results:

• trial_success_of_length_le: for k ≥ 3 and a satisfiable CNF on n variables whose clauses have at most k literals, one trial succeeds with probability at least ((k−1)/k)^{k−3} · (k/(2(k−1)))ⁿ / (3n + 1).
• trial_success: the k = 3 case, (3/4)ⁿ / (3n + 1).

Proof structure (each step is a named theorem):

1. hit_le_succeedProb: the walk dominates the biased walk hit k, which steps down with probability 1/k. The proof is by induction on the step budget and uses hit_succ_le (antitone in the distance). It needs only one literal of the chosen clause to move toward a fixed satisfying assignment, so no coupling argument is required.
2. choose_mul_le_hit: path counting.
3. pow_le_choose_mul: k^{ki} ≤ C(ki, i)·(k−1)^{ki−i}·(ki+1), the middle-weight bound for ((k−1)+1)^{ki}.
4. inv_le_hit: hit k (3d) d ≥ ((k−1)/k)^{k−3}·(k−1)^{−d}/(3d+1). Write d = (k−2)i + e with e < k − 2. The paths with i up-steps and i + d down-steps have length ki + e ≤ 3d.
5. sum_pow_hammingDist: averaging q^{dist} over a uniform start gives (1 + q)ⁿ.

Faithfulness and scope.

• Schöning (FOCS 1999) states the bound (k/(2(k−1)))ⁿ up to a polynomial factor. The factors ((k−1)/k)^{k−3} and 1/(3n+1) are explicit constants of this PR, not from the paper.
• The analysis allows any choice of unsatisfied clause (the code takes the first) and allows duplicate literals.
• Still open on Frontier track: exponential-time SAT algorithms (Schöning, PPSZ) #894: amplification over (2−2/k)ⁿ·poly(n) trials, a running-time statement in a fixed model (an M2 decision for Samuel), and PPSZ.

Abstracts. No impact. No selected abstract depends on this module. A headline is planned for M2.

Validation at e55fab79:

• scripts/check.sh: all six strict gates pass.
• scripts/check_hygiene.py passes.
• ComplexityTests/Schoening.lean covers:
  • a concrete satisfiable 3-CNF and a 4-CNF (k = 4) on which the bounds apply;
  • a satisfying start, which succeeds with probability 1;
  • an exact value of hit 3 3 1;
  • the middle-weight bound;
  • axiom guards.

Also adds the Schoening1999 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 e55fab7.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — APPROVED at e55fab7

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

Algorithm against Schöning (FOCS 1999). The algorithm matches Schöning's:

• a uniform start;
• then 3n steps, each flipping the variable of a uniformly chosen literal of an unsatisfied clause, and stopping as soon as the formula is satisfied.

Proof.

• Domination (hit_le_succeedProb). It needs only two facts. A literal flip changes the Hamming distance to σ⋆ by exactly one. At least one occurrence among the ≤ k literals of the chosen clause moves toward σ⋆, so the step moves toward σ⋆ with probability at least 1/k. Together with hit being antitone in the distance, this gives the domination; no coupling is needed.
• Recursion for hit. It is correct: from d + 1, a down-step goes to d with probability 1/k and an up-step to d + 2 with probability (k−1)/k. The test value hit 3 3 1 = 1/3 + (2/3)(1/9) is right.
• Bound. trial_success_of_length_le gives ((k−1)/k)^{k−3}·(k/(2(k−1)))ⁿ/(3n+1) for k ≥ 3, clause lengths ≤ k (duplicates allowed) and a satisfiable φ. That is Schöning's (k/(2(k−1)))ⁿ up to an explicit polynomial factor, as the docs say. The k = 3 case (3/4)ⁿ/(3n+1) follows.
• Time model. No running-time or amplification claim is made. The docs leave both open on Frontier track: exponential-time SAT algorithms (Schöning, PPSZ) #894.

Tests, scope and hygiene. The tests are concrete:

• a 3-CNF instance and a 4-CNF instance of the bound;
• a direct hit value;
• the binomial middle-term bound;
• axiom guards.

Scope is only the claimed files, ROADMAP and bib (FOCS 1999, pp. 410–414, doi 10.1109/SFFCS.1999.814612). Hygiene is clean.

Nonblocking:

1. Several lemmas are general combinatorics and would be reusable from Foundations rather than FineGrained/Schoening:
   • sum_pow_hammingDist (∑_σ q^{d(σ, τ)} = (1 + q)^n), next to Mathlib's hammingDist API;
   • hammingDist_flip;
   • pow_le_choose_mul, the middle binomial term.
2. The module doc's "about (2 − 2/k)^n independent trials find a satisfying assignment with high probability" describes M2, which is not proved yet. Mark it as the planned consequence, or cite where it will be proved.

[SamuelSchlesinger]

Restack (coordinator-claude-c4b0c164-20261023, validated coordinator fix). Rebased e55fab79 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 495d1d77b4a99adde008ccbdca0a803122dc5e35. I'll enqueue on green.