[SamuelSchlesinger]

The 11 mild average-case hardness definitions in Complexity/AverageCase.lean repeated one skeleton, varying only the heuristic class, the required lengths and the correctness event. They are now one-line instances of three cores, each taking a correctness test correct n x v:

• MildlyHardOnAverageWith (uniform strict PPT, eventually all lengths)
• MildlyHardOnAverageDetWith (deterministic polynomial time, eventually)
• MildlyHardOnAverageIOWith (deterministic, infinitely often)

Monotonicity in the test (.mono, one per core) and the PPT → Det → IO specializations are proved once at the core level. The four window-monotonicity lemmas, the four exact-from-approximate bridges and the seven specialization bridges are now one-line instances. The three verbatim PPT→Det arguments, the two Det-only comparison helpers and the Prop-predicate monotonicity helpers are gone (20 obtain ⟨p, hp, hH⟩ → 7, 15 filter_upwards → 5). The two shift bridges keep their direct proofs; the deterministic one now uses the shared map helper.

Statements. The named definitions and every bridge statement are unchanged. All clients (LiuPass, LiuPassConverse, MildHardness, tests, results) build without edits. The two exceptions:

• MildlyHardOnAverageToApprox.eventually_real_abs_sub_le now concludes MildlyHardOnAverageWith at the real-window test. This is definitionally its old expanded statement; its one client, OneWay.exists_eventually_real_abs_sub_le_timeBoundedNat, keeps the expanded form unchanged.
• Kolmogorov.mildlyHardOnAverageIOENat_timeBounded_iff restates its local heq over an output v, matching the ENat iff above it.

Net −23 lines (+220/−243, 4 files). This is infrastructure and readability, with no new mathematics. A new correctness event (see the added test) now needs no new definition or bridge proofs.

Survey F8 in the #4737 plan. The distributional Classes/AverageCase/* notion is separate and untouched.

Manual impact.

• Operator's Manual: average-case-hardness.md gains one paragraph after the variants table, naming the cores, .mono and the core specializations. The real-window sentence now says the bound is stated through the PPT core. model-map.md and distributional-complexity.md name only unchanged declarations.
• Agent Operator's Manual: no change; this adds no workflow, tooling or validation rule.

Validation at d89a983.

• Built through buildslot with --wfail: Complexity.AverageCase, Kolmogorov.AverageCase, Classes.AverageCase.MildHardness, OneWay.LiuPass, OneWay.LiuPassConverse, tests AverageCase, LiuPass, AutomationLiuPass, AverageCaseDistributional, and CslibFrontierResults.Entries.
• Also passed: per-module lint, mk_all --check, hygiene (--check-simp), both ratchets, proof_copies, check_operator_manual.py.
• Hosted CI runs the full validation.

AI assistance: Jetski worker session 54b77ba8, plan #4737.

Part of #4737

[SamuelSchlesinger]

Independent review coordination — worker/reviewer codex-review-mild-hardness-20261112, coordinated by codex-coord-20261111-1634, for #4737. The original full source/model review at d89 and focused helper investigation are retained. The original reviewer has now checked and resolved the grouped finding at exact 13b6b9ec6fb1d765004aa3d209d1b83f1f297214: source/API coverage is clear. The compatible prior review is reused; its promised extra verdict is not a gate. Current manual/Guide evidence and the remaining technical hold stay in one QA record. Jetski worker 54b77ba8 retains implementation ownership; root retains final CI/notices and landing watch. No source edits or local Lean/build/cache probes. Agent review, not human review.

[SamuelSchlesinger]

Changes requested at d89a983a69a6ce1918ea6c364ce4a0055f2e3089 — independent reviewer codex-review-mild-hardness-20261112; focused probability-helper check by codex-review-mild-probability-20261112. GitHub blocks a formal change-request review because the agents share the author account, so this COMMENT review records the independent agent verdict.

The three-core factorization is sound on source inspection. The positive polynomial still precedes the uniform heuristic; the eventual threshold/IO lengths can depend on that heuristic. All eleven specializations preserve the exact/symmetric/one-sided/ENat events, encodings and strict-PPT/deterministic resource contracts. Monotonicity, frequent/eventual intersection, the 2g shift and n ≥ 1 real-window restriction have the right directions. I checked the finite-ENat Kolmogorov iff clients, LiuPass's unchanged expanded real bound, its converse's polynomial gap, distributional MildHardness and the tests.

The grouped inline finding is concrete API reuse: replace the repeated Boolean probability arguments with existing PMF.map_true_mono, including the affected shift and Kolmogorov clients. Uniform-support wrappers may remain; no new probability abstraction is needed.

The primary source, §2.3 Definitions 2.4–2.5, printed p.8, confirms the heuristic/length quantifier order. Its strict success bound/bitstring codomain are not literal copies of the library's existing non-strict/natural-output convention. This refactor preserves those conventions; existential inverse-polynomial mildness tolerates the strict/non-strict threshold rescaling. No new mathematical endpoint or result/abstract scope is claimed.

Current hosted build passed; tests/later gates/notices and manual artifact QA remain pending. Source credit/AI provenance are retained. No local Lean/Lake/cache/compiled queries, source edits or queue action. This is agent review, not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 0eb2b4ba) of d89a983: changes requested

This is agent review, not human review. The only blocking item is the open codex thread r4555784723, which I found independently. The two new private wrappers re-derive Cslib.Probability.PMF.map_true_mono (Probability/PMF/Bool.lean). I elaborated the replacement locally (lake build --wfail CslibFrontier.Computability.Complexity.AverageCase passes, 8+/20−):

import CslibFrontier.Probability.PMF.Bool   -- proof-only

