theory: AntiEcho thin slice — Σ-dual of Echo (carrier + map-over + disjointness)

Lands the first four obligations from the `coecho.md` design note as
`proofs/agda/AntiEcho.agda` (renamed `antiecho-*` per user namespace
decision 2026-05-20):

  * `AntiEcho f y := Σ A (λ x → f x ≢ y)` — the carrier, the
    minimal-edit-distance Σ-dual of `Echo`. Same Σ-shape, same
    universe `a ⊔ b`, same proof-relevance posture as Echo; ≡ flips
    to ≢ = · ≡ y → ⊥. (antiecho-def)
  * `antiecho-intro : ∀ x → f x ≢ y → AntiEcho f y` — trivial pairing.
  * `antiecho-disjoint : ∀ x → f x ≡ y → f x ≢ y → ⊥` — per-element
    disjointness against Echo. The joint form
    `Echo f y → AntiEcho f y → ⊥` with possibly distinct witnesses is
    deliberately deferred (requires codomain decidability; lives in
    the partition lemma).
  * `antiecho-map-over : (g : A' → A) → AntiEcho (f ∘ g) y →
    AntiEcho f y` — source-side covariance; misses propagate back to
    the outer leg by re-applying g.

Naming decision (user, 2026-05-20). The new module is `AntiEcho`, NOT
`CoEcho`. The name `CoEcho` is already taken in
`EchoFiberTriangulation.agda` (lines 82–95) for the trivial
opposite-orientation fibre `∃ x . y ≡ f x` (Echo composed with `sym`).
That construction is a reorientation, not a dual. The negative dual
lands here under the distinct name `AntiEcho` so the two namespaces
stay fully separate. Both `EchoFiberTriangulation.CoEcho` and the new
`AntiEcho` are now pinned in `Smoke.agda`.

Deferred to follow-up slices (do NOT close anything):
  * obligation 5 `antiecho-partition-dec` — needs `DecEq B` on the
    codomain; lives in its own slice.
  * obligation 6 `antiecho-tropical-decompose` — crosses module
    boundaries (`EchoTropical.IsArgmin ≃ Echo × Π AntiEcho`) and
    deserves its own slice; the design note flags this as the
    structural-vs-quantitative payoff but the proof reaches beyond a
    thin-slice introduction.

Build invariants held: `--safe --without-K`, zero postulates, zero
escape pragmas. New module wired into `All.agda` as `open import
AntiEcho`; headline names (`AntiEcho`, `antiecho-intro`,
`antiecho-disjoint`, `antiecho-map-over`) pinned in `Smoke.agda` via
`using` clause so a rename/deletion fails CI fast.

Verification: `agda -i proofs/agda proofs/agda/All.agda` exits 0;
the build trace lists `Checking AntiEcho` and `Checking Smoke`
without errors, confirming both the module itself and the pinned
headlines typecheck.

Refs: docs/echo-types/roadmap.md "Negative / co-echoes" entry (CoEcho
formulation). Does NOT close that entry — only the carrier + the
first three small lemmas land; the partition and tropical
decomposition obligations remain.

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

Author: hyperpolymath

proofs/agda/All.agda

@@ -3,6 +3,7 @@
 module All where
 
 open import Echo
+open import AntiEcho
 open import EchoKernel
 open import EchoCharacteristic
 open import EchoResidue

proofs/agda/AntiEcho.agda

