theory: AntiEchoTropicalGeneric — generic-codomain lift of the tropical decomposition

proofs/agda/All.agda

@@ -18,6 +18,7 @@ open import EchoLinear
 open import EchoGraded
 open import EchoTropical
 open import AntiEchoTropical
+open import AntiEchoTropicalGeneric
 open import EchoIntegration
 open import EchoCNOBridge
 

proofs/agda/AntiEcho.agda

@@ -17,17 +17,25 @@
 -- 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.
+-- along the source. Obligation 5 (the partition-with-decidability
+-- lemma) lands below as `antiecho-partition-dec` and the
+-- codomain-decidability variant `antiecho-partition-codomain-dec`.
+-- Obligation 6 (the tropical decomposition `Echo × Π AntiEcho ≃
+-- IsArgmin`) lives in `AntiEchoTropical.agda` (concrete ℕ-scored
+-- form) and `AntiEchoTropicalGeneric.agda` (generic-codomain lift
+-- over an abstract `OrderedCodomain` interface).
 
 module AntiEcho where
 
 open import Level using (Level; _⊔_)
 open import Data.Empty using (⊥)
 open import Data.Product.Base using (Σ; _,_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no)
+
+open import Echo using (Echo)
 
 ----------------------------------------------------------------------
 -- antiecho-def — the carrier.
@@ -91,3 +99,38 @@ antiecho-map-over :
   {f : A → B} {y : B}
   (g : A' → A) → AntiEcho (f ∘ g) y → AntiEcho f y
 antiecho-map-over g (x , np) = g x , np
+
+----------------------------------------------------------------------
+-- antiecho-partition-dec — every source element classifies to one
+-- side, given decidability of `f x ≡ y`.
+--
+-- The companion to `antiecho-disjoint`. Disjointness ruled out
+-- `Echo` and `AntiEcho` *coinciding* on a shared `x`; this lemma
+-- says that for *any* `x`, decidability of `f x ≡ y` gives an actual
+-- classification of `x` into one side or the other. Together they
+-- exhibit `A` as the disjoint union of the Echo-side and the
+-- AntiEcho-side parameterised by `y`.
+--
+-- The asymmetric joint statement `Echo f y → AntiEcho f y → ⊥`
+-- (where the two sides carry *different* domain witnesses) is
+-- genuinely *not* a theorem and is not what is landed here:
+-- consider `f : Bool → Bool` with `f true = true` and
+-- `f false = false`; 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 correct content
+-- of "obligation 5" is the per-element classification below.
+
+antiecho-partition-dec :
+  ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B}
+  (x : A) → Dec (f x ≡ y) → Echo f y ⊎ AntiEcho f y
+antiecho-partition-dec x (yes p) = inj₁ (x , p)
+antiecho-partition-dec x (no  np) = inj₂ (x , np)
+
+-- Codomain-decidability variant: when *every* `b ≡ y` is decidable
+-- (typically because `B` has decidable equality), the classification
+-- closes uniformly over `f x`.
+
+antiecho-partition-codomain-dec :
+  ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B}
+  → (∀ b → Dec (b ≡ y)) → (x : A) → Echo f y ⊎ AntiEcho f y
+antiecho-partition-codomain-dec dec? x = antiecho-partition-dec x (dec? _)

proofs/agda/AntiEchoTropical.agda

@@ -33,8 +33,10 @@
 --
 -- 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).
+-- of `EchoTropical.agda`; the generic-codomain version lives in
+-- `AntiEchoTropicalGeneric.agda`, parameterised by an abstract
+-- `OrderedCodomain` interface (carrier `B`, `_≤_`, `_<_`, `≤⇒¬<`,
+-- `¬<⇒≤`).
 
 module AntiEchoTropical where
 

proofs/agda/AntiEchoTropicalGeneric.agda

