theory: antiecho-partition-dec — per-element classification (deferred obligation 5) (#90)

## Summary

Lands obligation 5 of `coecho.md` §5, deferred since the original
AntiEcho thin slice (PR #69, commit `428b4b8`): the per-element
partition of `A` into the Echo-side and the AntiEcho-side, given
decidability of `f x ≡ y`.

```agda
antiecho-partition-dec : ∀ {A B} {f : A → B} {y : B}
  (x : A) → Dec (f x ≡ y) → Echo f y ⊎ AntiEcho f y

antiecho-partition-codomain-dec : ∀ {A B} {f : A → B} {y : B}
  → (∀ b → Dec (b ≡ y)) → (x : A) → Echo f y ⊎ AntiEcho f y
```

Companion to the existing `antiecho-disjoint` (per-element). Together
they exhibit `A` as the disjoint union of the Echo-side and AntiEcho-
side parameterised by `y`: every `x` classifies to one side, and no
`x` appears on both.

## Correction to the prior preamble

The earlier comment claimed the asymmetric joint statement
`Echo f y → AntiEcho f y → ⊥` (with possibly *distinct* domain
witnesses) "requires decidability on the codomain to collapse the two
witnesses". That joint statement is **not** a theorem at any
decidability strength — counterexample with `f : Bool → Bool`,
`f = id`: both `Echo f true` (via `(true, refl)`) and `AntiEcho f true`
(via `(false, false≢true)`) are inhabited, so the joint statement is
refuted by the model. The actual content of the deferred "obligation
5" is the per-element classification above; the preamble is corrected
to say so explicitly.

## Test plan

* [x] `agda proofs/agda/AntiEcho.agda` exit 0
* [x] `agda proofs/agda/All.agda` exit 0 under `--safe --without-K`
* [x] `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`
* [x] Both new lemmas pinned in `Smoke.agda`
* [x] No postulates, no funext, no escape pragmas

## Scope

Tiny additive change. Disjoint from any open PR (#88 F3 touches
`EchoGradedComonad*` modules; this touches `AntiEcho` only).

The companion small deferral — generic-codomain
`antiecho-tropical-decompose`
(lifting `AntiEchoTropical.agda`'s concrete ℕ-scored version to an
abstract ordered-codomain interface) — is **not** addressed here; it
requires designing the interface and is a separate slice.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath