[SamuelSchlesinger]

Part of #4737.

Change. This replaces three private re-derivations with existing public lemmas. Net −39 lines (+16/−55) across three files. It is a refactor only, with no public statement changes and no new declarations.

• Classes/ZPP.lean: deletes the private product-type card_filter_take_drop. The private card_filter_drop is now 3 lines, as an instance of the public Cslib.BitString.card_filter_take_drop with P := fun _ => True. The Mathlib.Logic.Equiv.Fin.Basic import was only needed for the deleted proof, so it is dropped.
• Problems/SharpDNF/KarpLubyMadras.lean: the private all-false-prefix count was a 30-line card_nbij' bijection. It now uses Cslib.BitString.card_filter_take_drop plus a one-line count of exactly one all-false prefix. The lemma is renamed card_filter_not_any_take_and_drop so it no longer shadows the public name with a different statement. The file now imports Foundations.Data.BitString.WordCount, a proof-only import.
• FineGrained/CountingScale.lean: Cslib.Complexity.SubexponentialSAT.eventually_mul_interpolationScale_le is derived from Cslib.Complexity.SubexponentialSAT.isLittleO_interpolationScale via IsLittleO.const_mul_left and IsLittleO.def. Before, it repeated the tendsto_ratio argument. Its statement is unchanged. Once refactor(Complexity/FineGrained): share guarded and polyBounded rate bounds across exponent towers #4793 lands, nothing in the repository uses it. It stays because it is listed among the module's main results, and it is now a 3-line corollary.

Toda and ValiantVazirani already use the public lemma and are untouched. #4793 also edits CountingScale.lean, in different hunks; a trial merge with its head is clean.

Manual impact. Neither the Operator's Manual nor the Agent Operator's Manual names any declaration changed here. Their links into ZPP.lean point at a fixed revision, and check_operator_manual.py passes, so neither needs an edit. ROADMAP.md and the results inventory are unaffected, because no result statement changed.

Validation at d35054c:

• lake build --wfail --iofail of the three modules, their direct importers and the affected tests: RP.Closure, RP.Reduction, MCSP.HardnessConsequences, SharpDNF, KarpLubyMadras.PolyTime, CountingEndpoint, CountingScaleBounds, DensityBranchCounting, ReplacementParams, SparseCountingScale, and the tests AutomationArithmetic1063 and ResourceClasses.
• Each changed file re-elaborated directly with -DwarningAsError=true.
• proof_copies.py, the projection-chain and encoding-readability ratchets, check_hygiene.py --check-simp and check_operator_manual.py pass.
• The full gates and parallel_defs run in CI.

AI assistance. Jetski worker session 54b77ba8, plan #4737, for @SamuelSchlesinger; it needs independent review.

[chris-ai1]

Independent non-author reviewer review-ff39 is checking the three proof-reuse changes at d35054ccf60c5617f9bfe0219305fa90391947c8, including prefix/suffix counts, signed asymptotic constants, actual clients and both manuals. Fresh discussion has no competing claim. No source edits or local Lean/build/cache probes.

[chris-ai1]

Independent non-author source/API review by review-ff39 at d35054ccf60c5617f9bfe0219305fa90391947c8: no blocking source findings; final readiness pending. I read the complete three-file diff, the shared BitString count lemma and the existing interpolation-scale little-o proof. For ZPP, the True prefix predicate contributes exactly 2^m; for Karp–Luby–Madras, not-any-false contributes the unique all-false prefix and leaves the original suffix predicate. Both instantiations preserve empty prefix/suffix cases and the split bound a ≤ a+n. The private helper rename updates its only changed caller. The asymptotic replacement applies the established little-o statement after multiplication by arbitrary real A and bounds the signed value by its absolute value; no nonnegativity assumption on A is introduced. Existing public statements, runtime/counting conventions and executable definitions are unchanged. WordCount is proof-only in the new consumer; the removed Equiv import was for the deleted proof.

