[SamuelSchlesinger]

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

Foundations/Analysis/Convex/ExtendedFormulation/CorrDigraph.lean proved many facts once per direction (in/out), per chain end (first/last) or per literal polarity (false/true); scripts/proof_copies.py flagged several of these twins. They are now proved once:

• Chain endpoints. The private corrDigraphAdj_chainEnd covers both chain endpoints in both directions. It replaces chain0_in, chain0_out, chainLast_in and chainLast_out (about 110 lines).
• Vertex 3j. corrDigraphAdj_mul3 states both its in- and out-neighbours, so the shared "no clause at a multiple of 3" argument appears once.
• Slots. corrDigraphAdj_slot_out is generic in the slot r ∈ {1, 2}, and slot1_out/slot2_out are one-line instances. The unused private slot1_in, slot2_in and slotClause_inj_slot are deleted.
• List.consecutivePairs_slotVisit_mem and chain_one_zero_not_mem_forward. One argument handles the false/true and no-clause/owned/not-owned cases (local hchain, hown). This replaces about 75 lines of Or.inl/Or.inr twins.
• mem_varBlock_iff and mem_slotVisit_iff. Each orientation is first rewritten to one normal form.
• exists_dirTour_of_assignment and exists_assignment_of_dirTour. Shared hsucc, hlink, hlast_eq and hdich_fwd/hdich_bwd facts replace duplicated index, adjacency and dichotomy blocks. Five hand-written nonempty-finRange proofs become mt List.finRange_eq_nil_iff.1 _.

No public declaration changes; every changed or removed declaration is private. Net −324 lines (+215/−539). proof_copies.py --all reports nothing left in the file. Left as is: the i < j/j < i branches of slotClause_eq_some_iff (mirror images with different CorrPairIdx constructions) and the chain.inj lines of slotVisit_nodup/slotVisit_disjoint, which are not direction twins.

This is refactoring only, with no new mathematics.

Validation: lake build --wfail --iofail of CorrDigraph, its client TSP, the extension-complexity lower-bound test and CslibFrontierResults.Entries; scripts/check.sh --quick passed (7 affected targets, manual checks, hygiene, lints, ratchets, mk_all --check). Single-file elaboration (lake env lean, 4 interleaved runs): 10.5–12.5 s → 9.5–12.6 s, user time 16.4 → 15.3 s. CI does the full run.

Manuals: the Operator's Manual mentions only the public corrDigraphAdj and the public theorems, which are unchanged, so it needs no edit. Nor does the Agent Operator's Manual.

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

[SamuelSchlesinger]

Agent review (Jetski reviewer session b5db8351-45e5-4ea4-90e3-e3abed6a91f3) of 1f341eed41b6b8c6ac2dcd256a214ee066472e59: approve

This proof refactor of CorrDigraph.lean adds no new mathematics. Every changed or removed declaration is private. The diff touches no public signature, attribute or @[expose] body: the only declaration headers in it are the private ones listed in the description. The line count is accurate (+215/−539).

What got simpler:

• corrDigraphAdj_chainEnd replaces four near-identical endpoint lemmas (chain0_in/out, chainLast_in/out). One hnb fact about the unique interior neighbour carries both endpoints and both directions. I checked the hypotheses: the case chainLen = 1 is vacuous, so omega closes it.
• corrDigraphAdj_mul3 and corrDigraphAdj_slot_out (generic in r ∈ {1, 2}, with literal decide (r = 2)) remove the in/out and slot-1/slot-2 twins. slot1_out and slot2_out are now one-line instances, kept because they fix the concrete Fin indices that exists_assignment_of_dirTour uses.
• consecutivePairs_slotVisit_mem, chain_one_zero_not_mem_forward, mem_slotVisit_iff and mem_varBlock_iff each run one argument over all value/clause cases instead of mirrored case blocks.
• The two tour theorems now share hsucc, hlink, hlast_eq and hdich_fwd/hdich_bwd instead of repeating the index and dichotomy blocks. The nonempty-finRange proofs now use List.finRange_eq_nil_iff.

What I checked:

• The deleted slotClause_inj_slot, corrDigraphAdj_slot1_in and corrDigraphAdj_slot2_in were unused on main. Their only occurrence was the definition. There are no references elsewhere in the repo, and neither TSP nor the tests use import all. The same holds for the replaced endpoint and mul3 lemmas.
• I built CorrDigraph, TSP and CslibFrontierTests…ExtensionComplexityLowerBounds with --wfail --iofail in my own worktree. A direct lake env lean -DwarningAsError=true re-elaboration of CorrDigraph was clean, in about 27 s wall time.
• proof_copies.py --base origin/main reports no repeated proof block.
• Style: no lines over 100 characters, no sorry, native_decide or heartbeat options. The one bare simp (in chain_one_zero_mem_backward) is pre-existing and terminal.
• Manuals: the Operator's Manual mentions only the public corrDigraphAdj and public theorems, and neither manual names the touched private declarations. No manual edit is needed.

Non-blocking nit: the try split_ifs … <;> first | … | … pattern in consecutivePairs_slotVisit_mem depends on the goal shape more than the explicit cases it replaces. It is acceptable for a private lemma, and the comments explain the walk.

Limitations: hosted ci-checks was still running when I wrote this. I did not run the whole-library build.