[SamuelSchlesinger]

Part of #3725 (repeated proof machinery). Author: Jetski worker sessions 025a212a (delegating) and ec0fc1d6 (implementation), branch proofs/query-pcp-twins. This PR is its own task record.

Three small query-complexity refactors, one commit each, removing twins flagged by scripts/proof_copies.py:

1. SensitivitySeparation/Internal/RecursiveOne.lean. recursive_sensitivity_one_at and recursive_joint_one_at repeated the same counting step: the U/V unions, their bounds and the closing calc. The new private card_filter_le_of_acceptedRow makes it once. If every coordinate satisfying P changes a target child of the accepting row, or lies in a per-out-neighbour set S j with |S j| ≤ s, then #P ≤ o * s + r * sideSensitivity F true. Each caller now supplies only its child-change sets, their bound and its case split. The side and joint versions differ only there.
2. Quantum/WeightedAdversary.lean. The private sum_le_sqrt_of_eq_div_card (a sum over S of terms √L / #S is at most √L) makes ofUnweighted_load{Fst,Snd}_le one line each.
3. SensitivitySeparation/Internal/{RecursiveCandidates,RecursiveZero,RecursiveJointZero}.lean. The new public mem_targetCandidates_biUnion_of_flip sits next to its cardinality companion targetCandidates_biUnion_card_le in this internal module. It states that a flip repairing a rejected target child of a target candidate lies in their union. recursive_sensitivity_zero_at and recursive_joint_zero_at drop their identical 8-line target branch.

No existing statement or public name changes. Net −20 lines (+101/−121), with proof-body lines in the touched files going from 439 to 386.

Left as is, with reasons:

• PCP/ParallelRepetition/Embedding.lean's _condX/_condY lemmas rest on different library facts, and deriving one from the other would need a swapped-game condLaw that does not exist.
• SingleTape/CrossingSequence.lean's Splice.run_halts mirrors its branches through asymmetric left/right lemmas. Unifying them needs a tape-reflection symmetry for Turing machines, which is a separate project.
• The 7-line opening of the two zero-side hsub proofs differs in its nesting.

This is refactoring only, with no new mathematics.

Validation: lake build --wfail --iofail of RecursiveOne, RecursiveZero, RecursiveJointZero and WeightedAdversary; scripts/check.sh --quick passed. It covered 26 affected targets, including the AmbainisAdversary, SpectralAdversary and NayakWu clients and CslibFrontierResults.Entries, plus lint on 19 modules and mk_all --check. Single-file elaboration is unchanged within noise (RecursiveOne 7.2 → 4.3 s; others ±1 s). CI does the full run.

Manuals: neither the Operator's Manual nor the Agent Operator's Manual mentions these internal lemmas, so neither needs an edit.

AI assistance: prepared by AI agents (Jetski). Not reviewed by a human.

[SamuelSchlesinger]

Agent review claim: coordinator agy-634bba4c (session 634bba4c-9d3c-4f80-8d5b-6097f495b913) is reviewing head c7ec6c92e4049eeb478bcd6990e7b484045ae98f. This is agent review, not human review.

[SamuelSchlesinger]

Independent agent review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) at c7ec6c92e4049eeb478bcd6990e7b484045ae98f: APPROVE (holding queue until ci-checks completes and advisory notices are checked).

• Correctness & public API. Every existing public declaration name, signature, attribute, and exposed definition body is preserved unchanged.
  • SensitivitySeparation/Internal/RecursiveOne.lean: card_filter_le_of_acceptedRow cleanly factors the 30-line acceptedRow witness/projection cardinality bound shared by recursive_sensitivity_one_at and recursive_joint_one_at, matching @[expose]d sensitivityAt / jointSensitivityAt directly without intermediate unfold/convert plumbing.
  • Quantum/WeightedAdversary.lean: sum_le_sqrt_of_eq_div_card factors the pointwise-constant ∑ p ∈ S, f p ≤ √L bound (including the #S = 0 case without case-splitting on S.Nonempty), turning ofUnweighted_loadFst_le and ofUnweighted_loadSnd_le into one-liners. (Non-blocking note: the helper only uses 0 ≤ c rather than √L, and mul_inv_left_le could shorten its final cancellation line slightly.)
  • SensitivitySeparation/Internal/{RecursiveCandidates,RecursiveZero,RecursiveJointZero}.lean: mem_targetCandidates_biUnion_of_flip sits next to targetCandidates_biUnion_card_le with matching parameter order (label generalized from GoodLabeling T r, dropping unused NestedFamily F) and replaces the duplicate target-candidate membership blocks in both zero-side files.
• Deferred items & manuals. Verified the three items left as-is (ParallelRepetition/Embedding.lean, SingleTape/CrossingSequence.lean, and the RecursiveZero vs RecursiveJointZero outer card_le_card step): each has genuine structural asymmetry that would require new transport infrastructure rather than a small helper. Checked manual/ (algebraic-and-quantum.md, sources.md) and manual/AGENT_OPERATORS.md; no manual edits are needed.

This is agent review, not human review.