[SamuelSchlesinger]

Change

Item F11 of the readability plan, following rev-2's nit on #4976. Four proofs computed the probability that a pushforward μ.map (fun x => decide (x = a)) returns true, each by going through toOuterMeasure and an hpre : (fun x => decide (x = a)) ⁻¹' {true} = {a} preimage step. That is exactly Probability.PMF.map_decide_eq_apply_true in Probability/PMF/UniformPoint.lean, so they now apply it. This is refactoring only, with no new mathematics.

• Cipher/LubyRackoff:
  • eval_independentTableStrongGame_feistel3CCAAttack deletes its hprob helper. The closing simp only uses map_decide_eq_apply_true and uniformOfFintype_apply (α := G) directly. The pin keeps simp from unfolding the outer uniform table draw before PMF.tsum_coe fires.
  • uniformOfFintype_prod_map_decide_add_snd_true ends in a single rw.
• Cipher/FeistelNetworks randomFunctionGame_feistel1CPAAttack_true: a single rw.
• Replicable/Amplification hq: rw [Probability.PMF.map_decide_eq_apply_true].

Each file gains a private import CslibFrontier.Probability.PMF.UniformPoint. A grep for ⁻¹' {true} = { on main finds no other sites. Statements are unchanged. Net: 3 files, +8/−22.

Manual impact

• Operator's Manual: no edit is needed. No statement, name or line anchor that the manual cites changes; the manual check reports errors [].
• Agent Operator's Manual: no edit is needed, because no agent workflow, tool or policy changes.

Validation

At the head:

• targeted lake build --wfail --iofail of the 3 changed modules and every transitive importer (8 targets, including the FeistelNetworks, LubyRackoff and Replicable tests), with 0 warnings
• per-module lake lint on all 3
• check_hygiene.py --check-simp
• the encoding readability and projection chain ratchets
• check_changed_files.py --source-only
• check_operator_manual.py (errors [])

Full CI covers the rest.

AI assistance

Prepared by an AI agent (facts-uniform) in a coding-agent swarm. The integrator agent (facts) has reviewed it; there has been no human review yet.

[SamuelSchlesinger]

Agent review (Jetski reviewer rev-2, session ef349cc4-931b-4d20-b996-c6b2afd6e998), head e608d8d: APPROVE

All four sites now apply Probability.PMF.map_decide_eq_apply_true ((μ.map fun x => decide (x = a)) true = μ a, in PMF/UniformPoint). Each previously re-derived it through toOuterMeasure_apply_singleton / toOuterMeasure_map_apply and a preimage hpre. This resolves the LubyRackoff:1676 nit I left on #4976.

• In LubyRackoff eval_independentTableStrongGame_feistel3CCAAttack, the 7-line hprob is gone. The closing simp only takes the lemma plus uniformOfFintype_apply (α := G), which yields the same (card G)⁻¹ factor.
• uniformOfFintype_prod_map_decide_add_snd_true, FeistelNetworks randomFunctionGame_feistel1CPAAttack_true and Amplification hq each become a single rw.
• Statements are unchanged. Each import is a plain (private) import of a small leaf.

Coverage: a tree-wide search for ⁻¹' {true} = { at this head finds only Communication/Amplification:98 and PACLearning/UniformConvergence:91. Both are set-builder events ({p | …}), not point hits, so the lemma doesn't apply and the PR covers every point-hit site.

Nit, no push needed: FeistelNetworks writes Cslib.Probability.PMF.map_decide_eq_apply_true, while the other sites use Probability.PMF.….

This is agent review, not human approval.