@@ -0,0 +1,181 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- AntiEchoTropicalGeneric — generic-codomain lift of
+-- `AntiEchoTropical.agda`'s tropical decomposition.
+--
+-- The concrete module `AntiEchoTropical.agda` works on the specific
+-- candidate scoring `score : Candidate → ℕ`. This module lifts the
+-- same decomposition to *any* ordered codomain interface — a carrier
+-- `B`, an order `_≤_`, a strict order `_<_`, the bound-against-strict
+-- conversion `≤⇒¬<` (always available), and the not-strict-below
+-- conversion `¬<⇒≤` (the decidability content; concretely
+-- `Data.Nat.Properties.¬<⇒≥`-shape, but ANY witness suffices).
+--
+-- Three theorems land over the interface:
+--   * `antiecho-tropical-decompose-gen` — Σ-reshape iso; structural,
+--     `refl` round-trips, does *not* need the order at all.
+--   * `optimality-iso-gen` — `(∀ z → y ≤ s z)` ↔ `(∀ z → s z < y → ⊥)`,
+--     using `≤⇒¬<` / `¬<⇒≤` from the interface.
+--   * `tropdecomp-antiecho-to-gen` / `-from-gen` — the composite
+--     `TropEcho-like ↔ Echo × Π-of-AntiEcho-flavoured-misses`.
+--
+-- Scope. The Σ-shapes for `IsArgmin-like` and `TropEcho-like` are
+-- replayed locally over the interface (`IsArgminG` and `TropEchoG`)
+-- because the concrete `IsArgmin` / `TropEcho` in `EchoTropical.agda`
+-- are pinned to `Candidate → ℕ`. The concrete module is *unchanged*
+-- and remains the canonical landing for the ℕ-scored case; this
+-- module is the abstract sibling, not a replacement.
+--
+-- The original concrete module discharged the obligation comment
+-- "a generic-codomain version is deferred (would need a `≤`-bearing
+-- ordered codomain)" — that obligation is now landed here.
+
+module AntiEchoTropicalGeneric where
+
+open import Data.Empty using (⊥)
+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)
+
+----------------------------------------------------------------------
+-- Ordered codomain interface.
+--
+-- The minimum structure needed to land the tropical decomposition at
+-- a generic codomain. `B` is the codomain carrier; `_≤_` is the bound
+-- relation used on the optimality side; `_<_` is the strict order
+-- used in the AntiEcho-flavoured restatement; `≤⇒¬<` and `¬<⇒≤` are
+-- the two order conversions. Note that `¬<⇒≤` is the entire content
+-- of the "decidable order" hypothesis in the concrete ℕ case —
+-- factored out here as a field rather than baked into the codomain.
+
+record OrderedCodomain : Set₁ where
+  field
+    B    : Set
+    _≤_  : B → B → Set
+    _<_  : B → B → Set
+    ≤⇒¬< : ∀ {y n : B} → y ≤ n → n < y → ⊥
+    ¬<⇒≤ : ∀ {y n : B} → (n < y → ⊥) → y ≤ n
+
+----------------------------------------------------------------------
+-- The generic decomposition, parameterised by `OrderedCodomain` and
+-- an abstract scoring function `s : C → B` from any candidate set to
+-- the ordered codomain.
+
+module Generic (OC : OrderedCodomain) where
+  open OrderedCodomain OC
+
+  -- Re-introduce the Σ-shapes locally over the abstract codomain.
+  -- These mirror `EchoTropical.IsArgmin` / `TropEcho` exactly, with
+  -- `Candidate → ℕ` replaced by an arbitrary `s : C → B`.
+
+  IsArgminG : ∀ {C : Set} (s : C → B) → C → B → Set
+  IsArgminG s x y = s x ≡ y × (∀ z → y ≤ s z)
+
+  TropEchoG : ∀ {C : Set} (s : C → B) → B → Set
+  TropEchoG {C = C} s y = Σ C (λ x → IsArgminG s x y)
+
+  ------------------------------------------------------------------
+  -- The structural decomposition.  Pure Σ-reshape; the order is not
+  -- used.  Both round-trips `refl`.
+
+  antiecho-tropical-decompose-gen-to :
+    ∀ {C : Set} {s : C → B} {y : B} →
+    TropEchoG s y → Echo s y × (∀ z → y ≤ s z)
+  antiecho-tropical-decompose-gen-to (x , p , bnd) = (x , p) , bnd
+
+  antiecho-tropical-decompose-gen-from :
+    ∀ {C : Set} {s : C → B} {y : B} →
+    Echo s y × (∀ z → y ≤ s z) → TropEchoG s y
+  antiecho-tropical-decompose-gen-from ((x , p) , bnd) = x , p , bnd
+
+  antiecho-tropical-decompose-gen-to-from :
+    ∀ {C : Set} {s : C → B} {y : B}
+    (r : Echo s y × (∀ z → y ≤ s z)) →
+    antiecho-tropical-decompose-gen-to
+      (antiecho-tropical-decompose-gen-from r) ≡ r
+  antiecho-tropical-decompose-gen-to-from ((x , p) , bnd) = refl
+
+  antiecho-tropical-decompose-gen-from-to :
+    ∀ {C : Set} {s : C → B} {y : B}
+    (t : TropEchoG s y) →
+    antiecho-tropical-decompose-gen-from
+      (antiecho-tropical-decompose-gen-to t) ≡ t
+  antiecho-tropical-decompose-gen-from-to (x , p , bnd) = refl
+
+  antiecho-tropical-decompose-gen :
+    ∀ {C : Set} (s : C → B) (y : B) →
+    TropEchoG s y ↔ (Echo s y × (∀ z → y ≤ s z))
+  antiecho-tropical-decompose-gen s y =
+    mk↔ₛ′
+      (λ t → antiecho-tropical-decompose-gen-to   {s = s} {y = y} t)
+      (λ r → antiecho-tropical-decompose-gen-from {s = s} {y = y} r)
+      (λ r → antiecho-tropical-decompose-gen-to-from {s = s} {y = y} r)
+      (λ t → antiecho-tropical-decompose-gen-from-to {s = s} {y = y} t)
+
+  ------------------------------------------------------------------
+  -- AntiEcho-flavoured restatement of the optimality factor.  The
+  -- forward direction uses `≤⇒¬<` (always available); the backward
+  -- uses `¬<⇒≤` (the decidability content of the interface).
+
+  optimality-as-antiecho-flavour-gen-to :
+    ∀ {C : Set} {s : C → B} {y : B} →
+    (∀ z → y ≤ s z) → (∀ z → s z < y → ⊥)
+  optimality-as-antiecho-flavour-gen-to bnd z lt = ≤⇒¬< (bnd z) lt
+
+  optimality-as-antiecho-flavour-gen-from :
+    ∀ {C : Set} {s : C → B} {y : B} →
+    (∀ z → s z < y → ⊥) → (∀ z → y ≤ s z)
+  optimality-as-antiecho-flavour-gen-from no-miss z = ¬<⇒≤ (no-miss z)
+
+  ------------------------------------------------------------------
+  -- Composite: TropEchoG ↔ Echo × (Π-of-AntiEcho-flavoured-misses).
+  -- Forward + backward only, no extensionality on the Π factor (the
+  -- two Π-shaped sides are not propositionally equal in general
+  -- without funext; we keep them as a section/retraction pair, which
+  -- is what the concrete module already does).
+
+  tropdecomp-antiecho-gen-to :
+    ∀ {C : Set} {s : C → B} {y : B} →
+    TropEchoG s y → Echo s y × (∀ z → s z < y → ⊥)
+  tropdecomp-antiecho-gen-to t
+    with antiecho-tropical-decompose-gen-to t
+  ... | (e , bnd) = e , optimality-as-antiecho-flavour-gen-to bnd
+
+  tropdecomp-antiecho-gen-from :
+    ∀ {C : Set} {s : C → B} {y : B} →
+    Echo s y × (∀ z → s z < y → ⊥) → TropEchoG s y
+  tropdecomp-antiecho-gen-from (e , no-miss) =
+    antiecho-tropical-decompose-gen-from
+      (e , optimality-as-antiecho-flavour-gen-from no-miss)
+
+----------------------------------------------------------------------
+-- Sanity instance: the natural numbers.  Builds an `OrderedCodomain`
+-- record at ℕ with the same `≤⇒¬<` / `¬<⇒≤` lemmas the concrete
+-- `AntiEchoTropical.agda` uses internally.  Pinned so the interface
+-- is demonstrably inhabitable; downstream users can build their own
+-- instances at other ordered codomains (e.g. `Float`, integers,
+-- abstract semirings) without modifying this module.
+
+open import Data.Nat.Base using (ℕ; zero; suc; _≤_; _<_; z≤n; s≤s)
+open import Data.Empty using (⊥-elim)
+
+private
+  ℕ-≤⇒¬< : ∀ {y n : ℕ} → y ≤ n → n < y → ⊥
+  ℕ-≤⇒¬< z≤n     ()
+  ℕ-≤⇒¬< (s≤s p) (s≤s q) = ℕ-≤⇒¬< p q
+
+  ℕ-¬<⇒≤ : ∀ {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)))
+
+ℕ-ordered-codomain : OrderedCodomain
+ℕ-ordered-codomain = record
+  { B    = ℕ
+  ; _≤_  = _≤_
+  ; _<_  = _<_
+  ; ≤⇒¬< = ℕ-≤⇒¬<
+  ; ¬<⇒≤ = ℕ-¬<⇒≤
+  }

