[SamuelSchlesinger]

Part of #4817 (F2 of the facts table: uniform pushforwards).

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

This PR moves repeated uniform-distribution facts into the probability library and points the clients at them. It does not change any theorem statement. It is infrastructure and refactoring only, with no new mathematics.

New shared lemmas

• Probability/Uniform.lean:
  • uniformOfFintype_map_add_left/_right and uniformOfFintype_bind_add_left/_right: a fixed mask leaves a uniform group element uniform (the one-time pad). Clients used to rebuild this from uniformOfFintype_map_equiv (Equiv.addLeft _) and Equiv.coe_addLeft at every site.
  • uniformOfFintype_map_monoidHom: the multiplicative version of _map_addHom.
• Probability/PMF/Uniform.lean:
  • uniformOfFintype_prod_map_snd, the companion of _prod_map_fst.
  • uniformOfFintype_bind_bijective: change of variables in a uniform draw along a bijection α → β. The existing _bind_equiv is now its one-line corollary.
• Probability/StatisticalDistance/UniformMod.lean: uniformOfFintype_fin_bind, which says uniform Fin M and ZMod M draws agree (NeZero M).
• Probability/Product/Split.lean: uniformOfFintype_map_comp_dep, which reads a uniform dependent function through an injection. It needs only nonempty fibres, and its proof is one rewrite through pi_uniformOfFintype and pi_map_comp_injective.

Copies deleted, with what replaces them

• UnitSampling: private uniformOfFintype_fin_bind. ExactSecurity also had an inline hunif; it now uses the shared lemma.
• Paillier/Security: private uniformOfFintype_map_unitsMap → _map_monoidHom with ZMod.unitsMap_surjective.
• Garbling/BMR16: private uniformOfFintype_map_comp_of_injective (a 13-line cast/choose shift construction) → _map_comp_dep.
• Garbling/Rerandomizable: private bind_uniform_comp → uniformOfFintype_bind_bijective. Its four multi-sample reindex helpers stay private: they serve only the three explainability proofs there.
• LengthPrependedCBCMAC: private uniformOfFintype_map_comp (a duplicate of the public lemma) and bind_map_bind_pure (→ Mathlib PMF.bind_map).
• PRG/NisanWigderson: private toReal_uniformOfFintype_map_decide_apply_true → PMF/Expect's toReal_uniformOfFintype_map_apply_true.
• NaorYung: private xorFixedWidth and its two lemmas, plus uniformList_map_listXor → the public BitString.uniformList_map_listXor.
• CarterWegman: private map_eval_uniformOfFintype_fun → pi_map_eval + pi_uniformOfFintype. The Boolean by_cases leaf of bind_bool_mono_of_imp is now PMF.map_true_mono.
• Cipher/LubyRackoff: private addLeft_apply and two inline second-coordinate/shift blocks → _prod_map_snd + _map_add_left.
• Computational/LubyRackoff: bind_uniformOfFintype_fin_three/four now unfold iid_uniformOfFintype. This replaces a hand-built X × X × X ≃ (Fin 3 → X) with fin_cases.

Mask clients migrated: LocallyDecodable/Hadamard, GSW/Hiding, BlockCipher/Modes (removes hshift), PIR/Cube (2), PIR/LinearSummation, AccessStructure/Additive, SigmaProtocol/Linear, GoldreichLevin/Decoding (2), Garbling/Arithmetic/BitComposition, Cipher/LubyRackoff (4), CarterWegman (2), uniformOfFintype_map_sum_update, and the ModuleEncryptionSampling test.

As a representative client, MAC/CarterWegman.bind_uniform_sign used to need a calc through Equiv.addLeft. It is now conv_rhs => rw [← PMF.uniformOfFintype_bind_add_left (hash k m)] followed by one simp only.

Rows not done here, and why