@@ -0,0 +1,93 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- AntiEcho — the Σ-dual of Echo.
+--
+-- Given `Echo f y := Σ (x : A) , (f x ≡ y)` from `Echo.agda`, the
+-- minimal-edit-distance dual is `AntiEcho f y := Σ A (λ x → f x ≢ y)`:
+-- a domain element together with a constructive proof that `f x` does
+-- NOT hit `y`. Same Σ-shape, same universe `a ⊔ b`, same
+-- proof-relevance posture; `--safe --without-K`-clean.
+--
+-- Naming. The name `CoEcho` is ALREADY taken in
+-- `EchoFiberTriangulation.agda` for the trivial opposite-orientation
+-- fibre `∃ x . y ≡ f x` (Echo composed with `sym`). That construction
+-- is a reorientation, not a dual. The negative dual lives here under
+-- the distinct name `AntiEcho`. Cf. design note: `coecho.md` §6.
+--
+-- This thin slice lands obligations 1–4 from `coecho.md` §5 (renamed
+-- `antiecho-*`): the carrier, per-element disjointness against Echo,
+-- introduction from any witnessed miss, and contravariant `map-over`
+-- along the source. The partition-with-decidability lemma and the
+-- tropical decomposition (Echo × Π AntiEcho ≃ IsArgmin) are deferred
+-- to follow-up slices; see `coecho.md` §5 obligations 5–6.
+
+module AntiEcho where
+
+open import Level using (Level; _⊔_)
+open import Data.Empty using (⊥)
+open import Data.Product.Base using (Σ; _,_)
+open import Function.Base using (_∘_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
+
+----------------------------------------------------------------------
+-- antiecho-def — the carrier.
+--
+-- Same Σ-shape as `Echo`; only `≡` flips to `≢ := · ≡ y → ⊥`.
+-- Universe `a ⊔ b`, matching Echo exactly.
+
+AntiEcho :
+  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → B → Set (a ⊔ b)
+AntiEcho {A = A} f y = Σ A (λ x → f x ≢ y)
+
+----------------------------------------------------------------------
+-- antiecho-intro — introduction from a constructive miss.
+--
+-- Trivial: an inhabitant is exactly a pair of a domain element and a
+-- miss-proof. Mirrors `Echo.echo-intro` modulo the flip.
+
+antiecho-intro :
+  ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B}
+  (x : A) → f x ≢ y → AntiEcho f y
+antiecho-intro x np = x , np
+
+----------------------------------------------------------------------
+-- antiecho-disjoint — per-element disjointness against Echo.
+--
+-- A single `x : A` cannot witness both `f x ≡ y` and `f x ≢ y`; apply
+-- the negation to the equation. Note this is the PER-ELEMENT form,
+-- per `coecho.md` §2: the joint statement `Echo f y → AntiEcho f y → ⊥`
+-- with possibly distinct witnesses requires decidability on the
+-- codomain and lives in the deferred partition lemma. Here the witness
+-- is shared explicitly.
+
+antiecho-disjoint :
+  ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B}
+  (x : A) → f x ≡ y → f x ≢ y → ⊥
+antiecho-disjoint x p np = np p
+
+-- The asymmetric joint form `Echo f y → AntiEcho f y → ⊥` (where the
+-- two sides may carry different domain witnesses) is intentionally
+-- absent: it requires injectivity / decidability on the codomain to
+-- collapse the two witnesses, and lives in the deferred partition
+-- lemma (`coecho.md` §5 obligation 5). The per-element form above is
+-- the postulate-free, K-free primitive.
+
+----------------------------------------------------------------------
+-- antiecho-map-over — covariance along the source.
+--
+-- Given `g : A' → A`, an AntiEcho for the composite `f ∘ g` yields an
+-- AntiEcho for `f` by re-applying `g` to the source witness. The miss
+-- proof carries over unchanged: `f (g x) ≡ y` IS the proposition
+-- `(f ∘ g) x ≡ y`, so the same negation discharges both.
+--
+-- This is the SOURCE-side `map-over`: misses propagate from the
+-- composite back to the outer leg. Cf. `coecho.md` §4 design note 3
+-- ("contravariant MapOver"): the MapOver-style version (over a fixed
+-- codomain) is a follow-up; this slice ships the simpler composition-
+-- along-the-source form.
+
+antiecho-map-over :
+  ∀ {a a' b} {A : Set a} {A' : Set a'} {B : Set b}
+  {f : A → B} {y : B}
+  (g : A' → A) → AntiEcho (f ∘ g) y → AntiEcho f y
+antiecho-map-over g (x , np) = g x , np

proofs/agda/Smoke.agda

@@ -32,6 +32,20 @@ open import Echo using
   ; cancel-iso
   ; Echo-comp-pent-Σ-assoc
   )
+
+-- AntiEcho thin slice (theory/antiecho — Σ-dual of Echo). Lands the
+-- carrier, per-element disjointness, introduction, and source-side
+-- map-over. Distinct from `EchoFiberTriangulation.CoEcho` (which is
+-- the trivial opposite-orientation fibre `∃ x . y ≡ f x`); see
+-- `coecho.md` §6 for the naming rationale. Partition-with-decidability
+-- and tropical decomposition deferred to follow-up slices.
+open import AntiEcho using
+  ( AntiEcho
+  ; antiecho-intro
+  ; antiecho-disjoint
+  ; antiecho-map-over
+  )
+
 -- Pillar A of docs/echo-types/establishment-plan.adoc: the
 -- definitional Echo ≃ fib bridge, pinned so a rename fails CI fast.
 open import EchoFiberBridge using (fiber; echo→fib; fib→echo; echo↔fib)