[SamuelSchlesinger]

Change

Part of #4817 (row F7). Jetski session facts-encoding (helper of facts 0e8cfb07), branch readability/facts-encpair. #4881 has landed, and this PR now targets main with main merged.

Proofs that read a component back out of an encPair word kept re-proving unframe (encPair e₁ e₂ (a, b)) = e₁ a and dropFrame (encPair e₁ e₂ (a, b)) = e₂ b, either inline as have … := by simp [encPair_apply, unframe_frame_append] pairs or as local named lemmas. This PR states the two facts once, in a new small module MultiTape/Encodings/Pair/Projections.lean, and deletes every copy outside the files DH owns:

• unframe_encPair, dropFrame_encPair (generic), plus unframe_encPair_encBits and dropFrame_encPair_encBits for a raw bit-string component, which already strip encBits. Most sites pair two bit strings, and since encBits isn't reducible a generic rw would leave encBits ke behind.
• Deleted named copies: Lyubashevsky/Efficient's private unframe_encPair/dropFrame_encPair, Paillier's public unframe_encPair_encNat/dropFrame_encPair_encNat (GM now uses the generic lemmas; its open Paillier (…) line is gone, and its Paillier import is replaced by PowMod and a public UnitSampling), and the test helpers unframe_dropFrame_pair in AuthenticatedEncryption and SigmaLWECCANonvacuity.
• Deleted every inline have copy; each site now rewrites with the shared lemma directly. They were in EncryptThenMAC, MACThenEncrypt, Authenticated, CompositionCounterexamples, EncForge, Oracle/PP, Kolmogorov/MKtP and tests/CompositionCounterexamples. git grep -nE '(unframe|dropFrame) \(encPair' now finds only goal statements, the DH-owned sites and the PP/MKtP facts that compose a projection with a decoder or length.

What callers no longer repeat. For example, EncryptThenMAC.encryptThenMAC.decrypt_encrypt used to declare four haves (8 lines) before rw [hunframe_k, hdrop_k, hunframe_ct, hdrop_ct]. It now writes rw [unframe_encPair_encBits, dropFrame_encPair_encBits, …] directly.

Placement. Encodings/Pair.lean is vendored from crei and has 50 importers, so the lemmas go in a small module beside it rather than as a -- vendored: local addition. Only the files that use the lemmas import it. The marker records the lemmas as candidate additions to the vendored file. The lemmas are not @[simp]: encPair_apply together with unframe_frame_append/dropFrame_frame_append already rewrites that left-hand side, so simp normal form is unchanged.

Statements are unchanged apart from the deleted names: Paillier's two public _encNat lemmas, which the generic ones replace, and two test-file helpers.

Not in this PR. The DH-owned sites, ElGamal/ProbComp:106/110 (private _encBits copies) and tests/DiffieHellman:95, are recorded on #4817 for after the DH PR.

Authors of new files: Samuel Schlesinger.

Manual impact

• Operator's Manual: updated. In choosing-models.md, the encoding-reuse paragraph now points to the projection lemmas next to the existing pair-length link.
• Agent Operator's Manual: no edit needed. This PR changes no agent role, review or workflow procedure.

Validation

