Clone triage — duplication census + the extraction map

Instrument: just clones (tools/clone-report.py, Lean-aware token-window detector; comments stripped via tools/leanlex.py). Companion inventory: docs/notes/proof-assets.md (generated — what reusable proof machinery exists). Snapshot 2026-07-13 on main @ d6bb892e: 62 families ≥4×5 lines, duplicated mass ≈ 2171 normalized lines — ~4.4% of the 49k-line Lean tree. Re-run the tool for current numbers; this note's value is the shape analysis and the extraction timing, which change slowly.

The headline finding: the top families are NOT tactic-shaped

The tactics-survey recommended building @[bang_grind] / aesop rule sets. The census says that is not where our duplication lives. Every top-5 family is a segment of ONE underlying pattern — the outcome-refutation arm sweep in Bang/Backend/AbstractMachine.lean (~19-21 sites, each spelling ~10-15 arms):

match oM, h with
| (.term (.force a),   _, _, _, _), h => simp [Option.bind] at h
| (.term (.app a b),   _, _, _, _), h => simp [Option.bind] at h
| (.term (.perform …), _, _, _, _), h => simp [Option.bind] at h
… (one arm per Comp head constructor that CANNOT be the stepped-to outcome)

Machine witness (2026-07-13, lean_multi_attempt at AbstractMachine.lean:2361): substituting ANY tactic at an arm position is a syntax error ("Alternative force has not been provided", "unexpected token (") — the arms are match alternatives, not sequential goals. No tactic, grind included, can collapse them in place; the pattern spelling is syntactically mandatory. So a tactic macro is the wrong abstraction for the dominant family, and bang_grind has no consumer in the top-15. The survey's recommendation is deferred with a named resume trigger (below), not adopted on faith.

The extraction map (top families → right abstraction → WHEN)

Family (rank, mass)	Shape	Right abstraction	When
#1–#5: outcome-refutation arm sweeps, ~20 sites, AbstractMachine ~2360–3330 + 5540–6500	match alternatives (witnessed above)	step-outcome inversion lemma: one lemma characterizing `evalD … = some (o, …)` by `M`'s head constructor; each site's refuted arms collapse to one `rcases`	◊-sized proof refactor of green proofs — do it inside #169 wgcexec early-bank / the D5-resume increment, which rewrite these exact sites anyway. Do NOT churn them standalone.
#6, #7, #9: step-unfold headers (`cases hM : … with \| none => absurd \| some oM => rw; match …`), ~12 sites	half macro-shaped	a `step_cases hM h` tactic macro covers the header; the arms still need the inversion lemma	same window as above — the macro alone saves ~2 lines/site, not worth green-proof churn by itself
#8: `splitAtId` destructure, 9×6, AbstractMachine ~4076–4962	fully macro-shaped	`split_at_id_cases hsp hs` macro (cases + simp only + obtain, names fixed)	same file, same window; first genuinely macro-shaped candidate when that region is next opened
#10, #11: Wasm.lean rec-arm `none/some + obtain + mem_cons` blocks, 8×6	macro-or-lemma	small helper lemma over the recursion scheme	when Wasm.lean is next rewritten (D5-resume touches it)
remaining 51 families	long tail, mass ≤ 45 each	mixed	opportunistic; re-run `just clones` at each ◊

The rule the map encodes: extraction of proven duplication is bundled into the increment that already rewrites those sites (census risk paid once), never done as standalone beautification. New sweeps (the next D5-style engine port) should start from the inversion-lemma design instead of hand-spelling arms — that's where the ~130-site relay cost actually gets recovered.

Deferred with resume triggers

@[bang_grind] attr + aesop constructor sets (tactics-survey top-3): register when a measured pain point exists — i.e. a clone family or a relay report shows repeated row-algebra/typing-derivation discharge that grind only [bang_grind] would close. Not before: an attribute set with no consumer is dead weight in every future simp/grind debugging session.
Step-outcome inversion lemma: designed + landed inside #169 or D5-resume (whichever opens AbstractMachine.lean first). It also shrinks those increments: their new arms inherit the lemma instead of the sweep.
Clone-mass ratchet: once the inversion lemma lands, consider enrolling clone-report --min-count 8 mass into the fitness checks as a no-regression gate. Premature today (the mass is stable and the extraction window is named).

Discoverability contract

What exists: docs/notes/proof-assets.md — GENERATED inventory (custom tactics/attrs + @[simp] sets per module), regenerated by just regen-all, drift-gated by just checks (gen-proof-assets.py --check).
What's duplicated: just clones — run live, never snapshotted as truth.
Why no tactics yet: this note (the witness + the map).