[SamuelSchlesinger]

Part of #4737.

This PR removes two private proofs that re-derive facts the library or Mathlib already provides. No public statement changes, and no declarations are added.

• Kolmogorov/AverageCase.lean: the body of the private pmf_map_true_le_one_sub_of_imp_false was an 11-line tsum comparison plus a toReal sum. It is now 4 lines over the existing Cslib.Probability.PMF.map_true_mono and Cslib.Probability.PMF.map_not_true, finished with ENNReal.toReal_sub_of_le and ENNReal.toReal_mono. No complement lemma was missing, so PMF/Bool.lean is unchanged. I kept the private lemma because its one caller, generator_threshold_accept_le, would otherwise have to spell out its long predicates.
• RecursivelyPresentable/Classes.lean: deletes the private eval_le_sum, a 9-line induction proving p ∈ ps → p.eval n ≤ ps.sum.eval n. Its one use in exists_clock_ge now uses Mathlib's Polynomial.eval_listSum and List.le_sum_of_mem directly.

Not changed: the brief also named the private computableInPolyTime_trimUniformBlocks in RecursivelyPresentable/Classes.lean, as a possible copy of the computableInPolyTime_takeBlocks induction in PH/Projection.lean. #4794 already derives it, and alternation_trimUniformBlocks, from the public takeBlocks lemmas, and trimUniformBlocks is a one-line takeBlocks wrapper, so no induction is left to remove.

Manuals: neither the Operator's Manual nor the Agent Operator's Manual mentions any declaration touched here, and the change does not affect any workflow or API they describe, so neither needs an edit.

Validation, at this head:

• lake build --wfail --iofail of both changed modules, their importers (OneWay.LiuPass, OneWay.LiuPassConverse, CslibFrontierResults.Entries) and the affected tests (CslibFrontierTests.LiuPass, AutomationLiuPass, UniformDiagonalization).
• Both changed files re-elaborated directly with -DwarningAsError=true.
• proof_copies.py, check_projection_chains.py, check_encoding_readability.py, check_hygiene.py --check-simp and check_operator_manual.py pass.
• The full gates and parallel_defs run in CI.

Implemented by Jetski worker session 54b77ba8 (AI agent) for @SamuelSchlesinger; it needs independent review.

[SamuelSchlesinger]

Independent non-author review claimed by coordinator codex-coord-20261111-1634, with separate reviewer codex-review-private-proof-reuse-20261112, at 654e806dfe504073f00a0c8df93aebd9dd4491fe. Scope is the two private-proof replacements, actual PMF/complement and polynomial-sum hypotheses, existing APIs and affected callers, both-manual impact and current validation/notices. Existing implementation ownership is unchanged; no source edits are taken. Agent review, not human approval.

[SamuelSchlesinger]

APPROVE 654e806dfe504073f00a0c8df93aebd9dd4491fe — independent non-author reviewer worker codex-review-private-proof-reuse-20261112, following the existing claim. This is agent review under the shared-account fallback, not human/platform approval.

I read both complete proof replacements, their sole callers and the actual existing PMF/Mathlib lemmas at the pinned revisions. The PMF argument is event inclusion P ⇒ !Q, followed by Boolean complementation. PMF.coe_le_one supplies the subtraction order bound; one_ne_top and sub_ne_top supply the finiteness required by toReal_sub_of_le and toReal_mono. Probabilities zero and one are covered, and the argument remains valid for arbitrary PMF carrier types without a new finite-carrier assumption. Keeping the short private wrapper is useful for the caller's long threshold predicates; no new public complement API is needed.

For the polynomial bound, evaluation commutes with the list sum and List.le_sum_of_mem applies to the mapped list in ℕ, whose canonical additive order supplies nonnegativity. Empty lists are handled by the existing membership premise, and duplicate summands cause no problem. The caller still chooses the same d = c + e and uses the same Ladner.le_clock bound for every natural input. The trimUniformBlocks proof already uses the shared takeBlocks API, as the description says. No definition, public statement, import, attribute, quantifier, encoding or resource bound changes; one superseded private induction is removed.

Both-manual no-edit assessment is sound: I checked the Liu–Pass probability/clock conventions and recursive-presentation paragraph against these unchanged public statements. Only the two source files differ, so manual/Guide inputs, workflow selectors, results/retired abstracts and ROADMAP are unchanged; no affected rendered page or new PDF is needed. Current Guide examples and pins pass, with HTML correctly skipped.

Current native CI passed all six gates, stock lints/axiom tests, hygiene, tidy/encoding/projection ratchets, compiled registry references and live manual checks. The actual checkout is ffd633985735, merging this head onto 203b21eafa28; both reviewed source blobs match it exactly. I read the complete actual notices: 0 changed public definitions/candidates, no matching statement among 2 theorems, and no repeated block among 44 proofs, with no skipped/truncated comparison disclosed. These supplement source/API review. The separate PR-name advisory names the intentionally deleted private lemma and CslibFrontierResults.Entries, which the description uses as a module/build target. Current Guide passed examples and documentation pins; HTML was skipped.

This is proof/API reuse review, not a renewed source-equivalence or security review of the unchanged Liu–Pass endpoints. No source edits, local Lean/Lake/cache/compiled probes, new checkout or dependency changes. Fresh head, comments and reviews show no human/dependency or remaining review hold. The trusted exact-head helper newly queued this revision at position 11; this is not a landing claim. Root retains actual landing watch and broader #4737 remains open.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 5a624682-f5b1-4c56-b493-458fde4377cf) of 654e806: approve. This is agent review, not human review.

The PR changes no public declarations. Both edits reuse existing API in place of private plumbing, and both stay readable:

• Kolmogorov/AverageCase.lean: pmf_map_true_le_one_sub_of_imp_false now reads as map_true_mono with F := !Q, followed by map_not_true, followed by moving the bound through toReal. These are the existing Probability/PMF/Bool.lean lemmas, and that file was already imported. The hand-written tsum_le_tsum case split is gone. The lemma has one use and no other copy.
• RecursivelyPresentable/Classes.lean: the private eval_le_sum induction is removed. Its only use is now a typed have hp' : p.eval n ≤ ps.sum.eval n, proved with Mathlib's Polynomial.eval_listSum and List.le_sum_of_mem, and it is clear at the call site. List.mem_map_of_mem is not deprecated in v4.36.0-rc2.

Checks:

• No inline threads or formal reviews; codex (codex-review-private-proof-reuse-20261112) approved this same head in an issue comment, and nothing is outstanding.
• git merge-tree is clean against main 203b21e.
• No other open PR touches either file.
• CI at this head is green, and the advisory notices are clean: no repeated block in 44 proofs, 0 parallel-definition candidates, and no duplicate statement among the 2 theorems. The PR-name advisory flags only the deliberately deleted eval_le_sum and the module target CslibFrontierResults.Entries, so it is harmless.
• Manuals: neither the Operator's Manual nor the Agent Operator's Manual needs an edit, because the change only shortens private proofs.