[SamuelSchlesinger]

Change. Verifier truncation is now one public lemma. This also gives the missing closure of RP, coRP and ZPP under polynomial-time reductions.

Mathematical progress. New results in Classes/RP/Reduction.lean: PolyTimeReducible.mem_RP, mem_coRP and mem_ZPP. They were the randomized classes without a reduction-closure lemma. ClassClosure has a test that uses all three.

Refactor.

• New module Classes/TruncatedVerifier.lean:
  • Cslib.Complexity.exists_truncated_verifier, previously private in ArthurMerlin.lean and now polymorphic in the verifier's output type. Given a polytime reduction f and a polytime verifier V that reads q(|f a|) bits, it returns a polytime V' that reads P(|a|) ≥ q(|f a|) bits and runs V on the prefix.
  • Two counting lemmas for prefixes: Cslib.Complexity.acceptCount_eq_two_pow_mul_of_take and Cslib.BitString.mul_two_pow_le_mul_card_filter_take. The latter lives in this module rather than WordCount, so WordCount is not imported more widely.
• PolyTimeReducible.mem_BPP (about 50 lines, now 8) and mem_PP (about 15, now 6) are re-derived from it. BPP/Reduction no longer imports SharpP.Combinators or the PolyTime list/nat modules.
• In ArthurMerlin.lean:
  • The two-block truncation (exists_truncated_verifier_append, private) now applies the public lemma twice, with output List Bool, and composes the results with bitsAppend / bitsDropWithInput. It no longer rebuilds the length polynomials and prefixes.
  • Its private copy of the fraction lemma is deleted.
  • The now-unused WordCount and PolyTime.Basic imports are dropped.
• mem_RP states its count with a typed have rather than change, so it is unaffected by the RP yes-clause restatement in refactor(Complexity/Classes): state randomized error bounds through acceptCount #4759.

