theory: AntiEcho × IsArgmin tropical decomposition (#72)

## Summary

Cashes the headline claim from `/tmp/echo-types-exploration/coecho.md`
§3 ("Resolution of the EchoTropical tension") at the structural level:
`TropEcho` / `IsArgmin` decompose into Echo evidence + a Π-quantified
complement bound, with an AntiEcho-flavoured corollary exposing that
bound as a Π of negative data over the candidate set.

New module `proofs/agda/AntiEchoTropical.agda`. Neither `AntiEcho.agda`
(from #69) nor `EchoTropical.agda` is modified — the bridge stays
isolated so PR scope is tight.

### Headline theorem (both directions, both round-trips `refl`, packaged
as `_↔_`)

```agda
antiecho-tropical-decompose :
  ∀ (y : ℕ) → TropEcho y ↔ (Echo score y × (∀ z → y ≤ score z))
```

The forward direction projects `(x , p , bnd) ↦ ((x , p) , bnd)` — pure
Σ-re-association because the optimality factor `∀ z → y ≤ score z`
doesn't depend on `x`. The backward direction undoes it. Both
round-trips are definitionally `refl`. No decidability, no funext, no
path algebra. Packaged via stdlib `Function.Bundles._↔_` and `mk↔ₛ′`,
matching the convention from `Echo-comp-iso` / `cancel-iso`.

### `IsArgmin`-level restatement (the per-element identity)

```agda
isargmin-decompose :
  ∀ (x : Candidate) (y : ℕ) →
  IsArgmin x y ↔ ((score x ≡ y) × (∀ z → y ≤ score z))
```

`IsArgmin` IS the product by definition, so the iso to the product is
the identity. Pinned for callers thinking in `IsArgmin`-shaped terms.

### AntiEcho-flavoured corollary (the Π-bound as a Π of misses)

The optimality factor `∀ z → y ≤ score z` is equivalent on ℕ to the
AntiEcho-shaped statement "no candidate witnesses a value strictly below
`y`":

```agda
optimality-as-antiecho-flavour-to   : (∀ z → y ≤ score z) → (∀ z → score z < y → ⊥)
optimality-as-antiecho-flavour-from : (∀ z → score z < y → ⊥) → (∀ z → y ≤ score z)
```

with the small order-conversion lemmas `≤⇒¬<` / `¬<⇒≤` shipped
in-module. Composite version (Echo + Π-of-negation):

```agda
tropdecomp-antiecho-to   : TropEcho y → Echo score y × (∀ z → score z < y → ⊥)
tropdecomp-antiecho-from : Echo score y × (∀ z → score z < y → ⊥) → TropEcho y
```

This is the *Π-form* AntiEcho variant from `coecho.md` §1(c)
(`AntiEcho_Π = ¬ Echo`), specialised to the strict-below stratum. The
Σ-form `AntiEcho` carrier from `AntiEcho.agda` is the witness-recording
primitive; the Π-form above is the exhaustive global statement that
names what `IsArgmin` was carrying implicitly.

### Scope notes

- Specialised to the concrete `Candidate → ℕ` setting of
`EchoTropical.agda`. A generic-codomain version would need a `≤`-bearing
ordered codomain and the decidability hypothesis from `coecho.md` §3
closing remark — deferred.
- `Smoke.agda` pins all 14 headlines via `using` so silent renames or a
slide back to ad-hoc tropical decoration trips CI fast.
- `--safe --without-K` clean. No postulates. No funext. No path algebra
beyond constructor-driven trichotomy on `_≤_`/`_<_`.

### PR base / stacking

Branched from `origin/theory/antiecho-thin-slice` (so `AntiEcho` is in
scope) but **PR base is `main`** per the stacked-PR-orphan-trap policy.
The cumulative diff currently includes #69's content; when #69 merges
the diff simplifies automatically.

## Test plan

- [ ] CI runs `agda -i proofs/agda proofs/agda/All.agda` — exits 0.
- [ ] CI runs `agda -i proofs/agda proofs/agda/Smoke.agda` — exits 0.
- [ ] All 14 pinned headlines in `Smoke.agda` resolve.
- [ ] No new postulates / escape pragmas introduced.

**Note on local verification.** Settings restrictions in this sandbox
blocked local `agda` invocation on this worktree (the project's
`Bash(agda *)` allow rule did not apply to this session). Proofs are
pure Σ-currying / pattern-matching + two small ℕ order-conversion lemmas
— expected to typecheck on the existing CI gate.

## Refs

- Refs #69 — depends on the `AntiEcho` module from the AntiEcho thin
slice.
- Refs `docs/echo-types/roadmap.md` CoEcho entry ("Possibly resolves the
quantitative / structural tension hinted at by `EchoTropical`").
- Refs `/tmp/echo-types-exploration/coecho.md` §3 ("Resolution of the
EchoTropical tension") + §5 obligation 6 (`coecho-tropical-decompose`).

Does NOT Close anything. The CoEcho roadmap entry stays open until
decided by the owner; this PR cashes the structural half.

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

---------

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

Author: hyperpolymath

proofs/agda/All.agda

@@ -14,6 +14,7 @@ open import EchoEpistemic
 open import EchoLinear
 open import EchoGraded
 open import EchoTropical
+open import AntiEchoTropical
 open import EchoIntegration
 open import EchoCNOBridge
 

proofs/agda/AntiEchoTropical.agda

@@ -0,0 +1,212 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- AntiEcho × EchoTropical — the tropical decomposition.
+--
+-- Headline (this module). The tropical argmin carrier `TropEcho y`
+-- from `EchoTropical.agda` decomposes definitionally into Echo
+-- evidence and a Π-quantified complement bound:
+--
+--     TropEcho y  ↔  Echo score y × (∀ z → y ≤ score z)
+--
+-- Both round-trips are `refl` once the Σ-shape of `IsArgmin` is
+-- unfolded — no decidability, no funext, no path algebra. This
+-- cashes the headline claim from `/tmp/echo-types-exploration/coecho.md`
+-- §3 ("Resolution of the EchoTropical tension") at the structural
+-- level: `IsArgmin` is exactly Echo (positive provenance witness)
+-- conjoined with a uniform negative bound over the codomain
+-- complement — the structure that motivated naming `AntiEcho` in the
+-- first place. See `coecho.md` §5 obligation 6
+-- (`coecho-tropical-decompose`).
+--
+-- AntiEcho flavour of the optimality side. The Π-bound
+-- `∀ z → y ≤ score z` is equivalent (on ℕ) to the AntiEcho-shaped
+-- "no candidate produces a strict-below miss":
+--
+--     ∀ z → score z < y → ⊥
+--
+-- which reads "for every candidate `z`, the assumption that `z`
+-- scores strictly below `y` is empty" — a Π of negative data over
+-- the candidate set, exactly the AntiEcho idiom. The forward
+-- direction (`≤ ⇒ ¬<`) is uniform and unconditional; the backward
+-- direction (`¬< ⇒ ≤`) uses the decidable trichotomy on ℕ and so
+-- ships as a separate lemma in the AntiEcho-flavour corollary.
+--
+-- Scope. New module, neither `AntiEcho.agda` nor `EchoTropical.agda`
+-- is modified. Specialised to the concrete `Candidate → ℕ` setting
+-- of `EchoTropical.agda`; a generic-codomain version is deferred
+-- (would need a `≤`-bearing ordered codomain).
+
+module AntiEchoTropical where
+
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat.Base using (ℕ; zero; suc; _≤_; _<_; z≤n; s≤s)
+open import Data.Product.Base using (Σ; _×_; _,_; proj₁; proj₂)
+open import Function.Bundles using (_↔_; mk↔ₛ′)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+open import Echo using (Echo)
+open import AntiEcho using (AntiEcho)
+open import EchoTropical using (Candidate; score; IsArgmin; TropEcho)
+
+----------------------------------------------------------------------
+-- The headline decomposition: TropEcho ↔ Echo × Π-bound.
+--
+-- `TropEcho y` unfolds to
+--     Σ Candidate (λ x → score x ≡ y × (∀ z → y ≤ score z))
+-- and the inner second conjunct does not depend on `x`. So
+-- Σ-currying / re-association gives the iso with
+--     Echo score y × (∀ z → y ≤ score z)
+-- on the nose: both round-trips are `refl`, no decidability needed.
+--
+-- This is the structural half of the
+-- "Echo × Π AntiEcho ≃ IsArgmin" claim from `coecho.md` §3 — pure
+-- product re-shape. The AntiEcho reading of the Π factor is the
+-- corollary that follows.
+
+antiecho-tropical-decompose-to :
+  ∀ {y : ℕ} → TropEcho y → Echo score y × (∀ z → y ≤ score z)
+antiecho-tropical-decompose-to (x , p , bnd) = (x , p) , bnd
+
+antiecho-tropical-decompose-from :
+  ∀ {y : ℕ} → Echo score y × (∀ z → y ≤ score z) → TropEcho y
+antiecho-tropical-decompose-from ((x , p) , bnd) = x , p , bnd
+
+antiecho-tropical-decompose-to-from :
+  ∀ {y : ℕ} (r : Echo score y × (∀ z → y ≤ score z)) →
+  antiecho-tropical-decompose-to (antiecho-tropical-decompose-from r) ≡ r
+antiecho-tropical-decompose-to-from ((x , p) , bnd) = refl
+
+antiecho-tropical-decompose-from-to :
+  ∀ {y : ℕ} (t : TropEcho y) →
+  antiecho-tropical-decompose-from (antiecho-tropical-decompose-to t) ≡ t
+antiecho-tropical-decompose-from-to (x , p , bnd) = refl
+
+-- Packaged as a stdlib `_↔_` (bijection / bi-invertible map),
+-- matching the convention used for `Echo-comp-iso` and `cancel-iso`
+-- in `Echo.agda`.
+antiecho-tropical-decompose :
+  ∀ (y : ℕ) → TropEcho y ↔ (Echo score y × (∀ z → y ≤ score z))
+antiecho-tropical-decompose y =
+  mk↔ₛ′
+    (λ t → antiecho-tropical-decompose-to {y = y} t)
+    (λ r → antiecho-tropical-decompose-from {y = y} r)
+    (λ r → antiecho-tropical-decompose-to-from {y = y} r)
+    (λ t → antiecho-tropical-decompose-from-to {y = y} t)
+
+----------------------------------------------------------------------
+-- `IsArgmin`-level restatement.
+--
+-- The decomposition above lives at the `TropEcho` level (the Σ over
+-- candidates). The per-element version on `IsArgmin` is even more
+-- trivial: `IsArgmin x y` IS the product `score x ≡ y × (∀ z → y ≤ score z)`
+-- by definition, so the iso to the same product is the identity.
+-- Pinned for use by callers who think in `IsArgmin`-shaped terms.
+
+isargmin-decompose-to :
+  ∀ {x : Candidate} {y : ℕ} →
+  IsArgmin x y → (score x ≡ y) × (∀ z → y ≤ score z)
+isargmin-decompose-to (p , bnd) = p , bnd
+
+isargmin-decompose-from :
+  ∀ {x : Candidate} {y : ℕ} →
+  (score x ≡ y) × (∀ z → y ≤ score z) → IsArgmin x y
+isargmin-decompose-from (p , bnd) = p , bnd
+
+isargmin-decompose :
+  ∀ (x : Candidate) (y : ℕ) →
+  IsArgmin x y ↔ ((score x ≡ y) × (∀ z → y ≤ score z))
+isargmin-decompose x y =
+  mk↔ₛ′
+    (λ a → isargmin-decompose-to   {x = x} {y = y} a)
+    (λ r → isargmin-decompose-from {x = x} {y = y} r)
+    (λ _ → refl)
+    (λ _ → refl)
+
+----------------------------------------------------------------------
+-- AntiEcho-flavoured corollary: the Π-bound as a Π of negative data.
+--
+-- The optimality factor `∀ z → y ≤ score z` is equivalent on ℕ to
+-- the AntiEcho-shaped statement
+--
+--     ∀ z → score z < y → ⊥
+--
+-- "every candidate, treated as a potential strict-below witness
+-- against `y`, lands in the empty type" — a Π of AntiEcho-style
+-- negative evidence over the candidate set. This makes the Π factor
+-- of the decomposition syntactically AntiEcho-flavoured rather than
+-- just structurally a Π.
+--
+-- Forward direction (`bound → no-strict-below-miss`) is uniform on
+-- ℕ and unconditional. Backward direction (`no-strict-below-miss →
+-- bound`) uses the decidable trichotomy on ℕ; both directions are
+-- discharged here from the constructors of `_≤_` / `_<_` (no extra
+-- imports needed because the candidate-side `score` lands in ℕ
+-- explicitly, so we only need the two small order conversions
+-- below).
+--
+-- Per `coecho.md` §3 closing remark, the *generic-codomain* backward
+-- direction would need a decidable order on the codomain. Here we
+-- avoid that hypothesis by working over ℕ concretely (the codomain
+-- of `score`); decidable trichotomy on ℕ is pattern-matchable, so
+-- the conversion is constructive.
+
+-- y ≤ n → n < y → ⊥
+≤⇒¬< : ∀ {y n : ℕ} → y ≤ n → n < y → ⊥
+≤⇒¬< z≤n     ()
+≤⇒¬< (s≤s p) (s≤s q) = ≤⇒¬< p q
+
+-- ¬ (n < y) → y ≤ n
+¬<⇒≤ : ∀ {y n : ℕ} → (n < y → ⊥) → y ≤ n
+¬<⇒≤ {y = zero}  _    = z≤n
+¬<⇒≤ {y = suc _} {n = zero}  ¬p = ⊥-elim (¬p (s≤s z≤n))
+¬<⇒≤ {y = suc _} {n = suc _} ¬p = s≤s (¬<⇒≤ (λ q → ¬p (s≤s q)))
+
+-- The optimality factor, in AntiEcho-shaped form. A Π over
+-- candidates of a constructive miss-witness against any value
+-- strictly below `y`.
+optimality-as-antiecho-flavour-to :
+  ∀ {y : ℕ} → (∀ z → y ≤ score z) → (∀ z → score z < y → ⊥)
+optimality-as-antiecho-flavour-to bnd z lt = ≤⇒¬< (bnd z) lt
+
+optimality-as-antiecho-flavour-from :
+  ∀ {y : ℕ} → (∀ z → score z < y → ⊥) → (∀ z → y ≤ score z)
+optimality-as-antiecho-flavour-from no-miss z = ¬<⇒≤ (no-miss z)
+
+----------------------------------------------------------------------
+-- Composite: TropEcho ↔ Echo × (Π-of-AntiEcho-flavoured-misses).
+--
+-- The forward direction is the cleanest landing of the headline:
+-- TropEcho data yields Echo evidence + a Π of negative data of
+-- AntiEcho shape over the candidate set. The backward direction
+-- ships via `¬<⇒≤` on ℕ (decidable codomain hypothesis discharged
+-- concretely, not assumed abstractly).
+
+tropdecomp-antiecho-to :
+  ∀ {y : ℕ} → TropEcho y →
+  Echo score y × (∀ z → score z < y → ⊥)
+tropdecomp-antiecho-to t with antiecho-tropical-decompose-to t
+... | (e , bnd) = e , optimality-as-antiecho-flavour-to bnd
+
+tropdecomp-antiecho-from :
+  ∀ {y : ℕ} →
+  Echo score y × (∀ z → score z < y → ⊥) →
+  TropEcho y
+tropdecomp-antiecho-from (e , no-miss) =
+  antiecho-tropical-decompose-from
+    (e , optimality-as-antiecho-flavour-from no-miss)
+
+----------------------------------------------------------------------
+-- Note on the AntiEcho carrier appearance.
+--
+-- The Π factor `∀ z → score z < y → ⊥` does not name `AntiEcho`
+-- directly because `AntiEcho score y'` for a *specific* `y'` is
+-- "some candidate misses `y'`" — a Σ. The dual statement we need
+-- here is "no candidate witnesses a value strictly below `y`",
+-- which is a Π of *negations* of `score z ≡ y'` for `y' < y`.
+-- That is the *Π-form* AntiEcho variant (`coecho.md` §1(c),
+-- catalogued as `AntiEcho_Π = ¬ Echo`), specialised to the
+-- strict-below stratum. The Σ-form `AntiEcho` from `AntiEcho.agda`
+-- is the witness-recording primitive; the Π-form above is the
+-- exhaustive global statement. The headline of this module is the
+-- structural decomposition (TropEcho ↔ Echo × Π-bound); the
+-- AntiEcho-flavoured restatement is the syntactic bridge.

proofs/agda/Smoke.agda

@@ -324,6 +324,31 @@ open import EchoTropical using
   ; distinct-candidates-same-visible-distinct-echo
   )
 
+-- AntiEcho × EchoTropical (theory/antiecho-tropical-decompose):
+-- the headline "Echo × Π-bound" decomposition of TropEcho /
+-- IsArgmin from `coecho.md` §3 / §5 obligation 6. Both
+-- round-trips are `refl` once IsArgmin's Σ-shape is unfolded;
+-- the AntiEcho-flavoured corollary expresses the Π-bound as
+-- Π of negative data over the candidate set (Π-form AntiEcho,
+-- `coecho.md` §1(c)). Pinned so a rename or a slide back to
+-- ad-hoc tropical decoration fails CI fast.
+open import AntiEchoTropical using
+  ( antiecho-tropical-decompose-to
+  ; antiecho-tropical-decompose-from
+  ; antiecho-tropical-decompose-to-from
+  ; antiecho-tropical-decompose-from-to
+  ; antiecho-tropical-decompose
+  ; isargmin-decompose-to
+  ; isargmin-decompose-from
+  ; isargmin-decompose
+  ; ≤⇒¬<
+  ; ¬<⇒≤
+  ; optimality-as-antiecho-flavour-to
+  ; optimality-as-antiecho-flavour-from
+  ; tropdecomp-antiecho-to
+  ; tropdecomp-antiecho-from
+  )
+
 open import EchoIntegration using
   ( knowledge-preserved-under-choreo
   ; merged-at-residue