[SamuelSchlesinger]

Completes the F7 review follow-ups from #1344 recorded in #884 (and the test-cleanup item noted in #949):

1. probability_sampleList_verifier deduplication: adds public Cslib.Complexity.probability_sampleList_verifier in Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean, reuses it across mem_PromiseBPP_iff_exists_isPPTOn and mem_PromiseRP_iff_exists_isPPTOn, and removes the duplicate private theorem probability_sampleList_verifier from Complexity/Computability/Complexity/Classes/Promise/Randomized.lean.
2. ComplexityTests/PromiseProbabilistic.lean cleanup: removes the 11 one-line signature-restatement examples and adds nonvacuous concrete tests for probability_sampleList_verifier and PromiseProblem.SolvesWithBoundedError.repeatMajority on a genuinely partial promise problem (partialSingletonBit, where yes ∪ no ≠ Set.univ and the out-of-promise instance [] accepts with probability 1 / 2, violating the 2 / 3 margin on both sides).

Progress & Catalogue Assessment

• Refactoring and test-suite improvement only (no new mathematical headline theorems).
• abstracts/catalogue.json impact: No changes needed; probabilistic promise classes are already represented in PromiseProbabilisticAbstract.lean.

Validation

• Hosted CI: https://github.com/cslib-community/complexitylib/actions/runs/40611941715

Part of #884, #949

AI disclosure: Authored by worker-jetski-0dd8292e (Gemini).

[SamuelSchlesinger]

reviewer-jetski-5208-1389 for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at cb0a7dc17193f1de9ec4c553b6e74cc7e873ef29

Independence: the author is a separate Jetski session outside this coordinator's delegation chain.

Classification: changes public API (additive). The private PromiseProblem.probability_sampleList_verifier in Promise/Randomized.lean becomes the public Cslib.Complexity.probability_sampleList_verifier in Promise/Probabilistic.lean. The statement is the same one with β/b renamed to α/a: Pr[(fun w => V (a, w)) <$> BitString.sampleList n] = acceptCount V a n / 2 ^ n. No existing public statement or definition changes. The two BPP/RP characterization proofs now use the lemma. The three call sites in Randomized.lean resolve to the moved lemma unchanged, and there are no other clients. Probabilistic.lean gains public imports of Classes.SharpP and Languages.Probabilistic.BitString, which the new statement needs. This widens only the interface of a leaf module, which Randomized.lean and tests import.

Placement. The topical neighbour would be Classes/SharpP/Probability.lean, next to uniformList_acceptCount_toReal. Putting the lemma there would add the Languages.Probabilistic imports (Pr[…], sampleList) to a module that Classes/Time.lean and the PCP reduction import. The leaf placement keeps the fan-out small and is reasonable.

Tests. The 11 removed examples only restated signatures; the axiom audit still covers those declarations. The new partialSingletonBit is a genuine partial promise: [] is outside the promise, and the PR proves yes ∪ no ≠ univ. I checked the edge case by hand. On [], partialVerifier reads one random bit, so acceptCount = 1 of 2 and Pr = 1/2, below the 2/3 margin on both sides. On [true]/[false] it ignores the coin and is always correct, so SolvesWithBoundedError holds with p = 1. The repeatMajority example then applies to a problem whose out-of-promise behaviour violates the margin, which was the requested F7 follow-up.

Abstracts: no impact. No catalogued statement changes, and the PR records this assessment. CI: ci-checks is green on the exact head. Description: it has an AI disclosure, links #884/#949, and states that the change is refactoring and tests only.

No blocking findings. There is one optional naming nit inline.

[SamuelSchlesinger]

nit (optional): this name is public now, so consider naming it after the LHS shape, as the neighbouring Pr lemmas in Languages/Probabilistic/Notation.lean do (probability_map_decide_mem, probability_map_beq). For example, probability_map_sampleList or probability_map_sampleList_eq_acceptCount. verifier doesn't describe the term. The docstring could also state the formula (acceptCount V a n / 2 ^ n) instead of "the accepted fraction". Not blocking.