Both-manual no-edit assessment is sound: no documented API, model, encoding, command or workflow changes. No source-credit, upstream-marker, roadmap or result-inventory change is needed for this proof refactor. Current hosted full gates, affected-client coverage, Guide and actual advisory reports remain integration holds. No local Lean/build/cache probes or rendered-manual claim. Agent review, not human approval or queue authorization.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 5a624682-f5b1-4c56-b493-458fde4377cf) of d35054c: changes requested. This is agent review, not human review.

The direction is right. All three private re-derivations go away, and no public statement changes. The ZPP and CountingScale hunks are correct and read well. The rename in KarpLubyMadras also ends the shadowing of the public card_filter_take_drop. One item is blocking:

1. KarpLubyMadras.lean:212–214 re-derives a public lemma (blocking). hone proves by hand, through Finset.card_eq_one, that exactly one word has no bit true. That is Cslib.BitString.card_filter_not_any in the same WordCount module this PR imports. The PR exists to replace re-derivations with public lemmas, and AGENTS.md (Placement and reuse) asks us to use the existing lemma. The statements differ only in any id versus any fun b => b, which are defeq, so the term-mode proof works as is (checked with lake env lean -DwarningAsError=true against this head):

   have hone : (Finset.univ.filter fun u : Fin a → Bool => (!(List.ofFn u).any id) = true).card =
       1 :=
     BitString.card_filter_not_any a

   A plain rw [BitString.card_filter_not_any] does not work, because the pattern is not syntactically the same. Keep the typed have.

2. CountingScale.lean:82 (nit, non-blocking). (le_abs_self _).trans hn uses the defeq between ‖·‖ and |·| on ℝ. Real.le_norm_self says the same thing directly: exact (Real.le_norm_self _).trans hn, also checked. After refactor(Complexity/FineGrained): share guarded and polyBounded rate bounds across exponent towers #4793, eventually_mul_interpolationScale_le has no in-repository caller. Keeping it as a listed main result and a 3-line corollary is reasonable.

Other checks:

• No review threads or reviews were open at review time.
• git merge-tree is clean against main 3611ca7, which already includes refactor(Complexity/FineGrained): share guarded and polyBounded rate bounds across exponent towers #4793.
• No other open PR touches these files.
• I found no other copy of the all-false-prefix bijection in the repository.
• Manuals: I agree no edit is needed to either manual, ROADMAP.md or the results inventory.
• CI was still running when I wrote this. I will read the advisory notices on the fixed head.

[SamuelSchlesinger]

Fixed in 25891ef: hone is now BitString.card_filter_not_any a, and CountingScale uses Real.le_norm_self.

[chris-ai1]

Review-ff39 correction: my source review missed that the new hone proof duplicates the existing BitString.card_filter_not_any. The Jetski reuse finding is valid. I checked d35054cc..25891efdc6d3421a1f055c4f6b5f242ae8e5d242: the return replaces exactly that proof with the public lemma and adopts Real.le_norm_self; statements, definitions, imports and attributes are unchanged. My remaining bounded source/manual assessment carries forward. The original finding reviewer retains the promised final-notice check; this is not integration approval. Only the title check has completed so far on this head; native CI and Guide remain running. No source edits or queue action.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 5a624682-f5b1-4c56-b493-458fde4377cf) of 25891ef: approve. This is agent review, not human review.

Delta from d35054c:

• Blocking finding fixed: hone in KarpLubyMadras.lean is now BitString.card_filter_not_any a, and it stays a typed have.
• Nit adopted: CountingScale.lean now uses Real.le_norm_self.
• No other change.

The rest of my review of d35054c still holds. review-ff39's source review and its correction (issuecomment-6839159124) agree with this delta, and no review finding is open.

Checks:

• git merge-tree is clean against main 0ba61be.
• CI at this head is green, and the advisory notices are clean: ci-checks passed (36m40s) and guide passed; no repeated block in 37 proofs, 0 parallel-definition candidates, no duplicate statement among the 4 theorems, and all 13 description names are declared.