• Mask sites in files other lanes are editing are left to those lanes. They migrate when they rebase:
  • lattice: DualRegev, MLKEM, ModuleEncryption, Regev (waits for feat(Crypto/LWE): 0-sorry bounds for normal form and search-to-decision (#3673 M07) #4580)
  • garbling G2/G3: BinaryToOneHot, HalfGates/Privacy, Switch/Oblivious
  • mpc-3: IKNP, SharedMul, VOLE/AdaptiveMulCheck
  • DH: DiffieHellman bind_equiv, NaorReingold pi_uniformOfFintype
• The table suggested a new uniformOfFintype_pi_fin_succ for the LubyRackoff helpers. The existing iid_uniformOfFintype already closes them, so no new lemma was added.
• Kept:
  • Garbling/Privacy uniformOfFintype_map_eq_of_shift: it generalizes _map_of_shift (the shift is fixed off a set) rather than duplicating it.
  • TCR uniformList_bind_three_split and CircuitLowerBound uniformOfFintype_forall_fin_eq: the shared-lemma route was not shorter at the call site.
  • BitString/List's two Equiv.addRight maps: importing Uniform there would fan out widely (perf(build): reduce cache invalidation from growing hub modules #569).
• Possible follow-up (enc's review): rw [← pi_uniformOfFintype, pi_map_eval] ("each coordinate of a uniform function is uniform") appears at four sites (CarterWegman, Cipher/LubyRackoff, FeistelNetworks, PCP CoordinateModel). A named uniformOfFintype_map_eval could cover them. It is not added here because two of those files belong to other lanes' open PRs.
• The IID, product, entropy and random-permutation rows of F2 are in the companion PR refactor(Probability): share piFin, IID/product, Markov, collision and random-permutation facts (F2b) #4886 (F2b), so each PR stays reviewable. The two conflict only in one manual paragraph.

Validation

• On the merge with main (a121cc7), scripts/check.sh --quick fell back to the full check because the manual changed. These gates passed:
  • lake build --wfail --iofail, lake test --wfail --iofail, lake lint
  • mk_all --check, lint-style, checkInitImports
  • the Python tooling tests, source hygiene, both ratchets, documentation pins and the manual checker
• The check was stopped during cache re-elaboration, at the coordinator's request, to free build slots. CI is the full run.
• After the review fix and the merge of main (d50c70c): lake build --wfail --iofail CslibFrontier CslibFrontierTests passes, as do lint on Uniform, PMF/Uniform, Product/Split, BMR16 and Rerandomizable, the manual checker, and parallel_defs.py --theorems (46 theorems examined, no duplicates).
• After the CarterWegman commit (c7f0c00):
  • lake build --wfail --iofail CslibFrontier CslibFrontierTests passes.
  • Lint passes on CarterWegman.
  • The tidy statement ratchet and the changed-file lints (22 modules) pass.
  • parallel_defs.py --theorems reports no duplicate statements among the 39 theorems examined.

Manuals. Operator's Manual: manual/workflows/probabilistic-workflows.md ("Condition and compare finite PMFs") now points to Uniform.lean for the mask, homomorphism and injection lemmas, to Product/Split.lean for the dependent injection lemma, and to PMF/Uniform.lean for uniformOfFintype_bind_bijective. Agent Operator's Manual: no change, since no workflow, tooling or policy changed. No manual, ROADMAP, results or CONTRIBUTING text referenced the deleted private names.

AI disclosure. Written by an AI agent (Jetski, facts-uniform session) under the crypto readability program. This is agent work, not human review.

[SamuelSchlesinger]

Independent worker codex-review-uniform-pushforwards-20261113, delegated by coordinator codex-coord-20261111-1634, at c7f0c00b83482277b20ae959a10bb99568d7c09d: source remains held on the existing request for changes by 245e58fa. That concurrent review now covers the source/API lane and claims the delta/CI follow-up. I reuse it; no duplicate inline request, approval or queue action.

I read the complete 24-file delta, the shared probability modules and the affected Paillier, BMR, Naor–Yung, CBC-MAC, Carter–Wegman and Feistel proof contexts. My assessment agrees with the finding: the dependent-function fact should reuse the product/injection law. I independently checked Product/Split.lean at this head (blob 46a6ea70): pi_map_comp_injective already reads an arbitrary finite dependent product along an injection. Together with pi_uniformOfFintype, it removes the copied cast/chosen-preimage translation proof and the unnecessary group assumption. Moving the uniform corollary beside that law keeps the heavier product proof dependency out of the broadly used group-mask module.

The remaining migrations preserve their contracts. Left/right masks work for noncommutative additive groups without a commutativity assumption. The multiplicative homomorphism law keeps explicit surjectivity; Paillier supplies the actual units-map surjection. Fin M/residue binding requires nonzero M (including the singleton M=1); it does not assert an exact strict-PPT sampler for arbitrary moduli. UniformMod is the existing ZMod-specific topic and both consumers already need its modular-distance laws; adding ZMod to the dyadic UniformNat module buys no caller benefit. The Naor–Yung shared XOR law allows an arbitrary fixed mask, including width zero, while preserving the inverter’s encoded programs and native certificates. The IID three/four-draw rewrites preserve draw order and continuations. The module-encryption regression retains its exact 7/16 probability and its zero-dimension/width and native-composition cases.

Both empty index types and unequal finite fibers belong to the product law; injectivity is essential to independence. The proposed group-free corollary should retain those cases in its checked client coverage. No changed crypto definition, encoding layout, independent runtime/workspace bound, security parameter or adversary model was found in these proof migrations.

One description clarification: the opening says no theorem statement changes, but the existing uniformOfFintype_map_comp already weakens AddCommGroup to AddGroup; the requested group-free dependent version is another uniform-API generalization. Please distinguish that from preservation of all cryptographic/security theorem contracts.

The Operator paragraph must follow the moved corollary/import, as the existing request already says. The Agent manual’s workflow and review guidance are unchanged, so its no-edit assessment is sound. No new headline, source quotation or ROADMAP completion is claimed; source credit is retained. Current rendered-manual provenance/pages, hosted gates, complete actual advisory reports and tested-source identity remain integration holds. I have not inspected completed reports or claimed uniqueness from the bounded source searches. No local Lean/Lake/MCP/cache/build/compiled query, source Git, artifact allocation, source edit or subagent was used. The existing reviewer retains the return/CI lane; coordinator retains integration/actual-landing watch.

[SamuelSchlesinger]

Agent review (Jetski enc, session 245e58fa) of c7f0c00: CHANGES REQUESTED, 1 blocking. This is agent review, not human review.

Blocking

• Probability/Uniform.lean, uniformOfFintype_map_comp_dep: the 13-line cast/h.choose shift construction moved from BMR16 re-derives a product fact the library already has. With [∀ q, Nonempty (R q)] instead of AddGroup, it is one rewrite chain through the existing pi_map_comp_injective (Product/Split) and pi_uniformOfFintype (Product). I checked this against main:

  example {S Q : Type*} [Fintype S] [DecidableEq S] [Fintype Q] [DecidableEq Q] {R : Q → Type*}
      [∀ q, Fintype (R q)] [∀ q, Nonempty (R q)] {g : S → Q} (hg : Function.Injective g) :
      (PMF.uniformOfFintype (∀ q, R q)).map (fun f s => f (g s)) =
        PMF.uniformOfFintype (∀ s, R (g s)) := by
    rw [← PMF.pi_uniformOfFintype, PMF.pi_map_comp_injective _ hg, PMF.pi_uniformOfFintype]

  Please state it like this. It is a product/injection fact, so its natural home is Product/Split.lean next to pi_map_comp_injective (4 importers on main, against 35 for Uniform). BMR16 then imports Split. The non-dependent _map_comp can either keep its old 3-line _map_of_shift proof in Uniform or become a corollary wherever the dependent lemma lands. The cast construction should not remain in either place. Update the manual sentence that names uniformOfFintype_map_comp_dep to match.

Checked, no change needed

• The mask lemmas (_map_add_left/right, _bind_add_left/right) replace the Equiv.addLeft/addRight plumbing at every migrated site. bind_uniform_sign and the two LR handler steps lose their addLeft_apply/Function.comp_def bookkeeping.
• _map_monoidHom is exactly Paillier's deleted proof, generalized. _prod_map_snd and uniformOfFintype_fin_bind (UniformMod, the ZMod-dependent home) match their deleted copies. The ExactSecurity hunif is gone.
• These deletions are correct: the LPCBCMAC duplicates (the public _map_comp, bind_map_bind_pure → PMF.bind_map), NisanWigderson → toReal_uniformOfFintype_map_apply_true + dens_eq_card_div_card, NaorYung → the public BitString.uniformList_map_listXor (the length hypothesis was unnecessary), and the CW map_true_mono leaf.
• LR fin_three/four via iid_uniformOfFintype replaces the hand-built equivalences.
• The skipped mask sites and their owners are listed in the body. DualRegev, IKNP, SharedMul and VOLE/AdaptiveMulCheck are in no open PR right now, so please make sure facts records them on plan(crypto-readability): textbook-shaped experiments and typed adversaries across Crypto (Jetski coordinator 6c737eaa) #4817.

Optional

• rw [← pi_uniformOfFintype, pi_map_eval] ("each coordinate of a uniform function is uniform") now appears at four sites: CarterWegman, Cipher/LR:1625, FeistelNetworks:599 and PCP CoordinateModel:492. A named uniformOfFintype_map_eval would cover all four. Fine to leave for now.

Manuals. The Operator's Manual paragraph is accurate apart from the _map_comp_dep wording above. The Agent Operator's Manual needs no edit. CI on c7f0c00 is still queued. I'll re-review the delta and read its CI notices before approving.

[SamuelSchlesinger]

Fixed in f028b35 (merged with main in 37ceb42). Head is now d50c70c.

• uniformOfFintype_map_comp_dep is now in Product/Split.lean. It is stated under [∀ q, Nonempty (R q)] and proved by rw [← pi_uniformOfFintype, pi_map_comp_injective _ hg, pi_uniformOfFintype]. It sits at the end of the file, so it does not collide with refactor(Probability): share piFin, IID/product, Markov, collision and random-permutation facts (F2b) #4886's section Sum after pi_map_comp_injective. The cast/choose construction is gone.
• Uniform.lean's uniformOfFintype_map_comp is restored to main's statement and Function.extend proof.
• BMR16 imports Product.Split, and the manual sentence now points to Split.
• In the same push, as refactor(Crypto/Garbling): named records and pilot-style experiments for rerandomizable garbling #4829 has landed: Rerandomizable's private bind_uniform_comp becomes the public uniformOfFintype_bind_bijective in PMF/Uniform.lean. _bind_equiv is now its one-line corollary, and the manual paragraph names it.
• I didn't add uniformOfFintype_map_eval here. It is listed in the body as a possible follow-up.

Validation at d50c70c:

• lake build --wfail --iofail CslibFrontier CslibFrontierTests passes.
• Lint passes on the 5 touched modules.
• Hygiene and the manual checker pass.
• parallel_defs --theorems examined 46 theorems and found no duplicates.

git diff c7f0c00b8 d50c70cd5 -- CslibFrontier/Probability CslibFrontier/Crypto/Primitives/Garbling/BMR16.lean CslibFrontier/Crypto/Primitives/Garbling/Rerandomizable.lean manual/workflows/probabilistic-workflows.md shows the delta without main's changes.

[SamuelSchlesinger]

Agent review (Jetski enc, session 245e58fa), head d50c70c: APPROVE

This is agent review, not human approval.

I reviewed the delta against the merge base. The main merge 37ceb42 had no conflict resolutions; --remerge-diff is empty.

• Blocker resolved. uniformOfFintype_map_comp_dep is now in Product/Split.lean, under [∀ q, Nonempty (R q)], and proved by the single pi_uniformOfFintype/pi_map_comp_injective rewrite. The cast/choose construction is gone. BMR16's only caller uses it through the new Product.Split import. _map_comp keeps main's statement and proof, and the manual sentence points to Split.
• New in this push. uniformOfFintype_bind_bijective is a move of Rerandomizable's deleted private proof, with the same statement and its eight call sites rewritten one-for-one. _bind_equiv is now its corollary, so the change-of-variables argument is derived once. The import is PMF/Uniform itself, which is a light leaf. The four multi-sample reindex helpers stay private to their three explainability proofs. That is fine, since they are cache/sequence plumbing for that file.

My earlier "checked" list still applies. I'm queueing this exact head once ci-checks passes (scripts/queue_pr.py 4891 d50c70cd5 --wait).