[SamuelSchlesinger]

Part of #4817.

Change

This PR deletes private or inline copies of facts that the library already has, and shares the two arguments that were proved twice. It is refactoring only, with no new mathematics, and no theorem statement changes.

Jetski session facts-game (helper of facts 0e8cfb07), branch readability/facts-f9.

• Game.bind_apply_le_add_bind_apply (Crypto/Game, candidate section): both halves now come from the existing Probability.PMF.bind_apply_le_add_on_support, in place of an inline tsum comparison. Crypto/Game gains a private import CslibFrontier.Probability.PMF.Bind, so its public interface is unchanged.
• ProbComp.interpret_unifFin (from refactor(Crypto): shared game/protocol facts (F3) #4865) replaces local interpret_query_eq_self steps at ten sites: UC/Machine closeProgram_sample, Oracle/Run run_sample, RandomFunctionHybrid, BMR16 (×2), BinaryToOneHotObliviousness, FreeXOR, Garbling/Privacy, Switch/Oblivious (×2), and hshift in the AssumptionNonvacuity test (now hneg.shift 1). SSP/Hybrid:376 and UC/Linking:166 stay as they are, because they interpret a generic OracleComp.query handler, not unifFin.
• OracleComp.IsQueryBounded.isCostBounded_mul (new leaf Languages/Probabilistic/QueryCount/Scale.lean): at most n calls, each satisfying a QueriesSatisfy predicate on which calls cost at most c, cost at most n * c. isCostBounded_mul_of_forall_le is the all-calls case. They replace two private copies of the same induction: isCostBounded_of_queriesSatisfy_mul in WordRAM/Randomized/Defs (Renfei Zhou) and isCostBounded_const_of_isQueryBounded in UC/Linking (Karn Seth). Representative caller: Machine.isQueryBounded_runFrom now passes h.isCostBounded_mul_of_forall_le fun _ => le_rfl instead of a local induction. The lemma lives in a leaf, not in QueryCount.lean, because QueryCount has 1247 transitive importers (perf(build): reduce cache invalidation from growing hub modules #569). Both clients import the leaf privately.
• ProbComp.eval_bind_pi_update (moved to Languages/Probabilistic/Vector, public): resampling one coordinate of pi programs from its own program leaves the law unchanged. It was private in SSP/Hybrid (Karn Seth) and now sits beside eval_pi_bind. It needs no finiteness assumption.
• UC/Commitment: the private pmf_bind_eq_pure helper is deleted. Its two uses call core bind_congr with Mathlib's PMF.bind_const. The private succProbability_pure_false stays local: it has one client, and adding it to Crypto/Game (586 transitive importers) would not pay for itself.

Authors of new files: QueryCount/Scale.lean names Samuel Schlesinger, the originator of #4817 and the person whose agents did the work. The two proofs it replaces are credited above.

Manual impact

• Operator's Manual: workflows/probabilistic-workflows.md gains one sentence in the query-budget paragraph, pointing to QueryCount/Scale.lean. No other passage names a changed declaration. The deleted helpers were private, and git grep finds none of the touched names in manual/ or guide/.
• Agent Operator's Manual: no change. No workflow, tooling or instruction is affected.

Validation

• A targeted lake build --wfail --iofail passes on 28 targets: every changed module, representative importers (UC/Execution, CramerShoup, CTRMode, OFBMode, MPC/Yao) and the related tests (UCCommitment, SSP, AssumptionNonvacuity, Garbling, GarblingBMR16, GarblingOneHot, GarblingSwitch, FreeXOR). Before the rebase onto main, a 22-target build also covered PRF/Finite.
• lake lint on all 15 changed library modules; check_hygiene.py --check-simp; mk_all --check; the operator-manual checker (errors []); both ratchets; the source-only changed-file lints (CLEAN).
• Duplicate-statement and parallel-definition notices need whole-library outputs, so CI covers them.
• Overlap: refactor(Crypto): typed block-mode CPA experiments and simulate reduction #4980 (queued) rewrites the RandomFunctionHybrid proof touched here and edits the next line in Switch/Oblivious. Once it lands, this PR merges main once and takes refactor(Crypto): typed block-mode CPA experiments and simulate reduction #4980's side in RandomFunctionHybrid. refactor(Circuit): share wire-order locality of labelling rounds in Circuit/Local #4998 and refactor(Crypto): word-level PRF/PRP/weak-PRF games on ProbOracleComp.run #5022 merge cleanly.

AI assistance

Prepared by an AI agent (Jetski). The facts integrator agent reviewed it; no human has reviewed it yet.

[SamuelSchlesinger]

Review (Jetski revc-2, session 7eb004ef-055e-4c26-8b2e-bee0bc58f5fc) at 4e12440: APPROVE. This is agent review, not human approval.

I read the full diff. Each shared fact now has one home, and the callers use it:

• QueryCount/Scale.lean is a small leaf. It replaces the private scaling copies in WordRAM/Randomized/Defs and UC/Linking without growing a hub.
• eval_bind_pi_update moves to Vector as public API, and interpret_unifFin replaces the open-coded unfoldings at its call sites.
• Game.bind_apply_le_add_bind_apply now derives from PMF.bind_apply_le_add_on_support instead of repeating the argument.
• UC/Commitment's pmf_bind_eq_pure becomes bind_congr plus PMF.bind_const.
• The AssumptionNonvacuity test now uses hneg.shift 1.

The new public names don't collide with existing declarations. I reviewed both manuals: the one manual sentence matches the code, and the Agent Operator's Manual needs no edit.

Validation at this head:

• lake build --wfail --iofail of all 16 changed modules and the test: 7470 jobs, no warnings.
• runLinter on Scale, Vector, Game, UC/Commitment, UC/Linking, WordRAM/Randomized/Defs and SSP/Hybrid.
• check_hygiene --check-simp on the changed files, the source expose/new-test checks, and the manual checker (errors []).
• 0 unresolved threads.

I'll queue this head once ci-checks and guide are green. If #4980 lands first, please merge main (taking #4980's side in RandomFunctionHybrid, as the body says) and I'll review the remerge delta.

[SamuelSchlesinger]

Coordinator pre-queue verification (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) on 4e12440fc9908ed38bce31347f3c380e9b824c87:

• Reviewed the 18-file diff alongside revc-2's approval (#issuecomment-6846644615): shared PMF, unifFin, and QueryCount/Scale.lean lemmas cleanly replace local duplicates across 11 client modules.
• CI advisories (ci-checks run 43381811562): 0 repeated proof blocks across 372 proofs, 0 parallel definitions, 0 duplicate theorem statements across 18 theorems; check_pr_names flags only the 3 intentionally deleted private helpers (isCostBounded_of_queriesSatisfy_mul, isCostBounded_const_of_isQueryBounded, pmf_bind_eq_pure).
• Visually inspected rendered cslib-frontier-operators-manual.pdf from build run 43381811505 (4e12440fc9908ed38bce31347f3c380e9b824c87) at PDF p. 62 (printed p. 54, Worked example 6.2 in manual/workflows/probabilistic-workflows.md): the QueryCount/Scale.lean call-to-cost budget sentence and hyperlink render cleanly with no layout or glyph defects.

Enqueueing 4e12440fc9908ed38bce31347f3c380e9b824c87. This is agent review, not human review.

[SamuelSchlesinger]

Merge-delta review (Jetski revc-2, session 7eb004ef-055e-4c26-8b2e-bee0bc58f5fc), 4e12440..ef9a964: APPROVE. Agent review, not human approval.

git show --remerge-diff ef9a9646f shows the conflicts are resolved correctly:

• RandomFunctionHybrid: takes main's side. refactor(Crypto): typed block-mode CPA experiments and simulate reduction #4980's run_* proof supersedes F9's edit there, and RFH drops out of the PR.
• Switch/Oblivious idealGame_reduction: keeps refactor(Crypto): typed block-mode CPA experiments and simulate reduction #4980's simp list, including ProbOracleComp.run, and replaces its local hself with ProbComp.interpret_unifFin. That is F9's intent, and no hself or interpret_query_eq_self is left in the file.
• probabilistic-workflows: the Scale sentence now follows "Neither bound by itself…", so "Neither" again refers to the two bounds.

Against main, the PR is now 17 files, +110/−101. It also merges cleanly with the current main ae78516.

Validation at ef9a964:

• lake build --wfail --iofail of the 15 changed modules and test plus RandomFunctionHybrid: 7478 jobs, no warnings.
• runLinter on Oblivious, whole-tree check_hygiene.py --check-simp, and the manual checker (errors []).

I'll add the p. 62 rendered record once manual run 43389621944 finishes, then queue this head when ci-checks and guide are green.