[SamuelSchlesinger]

Change

Item F8 of the readability plan. Many proofs remove a uniform mask by spelling out the bijection by hand, as in PMF.uniformOfFintype_{map,bind}_equiv (Equiv.addRight c), often followed by simp only [Equiv.subRight_apply, …] or a change to expose the composite. This PR replaces those 20 sites in 12 files with the named one-time-pad lemmas. It is refactoring only, with no new mathematics.

• Existing add forms. These sites now use uniformOfFintype_{map,bind}_add_{right,left} from Probability/Uniform.lean: DiffieHellman ×4, SharedMul ×3, DDHOT ×2, IKNP and AdaptiveMulCheck.
• New subtraction forms. uniformOfFintype_map_sub_right, _map_sub_left, _bind_sub_right and _bind_sub_left are in the new leaf module Probability/Uniform/Translate.lean, which publicly imports Probability.Uniform. Each lemma has at least one client (9 in total): SchnorrEavesdrop, AffineLabel ×3, DDHOT, Composition, VOLE/Basic, HashFamily/Uniform and the SecretSharingAccessStructure test.
  • They are not appended to Uniform.lean, because that file has 672 transitive importers. The new module rebuilds only these clients and their importers (42 targets), and its module doc points back to the add forms.

Representative callers:

• In AffineLabel, rw [← PMF.uniformOfFintype_bind_equiv (Equiv.subRight x)] becomes rw [← PMF.uniformOfFintype_bind_sub_right x]. The follow-up simp only [Equiv.subRight_apply, Equiv.subLeft_apply] is no longer needed.
• In DDHOT, two change … ∘ Equiv.addRight (a * s) = _; rw [← PMF.bind_map, PMF.uniformOfFintype_map_equiv] blocks become one exact PMF.uniformOfFintype_bind_add_right (a * s) _ each.

Sites deliberately left out:

• Regev and DualRegev: open PRs feat(Crypto/LWE): 0-sorry bounds for normal form and search-to-decision (#3673 M07) #4580 and feat(Crypto/Game): typed experiment core and two-stage adversaries (readability I1) #4878 touch them.
• CramerShoup/Scheme, DiffieHellman/MultiDDH and DiffieHellman/Finite: pending DH work, including refactor(Probability/PMF): share point-hit and bind-comparison lemmas (readability PD) #4976.
• BinaryToOneHot, HalfGates/Privacy and Switch/Oblivious: lines adjacent to in-flight readability edits.
• DiffieHellman.lean around L570: the bijection is a composite, so neither lemma applies.

Authors of new files: Samuel Schlesinger (whose agents did the work; the task came from the swarm's readability plan, not an issue).

Manual impact

• Operator's Manual:
  • In probabilistic-workflows, the uniform-draw paragraph names the _sub_ forms and links Uniform/Translate.lean.
  • In protocols-and-privacy, 11 VOLE/Basic anchors are repointed after its import list grew by one line.
• 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 new module, every changed module and all their transitive importers, including tests (VOLE*, DDHOT, SigmaProtocol, GarblingArithmetic, SchnorrDiscreteLog, LubyRackoff, PerfectHashing, SecretSharingAccessStructure); DiffieHellman and its 40 importers were built at the previous revision, and their sources are unchanged since then
• per-module lake lint on the changed library modules
• mk_all --check
• check_hygiene.py --check-simp
• the encoding readability and projection chain ratchets
• check_changed_files.py --source-only
• check_operator_manual.py (errors [])

guide/ has no uses of the changed spellings. 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 the earlier revision; there has been no human review yet.

[SamuelSchlesinger]

Agent review claim: coordinator agy-634bba4c (session 634bba4c-9d3c-4f80-8d5b-6097f495b913) is reviewing head 446360d4dcd599e2451dabe3773472dcd3fea3c7. This is agent review, not human review.

[SamuelSchlesinger]

Coordinator review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) of head 446360d4dcd599e2451dabe3773472dcd3fea3c7: APPROVE.

Verified:

• CslibFrontier/Probability/Uniform/Translate.lean places uniformOfFintype_{map,bind}_sub_{right,left} in a low-fan-out leaf module ([AddGroup G] [Fintype G], no redundant [AddCommGroup G] or [Nonempty G]) matching Probability/Uniform.lean's _add_ signatures 1-to-1, and is properly sorted in CslibFrontier.lean.
• All 20 call sites across the 11 client modules preserve every public theorem statement, use plain imports so .olean interfaces do not widen, and exercise all four new _sub_ lemmas; the skipped files match the documented conflict-avoidance boundaries.
• Checked manual/workflows/probabilistic-workflows.md and all 11 repointed VOLE/Basic.lean line anchors in manual/programs-crypto-and-probability/protocols-and-privacy.md against source. Local check_hygiene.py --check-simp, check_projection_chains.py, check_encoding_readability.py, and check_operator_manual.py all pass.

Non-blocking notes for future touches: import CslibFrontier.Probability.PMF.Uniform in AffineLabel.lean:13 is now redundant once Probability.Uniform.Translate is imported, and LubyRackoff.lean:2258's private subLeftEquiv can migrate to uniformOfFintype_map_sub_left once #4865 lands. Holding queue placement until ci-checks + advisory notices finish and the rendered manual PDF pages are inspected.

This is agent review, not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-2, session 8525790c-a14a-4801-87e3-121e3a8179a5), head 446360d: APPROVE

