[SamuelSchlesinger]

Fixes four issues found by an external agent review shared by Samuel. The PR changes documentation and tests only: no library statement or definition changes.

1. LiuPass.lean time-bound note. The note credited the polynomial threshold ∃ p, ∀ t ≥ p to "polynomial-overhead universal simulation" (DescriptionMethod.exists_etimeBoundedComplexity_universalTM_le_ofMultiTapeTM). That theorem is clock-preserving: it uses the same t on both sides and adds only a description-length constant. The rewritten note says where the threshold actually comes from. exists_timeBounded_of_computableInPolyTime takes the generator's own ComputableInPolyTime running-time certificate, gets constants c', d', and sets p₀(n) = (c'+1)(n+1)^(d'+1). Theorem 5.2 then shifts this to p_G(m) = p₀(m + 2γ + 3) to cover the encoded truncation count. The note keeps the explicit statement that only the polynomial-threshold form is proved, and keeps the convention that K^t counts steps of the described machine. The module's label "M2a polynomial-overhead form" carried the same misattribution, so every remaining occurrence now reads "M2a polynomial-threshold form".
2. ROADMAP.md. The Liu–Pass converse (exists_oneWay_of_mildlyHardOnAverage_timeBoundedNat and the equivalences) landed in feat(Crypto/OneWay): prove Liu-Pass M2b converse and headline equivalences #1005, so this PR drops it from the open directions. In its place, the roadmap now lists the near-linear regime of Theorem 3.1 (c).
3. ComplexityTests/Crypto/HybridEncryption.lean. The existing leakingEncaps fixture stays as the length-boundary case: its leaked key has n + 1 bits, so a length mismatch alone detects it. The new fixture sameLengthLeakingEncaps n pk := pure (pk, pk) leaks a uniform n-bit key under toyKeyGen. The tests prove:
   • the real game accepts with probability 1 (eval_kemRealGame_sameLengthLeaking);
   • the ideal game accepts with probability 2⁻ⁿ (eval_kemIdealGame_sameLengthLeaking_true);
   • the advantage is exactly 1 - 2⁻ⁿ for every n (advantage_kem_sameLengthLeaking), with instances at n = 1 (1/2) and n = 2 (3/4);
   • the fixture is not IND-CPA secure (not_kemINDCPA_sameLengthLeaking);
   • the fixture has a PPT certificate (sameLengthLeakingEncaps_ppt).
4. ComplexityTests/GKRProtocol.lean. The module doc now gives the correct breakdown of 5/101: two sumcheck challenges of at most 2/101 each and one line challenge of at most 1/101. The output step adds nothing, because the output layer has width 0.

Source check (arXiv:2009.11514v1, checked against the PDF). Theorem 3.1 (c), §3, p. 9: "For all constants d > 0, ε > 0, and every polynomial t(n) ≥ (1 + ε)n, K^t is mildly hard-on-average to (d log n)-approximate." §5.1, p. 11: "We say that G has rate-1 efficiency if its running time on inputs of length n is bounded by n + O(n^ε) for some constant ε < 1." Theorem 5.2 (§5.2, p. 11) assumes a rate-1 efficient condEP-PRG, and Theorem 5.6 (§5.3, p. 17) builds one from OWFs by padding. The near-linear range therefore rests on the generator's rate-1 running time, not on rate-1 universal simulation. The old note's phrase "rate-1 universal simulation" was corrected to match, and the ROADMAP direction uses the same wording.

Review classification. Documentation- and test-only. The new declarations are test fixtures and test theorems in ComplexityTests; no library statement, definition, abstract or security claim changes.

Abstracts. No impact: no abstract or catalogue entry refers to the changed text.

Validation. Local: all six scripts/check.sh gates, check_hygiene.py, check_changed_files.py --base origin/main and lake exe mk_all --check pass. The touched modules were rebuilt after rebasing onto #1027. CI: ci-checks run 40202414571.

AI disclosure: written by worker-claude-docfix-c4b0c164 (Claude Code), delegated by coordinator-claude-c4b0c164-20261023.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-40 (agent review) at 122eb27.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-40 — APPROVED at 122eb27 (delegated-review exception, AGENTS.md; classification: documentation- and test-only)

Agent review, not human approval.

• Classification. Every changed line in LiuPass.lean sits inside a /-! … -/ or /-- … -/ block. The rename from "polynomial-overhead" to "polynomial-threshold" is doc-only, and no occurrence of the old label remains anywhere in the repo. GKRProtocol.lean changes only its module doc. The new declarations are test fixtures and test theorems in ComplexityTests.Crypto.HybridEncryption. No library statement, definition or abstract changes.
• LiuPass attribution, checked against the proof. The proof of CondEPPRG.exists_mildlyHardOnAverageToOneSidedApprox_timeBoundedNat_log_succ gets p₀ from exists_timeBounded_of_computableInPolyTime (computableInPolyTime_truncGen hG_poly). In that proof, p₀ = (c_tm+1)(X+1)^(d_tm+1) comes from polynomiallyBounded_iff_le applied to the certificate's time bound. The proof then sets pG = p₀.comp (X + C (2γ+3)), and hlen_enc bounds the encoded (count, seed) length by m + (2γ+3). truncGen takes the count in unary and drops that many trailing bits. exists_etimeBoundedComplexity_universalTM_le_ofMultiTapeTM uses the same t on both sides, with an additive constant only (a zero-time-overhead Simulation). The new note matches all of this.
• Source wording, checked against the arXiv:2009.11514v1 PDF. §1.2 p. 7: "a cond EP-PRG that can be computed in time n + O(n^α), where α < 1 — we refer to this as a rate-1 efficient PRG". §5.1 p. 11 defines rate-1 efficiency as running time n + O(n^ε) for some ε < 1. Theorem 5.2 (§5.2, p. 11) assumes a rate-1 efficient µ-condEP-PRG. Theorem 5.6 (§5.3, p. 17) builds one from OWFs by padding. The source's U has polynomial overhead, but U(Π, 1^t) runs M(w) for t steps (§2.2, p. 8), so the near-linear range does rest on the generator's running time. Every locator is correct.
• ROADMAP. The converse landed in feat(Crypto/OneWay): prove Liu-Pass M2b converse and headline equivalences #1005, so removing it closes that direction. The replacement is a single direction with no status notes, and it describes the remaining gap accurately.
• Tests. kemRealGame and kemIdealGame match Encryption/Hybrid.lean: the real challenge is (pk, (pk, pk)) and the ideal one is (pk, (kIdeal, pk)). So the real game accepts with probability 1 and the ideal game accepts with probability 2⁻ⁿ, and the advantage is exactly 1 − 2⁻ⁿ. Truncated subtraction is exact here because 2⁻ⁿ ≤ 1, and the advantage is 0 at n = 0, as it should be. The values 1/2 and 3/4 at n = 1, 2 are correct. not_kemINDCPA_sameLengthLeaking adds the negligible 2⁻ⁿ to get the constant 1, which is a sound and nonvacuous rejection.
• GKR. By protocol_sound, the error is (width depth + Σ 5·width i)/|F|. With width 0 = 1 and width 1 = 0, that is two degree-2 sumcheck rounds at 2/101 each, one line step at 1/101, and 0 for the output step. The new text gives this breakdown.
• CI and merge. Hosted ci-checks (run 40202414571) and check-title are green at the exact head. mergeStateStatus is CLEAN, and git merge-tree against current origin/main reports no conflicts.

Nonblocking nits:

1. LiuPass.lean module doc: "gives the generator's multi-tape machine enough steps to print each output from its seed" would be more exact as "the truncated generator's machine … from the encoded (count, seed) input". The preceding sentence already names the truncated generator, so this is optional.
2. uniformList_bind_decide_eq_apply_true is a general point-probability fact about BitString.uniformList, and the library has no equivalent yet. It could move to Probability/BitString.lean later. Keeping it test-local is fine.