Item 127: Defeaters as undercutting occurrences: the grounded extension with attacks

Occurrence.defeaters is read as the ports whose defeat also undercuts the occurrence (WarrantEntitlement.undercut), which makes a warrant's forms share one defeat condition and makes the survivors the least fixed point of a monotone step. The argumentation-theoretic reading — a defeater is an occurrence that undercuts when it is itself active — makes the step non-monotone and the right notion the grounded extension of Dung's characteristic function (defended iff every active attacker is attacked by the set). Wanted: the attack reading as a second rule on Grounds, its grounded extension as a fixed point, the theorem that the two rules agree when no defeater is an occurrence of the grounds, and a fixture where an undercutter is itself defeasible.

Deliverable shape: lean-proved; the agreement theorem. Acceptance check: the Lean audit clean; WarrantInductorWitness.survivors_eq unchanged. Context: DECISIONS.md 2026-10-22; WarrantEntitlement.liveGiven. Consumed by: fixtures with undercutting defeaters that are themselves warrants.