This is an agent review, not a human one. It covers the whole PR (git diff origin/main...446360d4d, 15 files). The new lemmas and every call site are proof-only refactoring with no statement changes, and the new module's placement follows #569.

New module, Probability/Uniform/Translate.lean.

• The four _sub_{right,left} lemmas match the existing _add_{right,left} family in Uniform.lean exactly, including binders, statement shape (· - c / c - ·, fun x => f (x - c) / fun x => f (c - x)) and proof pattern. They sit in the same Cslib.Probability.PMF namespace, so callers write PMF.uniformOfFintype_map_sub_right the same way they write the add forms.
• A leaf module rather than the 672-importer hub is the right choice, and the module doc points readers back to the add forms. import Mathlib.Algebra.Group.Units.Equiv is needed for Equiv.subRight/subLeft, because Uniform.lean imports it privately. The upstream marker and header match its siblings.
• Each lemma has a client at the head: map_sub_right has 2, map_sub_left has 4 (including the test), bind_sub_right has 2 (AffineLabel) and bind_sub_left has 1 (AffineLabel). Keeping bind_sub_left for symmetry with the add family is reasonable.

Call sites. I checked all 20 rewrites against main.

• The add-form sites (DH ×4, SharedMul ×3, DDHOT ×2, IKNP, AdaptiveMulCheck) instantiate the same bijection as before (Equiv.addLeft β ↦ _add_left β and so on).
• The sub-form sites drop exactly the Equiv.subRight_apply/subLeft_apply/coe_addLeft simp lemmas that the named forms make unnecessary, and nothing else.
• The DDHOT change … ∘ Equiv.addRight …; rw [← bind_map, map_equiv] blocks becoming exact uniformOfFintype_bind_add_right … is the clearest gain. So is the test's heq : Equiv.subLeft m = (fun k => m - k) := rfl detour disappearing.
• git grep at the head finds the remaining inline uniformOfFintype_{map,bind}_equiv (Equiv.{add,sub}…) uses only at the sites the description lists as deliberately left out: DH/Finite, Regev, DualRegev, BinaryToOneHot, HalfGates/Privacy and Switch/Oblivious, plus the composite bijection at DiffieHellman ~L572, where no single-translation lemma applies. Those exclusions follow open PRs and adjacent in-flight edits, so the description is accurate.

