[SamuelSchlesinger]

The three- and four-round Feistel hybrid arguments repeat equalities that commute independent samples before applying the same advantage bound. A private averaging lemma combines the commutation with the existing averaging inequality, so each hybrid hop expresses its reduction directly. The triangle inequalities also use simpler real coercions.

Removes 128 net source lines; the main hybrid proof bodies shrink from 81/131 to 33/51 lines. Existing definitions, theorem statements, and security bounds are unchanged. Curated abstracts: no impact on statements, scope, or rendering. The LubyRackoff changes in #1099 at aab6991 merge cleanly with this patch; there is no dependency on that PR.

Validation: Hosted CI passes at the current revision. Independent agent review approves the proof refactor. This supersedes the earlier interrupted local full-suite run.

AI assistance: ChatGPT authored the refactor; a non-authoring delegated agent reviewed it. A separate publication review verified source identity and the independent split. These are agent reviews, not human or maintainer approval.

[SamuelSchlesinger]

coordinator-codex-queue-20261028-ready-c — approve at 78ae030b4d49ac1edeee98a1371e73ddde4151b6 (independent agent review, not human approval).

The private averaging helper commutes only independent samples and then applies the existing advantage bound. Its three- and four-round clients preserve the reduction hypotheses, games and additive losses. The triangle-inequality edits only simplify coercions; no public definition or theorem statement changes. No selected-abstract or scope impact. Exact-head hosted CI passes; it supplies the full validation that the draft description says was pending. I reviewed source and reused hosted validation without a local build.

[chris-ai1]

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

Full review. The PR has one commit on top of main. Classification: proof-only, plus one new private helper.

• Statements: no public signature or docstring changes in LubyRackoff.lean. The diff touches only the proofs of advantage_feistel3KeyedGame_feistel3RandomRoundsGame_le, advantage_feistel3KeyedGame_randomFunctionGame_le, advantage_feistel3KeyedGame_idealPermGame_le and advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le.
• Helper: private theorem advantage_bind_right_le swaps the outer sample p/q with an independent inner sample d (PMF.bind_comm) and then applies the existing Game.advantage_bind_le. The statement is correct. The keyed-hop clients chain it once for each remaining independent key and then discharge h₁… with a small simpa only that unfolds prfSingle*Game/interpret_*Reduction*. This is the same reasoning as the deleted hl/hr equalities, now visible in one place. The hops whose outer samples are random functions still use Game.advantage_bind_le directly, as they did before. The triangle steps replace the exact_mod_cast restatements with NNReal.coe_le_coe.mpr + simp only [NNReal.coe_add]. Same content, no hidden steps.
• nit: the helper says nothing specific to Feistel and is the commuted form of Game.advantage_bind_le. If another file needs the same commute-then-average step (many crypto files call PMF.bind_comm before averaging), it could move to Complexity/Crypto/Game.lean as public API. Keeping it private here is acceptable.
• Hygiene: non-terminal simps are simp only, and each terminal simpa only is a short unfolding. No heartbeat options.
• Description: net −128 lines matches the diffstat (+80/−208).
• CI: ci-checks and check-title pass at this head.

Limits: I did not build locally, and I did not check the claim that this PR merges cleanly with #1099.