[SamuelSchlesinger]

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

Small, independent twin removals across seven circuit-complexity files. Each was flagged by scripts/proof_copies.py, and each now makes its argument once:

• Circuit/CriticalPath.lean. In exists_bottleneck_of_not_disjoint_criticalPath, the 16-line hX/hY twin (a wire of one prefix depends only on its own input) is one local hprefix, instantiated for each prefix. nodup_criticalPathAux reuses rank_lt_of_mem_tail_criticalPathAux instead of re-deriving the rank step.
• Circuit/Boolean/Unbounded/Certificate.lean. In getD_evalCode_eq_iff_of_claimable, the and m | or m cases share one alternative, so their 9-line tail is no longer duplicated.
• Circuit/Decomposable.lean. The private finite_values_prod_contexts proves that the rectangle values v ×ˢ contexts v is finite. finite_values_of_nonempty_contexts and finite_contexts_of_nonempty_values then follow from Mathlib's Set.Finite.of_prod_left/of_prod_right, which replaces two 10-line injectivity proofs.
• Circuit/Rational/SmallExpansion.lean. The private rootMultiplicity_basis_le serves both bases in order_reversal_sum.
• Circuit/Fusion/Graph.lean. literals_sourceRefinement shows once that each literal reads only one side, which replaces four copies of the containment argument.
• Circuit/Boolean/CriticalPath.lean. The private table_eq/comp_eq_table hold the tabulation and the 64-case check used by both not_isAndType_comp_of_isAffineOp and not_isXorType_comp_of_not_isAffineOp.
• Circuit/DagProtocol.lean. The private exists_sep_of_mem handles the empty-rectangle cases, which a constant separates. exists_sep_const, exists_sep_differsAt and exists_sep_exceedsAt use it.

No public statement, attribute, name or exposed body changes; the only declaration-line changes are new or moved private helpers. Net −50 lines (+117/−167). proof_copies.py reports no repeated block in the touched files. Dropped: Occurs.toFun_eq_true in NNF/Rectangle.lean, where a shared step would need the sibling-swap facts and would not be shorter. The hprefix in CriticalPath.lean saves only 6 lines; its value is that it states the x/y symmetry once.

This is refactoring only, with no new mathematics.

Validation: lake build --wfail --iofail of each touched module; scripts/check.sh --quick passed. That run covered the affected modules and clients, including CslibFrontierTests.{WeftOneCertificate,NonVacuity,DagProtocol}, Fusion/Graph/*, Rational/Rectangular and the PRF circuit lower bound, with lint on 63 modules, hygiene, changed-file lints, ratchets and mk_all --check. Single-file elaboration (lake env lean, one run each on a noisy host, before → after): CriticalPath 14.4 → 13.0 s, Certificate 13.1–26.3 → 14.1–15.5 s (one 35.3 s outlier), Decomposable 6.2 → 4.2 s, SmallExpansion 14.5 → 15.4 s, Fusion/Graph 5.2 → 4.6 s, Boolean/CriticalPath 6.2 → 6.0 s, DagProtocol 6.8 → 7.9 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 (Jetski reviewer session 8a19d70d-301c-44e4-b4ac-9604ca6b59c8) of 2d4057fe3507486955477cb6bd139ae9a65fcedb: approve

This is refactoring only: seven independent twin removals in Computability/Circuit/, and no statement changes. I read the full diff against origin/main and the surrounding proofs at the head. Public statements, names and attributes are unchanged, and no @[expose] body is touched. Every new helper is private and sits in the file that uses it. I found no sorry, native_decide, heartbeat option or line over 100 characters. Non-terminal simps are simp only, and simp_all appears only as a terminal call in the moved 64-case check.

Here is how each item holds up:

• nodup_criticalPathAux is the clearest improvement. Instead of re-deriving the rank step and splitting on head/tail, it now applies rank_lt_of_mem_tail_criticalPathAux (fuel + 1) v v, which takes 4 lines where the old proof took 12.
• hprefix is the weakest item, but I think it is still worth keeping. The block shrinks from 41 lines to 35, which matches the PR's "6 lines". The two 17-line inductions really did differ only by swapping x/y, Px/Py, hclosedX/hclosedY and disjoint_left/disjoint_right. The proof is now written once, and the new comment explains why a slot read from outside P lies on neither prefix. On the downside, the local statement takes six hypotheses, and each instantiation is about as long as the statement it proves. Optional nit: the input_mem_criticalPath_iff lambda appears twice and could be bound once before hX.
• Certificate. Merging the and m | or m alternatives is a straightforward deduplication. The combined simp only covers both interpretations, and the 9-line tail is now shared.
• Decomposable. This is a real improvement. finite_values_prod_contexts together with Mathlib's Set.Finite.of_prod_left/of_prod_right replaces two hand-written injectivity arguments.
• SmallExpansion. rootMultiplicity_basis_le is a direct extraction of the old hbd/hcd. I found no Mathlib rootMultiplicity ≤ natDegree lemma that would make it unnecessary.
• Fusion/Graph. hdep separates "each literal reads one half" from building the witness. The four branches shrink to one-line simps, and the witness is built twice instead of four times.
• Boolean/CriticalPath. table_eq and comp_eq_table replace the two convert … using 2 blocks plus their hG' setup, so both theorems are now a rw followed by an exact.
• DagProtocol. exists_sep_of_mem handles the empty-side cases once, which removes 8–10 lines from each of exists_sep_differsAt and exists_sep_exceedsAt. After this change, exists_sep_const has a single caller and a one-line body. Keeping it as a named fact is fine.

Minor point about the description: it cites a per-file elaboration table "in the implementation notes", but those notes are not linked from the PR. Either link them or drop the reference. This does not block approval.

The PR states that no manual needs an edit, and I agree: none of the touched declarations appear in manual/ or guide/. I did not build locally. CI on this head was still pending when I wrote this review, so I am relying on CI for the --wfail build and for the repeated-block and duplicate-statement notices.