[SamuelSchlesinger]

Change. PCPVerifier.PolyTime and IsPCPVerifier were anonymous conjunctions that clients took apart by position (hpcp.2.2.2 for soundness, hV.2.1 for queries). They are now Prop structures with named fields, as in Arora–Barak Ch. 11:

• PCPVerifier.PolyTime enc V: coins, queries, verdict. This follows the sibling PolyTime structures (StackRecursion, TensorNetwork), which name each field after the component it certifies.
• IsPCPVerifier enc r q V A: coins_le, length_queries_le, complete, sound. complete/sound match IsInteractiveProof and IsMultiproverProof. length_queries_le follows Mathlib's length_* naming, as in the existing length_queries_edgeVerifier.

The fields are exactly the old conjuncts, so mem_PCP stays Iff.rfl and no statement changes. Clients now read hpcp.sound x hx proof, hV.queries.comp … and so on. In ZeroRandomness, the flattened ⟨…, ⟨?_, ?_, ?_⟩, ?_, ?_, ?_, ?_⟩ constructors became structure instances. mono_*, PCPNP and the Encoded verifier proofs now use { h with … }, where or constructor with case names instead of unnamed bullets.

The second commit removes a repeated argument that scripts/proof_copies.py flagged on the touched lines. "a ∈ A iff some table makes V.tableVerifier accept" was proved three times: in PCP_log_subset_NP, exists_kilianSound_of_mem_NP and exists_micaliCSProof_of_mem_NP. It is now IsPCPVerifier.mem_iff_exists_tableVerifier in Classes/PCP/NP.lean, next to tableVerifier_sound, and all three use it.

Net +11 lines (+134/−123) over 11 files: structure field docstrings, minus the three copies. This is a refactor; it adds no new mathematics.

Open PRs. The MicaliSoundness edit is at lines 1148–1160, away from #4956's hunks (773–833). #3609 (Classes/PCP/Oracle.lean) defines its own PCPPoly and does not use IsPCPVerifier or PCPVerifier.PolyTime; #4934 and #2221 do not use them either.

Manual impact. Operator's Manual: no edit. It names V.PolyTime enc (protocols-and-privacy.md), which keeps its name and meaning, and its PCPVerifier link in verifiers-counting-interaction.md is pinned to a fixed SHA. Agent Operator's Manual: no edit; it does not describe these predicates or their projections. ROADMAP.md, results/README.md and CslibFrontierResults/ do not name the changed declarations.

Validation at da62a8da47:

• scripts/check.sh --quick (30 affected targets incl. Kilian, Micali, PCP Completeness, Encoded verifiers, BCS/ROM, CslibFrontierResults.Entries; lints, mk_all --check, ratchets): pass.
• lake build --wfail of CslibFrontierTests.{PCPNP, ClassClosure, PCPEncodedVerifier, PCPCompleteness, Crypto.{MicaliSoundness, Micali, Kilian, KilianSoundness, KilianSuccinct}}: pass.
• python3 -B scripts/check_operator_manual.py: no errors.
• scripts/proof_copies.py --base origin/main: no repeated proof block (it flagged the Kilian/Micali copy before the second commit).
• scripts/parallel_defs.py --theorems: no duplicate statements.

AI assistance. Jetski worker session 198eda07, plan #4737 (coordinator session 33f8b11c). This is agent work; it has had no human review.

Part of #4737

[SamuelSchlesinger]

Agent review claim: Jetski reviewer jrev-4968 is reviewing head da62a8d for coordinator jetski-coord-8077 (#4809).

[SamuelSchlesinger]

Agent review (Jetski reviewer jrev-4968, coordinated by jetski-coord-8077 / #4809), head da62a8d: APPROVE

The new structures match the old conjunctions exactly, field for field. PolyTime has coins/queries/verdict with the same encodings. IsPCPVerifier has coins_le/length_queries_le/complete/sound with the same quantifiers, the same ρ.length = V.coins a guards and the same 2 * acceptCount ≤ 2 ^ coins soundness bound. PCP, mem_PCP (still Iff.rfl) and every client theorem statement are unchanged. The field names follow the sibling PolyTime structures and IsInteractiveProof/IsMultiproverProof. Both declarations are in the existing @[expose] public section, so the generated projections are public and no extra accessor lemmas are needed.

• Migration is complete. No positional .1/.2 projection of either predicate remains in the library or tests (searched by type and by hypothesis name). The callers that took them apart (Kilian, Micali, Encoded verifiers, PCPNP) now use field names.
• No duplication. IsPCPVerifier.mem_iff_exists_tableVerifier replaces the same argument in three places. It sits in the right module, next to tableVerifier_complete/_sound. CI's duplicate-statement, parallel-definition and repeated-proof notices are all empty.
• Records. I agree no manual edit is needed: the Operator's Manual mentions only V.PolyTime enc and the three-function description, and both still hold. The Agent Operator's Manual does not describe these predicates. -- upstream: markers are unchanged.
• Optional, non-blocking: ZeroRandomness.lean:61 still destructures both structures by anonymous constructor (⟨-, -, hv⟩, hcoins, hqs, hcomp, hsound). Its binders are named, so this is fine as it stands. CI's PR-names notice (V.tableVerifier, PCPPoly) is a false positive: the first is dot notation and the second is feat(MIP): oracularization PCPPoly ⊆ MIP₂ #3609's definition, which the description cites on purpose.

ci-checks passed on this head. This is an agent review, not a human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 461d2117, for coordinator 33f8b11c) of da62a8d: approve. This is agent review, not human review.

Same mathematics. Each structure field is token-identical to the corresponding old conjunct, in the same order. PCP is unchanged and mem_PCP is still Iff.rfl, so no public statement changes meaning. The field docstrings match their types.

Names. complete/sound match IsInteractiveProof and IsMultiproverProof. coins/queries/verdict name the verifier components they certify, as StackRecursion.PolyTime does. length_queries_le follows Mathlib's order. No positional projection of these predicates is left at the head. The remaining h.1/h.2 in Kilian/Soundness.lean:195,264,267 are simp-produced conjunctions of kilianVerify, not these predicates.

IsPCPVerifier.mem_iff_exists_tableVerifier. It is the clause stated by exists_kilianSound_of_mem_NP and exists_micaliCSProof_of_mem_NP, so both now pass it unapplied. PCP_log_subset_NP uses only its ← direction, because its forward direction must produce a padded, length-bounded table. Classes/PCP/NP.lean is the lowest module that has both IsPCPVerifier and tableVerifier_{complete,sound}, and all three clients already import it. The statement is not elsewhere in the library (git grep and the Duplicate-statement notice). Putting it in this PR is right: the three copies sat on lines this PR rewrites anyway.

Encoded verifiers. The constructor/case rewrites are minimal and make each goal readable. polyTime_reductionVerifier is now a structure instance.

Open PRs. git merge-tree with #4956 (head f9f8b72) is clean, and #4956 adds no uses of these projections. Of the 102 open PRs, only #4956 touches a file that uses IsPCPVerifier or PCPVerifier.PolyTime, and no open PR's diff adds a projection of either. That covers #3609, #4934 and #2221.

Manuals. I agree no edit is needed. The Operator's Manual mentions V.PolyTime enc and V.tableVerifier only by name, and its PCPVerifier link is pinned to a SHA. The Agent Operator's Manual, ROADMAP.md, results/ and CslibFrontierResults/ do not describe these predicates.

CI. ci-checks passes at this head. The Repeated-proof-block notice found none in 112 proofs, the Parallel-definition notice none among 2 declarations, and the Duplicate-statement notice none among 20 theorems. The PR-names notice flags V.tableVerifier (dot notation) and PCPPoly (#3609's declaration); both are false positives.

Non-blocking nits:

• Classes/PCP/ZeroRandomness.lean:61 still destructures both structures by position (⟨V, c, d, ⟨-, -, hv⟩, hcoins, hqs, hcomp, hsound⟩). The binder names keep it readable. Taking hV, hpcp and using hV.verdict, hpcp.coins_le etc. would match the rest of the PR.
• The Kilian.lean module docstring (around line 51, "The tables accepted by V.tableVerifier are exactly the witnesses of PCP_log_subset_NP") could cite IsPCPVerifier.mem_iff_exists_tableVerifier, as Kilian/NP.lean now does.

Limits: I relied on hosted CI and did not build locally. There were no open review threads at this head.