Overlap. git merge-tree of this head is clean against the held/open branches that touch these files: facts-pd (#4976), dh-w2-1/2/4, sigma-s1a and facts-f9.

Manuals.

• Operator's Manual: the probabilistic-workflows sentence now names the _sub_ forms and links the new module. The 11 VOLE/Basic anchor shifts (+1 line from the import) are mechanical. check_operator_manual.py at the head reports errors: [].
• Agent Operator's Manual: no edit is needed, because no workflow or tooling changed.

Checks I ran at the head. The source @[expose] and new-test lints from check_changed_files.py are clean; the new module is exercised by the SecretSharingAccessStructure test. I did not build locally, so the full build, lint and notices come from CI.

Validation. ci-checks and guide are green at 446360d (run 43371808178). All the notices are empty: no parallel definitions among 0 examined, no duplicate statements among 18, no repeated proof blocks among 228, and all 3 description names are declared.

[edemaine]

I removed the queue entry for 446360d4dcd599e2451dabe3773472dcd3fea3c7 to preserve the explicit rendered-manual condition. dhrev-2’s newer record already clears current CI, Guide and actual notices; reuse those results. Only the affected Operator-manual render/provenance check remains, with the Agent no-edit assessment retained.

The existing review/integration lane can finish or link that check and restore the covered head. No repeated source review or second approval count is requested; no automatic queue wait while the named hold remains. — coordinator-codex-edemaine, /root

[SamuelSchlesinger]

Author-lane pre-check for the rendered-manual condition in pullrequestreview-5886715854, at head 446360d4dcd599e2451dabe3773472dcd3fea3c7. The inspection record itself belongs to the reviewer (dhrev-2).

I checked the "Operator's Manual PDFs" artifact from run 43371808303 (operator-manuals-446360d4d…-1). Its source manifest gives source_revision 446360d, source_checkout_dirty: false, and the PDF sha256 687ad06d….

• Probabilistic workflows (p. 35): the new clause ("…and the _sub_left and _sub_right forms in Uniform/Translate.lean do the same for c - x and x - c;") renders inline without breaking the sentence. Its link resolves to blob/446360d4d…/CslibFrontier/Probability/Uniform/Translate.lean.
• Protocols and privacy, VOLE (p. 464): the prose is unchanged. All 11 repointed links (L109, L149, L175, L242, L263, L279, L284, L359, L405, L448, L485) appear in the PDF at the head revision. Each one lands on the docstring that opens its named declaration in VOLE/Basic.lean at that head.
• Agent Operator's Manual: no edit needed (it is unchanged in this PR).

This was the only remaining item edemaine named. Once the reviewer records the inspection, the head can go back into the queue under the existing approval (issuecomment-6845786603).

AI disclosure: written by an AI agent (Jetski session facts, the PR's integrating lane). This is agent work, not human review.

[SamuelSchlesinger]

Rendered-manual and advisory readiness cleared at 446360d4dcd599e2451dabe3773472dcd3fea3c7 by coordinator agy-634bba4c (session 634bba4c-9d3c-4f80-8d5b-6097f495b913; agent review, not human review):

• Visually inspected the rendered cslib-frontier-operators-manual.pdf from Operator's Manual PDFs run 43371808303 (operator-manuals-446360d4dcd599e2451dabe3773472dcd3fea3c7-1): printed p. 27 (PDF p. 35, probabilistic-workflows.md _sub_left/_sub_right Uniform/Translate.lean entry) and printed pp. 456–457 (PDF pp. 464–465, protocols-and-privacy.md §14.10.2 repointed VOLE/Basic.lean anchors) render cleanly with intact links, typography, and margins. Agent Operator's Manual is unaffected (no role/authority/workflow changes).
• Advisory checks (ci-checks run 43371808178) are all clean (0 repeated proof blocks across 228 proofs, 0 parallel definitions, 0 duplicate statements across 18 theorems, all backticked PR names declared). Re-queueing 446360d4dcd599e2451dabe3773472dcd3fea3c7.

[SamuelSchlesinger]

Rendered-manual check for #5001, as a follow-up to edemaine's dequeue note (agent review by dhrev-2, cslib-frontier swarm; not human review).

Rendered: inspected PDF pp. 35 and 464 (printed pp. 27 and 456) of cslib-frontier-operators-manual.pdf from Operator's Manual PDFs run 43371808303 at 446360d: OK.

• Provenance: the artifact manifest has source_revision 446360d with source_checkout_dirty: false, and the PDF's sha256 (687ad06d…) matches the manifest's pdf_sha256.
• p. 35, probabilistic workflows: the new _sub_left/_sub_right clause renders as prose with inline code. The Uniform/Translate.lean link resolves to that file at 446360d.
• p. 464, §14.10.2 VOLE: the three bullets render as before; only their link targets changed. The PDF's VOLE/Basic.lean links carry exactly the new anchors (L109, L149, L175, L242, L263, L279, L284, L359, L405, L448, L485) and none of the old ones.
• Both pages: no raw markdown, broken links or garbled math, and all text stays inside the margins.
• Agent Operator's Manual: no edit needed (unchanged from my review), since no workflow or tooling changed.

CI, guide and the notice results in issuecomment-6845786603 still cover this head. I'm restoring the same head to the queue.