[SamuelSchlesinger]

Change. Four pairs of copied proof steps within single FineGrained files now share one helper each. This is refactoring only, with no new mathematics. Net −24 lines (75+/99−).

• CircuitCounting: the new private computableInPolyTime_reachGateTest proves once that the reachable-gate predicate is polynomial-time computable. computableInPolyTime_toCSPRaw and computableInPolyTime_reachGateCountRaw used to repeat its 13-line derivation (−6).
• Randomized, exists_solvesWithErrorInTimeO_poly_iff: the yes and no branches repeated the padding fact, the power split and the scaling step. The new local hscale carries an error bound from the padded verifier's seed length to p.eval, and hV'_prefix states the padding fact once. Each branch is now one call. The separate local count identity had only that one user, so it is folded into hscale.
• Randomized, amplify_twoSided: the new local hmaj bounds majority-vote failures for any seed set G with (1 - ε₁) * 2 ^ ℓ a ≤ G.card. The yes and no branches used to repeat the cardinality rewrites and the final scaling. Together the two Randomized items save 13 lines.
• Diameter, mem_edges_toDiameter: the new private mem_bitEdges (cases b <;> simpa) replaces two copies of the bitEdges case analysis (−5). The survey suggested rcases … <;>, but the two branches land in different disjuncts, so a membership lemma is the shared part.

Each helper reads more clearly than the copies it replaces, so nothing from the survey item was dropped. Left out as planned: CliqueGrouping:1018 (after #4838) and CountingCSP/CountingFiniteCSP (after #4515). No public declaration changed.

Manual impact. Operator's Manual: no edit. native-counting.md links Randomized.lean and names amplify_twoSided without line anchors, and no public name changed. Agent Operator's Manual: no edit, since it covers workflow. ROADMAP.md and the results inventory don't name these private proofs.

Validation (at 549ab5b, on main bf1db7c): buildslot lake build --wfail of the three modules, their clients GapETH, ContractionCircuitCounting and MaxSAT.Reduction, and the tests FineGrainedRates, CircuitCounting and FineGrained.Diameter. Also lake exe mk_all --check, check_operator_manual.py, the encoding readability and projection chain ratchets, and proof_copies.py --base origin/main, which finds no repeated block. Full validation by hosted CI.

AI assistance. Jetski worker session a924892d, plan #4737.

Part of #4737.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 39f68e58) of 549ab5b: approve. This is agent review, not human review.

The change is refactoring only. I compared each removed block with its replacement. The diff only touches proof bodies, so no public statement changes, and every new helper is private or a local have.

• CircuitCounting: computableInPolyTime_reachGateTest states the gate predicate with the same function and encoders as the two hpred copies it replaces, and filterWithInput/countPWithInput consume it unchanged. The docstring describes the shared predicate correctly.
• Diameter: mem_bitEdges is exactly the case split of bitEdges (two hub edges, plus the vector edge when b = true). Both branches of mem_edges_toDiameter now pick the disjunct they need from it. A lemma is the right shared piece here, because the two branches land in different disjuncts.
• Randomized, _poly_iff: hscale now carries a bound ≤ B * 2 ^ ℓ a up to p.eval, and hV'_prefix states the padding fact once. The yes branch applies it to the negated verifiers through congrArg (!·), and the no branch is one term. The count identity had no other user, so moving it inside is right.
• Randomized, amplify_twoSided: the hypotheses of hmaj (any seed set G with (1 - ε₁) * 2 ^ ℓ a ≤ G.card) are exactly what both branches establish. Stating hG with 2 ^ ℓ a also removes the two Fintype.card rewrites.

Nothing in these files can reuse the helpers further: the other bitEdges uses are constructive simp calls. The fun_prop in reachGateTest runs with the same local facts as before.

CI is green on this head. Notices: no repeated proof block (151 proofs examined); no changed public definition; no duplicate statement (7 examined). The PR-names notice flagged hscale_gen, which was the old local name, and the current description no longer uses it.

Threads: there are no inline threads, reviews or PR comments on this PR.

Manuals: no edit needed in either. native-counting.md names amplify_twoSided without line anchors and no public name changed, and the Agent Operator's Manual's workflow scope is unaffected. ROADMAP.md and the results inventory don't refer to these proofs.

Queueing this head.