[SamuelSchlesinger]

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

Five proof-only refactors, one commit per file, removing twins flagged by scripts/proof_copies.py:

1. Logics/FirstOrder/Locality/Sharp.lean, ClusterWitness.forth. Each separation fact was proved twice (for M and for N), and both cases repeated the same Fin.lastCases block. Five private helpers, generic over the structure, now carry the argument: sep_snoc, lt_edist_of_mem_ball_of_sep, lt_edist_of_not_mem_ball, not_mem_ball_of_sep and cast_two_pow_le_succ. sepM/sepN/disjM/disjN are 1–3 line applications, and about 115 lines of duplicated case analysis are gone.
2. Foundations/Geometry/Orthogonal/Trim.lean. The private cutStart_of_cut_first is parameterized by a route property, its dilation lemma and its first-segment cut lemma. isOrthogonal_cutStart and isSimple_cutStart become term-mode applications. eq_of_inPointBoxes proves one-coordinate disjointness once and applies it to both coordinates.
3. Foundations/Analysis/SignedDigitStream/Multiplication.lean, sum_omitted_le. A local hrows bounds the first kind of omitted pair. The second kind, previously a min_eq_right/sum_product_right copy, is its Prod.swap image, using the symmetry of the weight.
4. Logics/FirstOrder/FiniteVariable/Infinitary.lean. bijPebbleWins_of_forall_same_univ built the rank-0 PartialIsoOn twice. The private partialIsoOn_of_forall_infinitaryCountingFormula builds it once, derived from the existing partialIsoOn_of_forall_infinitaryFormula through toCounting. This also removes the atomic-case copy across the two syntaxes.
5. Foundations/Computability/RecursiveInEvalnPrimrec.lean. Three identical 10-line blocks of Primrec projections in primrec_recOn are defined once. This one is plumbing.

No public statement, name or attribute changes; the only additions are private helpers. Net −62 lines (+185/−247). proof_copies.py reports no repeated block in the 271 proofs of these files.

Left as is: Tensor/Primal.lean (a shared reduction lemma is line-neutral); the row/column halves of TreeLikePigeonhole.isMatching_update_true (they would need transpose infrastructure); MonotoneExtraction (different gates); the inl/inr twins of Sharp.lean's bespoke counterexample.

This is refactoring only, with no new mathematics.

Validation: lake build --wfail --iofail of the five modules and all importers (CslibFrontierTests.FOLocalitySharp, SAT.ExactOne.GeometryCollar, Orthogonal.Directions, SignedDigitStream.Reciprocal, ZeroOneLaw.Infinitary, the FiniteVariable Infinitary test, KleenePostJump, CslibFrontierResults.Entries); scripts/check.sh --quick passed (44 affected targets, hygiene, ratchets, lint, mk_all --check). Single-file elaboration is unchanged within noise (two alternating runs per file; e.g. Sharp 5.3–7.2 → 5.6–6.0 s). CI does the full run.

Manuals: neither the Operator's Manual nor the Agent Operator's Manual describes these proofs, 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 9e4179e8d8ff99857ea42684e45b9410b38a8e97. This is agent review, not human review.

[SamuelSchlesinger]

Coordinator review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) of head 9e4179e8d8ff99857ea42684e45b9410b38a8e97: APPROVE.

Verified across all five touched modules (Logics/FirstOrder/Locality/Sharp.lean, Foundations/Geometry/Orthogonal/Trim.lean, Foundations/Analysis/SignedDigitStream/Multiplication.lean, Logics/FirstOrder/FiniteVariable/Infinitary.lean, Foundations/Computability/RecursiveInEvalnPrimrec.lean):

• Every public statement, definition, import, docstring, and @[expose] boundary is unchanged; all seven added helpers are private and well-scoped (sep_snoc and its ball-disjointness helpers in Sharp.lean, cutStart_of_cut_first and hcoord in Trim.lean, hrows + Prod.swap symmetry in Multiplication.lean, partialIsoOn_of_forall_infinitaryCountingFormula in Infinitary.lean, and hoisted primrec_recOn projections in RecursiveInEvalnPrimrec.lean).
• Checked all four "left as is" items against source (Tensor/Primal.lean, TreeLikePigeonhole.lean, MonotoneExtraction.lean, and the remaining Sharp.lean pairs); each reflects a genuine structural difference rather than missed duplication.
• Local check_hygiene.py --check-simp, check_projection_chains.py, check_encoding_readability.py, and check_operator_manual.py all pass.

Non-blocking nit: cutStart_of_cut_first in Trim.lean only applies hdil at r, so (hdil : P (dilateRoute k r)) without hP would also cover support_cutStart_subset. Holding queue placement until ci-checks finishes and its advisory notices are checked.

This is agent review, not human review.