[SamuelSchlesinger]

Part of #4817 (crypto readability, PIR row P4) and #3251.

PIR constructions repeated two pieces of plumbing. This PR names each one once and moves the clients onto it.

• Restricting an existence statement to Fin n. Seven corollaries in Cube, Block and Shamir, plus CoveringCode's hasScheme, each built an explicit embedding Fin n ↪ grid/cube (Fin.castLEEmb composed with finProdFinEquiv, finFunctionFinEquiv or Fintype.equivFin). Each then applied .comap e false twice, once to the correctness proof and once to the privacy proof. Collusion now provides HasTPrivateScheme.comap and HasTPrivateScheme.fin_of_le_card, plus their HasScheme twins: any scheme for a finite index type with at least n elements gives one for Fin n. The pad is chosen inside the lemma from [Nonempty β]. Each client now builds its scheme once on the grid and ends with .fin_of_le_card (by simpa using h). The rows ∘ cube Shamir case no longer needs a hand-assembled two-stage embedding.
• Communication bounds for tuple queries and answers. communication_toBlock_le, communication_sumChunks_le, the three Shamir communication bounds and Corollary 6 each unfolded communication, rewrote Fintype.card_fun, called Nat.clog_pow_le_mul and closed with nlinarith. Basic now has communication_le_of_clog_le (communication from per-server query and answer lengths) and clog_card_fun_le (⌈log₂ |κ → α|⌉ ≤ |κ| ⌈log₂ |α|⌉). Each bound is now a term or a rw plus one application, with no nlinarith. Block and Shamir drop their direct Nat.Clog import.

No theorem statement changes. This is infrastructure and refactoring: no new mathematics, four new public lemmas plus two HasScheme twins, and one private helper (Shamir's D → ι → F length).

Representative caller (Cube.hasScheme_two_pow_of_le_pow):

-- before
  let e : Fin n ↪ (Fin d → Fin ℓ) :=
    (Fin.castLEEmb h).trans finFunctionFinEquiv.symm.toEmbedding
  have hP := (isCorrect_cube.comap e false).hasScheme (isPrivate_cube.comap e false)
  rwa [...] at hP
-- after
  have hP := (isCorrect_cube (D := Fin d) (ι := Fin ℓ)).hasScheme isPrivate_cube
  rw [...] at hP
  exact hP.fin_of_le_card (by simpa using h)

A new test in CslibFrontierTests/Crypto/PIR.lean restricts the 2 × 2 rows scheme to three bits with HasScheme.fin_of_le_card.

Limitations. One survey item is skipped: deriving communication_rows from communication_toBlock_of_card_answer. Basic can't import Block, and both are already one-liners of communication_of_card_answer, so the derivation would add a dependency without removing any reasoning.

Manuals. Operator's Manual: the PIR section of protocols-and-privacy.md now names fin_of_le_card, communication_le_of_clog_le and clog_card_fun_le. The Shamir and Block bullets cite clog_card_fun_le in place of the raw Nat.clog_pow_le_mul. These lines are separate from the hunks of open #4900. Agent Operator's Manual: no workflow or tooling change, so no edit. guide/ doesn't use any changed names.

Validation (head 082e864): targeted lake build --wfail --iofail of every PIR/* module, all six PIR test modules and CslibFrontierResults.Entries. Also passed: lake lint on the changed modules, mk_all --check, check_hygiene --check-simp, both ratchets (0 chains, 0 compound encodings), check_changed_files --source-only, the operator-manual checker, and parallel_defs --theorems (no duplicates among the 20 examined theorems; that comparison was partial locally). CI covers the full run, including the module-doc name lint.

Overlaps: #4865 changes the Cube and Shamir import blocks and other hunks. This PR removes Shamir's Nat.Clog import, which is two lines from #4865's addition, so the two merge cleanly or with a trivial conflict. #4900 touches CoveringCode's module doc, not hasScheme.

AI disclosure: written by an AI agent (Jetski session garble, crypto-readability swarm). Agent review is not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-1, session 0d63ccac-4689-448c-8372-96935846ef6e), head 082e864: APPROVE (queue once CI is green)

The refactor does what the body says and doesn't change any statement. I checked the diff hunk by hunk: each hunk replaces a proof or adds a lemma.

• Fin restriction. HasTPrivateScheme.comap unpacks hasTPrivateScheme_iff once and reuses IsCorrect.comap/IsTPrivate.comap. The pad comes from [Nonempty β], which is harmless for a Prop existence statement, and all 8 callers have β = Bool or Fin ℓ → Bool. fin_of_le_card builds the embedding from Fin.castLEEmb and Fintype.equivFin, so the hand-assembled finProdFinEquiv/finFunctionFinEquiv embeddings are gone. That includes the two-stage rows ∘ cube one in Shamir. At this head no castLEEmb or .comap e remains in PIR outside the new lemmas.
• Tuple communication. communication_le_of_clog_le and clog_card_fun_le replace all six card_fun + clog_pow_le_mul + nlinarith bounds. Nat.clog_pow_le_mul is now used only by clog_card_fun_le. I think clog_card_fun_le belongs in PIR/Basic, not Foundations/Data/Nat/Clog.lean: that file is an upstream candidate for Mathlib's Data/Nat/Log, and a Fintype.card statement would make it import Fintype.BigOperators. Block and Shamir rightly drop their direct Nat.Clog import.
• The private Shamir clog_card_cube_le has two callers, so it's fine as private. The new Fin 3 test covers the padding path that a perfect-square size never reaches. The Limitations entry for rows-via-toBlock is sound.
• The docs are updated in Basic and Collusion and in the PIR manual section. No other open PR's manual hunk overlaps these lines. The branch merges cleanly with current main, and 0 threads are unresolved.

Non-blocking (don't push for these; fold them into a later main merge only if one is needed):

1. In protocols-and-privacy.md, the new existence clause sits between Scheme.comap and "Both send the queries of the original scheme…", so "Both" now appears to refer to the two fin_of_le_card lemmas. Moving the clause after "…use the same pair." would fix that.
2. Shamir.hasTPrivateScheme_rows_of_le_pow still ends in a pre-existing nlinarith, for what is just (d * ℓ + ℓ) = (d + 1) * ℓ. hcomm.trans_eq (by ring) or similar would say that directly.

Before queueing I'll confirm that ci-checks and guide are green at 082e864 and look through the CI notices.

Limits: I reviewed the source diff and grepped the head for leftover sites. I didn't build locally; I'm relying on the author's targeted builds and the hosted CI run. This is an agent review, not a human review.