• At head ea700fb8 (main merged after refactor(Crypto): move ZMod/BitString encodings, integer-box samplers, powMod and unitOrOne to shared modules #4881 and refactor(Crypto/Signature): share the signature-length bound and drop duplicate plumbing #4879), a targeted lake build --wfail --iofail passes for the new module, every edited library module, and the client tests CslibFrontierTests.Crypto.{AuthenticatedEncryption, CompositionCounterexamples, SigmaLWECCANonvacuity, Paillier, GoldwasserMicali, Lyubashevsky}. At head f90edae8 (GM import fix), CslibFrontier.Crypto.Computational.GoldwasserMicali and CslibFrontierTests.Crypto.GoldwasserMicali build again with --wfail --iofail.
• lake exe mk_all --check, check_hygiene.py on the changed files, the encoding readability and projection chain ratchets, and the manual checker all pass.
• CI does the full validation run.

AI assistance

Written by an AI agent (Jetski, swarm worker facts-encoding) under the direction of Samuel Schlesinger: it added the lemmas, migrated the sites, edited the manual and ran the checks. No human has reviewed this PR yet.

[SamuelSchlesinger]

Agent review (Jetski mac session 30c9671c-112b-428f-8ed2-e9847d5bfa64), head ea700fb: APPROVE

The facts are stated once. unframe_encPair and dropFrame_encPair are proved by unframe_frame_append/dropFrame_frame_append. The _encBits forms are one-line specializations of these, not separate proofs. Not @[simp] is the right call, since encPair_apply plus the frame lemmas already rewrite the left-hand side. Placing them in a small leaf module beside the vendored Pair.lean avoids adding to its 50 importers, and each client imports the module privately.

The callers use the shared lemmas. Every removed have pair now rewrites with the shared lemma: EncryptThenMAC, MACThenEncrypt, Authenticated, CompositionCounterexamples, EncForge, Oracle/PP, Kolmogorov/MKtP and the 3 tests. Efficient's private pair is gone. git grep -E '(unframe|dropFrame) \(encPair' at the head finds only goal statements, the DH-owned sites, PP:344 (now rw [dropFrame_encPair] before the decoder step) and MKtP:353 (a length fact, now rw [dropFrame_encPair]; simp).

Paillier and GM. unframe_encPair_encNat/dropFrame_encPair_encNat are deleted, and every Paillier and GM use now calls the generic lemmas. The open Paillier (…) line is gone. No open PR's diff adds a use of the deleted names, including #4901, #4887 and the held enc/dh branches.

The DH sites are recorded. ElGamal/ProbComp:106/110 and tests/DiffieHellman:95 are on #4817 (issuecomment-6841094428, "After DH" list). ElGamal's private _encBits copies share the new names. They don't clash today because ElGamal doesn't import Projections, but the DH follow-up should delete them rather than add the import alongside them.

Non-blocking. About 20 larger simp [encPair_apply, …_frame_append, …] calls remain, in CarterWegman, Hybrid, MerkleSignature, CramerShoup and elsewhere. They rewrite as part of a bigger normalization and are not restated copies, which is consistent with this PR's scope and with the module doc's guidance. One is closer to a copy: DEMCCA:177's simpa only [encPair_apply, encBits_apply, unframe_frame_append] using congrArg unframe h could probably be simpa only [unframe_encPair_encBits] using congrArg unframe h (I haven't elaborated it). Optional.

Manuals. The choosing-models.md sentence points to the new lemmas, and no AOM edit is needed. There are no unresolved review threads.

This is an agent review, not a human review. I'll queue it once ci-checks is green and its notices are read.

[SamuelSchlesinger]

Agent review (Jetski reviewer jrev-4904, coordinated by jetski-coord-8077 / #4809), head ea700fb: CHANGES REQUESTED, one small cleanup item. This is agent review, not human review.

Crypto/Computational/GoldwasserMicali.lean:12 still has public import CslibFrontier.Crypto.Computational.Paillier, but GM no longer uses anything from Paillier. #4881 moved powMod/unitOrOne out, and this PR deletes the _encPair_encNat pair and the open Paillier line. The import now only makes GM and its clients rebuild whenever Paillier changes.

Fix, checked in a private worktree: replace it with public import CslibFrontier.Complexity.PolyTime.Nat.PowMod and make the existing import …Crypto.Computational.UnitSampling public. lake build --wfail --iofail passes for CslibFrontier.Crypto.Computational.GoldwasserMicali and CslibFrontierTests.Crypto.GoldwasserMicali.

Everything else agrees with the 03:14 approval:

• The four lemmas are stated correctly and in the right generality.
• The leaf module is a good home for them.
• Every deleted copy is subsumed, and the public _encNat pair's only callers (in GM) are migrated.
• The remaining ElGamal/ProbComp and DH-test copies are deferred to refactor(Crypto): typed Diffie–Hellman experiments and adversaries #4874 per plan(crypto-readability): textbook-shaped experiments and typed adversaries across Crypto (Jetski coordinator 6c737eaa) #4817.
• The manual edit is correct.
• The restack is clean: 16 files, nothing unrelated.

Please hold queueing until this import is fixed; a one-line delta check will follow.

[SamuelSchlesinger]

Fixed in f90edae: GoldwasserMicali now imports …PolyTime.Nat.PowMod publicly in place of Paillier, and UnitSampling is now a public import. lake build --wfail --iofail passes for CslibFrontier.Crypto.Computational.GoldwasserMicali and CslibFrontierTests.Crypto.GoldwasserMicali, and hygiene is clean.

[SamuelSchlesinger]

Agent review (Jetski mac session 30c9671c), head f90edae: APPROVE (the delta over ea700fb).

GoldwasserMicali now imports PolyTime.Nat.PowMod and UnitSampling publicly, in place of Computational.Paillier. Those two modules supply powMod and unitOrOne, which are the only names GM used through Paillier. GM is imported only by the root aggregate and CslibFrontierTests/Crypto/GoldwasserMicali.lean, and the author's targeted build covers that test, so no client depended on reaching Paillier through GM. This resolves jrev-4904's finding. There are 0 unresolved threads. I'll queue once ci-checks is green and I've read its notices.

This is an agent review, not a human review.