proofs/agda/Smoke.agda

@@ -34,16 +34,20 @@ open import Echo using
   )
 
 -- 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.
+-- carrier, per-element disjointness, introduction, source-side
+-- map-over, and per-element partition with decidability of `f x ≡ y`
+-- (obligation 5). Distinct from `EchoFiberTriangulation.CoEcho`
+-- (which is the trivial opposite-orientation fibre `∃ x . y ≡ f x`);
+-- see `coecho.md` §6 for the naming rationale. Tropical decomposition
+-- lives in `AntiEchoTropical.agda`; the generic-codomain lift of it
+-- remains deferred.
 open import AntiEcho using
   ( AntiEcho
   ; antiecho-intro
   ; antiecho-disjoint
   ; antiecho-map-over
+  ; antiecho-partition-dec
+  ; antiecho-partition-codomain-dec
   )
 
 -- Pillar A of docs/echo-types/establishment-plan.adoc: the
@@ -522,6 +526,17 @@ open import AntiEchoTropical using
   ; tropdecomp-antiecho-from
   )
 
+-- Generic-codomain lift of the tropical decomposition. Same headline
+-- theorems as `AntiEchoTropical` above, but parameterised by an
+-- abstract `OrderedCodomain` interface (carrier B, ≤/<, ≤⇒¬<, ¬<⇒≤)
+-- rather than fixed to ℕ. Sanity instance `ℕ-ordered-codomain`
+-- pinned so the interface is demonstrably inhabitable.
+open import AntiEchoTropicalGeneric using
+  ( OrderedCodomain
+  ; ℕ-ordered-codomain
+  ; module Generic
+  )
+
 open import EchoIntegration using
   ( knowledge-preserved-under-choreo
   ; merged-at-residue