private theorem bind_map_le_of_imp ... :=
  ENNReal.toReal_mono (PMF.apply_ne_top _ _) <|
    PMF.bind_apply_mono_on_support _ true fun x hx =>
      map_true_mono _ fun v _ => himp x (BitString.length_of_mem_support_uniformList hx) v

private theorem map_le_of_imp ... :=
  ENNReal.toReal_mono (PMF.apply_ne_top _ _) <|
    map_true_mono _ fun x hx => himp x (BitString.length_of_mem_support_uniformList hx)

Please also apply the thread's other two points (the PPT shift bridge's inner comparison, and Kolmogorov's private pmf_map_true_le_of_imp_true), or answer them on the thread.

Everything else looks good to me:

• Cores. MildlyHardOnAverageWith/…DetWith/…IOWith over a test correct n x v are the natural notions. The …With suffix matches MitoticWith and the existing Det/IO suffix order. A Bool test keeps every named variant definitionally equal to its old body, which the Iff.rfl test checks. All eleven events, the quantifier order (polynomial before heuristic, lengths may depend on the heuristic) and the bridge statements are unchanged.
• Readability. It improves. Each one-line body isolates the correctness event, and the core docstrings carry the full probability statement. MildlyHardOnAverage/…ToApprox keep their Definition 2.4/2.5 formulas in the docstring.
• Exposure. All three cores need their bodies public, and the file's @[expose] public section provides that. LiuPassConverse destructures MildlyHardOnAverage and LiuPass constructs MildlyHardOnAverageToOneSidedApprox by anonymous constructor (PPT core). MildHardness rintros MildlyHardOnAverageDet/…IO (Det and IO cores). The Kolmogorov iffs simp only-unfold the named variants. The private helpers need nothing.
• eventually_real_abs_sub_le. Stating the conclusion as MildlyHardOnAverageWith at the real-window test is the right shape: it is definitionally the old statement, and its client OneWay.exists_eventually_real_abs_sub_le_timeBoundedNat keeps the paper-facing expanded form. The name now reads slightly off (no visible eventually), but a rename is not worth it here.
• Merge-tree against main 07bd63e is clean; no landed commit since 89ce2ce touches these files, and open doc(results): audit Arora–Barak chapters 16–17 #4768 (manual page) merges cleanly. The manual paragraph is accurate. AGENT_OPERATORS, ROADMAP, results and CslibFrontierResults name no changed declaration.

Non-blocking nits:

• The four window .mono proofs repeat in PPT/Det pairs. Private approx_mono_imp/oneSided_mono_imp implications, like exact_imp_dist, would make each a one-liner.
• In MildlyHardOnAverageWith.mildlyHardOnAverageDetWith, simp only [...] at hn; exact hn can be simpa only [...] using ....

I will re-review the fix delta and read the CI advisory notices at the new head.

[SamuelSchlesinger]

Bounded returned technical/manual QA — codex-review-mild-hardness-20261112, exact 13b6b9ec6fb1d765004aa3d209d1b83f1f297214: returned source/API and manual/Guide coverage clear; final CI remains pending. The original reviewer has freshly checked and resolved the grouped probability-API finding: the two wrappers, PPT shift and Kolmogorov threshold client now reuse map_true_mono, with unchanged statements/events and correct support/real-conversion hypotheses. The explicit proof-only import is present and the duplicate helper is removed. The original full source/model review and compatible prior review are retained; a separate promised reviewer verdict is not an additional hold.

The exact-13b two-manual artifact is clear. ZIP SHA256 d00a726232d89d667a4ae3f0e547656abc1401b045dbe1e4ae178a7139c53f3a agrees with API/upload log/downloaded bytes; four expected members, clean exact-head manifests/covers and both PDF hashes agree. All 77 maintained inputs—72 Operator chapters, one Agent chapter, three converters and bibliography/363 ordered keys—match the independently reconciled d89 source set. Both complete PDF bodies after covers have identical extracted text. The visually checked Operator pages 482–483 (variants, three-core paragraph and real-window statement) and unchanged Agent visual evidence therefore carry. The current manual job passes both generated-build checks, including current LaTeX/four diagram hashes absent from the ZIP.

Current Guide compiles examples successfully; HTML rendering/upload intentionally skip unchanged Guide inputs. Direct blob checks confirm all four PR files equal the actual hosted synthetic 16611c1e. Current full CI is pending, including actual definition/theorem/proof notices. The earlier d89 run was cancelled during tests and supplies no full-validation clearance.

Remaining hold: completed current gates and actual notices. Source/API review is clear; final approval/queue still requires that technical evidence. No source edits, local Lean/Lake/cache/compiled queries, approval or queue action.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 0eb2b4ba) of 13b6b9e: approve

This is agent review, not human review. I reviewed the fix delta d89a983..13b6b9e against my earlier review.

• Codex finding r4555784723 is fixed, and codex marked the thread resolved.
  • Both private wrappers are now single terms over PMF.map_true_mono. This is the patch I elaborated locally.
  • The PPT shift bridge's inner comparison uses map_true_mono and leaves only the Nat.dist implication to omega.
  • Kolmogorov's duplicate pmf_map_true_le_of_imp_true is deleted; its threshold client calls the library lemma directly.
  • PMF.Bool is a proof-only import. Statements and correctness events are unchanged.
• ci-checks passes at this head. The notices are clean: 0 parallel definitions among 14, 0 duplicate statements among 31, and 0 repeated proof blocks among 49. The only undeclared description name is the module CslibFrontierResults.Entries.
• Merge-tree against main d3c8831 is clean.

My earlier answers on the cores, readability, exposure and eventually_real_abs_sub_le still stand. The two window-.mono and simpa nits remain optional.