From 40373fc6189dd838cf644d2d48979106f3e83e7b Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 19:14:08 +0100 Subject: [PATCH 1/2] =?UTF-8?q?theory:=20antiecho-partition-dec=20?= =?UTF-8?q?=E2=80=94=20per-element=20classification=20given=20Dec=20(f=20x?= =?UTF-8?q?=20=E2=89=A1=20y)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lands obligation 5 of `coecho.md` §5 (deferred since the original AntiEcho thin slice in PR #69 / commit 428b4b8): the per-element partition of A into the Echo-side and the AntiEcho-side, given decidability of `f x ≡ y`. 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. Also corrects a misleading line in 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 genuinely *not* a theorem at any decidability strength — Bool counterexample with `f = id` simultaneously inhabits both sides at `y = true`. The deferred-but-now-landed obligation 5 is the per-element classification above, not joint disjointness; the preamble is rewritten to say so. Build: --safe --without-K, zero postulates, no funext. Both `antiecho-partition-dec` and `antiecho-partition-codomain-dec` pinned in `Smoke.agda`. `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0. Refs: project_echo_types_swarm_2026_05_20 (small deferrals) Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/agda/AntiEcho.agda | 49 ++++++++++++++++++++++++++++++++++++--- proofs/agda/Smoke.agda | 14 +++++++---- 2 files changed, 55 insertions(+), 8 deletions(-) diff --git a/proofs/agda/AntiEcho.agda b/proofs/agda/AntiEcho.agda index d9b2de4..8f0a1e4 100644 --- a/proofs/agda/AntiEcho.agda +++ b/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`; the generic-codomain +-- form (lift from the concrete ℕ score to an abstract ordered codomain +-- interface) remains deferred. 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? _) diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 7519ee9..e8f7007 100644 --- a/proofs/agda/Smoke.agda +++ 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 From cb037f111b802a1ca25cf5ca95d09ab368f9eb86 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 19:25:03 +0100 Subject: [PATCH 2/2] =?UTF-8?q?theory:=20AntiEchoTropicalGeneric=20?= =?UTF-8?q?=E2=80=94=20generic-codomain=20lift=20of=20the=20tropical=20dec?= =?UTF-8?q?omposition?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lifts the concrete ℕ-scored tropical decomposition from `AntiEchoTropical.agda` to an arbitrary ordered codomain. Closes the "deferred (would need a `≤`-bearing ordered codomain)" remark in the concrete module's preamble. New module: `EchoGradedComonadInstance2.agda`-style — concrete interface, sanity instance at ℕ, all theorems parameterised by the interface. `OrderedCodomain` interface: 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 first three are pure structure; the latter two are the order conversions. `≤⇒¬<` is always available; `¬<⇒≤` is the entire content of the "decidable order" hypothesis in the concrete ℕ case — factored out as a field rather than baked into the codomain. Three theorems land in `module Generic (OC : OrderedCodomain)`: * antiecho-tropical-decompose-gen — pure Σ-reshape iso, refl round-trips, does NOT use the order at all * optimality-as-antiecho-flavour-gen-to/from — uses ≤⇒¬< / ¬<⇒≤ * tropdecomp-antiecho-gen-to/from — the composite Sanity instance `ℕ-ordered-codomain : OrderedCodomain` is pinned in Smoke.agda so the interface is demonstrably inhabitable. Downstream users can build their own instances at other ordered codomains (integers, rationals, abstract semirings) without modifying this module. Preamble updates in two existing files (zero-diff to Agda content): * AntiEcho.agda — obligation 6 line updated: now points to both the concrete and generic landings * AntiEchoTropical.agda — "generic-codomain version is deferred" replaced by a pointer to the new module Build: --safe --without-K, zero postulates, no funext, no escape pragmas. Wired into All.agda; OrderedCodomain, ℕ-ordered-codomain, and module Generic pinned in Smoke.agda. `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0. Depends on: #90 (antiecho-partition-dec). Branch based on antiecho-partition-dec; will rebase onto main once #90 lands. Refs: project_echo_types_swarm_2026_05_20 (small deferrals) Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/agda/All.agda | 1 + proofs/agda/AntiEcho.agda | 6 +- proofs/agda/AntiEchoTropical.agda | 6 +- proofs/agda/AntiEchoTropicalGeneric.agda | 181 +++++++++++++++++++++++ proofs/agda/Smoke.agda | 11 ++ 5 files changed, 200 insertions(+), 5 deletions(-) create mode 100644 proofs/agda/AntiEchoTropicalGeneric.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 0c8e5c4..f5a9753 100644 --- a/proofs/agda/All.agda +++ b/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 diff --git a/proofs/agda/AntiEcho.agda b/proofs/agda/AntiEcho.agda index 8f0a1e4..3753f07 100644 --- a/proofs/agda/AntiEcho.agda +++ b/proofs/agda/AntiEcho.agda @@ -21,9 +21,9 @@ -- 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`; the generic-codomain --- form (lift from the concrete ℕ score to an abstract ordered codomain --- interface) remains deferred. +-- IsArgmin`) lives in `AntiEchoTropical.agda` (concrete ℕ-scored +-- form) and `AntiEchoTropicalGeneric.agda` (generic-codomain lift +-- over an abstract `OrderedCodomain` interface). module AntiEcho where diff --git a/proofs/agda/AntiEchoTropical.agda b/proofs/agda/AntiEchoTropical.agda index 305f5ce..255cba3 100644 --- a/proofs/agda/AntiEchoTropical.agda +++ b/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 diff --git a/proofs/agda/AntiEchoTropicalGeneric.agda b/proofs/agda/AntiEchoTropicalGeneric.agda new file mode 100644 index 0000000..380d68f --- /dev/null +++ b/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 = ℕ + ; _≤_ = _≤_ + ; _<_ = _<_ + ; ≤⇒¬< = ℕ-≤⇒¬< + ; ¬<⇒≤ = ℕ-¬<⇒≤ + } diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index e8f7007..3c1127c 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -526,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