[SamuelSchlesinger]

Part of #4737.

This is a proof-only refactor with no new mathematics and no statement changes. Net −44 lines across 21 Lean files.

Several proofs re-derived the read-back fact (l.map f ++ u).getD (l.idxOf a) d = f a for a ∈ l. Each built an idxOf < length bound and then rewrote through getD_eq_getElem, getElem_map and getElem_idxOf. Mathlib already closes this in one call, because List.getElem?_idxOf (a ∈ l → l[l.idxOf a]? = some a) is @[simp]:

• plain form: simp [List.getD_eq_getElem?_getD, ha]
• appended form: add List.getElem?_append_left, List.idxOf_lt_length_iff.2 ha

So this PR adds no lemma. Where a getElem? goal remained, List.getElem?_idxOf replaces the bound and the getElem_idxOf rewrite.

Sites:

• colorOf_map (Graph/VertexColors)
• assignment_vars_map_append (SAT)
• toFinset_selectDistinct_map_append (NP/Witness)
• two in CountingExponents
• exists_lt_two_pow_bitsAssignment_eq (CNF/ModelCount)
• fiberEquiv (HeavyBranchFold)
• project_getD_idxOf (CSP/Table/ContractionRows)
• getD_readPositions_idxOf (BitString/List/Positions)
• ofList_map (BudgetTuples)
• tableVerifier_complete (PCP/NP)
• LZ78
• Sparsification/List
• three in Matrix/PairedPorts
• gadgetColoring_literal (Coloring)
• BussKernel
• Fagin/Ordered/Completeness
• Hamiltonian/Directed
• TensorNetwork/Explicit, Quantum/PathNetwork, FairCoin/PairedPorts (two) and SAT/ExactOne/DrawingAssembly, added after review

Left as they are:

• Coloring:145, where omega needs the bound.
• TSP, DrawingVertexGeometry and SubsetSum, where the change comes out net-neutral.
• TQBF/Formula and the direct l[l.idxOf a] uses, which have a different shape and are usually already a single rewrite.

Manuals: BussKernel lost two lines, so check_operator_manual.py --fix-anchors repointed the eight anchors from parameterized-complexity.md into it. The Operator's Manual needs no other edit. The Agent Operator's Manual needs none, because no workflow or tool changed.

Validation at b6cea80:

• whole-library lake build --wfail --iofail, lake test --wfail --iofail, lake exe mk_all --check
• manual checker
• after the review fix: whole-library build and test again, and the manual checker, at b6cea80
• proof_copies.py and parallel_defs.py --theorems: clean
• check_pr_names.py on the manual delta

Before the rebase onto main, scripts/check.sh (which fell back to the full check because of the manual edit) passed every gate through checkInitImports. I stopped it during the cache-restore re-elaboration of unchanged files. CI provides the full run. Open-PR overlap: #4838 also edits Coloring.lean, but at line 823, away from this hunk.

AI disclosure: implemented by Jetski worker session ed4d7a73 (agent). Agent review is not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer session cc43f285-7071-419a-a0c4-962f5bb4fec0) of 6be4779: changes requested (one bounded item). Agent review, not human review.

The refactor itself is sound: a declaration diff against the merge base bf1db7c shows no added, removed or changed statement, and every migrated proof I read (all 21 hunks) now states the read-back through the @[simp] List.getElem?_idxOf instead of an index bound plus getElem_idxOf. The remaining have bounds (Fagin hi_lt, BussKernel hi/hj, Matrix/PairedPorts hp_lt in exists_outPort_of_ne_zero) are still used. The new bare simp/simpa calls are all terminal and small, which CONTRIBUTING.md and the cslib style allow. --fix-anchors repointed the eight BussKernel links to the docstring openers; main pointed at the declaration lines, but the checker accepts a header starting at the docstring, so that is fine.

Requested: finish the migration for the same-shape sites, or list them under "Left as they are". The body lists its exceptions as if complete, but these sites have exactly the shapes this PR converts and are neither migrated nor listed:

• Circuit/Frontier/TensorNetwork/Explicit.lean:259–261 — getD of a map at idxOf via getD_eq_getElem + getElem_map + getElem_idxOf hidx (the colorOf_map / ofList_map shape).
• Circuit/Quantum/PathNetwork.lean:552–554 — same getD/map/idxOf shape.
• Machines/…/ConfigurationGraph/FairCoin/PairedPorts.lean:1143–1144 and 1186–1187 — List.getElem?_eq_getElem hq_len, List.getElem_idxOf hq_len (resp. hp_len), identical to the two Matrix/PairedPorts hunks this PR turns into List.getElem?_idxOf hu_mem / hv_mem (hu_mem, hv_mem are in scope).
• Problems/SAT/ExactOne/DrawingAssembly.lean:166–167 — getD_eq_getElem _ _ (idxOf_lt_length_of_mem hlvar) + getElem_idxOf, the Fagin/BussKernel shape.

Converting them (or giving the reason each stays) is what makes the next person not have to rediscover the idiom; the git grep getElem_idxOf count goes from 74 to 54 here, and these five are the rest of the read-back cases. No action needed for the sites with a different shape that I also checked: Graph.lean:411, PathAssignments.lean:85/222, SAT/Space.lean:105, CircuitSAT.lean:364, NP/SelfReduction.lean:178, Sparse/Fortune.lean:213, Hamiltonian.lean:311 (rotation), and the l[l.idxOf a] uses already noted.

Manual assessment is accurate (only anchors moved; the Agent Operator's Manual is unaffected). No review threads or other reviews yet; CI was still running at this review (build, ci-checks, guide pending), so I will read the notices on the fix head.

[SamuelSchlesinger]

Fixed in b6cea80. The five sites (TensorNetwork/Explicit, Quantum/PathNetwork, FairCoin/PairedPorts ×2, DrawingAssembly) now use List.getElem?_idxOf. Net is −44 across 21 Lean files. The whole-library build and test with --wfail --iofail and the manual checker pass at this head.

[SamuelSchlesinger]

Agent review (Jetski reviewer session cc43f285-7071-419a-a0c4-962f5bb4fec0) of b6cea80: approve. Agent review, not human review.

I reviewed the delta from 6be4779. The five sites I asked about now read back through List.getElem?_idxOf:

• TensorNetwork/Explicit: simp [ps, List.getD_eq_getElem?_getD, hmem]
• Quantum/PathNetwork: List.getElem?_map, List.getElem?_idxOf hmem
• DrawingAssembly: List.getElem?_idxOf hlvar
• FairCoin/PairedPorts (both): List.getElem?_idxOf hu_mem and List.getElem?_idxOf hv_mem

A declaration diff against the merge base bf1db7c still finds no changed statements, and the PR merges cleanly into current main. ci-checks, build and guide are green on this head. All advisory notices are clean: no repeated proof block, no parallel definitions, no duplicate statements, and every name in the description resolves. The PR has no other reviews or open threads.

Queueing this exact head.