[SamuelSchlesinger]

Two docstring corrections from post-merge source spot audits (agent audits by coordinator-jetski-cc188c00, recorded on #1582 and #1605). Both narrow a source claim to what the Lean statement actually proves. No declaration, statement or proof changes.

• SumsetCover.lean (feat(circuit): prove XOR convolution via reusable image sparsification #1582): exists_add_cover was described as "the characteristic-two case of [Ellenberg2017Sumsets, Theorem 1]". Theorem 1 covers every finite field F_q, so its characteristic-two case includes F_{2^k}ⁿ. The Lean statement is the case q = 2 (ι → Bool, with bound 3·#{S : #S ≤ n/3} = M(F₂ⁿ)). It now says "the case q = 2 (the field 𝔽₂)".
• PPSZ/Frozen.lean (feat(fine-grained): PPSZ for every satisfiable k-CNF, k >= 3 #1605): guessProb_le_of_frozen was described as the finite-depth form of [SchederSteinberger2017, Theorem 4], "w-implication of depth h has error at most 1 - qbar k h". SS17's error (Definition 2, p. 9:4) bounds E_π[J_x] for every variable, liquid ones included, while the Lean theorem assumes x is frozen. Both the module docstring and the theorem docstring now say it is the frozen-variable part of that theorem. This matches how the PR already describes herr against Definition 2.

Docs-only. check_hygiene.py passes on both files, and the added lines are ≤ 100 characters. No abstracts or rendering are affected (no-impact assessment). The ImageSparsification "original vs cited" question on #1582 is still awaiting its author and is not included.

AI disclosure: written by coordinator-jetski-cc188c00 (Jetski agent run by @SamuelSchlesinger), from source checks against arXiv:1612.01929v2 and LIPIcs CCC 2017 art. 9 made by its audit subagents.

[SamuelSchlesinger]

reviewer-jetski-cc188-docs2 (agent review, not human approval): CHANGES REQUESTED at d0483e9.

One wording problem: in SS17 (p. 9:4), Definition 2 bounds E_π[J_x] for every variable x of F, and J_x is set only when x is frozen in F|β; guesses made while x is liquid count toward I_x, not toward the error. So "Their error notion (Definition 2) also covers liquid variables" can be read as saying that liquid guesses count as error. Suggested wording: "Their error notion (Definition 2) quantifies over every variable, including those liquid in F that become frozen in F|β; this bound needs x frozen under restrict σ T." Also, the module docstring now has an orphaned short line ("algorithm fixes more"), so please rewrap that paragraph. Everything else checks out: the diff touches only docstrings, all lines are at most 100 characters, guessProb_le_of_frozen assumes Frozen φ (restrict σ T) x, and exists_add_cover is stated for Finset (ι → Bool) with the 3 * #{S | #S ≤ n/3} bound. That bound matches Ellenberg's Theorem 1 (arXiv:1612.01929, any finite field F_q) at q = 2. CI (Lean Action CI/ci-checks) is still pending.

[SamuelSchlesinger]

reviewer-jetski-cc188-docs2 (agent review, not human approval): APPROVE at b886645 (delegated-review exception, AGENTS.md; classification: documentation-only).

I reviewed the delta from d0483e9. Both earlier findings are fixed. The sentence now says that SS17 Definition 2 quantifies over every variable, including variables liquid in F that become frozen in F|β, and that this bound needs x frozen under restrict σ T. That matches the paper (p. 9:4) and guessProb_le_of_frozen's Frozen hypothesis. The paragraph is rewrapped with no orphan line, all lines are at most 100 characters, and the delta touches only one docstring paragraph. CI at this head is still pending (only the title check is listed so far), so merging should wait for the required checks.

[chris-ai1]

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

This is a full review of the two docs-only commits d0483e93 and b886645c on top of fd5580d2. They touch 2 files. No declaration, statement, proof or import changes. No blocking findings.

• PPSZ/Frozen.lean. The module docstring and the guessProb_le_of_frozen docstring now call the bound "the frozen-variable part" of SS17 Theorem 4. After b886645c, the module docstring also says that SS17's Definition 2 quantifies over every variable, including those liquid in F that become frozen in F|β, while this bound needs x frozen under restrict σ T. That is accurate: the theorem assumes Frozen φ (restrict σ T) x. It also matches what I checked on feat(fine-grained): PPSZ for every satisfiable k-CNF, k >= 3 #1605, where herr of round_success_ge_of_guess_le is Definition 2 restricted to frozen variables. The SS17 and Hertli locators are unchanged.
• SumsetCover.lean. "the characteristic-two case of [Ellenberg2017Sumsets, Theorem 1]" becomes "the case q = 2 (the field 𝔽₂)". That is the accurate narrowing. The statement is over ι → Bool, while Theorem 1 covers every 𝔽_q, including 𝔽_{2^k}.

Checks.

• Every added line is at most 99 characters.
• git merge-tree against current main merges cleanly.

Nit. b886645c rewrapped the paragraph and fixed the short line I would have flagged. F and F|β are the paper's notation and are not defined in the docstring. Writing "φ" and "φ.restrictBy β" would be clearer, but this is optional.

Limits.

• check-title passes. ci-checks was still in progress when I posted.
• I did not re-read the papers for this delta and rely on the locators checked earlier.