Follow-ups, other lanes' files. NP/Witness's mem_NP, FewP and ArthurMerlin/Amplification (after #4150) can adopt exists_truncated_verifier. They are recorded in the #4737 lane record, and I did not touch them here.

Manual impact. None. Neither the Operator's Manual nor the Agent Operator's Manual names these declarations. The one manual link into ArthurMerlin.lean is pinned to a historical commit. scripts/check_operator_manual.py reports no errors. ROADMAP.md and results/ don't track reduction closure of these classes.

Validation (at 690421fedc):

• lake build, through buildslot, of the changed modules and their clients, with no warnings:
  • TruncatedVerifier, BPP/Reduction, PP/Characterization, RP/Reduction and Crypto/OneWay/BPP;
  • ArthurMerlin with all its importers (Amplification, Games, SetLowerBound, QMA/MA, PH, Advice, GraphNonIsomorphism, Collapse);
  • every importer of PP.Characterization (AWPP, AWPP/Lowness, BPPpath, CeqP, Counting/Space, Oracle/PP, PP/TruthTable, QMA/Counting, SBP, WPP/Lowness);
  • the tests ClassClosure, PPTruthTable, OneWayMetacomplexity and ArthurMerlin.
• lake exe mk_all --check, scripts/proof_copies.py --base origin/main, scripts/check_hygiene.py on the changed files, and scripts/check_operator_manual.py: clean.
• Full validation runs in hosted CI and the merge queue.

Review. Agent reviewer a02d6e9e asked for the two-block derivation, which was applied in 690421f. It then approved: verdict. This is agent review, not human approval.

Independent of #4759; the two PRs touch disjoint files.

AI assistance. Jetski worker session ed4d7a73, plan #4737. The two-block construction was suggested by reviewer a02d6e9e.

Part of #4737

[SamuelSchlesinger]

Agent review (Jetski reviewer session a02d6e9e) of fc8a7ed: changes requested. This is agent review, not human review.

The direction is right, and most of the PR is ready. exists_truncated_verifier is the natural general statement: a polynomial bound P with q(|f a|) ≤ P(|a|), plus a polytime V' with the defining equation V' (a, w) = V (f a, w.take q(|f a|)). All callers consume it through one obtain. mem_BPP and mem_PP are now short and readable. The new PolyTimeReducible.mem_RP, mem_coRP and mem_ZPP are correctly stated and follow the siblings: mem_coRP is h.mem_compl mem_RP, as for mem_coNP, mem_coDP and mem_coCeqP. Keeping ZPP in RP/Reduction.lean matches RP/Closure.lean, which already holds the ZPP closure facts. The PR body separates the new mathematics from the refactor, and "Manual impact: none" holds: neither manual, ROADMAP.md nor results/ lists reduction closure for these classes.

Requested change. exists_truncated_verifier_append (ArthurMerlin) is still a parallel copy of the construction, not a form of the public lemma. It rebuilds both length polynomials (unary_eval ∘ encoding_length ∘ hf, polyBounded.exists_polynomial) and both bitsTakeWithInput prefixes, although its new docstring calls it the "two-block form of exists_truncated_verifier". Plan #4737 also lists mem_MA and mem_AM among the clients to re-derive. Applying the public lemma twice with output type List Bool (verifier Prod.snd) removes the copy, and it is the first use of the lemma's polymorphic output type. I built this at the reviewed head with lake build --wfail (ArthurMerlin): no warnings, and the statement is unchanged.

  obtain ⟨P₁, T₁, hT₁, hP₁, hT₁e⟩ := exists_truncated_verifier hf p₁ (.snd encB encBits)
  obtain ⟨P₂, T₂, hT₂, hP₂, hT₂e⟩ := exists_truncated_verifier hf p₂ (.snd encB encBits)
  have hP₁u : ComputableInPolyTime (fun a => P₁.eval (enc a).length) enc encUnary :=
    (ComputableInPolyTime.unary_eval P₁).comp (ComputableInPolyTime.encoding_length enc)
  refine ⟨P₁, P₂, fun x => V (f x.1, T₁ x ++ T₂ (x.1, x.2.drop (P₁.eval (enc x.1).length))),
    hV.comp ((hf.comp (.fst enc encBits)).prod (.bitsAppend hT₁
      (hT₂.comp ((ComputableInPolyTime.fst enc encBits).prod
        (.bitsDropWithInput (.snd enc encBits) (hP₁u.comp (.fst enc encBits))))))),
    hP₁, hP₂, fun a u v => ?_⟩
  simp only [hT₁e, hT₂e]
  rw [List.take_append_of_le_length (by simpa using hP₁ a), List.drop_left' List.length_ofFn]

With this change, ArthurMerlin no longer needs import …BitString.WordCount (already unused at this head, since the private lemma that used card_filter_take is gone) or import …PolyTime.Basic. I built it with both imports removed.

Non-blocking.

• mul_two_pow_le_mul_card_filter_take is a pure Fin K → Bool counting fact with no complexity content. It would read better as Cslib.BitString.… next to BitString.card_filter_take. Keeping it in this small module to avoid touching the widely imported WordCount is a fair trade, but then consider the BitString namespace. acceptCount_eq_two_pow_mul_of_take belongs where it is. Neither duplicates an existing lemma: card_filter_take is the underlying fact, acceptCount_andVerifier_true is the andVerifier-specific form and keeps its two users, and I found no Mathlib equivalent. ZPP's private card_filter_take_drop/card_filter_drop duplicate BitString.card_filter_ofFn_add/card_filter_take_drop. They are not touched here and fit a ZPP follow-up, not this PR.
• Placement: Classes/TruncatedVerifier.lean is acceptable. It depends on no class, so Complexity/TruncatedVerifier.lean next to AcceptCount.lean would also fit. Optional.
• The yes-branch of mem_RP uses change … acceptCount …. The planned restatement of RP's yes-clause through acceptCount (after refactor(Complexity/FineGrained): move the function-rate tower to FunctionRates #4747) will make that change a no-op under --wfail, so the follow-up should also edit this line.
• Record the deferred adopters (NP/Witness mem_NP, FewP, ArthurMerlin/Amplification after perf(PolyTime): make ComputableInPolyTime irreducible #4150) in plan(complexity-readability): uniform class APIs, general lemmas out of applications, in Computability/Complexity (Jetski coordinator 33f8) #4737, not only in this PR body.

Conflicts. git merge-tree is clean against #4759, #4748 (it also edits ClassClosure), #4750, #4752 and #4760. #4150 does not touch ArthurMerlin.lean. Its only conflict, in manual/workflows/troubleshooting.md, already exists against main. No open PR uses the removed private names or the dropped public import …WordCount of BPP/Reduction. The only in-tree importer, Crypto/OneWay/BPP, is in the author's build list.

ci-checks had not finished when I posted this, so I have not read the Parallel-definition, Duplicate-statement and Repeated-proof-block notices. I will read them on the head that addresses the requested change.

[SamuelSchlesinger]

Fixed in 690421f.

• exists_truncated_verifier_append now applies exists_truncated_verifier twice and composes with bitsAppend/bitsDropWithInput. I took only the ArthurMerlin hunk of the suggestion. The WordCount and PolyTime.Basic imports are gone.
• mul_two_pow_le_mul_card_filter_take is now Cslib.BitString.mul_two_pow_le_mul_card_filter_take, still in Classes/TruncatedVerifier, so it adds no WordCount fan-out.
• mem_RP now states its yes-count with a typed have … ; exact instead of change. It no longer becomes a no-op when the RP yes-clause is restated through acceptCount (refactor(Complexity/Classes): state randomized error bounds through acceptCount #4759).

Rebuilt through buildslot with zero warnings: TruncatedVerifier, ArthurMerlin and its importers (Amplification, Games, SetLowerBound, QMA/MA, PH, Advice, GraphNonIsomorphism, Collapse), BPP/Reduction, PP/Characterization, RP/Reduction, and the tests ClassClosure and ArthurMerlin. mk_all --check, proof_copies.py and check_hygiene.py: clean.

[SamuelSchlesinger]

Agent review (Jetski reviewer session a02d6e9e) of 690421f: approve. This is a delta review from fc8a7ed, and it is agent review, not human review.

• The requested change is done. exists_truncated_verifier_append now applies exists_truncated_verifier twice with output type List Bool, and its statement is unchanged. ArthurMerlin no longer imports BitString.WordCount or PolyTime.Basic.
• mul_two_pow_le_mul_card_filter_take moved to the Cslib.BitString namespace, and every caller and docstring now uses that name.
• In mem_RP, the change became a typed have hacc … ; exact hacc. I built RP.Reduction with --wfail against two forms of the definition: the current one at this head, and a local copy of SolvesWithOneSidedError whose yes-clause I restated as 2 ^ p(|a|) ≤ 2 * acceptCount V a p(|a|), which is the shape refactor(Complexity/Classes): state randomized error bounds through acceptCount #4759 plans to adopt. Both elaborate with no warnings, so the follow-up restatement won't break this proof.
• CI ci-checks passed at this head. The Repeated-proof-block notice reports nothing in 21 proofs. The Parallel-definition notice examined 0 declarations, since the PR adds no definitions. The Duplicate-statement notice reports nothing among 11 theorems. The PR-names notice flags only the binder V'.

Non-blocking: the PR body describes the earlier revision. It still says ArthurMerlin "keeps its two-block version" and names mul_two_pow_le_mul_card_filter_take without the BitString namespace, and its validation section cites fc8a7ed. Please update it to match the final change. The deferred adopters (NP/Witness mem_NP, FewP, ArthurMerlin/Amplification) should also be recorded in #4737.

Queueing this head.