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] =?UTF-8?q?theory:=20antiecho-partition-dec=20=E2=80=94=20?= =?UTF-8?q?per-element=20classification=20given=20Dec=20(f=20x=20=E2=89=A1?= =?UTF-8?q?=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