diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index 4a74b15..ffa468e 100644 --- a/docs/echo-types/MAP.adoc +++ b/docs/echo-types/MAP.adoc @@ -275,6 +275,24 @@ honest-bound matched-negative block. is the fold's homomorphism law, NOT full SQL GROUP-BY operational semantics; `avg` is deliberately absent (not a monoid — express as `sum / count`). `proofs/agda/EchoAggregation.agda`. `[REAL]` +* *Variance verdict (monad / comonad / adjunction)* — resolves, in + `--safe` Agda rather than asserting it, the precise variance of the + loss-graded modality. Accumulation is the graded-MONAD multiplication + `accumulate : D_r (D_s A) → D_{r+s} A` (total + canonical, definable + from the layered data alone; `= Echo-comp-iso-from`); recoverability is + exact on the grade-0 fibre (`recoverable-fibre = A↔ΣEcho`, the + section/retraction adjunction); the graded-COMONAD direction fails for + genuine loss (`no-bare-recovery`, the canonical collapse has no section + via `no-section-of-collapsing-map`); and the "graded comonad" reading is + the LOSSLESS complement-storing writer of `EchoGradedComonadF1`, whose + `δ` is `coe` along a type equality and is therefore inverted by + `μ-writer`. Sharpens R-2026-05-18: echo-types is "exact on a homotopy + fibre rather than complement-storing". Honest-bound: the verdict is + about the SHAPE of the canonical structure maps and the LOCUS of + recoverability, not a universal categorical impossibility theorem + (matched `NotProved-*` block). See + `docs/echo-types/variance-resolution.adoc`. + `proofs/agda/EchoVariance.agda`. `[REAL]` *Curated suite — single-file entry point.* The narrative deliverable that pulls the Tier-1 / Tier-2 / Tier-3 named theorems diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc index f3564a8..f1c1740 100644 --- a/docs/echo-types/echo-kernel-note.adoc +++ b/docs/echo-types/echo-kernel-note.adoc @@ -125,7 +125,7 @@ kernel** — the boundary is real and lives outside this core. *Application/extension modules* (also added via the same sweep): `EchoEntropy`, `EchoLLEncoding`, `EchoProvenance`, `EchoSecurity`, `EchoProbabilisticSupport`, `EchoDifferential`, `EchoDeniability`, - `EchoAggregation` + `EchoAggregation`, `EchoVariance` are derived domain applications mapped under their own headings in MAP.adoc. `EchoDeniability` formalises residue deniability: the perfect (constant / no-section) case and the partial (injective / @@ -140,6 +140,17 @@ kernel** — the boundary is real and lives outside this core. `Example-PairSum` instance the oikos/betlang alib note cites (`pairSum` IS the `sumMonoid` fold). Imports `Echo` + `EchoNoSectionGeneric`. + `EchoVariance` resolves, in `--safe` Agda rather than asserting it, + the monad / comonad / adjunction status of loss accumulation + (`docs/echo-types/variance-resolution.adoc`): accumulation is the + graded-MONAD multiplication `accumulate : D_r (D_s A) → D_{r+s} A` + (total + canonical, `= Echo-comp-iso-from`); recoverability is exact on + the grade-0 fibre (`recoverable-fibre = A↔ΣEcho`, the section/retraction + adjunction); the graded-COMONAD direction fails for genuine loss + (`no-bare-recovery`, via `no-section-of-collapsing-map`); and the + "graded comonad" reading is the LOSSLESS complement-storing writer + (`μ-writer` inverts F1's `δ`). Imports `Echo`, `EchoCharacteristic`, + `EchoNoSectionGeneric`, `EchoTotalCompletion`, `EchoGradedComonadF1`. | *Earn-back gate modules* + (derived / scoped; not kernel) diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc index aa5f43c..a93884d 100644 --- a/docs/echo-types/paper.adoc +++ b/docs/echo-types/paper.adoc @@ -1270,6 +1270,28 @@ via a genuine non-graph `StepND` model (§6 NOTE, `EchoStepNDModelF2.agda`). The graded-comonad, modality-level model-independence, and conservativity rows remain fully retracted. +*Variance resolved (follow-up F-2026-06-19, 2026-06-19).* The +graded-comonad row is now *positively resolved*, not merely retracted. +The sharpened understanding of an echo-type — a tropically-graded +modality of structured loss over the min-plus semiring, recoverable +*exact on a homotopy fibre rather than complement-storing* — left a +precise live question: the combining direction of loss is monadic +(accumulation is `μ : D_r (D_s A) → D_{r+s} A`), so is the right word +graded comonad, graded monad, or graded adjunction? `EchoVariance.agda` +settles it in `--safe` Agda (`docs/echo-types/variance-resolution.adoc`): +(i) accumulation is the graded-MONAD multiplication, total and canonical +(`accumulate = Echo-comp-iso-from`); (ii) recoverability is exact on the +grade-0 fibre, the section/retraction *adjunction* +(`recoverable-fibre = A↔ΣEcho`); (iii) the graded-COMONAD direction fails +for genuine loss — bare-residue recovery is the no-section obstruction +(`no-bare-recovery`); and (iv) the "graded comonad" reading is the +LOSSLESS complement-storing writer (`EchoGradedComonadF1`'s `δ` is `coe` +along a type equality, inverted by `μ-writer`), i.e. the resource +neighbour, not the loss modality. Net: echo is a graded *monad* of +accumulation with a fibre-exact section/retraction *adjunction*; it is +*not* a graded comonad. This sharpens the retracted row from "withdrawn" +to "decided against", and does not resurrect any retracted prose. + == Post-establishment structural extensions (2026-05-27) A substantial layer of structural mechanisation landed after the diff --git a/docs/echo-types/variance-resolution.adoc b/docs/echo-types/variance-resolution.adoc new file mode 100644 index 0000000..f349448 --- /dev/null +++ b/docs/echo-types/variance-resolution.adoc @@ -0,0 +1,235 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += Echo Types — Variance Resolution (monad / comonad / adjunction) +:date: 2026-06-19 +:toc: macro +:toclevels: 3 +:sectnums: +:sectnumlevels: 3 + +[.lead] +This note resolves, *in `--safe` Agda rather than by assertion*, the +precise variance of the loss-graded echo modality: is it a graded +comonad, a graded monad, or a graded adjunction? The resolution is +mechanised in `proofs/agda/EchoVariance.agda` and its headlines are +pinned in `Smoke.agda`. It is written to *inform the redesign* of the +repository's modality/measure architecture. + +toc::[] + +== The live question + +The current, sharpened understanding of an echo-type: + +[quote] +____ +An echo-type is a tropically-graded modality of structured information +loss — an instance of graded-(co)monad machinery over the min-plus +semiring (ℕ ∪ {∞}, min, +), with a section/retraction pair whose +round-trip is *exact on a homotopy fibre* rather than over-approximating +or complement-storing — whose monad/comonad/adjunction status is being +pinned down formally. +____ + +The variance was genuinely unsettled, and for a concrete reason. The +*combining* direction of loss is monadic: accumulation has the shape +`μ : D_r (D_s A) → D_{r+s} A`. So the right word — "graded comonad", +"graded monad", or "graded adjunction (with the section as +unit/counit)" — was a live question to be *resolved in Agda, not +asserted*. + +Two pre-existing facts framed the question: + +* *R-2026-05-18* (`docs/retractions.adoc`) already RETRACTED the + unqualified "graded comonad" claim on `EchoGradedComonad`, reframing + it as a loss-graded *reindexing* modality with **no nested + `D_r D_s`**. So the structure the question is actually about — the + nested comultiplication/multiplication — had not been built where the + retraction left things. +* *Gate F1* (`EchoGradedComonadF1`) DID build a genuine nested graded + comonad with `δ : D (m+n) ⇒ D m (D n)`. But — see §4 — its model + stores its residue, which turns out to be the crux. + +== How the tropical semiring already splits across two axes + +The repository architecture (the `Echo.Modality.*` / `Echo.Measure.*` +foundation surface) already decomposes the min-plus semiring along +exactly the two axes the variance question lives on: + +[cols="1,3,3a",options="header"] +|=== +| Tropical op | Role | Where it lives + +| `min` (⊕, the order / lattice) +| The thin echo *index*. `degrade` reindexes along it. This is the + proof-relevant modality *core* — deliberately semiring-free + (the *measure-independence invariant*). +| `Echo.Index.ThinPoset`, `Echo.Modality.{Interface,Core}` + +| `+` (⊗, accumulation) +| The residue *measure*: a lossy, monotone *observation* + (`measure x ≤ measure (degrade p x)`). The accumulation + `μ : D_r D_s → D_{r+s}` the live question names lives on *this* axis. +| `Echo.Measure.{Interface,Examples}` (incl. `tropical-cost-measure`) +|=== + +So "is loss a comonad or a monad?" is really two questions on two axes: +what is the variance of the `min`-graded reindexing (the modality core), +and what is the variance of the `+`-graded accumulation (the measure / +nesting)? + +== The verdict + +Each clause below is a *pinned theorem* in `EchoVariance.agda`, not a +slogan. `--safe --without-K`, zero postulates; every artefact reuses an +existing kernel theorem. + +=== (1) Accumulation is monadic + +`accumulate : Σ B (λ b → Echo f b × (g b ≡ y)) → Echo (g ∘ f) y` +(`= Echo-comp-iso-from`) is the combining map: a nested loss (an +`f`-echo sitting under a `g`-step) collapses to a single +`(g ∘ f)`-echo. It is *total* and *canonical*: it is definable from the +layered data alone — the factoring `(f, g)` is exactly its input, so no +choice is made. This is the graded-MONAD multiplication shape +`μ : D_r (D_s A) → D_{r+s} A`; the loss magnitudes add. + +=== (2) Recoverability is exact on the fibre + +For a *fixed factoring*, `accumulate` and `split-with-factoring` +(`= Echo-comp-iso-to`) are mutually inverse — both round-trips are +`refl` (`accumulate-split-id`, `split-accumulate-id`). The fibre stores +the loss *precisely*: no over-approximation, no stored complement. + +At grade 0 this is the totality isomorphism +`recoverable-fibre : A ↔ Σ B (Echo f)` (`= A↔ΣEcho`). Its `encode` +(unit) and `decode` (counit) ARE the section/retraction pair — the +unit/counit of the *adjunction* reading. So the "graded adjunction" +candidate is correct, and it is *exact on a homotopy fibre*, precisely as +the sharpened understanding requires. + +=== (3) The comonad direction fails for genuine loss + +A graded *comonad* would supply a *natural* `δ` on the BARE residual +functor: recover the intermediate/layered data from a residue *without +being handed a factoring*. For genuine loss that is exactly the +irreversibility obstruction. The canonical collapse +`collapse : Bool → ⊤` has *no section*: `no-bare-recovery` (via +`no-section-of-collapsing-map`) refutes any `raise : ⊤ → Bool` with +`raise ∘ collapse ≡ id`. + +The forgotten bit is retained on the *fibre* +(`fibre-retains-lost-bit : echo-true ≢ echo-false`, two distinct echoes +over the same residue `tt`) but is *not* a recoverable complement of the +residue — which is exactly why `no-bare-recovery` holds while +`accumulate-split-id` is `refl`. + +=== (4) The "graded comonad" reading is the complement-storing neighbour + +`EchoGradedComonadF1` is a genuine nested graded comonad — but its model +`D r A = A × Boolʳ` (`R X = X × Bool`) *retains* its residue layers. Its +comultiplication is `δ = coe (D-+ m n A)` along the *type equality* +`D (m+n) A ≡ D m (D n A)`, hence INVERTIBLE. `EchoVariance` exhibits the +inverse `μ-writer = coe (sym (D-+ m n A))` and proves both round-trips +(`writer-μ-section`, `writer-δ-section`): the writer is *simultaneously* +a graded comonad and a graded monad. + +That bi-directionality is the signature of a COMPLEMENT-STORING +(resource / coeffect) modality — the loss is not actually lost, it is +filed in the `Bool` layer. This is precisely what the sharpened +understanding says echo-types is *not*: "exact on a homotopy fibre rather +than ... complement-storing". So the graded-comonad reading does not +contradict the verdict; it silently *changes the modality* to the +lossless resource neighbour. + +=== One-line resolution + +[.lead] +Echo-types (fibre-based loss) is a *graded monad* of accumulation (the +`+` axis) together with a section/retraction *adjunction* that is exact on +the grade-0 fibre; it is *not* a graded comonad. The `min` axis (order / +`degrade`) carries the reindexing modality; the `+` axis (accumulation) +carries the monad. The graded-comonad reading is available only on the +complement-storing writer, which is lossless and hence a different +(resource-flavoured) modality. + +This sits the echo modality exactly where the landscape places it: at the +intersection of the grading axis (Katsumata; Fujii–Katsumata–Melliès; +Orchard–Petricek coeffects) and the modal axis, with the modality's +content being *information loss* rather than resource usage, distinguished +from its neighbours by the tropical (worst-case, non-probabilistic) grade +and by carrying recoverability as *fibre-level* rather than +*complement-level* structure. + +== Consequences for the redesign + +. *Keep the modality/measure split; it IS the variance answer.* The + `min` axis (`Echo.Modality.*`, thin-poset `degrade`) and the `+` axis + (`Echo.Measure.*`, accumulation) should remain separate surfaces. The + variance question dissolves once they are not conflated: reindexing + (order) and accumulation (measure) have different variances. + +. *Name the accumulation monad on the measure axis.* The `+`-graded + accumulation `μ : D_r D_s → D_{r+s}` is the graded-monad multiplication. + A future `Echo.Measure.Accumulation` (or similar) can package + `accumulate` + the grade-0 unit as the graded monad of loss, with the + tropical `+` (and `∞` as the absorbing "fully unrecoverable" grade) as + the grade monoid. `EchoVariance.accumulate` is the kernel-level witness + it would build on. + +. *Read `EchoGradedComonad` / F1 / F3 as the complement-storing + neighbour, on the record.* They are correct Agda and a useful + contrast object (the resource sibling), but they are *not* the echo + modality of genuine loss. Any downstream prose that calls echo "a + graded comonad of loss" without the complement-storing caveat is + re-introducing the R-2026-05-18 overclaim. `EchoVariance` is the pin + that fails CI if that slide recurs. + +. *The adjunction is the honest headline for recoverability.* "Exact on + a homotopy fibre" = the grade-0 `A ↔ Σ B (Echo f)` section/retraction. + Recoverability should be stated as this adjunction unit/counit, never as + an all-grade comonadic `extract`/`duplicate` (which would falsely imply + recovery off the fibre). + +== Honest scope + +The verdict is about the *shape* of the canonical structure maps and the +*locus* of recoverability — not a universal categorical impossibility +theorem. Matched-negatives are pinned in `EchoVariance` as `NotProved-*` +⊤-aliases: + +* *Not claimed:* that no graded comonad of any kind touches Echo — F1 is + one, on the complement-storing writer. The claim is that *genuine* + (fibre-based, non-complement-storing) loss is not a graded comonad. +* *Not claimed:* a numeric realisation of the full min-plus grade semiring + (with `∞`) carrying the entire graded-monad law triangle. The measure + seam (`tropical-cost-measure`) supplies the tropical carrier; this work + pins only the variance *shape*. Completing the law triangle over + `ℕ ∪ {∞}` is the natural next rung (consequence 2 above). +* *Not claimed:* that `split-with-factoring` is non-canonical. Given the + factoring it is the unique inverse (clause 2). The obstruction (clause + 3) is strictly about recovery from a *bare* residue with no factoring + supplied. + +== Provenance + +* Mechanisation: `proofs/agda/EchoVariance.agda` (`--safe --without-K`, + zero postulates); pinned in `proofs/agda/Smoke.agda`; wired into + `proofs/agda/All.agda`; classified in + `docs/echo-types/echo-kernel-note.adoc` and `docs/echo-types/MAP.adoc`. +* Reused kernel theorems: `Echo.Echo-comp-iso-{to,from,to-from,from-to}`, + `EchoNoSectionGeneric.no-section-of-collapsing-map`, + `EchoTotalCompletion.A↔ΣEcho`, and `EchoGradedComonadF1.{δ,D-+,coe}`. +* Relationship to the ledger: this *resolves* the variance left open by + R-2026-05-18; it does not resurrect any retracted prose. + +== Revision history + +[cols="1,3",options="header"] +|=== +| Date | Change + +| 2026-06-19 +| Initial resolution. `EchoVariance.agda` lands the five-clause verdict; + this note records it and the redesign consequences. +|=== diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index a88188d..683ebf0 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -102,6 +102,7 @@ open import EchoGradedComonadF1 -- Gate F1 PASSED (graded comonad on iterated-re open import EchoGradedComonadInterface -- Gate F3 abstract record open import EchoGradedComonadInstance1 -- Gate F3 instance 1 (F1 at (ℕ, +, 0)) open import EchoGradedComonadInstance2 -- Gate F3 PASSED — instance 2 at (List Tag, ++, []) +open import EchoVariance -- variance verdict: monad (accumulation) + fibre adjunction, NOT comonad -- Foundation P1: external-fibre triangulation. Echo agrees with the -- standard library's OWN independently-authored notions diff --git a/proofs/agda/EchoVariance.agda b/proofs/agda/EchoVariance.agda new file mode 100644 index 0000000..0779c4d --- /dev/null +++ b/proofs/agda/EchoVariance.agda @@ -0,0 +1,245 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell + +-- EchoVariance — resolving, IN --safe AGDA RATHER THAN ASSERTED, the +-- monad / comonad / adjunction variance of loss accumulation. +-- +-- THE LIVE QUESTION (the new understanding of echo-types). An echo-type +-- is a tropically-graded modality of structured information loss: an +-- instance of graded-(co)monad machinery over the min-plus semiring +-- (ℕ ∪ {∞}, min, +), with recoverability "exact on a homotopy fibre +-- rather than over-approximating or complement-storing". Its precise +-- variance was unsettled: the *combining* direction of loss is monadic +-- (accumulation is μ : D_r (D_s A) → D_{r+s} A), so is the right word +-- "graded comonad", "graded monad", or "graded adjunction (with the +-- section as unit/counit)"? R-2026-05-18 (docs/retractions.adoc) +-- already RETRACTED the unqualified "graded comonad" claim on +-- `EchoGradedComonad`, reframing it as a loss-graded *reindexing* +-- modality with NO nested D_r D_s. This module supplies the nested maps +-- the question is actually about, and lets the type-checker decide. +-- +-- HOW THE TROPICAL SEMIRING SPLITS ACROSS THE TWO AXES (already the +-- repo's architecture): +-- * min (⊕, the order / lattice) is the thin echo INDEX +-- (`Echo.Index.ThinPoset`); `degrade` reindexes along it. This is the +-- proof-relevant modality CORE, deliberately semiring-free. +-- * + (⊗, accumulation) is the residue MEASURE (`Echo.Measure.*`), a +-- lossy, monotone OBSERVATION. The accumulation μ : D_r D_s → D_{r+s} +-- the live question names lives on THIS axis. +-- +-- THE VERDICT (each clause proved below, not asserted): +-- +-- (1) ACCUMULATION IS MONADIC. The combining map μ on the genuine +-- (fibre) loss modality — nested loss → combined loss — is total +-- and CANONICAL: it is definable from the layered data alone (the +-- factoring is its input). `accumulate` = `Echo-comp-iso-from`. +-- This is the graded-monad multiplication shape; the loss +-- magnitudes add. +-- +-- (2) RECOVERABILITY IS EXACT ON THE FIBRE. For a FIXED factoring, +-- accumulate and split are mutually inverse (both round-trips +-- `refl`): the fibre stores the loss precisely — not over- +-- approximating, not complement-storing. At grade 0 this is the +-- totality iso `A ↔ Σ B (Echo f)` (`recoverable-fibre`): the +-- section/retraction pair, i.e. the unit/counit of the ADJUNCTION +-- reading. +-- +-- (3) THE COMONAD DIRECTION FAILS FOR GENUINE LOSS. A graded comonad +-- would supply a NATURAL δ on the BARE residual functor: recover the +-- intermediate/layered data from a residue WITHOUT being handed a +-- factoring. For genuine loss that is exactly the irreversibility +-- obstruction: the canonical collapse has NO section +-- (`no-bare-recovery`). The forgotten bit is retained ON THE FIBRE +-- (`fibre-retains-lost-bit`) but is NOT a recoverable complement of +-- the residue. +-- +-- (4) THE "GRADED COMONAD" READING IS THE COMPLEMENT-STORING NEIGHBOUR. +-- `EchoGradedComonadF1` IS a genuine nested graded comonad — but its +-- model `D r A = A × Boolʳ` RETAINS its residue layers, so its δ is +-- `coe` along a TYPE EQUALITY `D (m+n) A ≡ D m (D n A)`, hence +-- INVERTIBLE. We exhibit the inverse `μ-writer` and prove both +-- round-trips: the writer is simultaneously a graded comonad AND a +-- graded monad. That bi-directionality is the signature of a +-- COMPLEMENT-STORING (resource / coeffect) modality — precisely what +-- the new understanding says echo-types is NOT. +-- +-- ONE-LINE RESOLUTION. Echo-types (fibre-based loss) is a GRADED MONAD of +-- accumulation (the + axis) together with a section/retraction ADJUNCTION +-- that is exact on the grade-0 fibre; it is NOT a graded comonad — the +-- comonad reading silently substitutes the complement-storing writer, +-- which is lossless. The min axis (order / `degrade`) carries the +-- reindexing modality; the + axis (accumulation) carries the monad. +-- +-- --safe --without-K, zero postulates. Everything reuses existing kernel +-- theorems (`Echo-comp-iso`, `no-section-of-collapsing-map`, `A↔ΣEcho`, +-- and F1's `δ`/`D-+`/`coe`); nothing here is new trust. + +module EchoVariance where + +open import Level using (Level) +open import Function.Base using (_∘_) +open import Function.Bundles using (_↔_) +open import Data.Nat.Base using (ℕ; _+_) +open import Data.Bool.Base using (Bool; true; false) +open import Data.Product.Base using (Σ; _,_; _×_) +open import Data.Unit.Base using (⊤) +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym) +open import Relation.Nullary using (¬_) + +open import Echo + using ( Echo + ; Echo-comp-iso-to ; Echo-comp-iso-from + ; Echo-comp-iso-from-to ; Echo-comp-iso-to-from ) +open import EchoCharacteristic + using ( collapse ; echo-true ; echo-false ; echo-true≢echo-false ) +open import EchoNoSectionGeneric using ( no-section-of-collapsing-map ) +open import EchoTotalCompletion using ( A↔ΣEcho ) +open import EchoGradedComonadF1 using ( D ; δ ; D-+ ; coe ) + +private variable + ℓa ℓb ℓc : Level + A : Set ℓa + B : Set ℓb + C : Set ℓc + +---------------------------------------------------------------------- +-- (1) ACCUMULATION IS MONADIC — μ : D_r (D_s A) → D_{r+s} A. +-- +-- A "nested loss" is an f-echo sitting under a g-step: the layered data +-- `Σ B (λ b → Echo f b × (g b ≡ y))`. `accumulate` composes the two +-- layers into a single (g ∘ f)-echo. It is TOTAL and CANONICAL: it is +-- definable from the layered data alone — the factoring (f, g) is exactly +-- its input — so no choice is made. This is the graded-MONAD +-- multiplication shape, and the loss magnitudes accumulate (the +-- (g ∘ f)-fibre carries both the f-witness and the g-witness). +---------------------------------------------------------------------- + +accumulate : + (f : A → B) (g : B → C) {y : C} → + Σ B (λ b → Echo f b × (g b ≡ y)) → Echo (g ∘ f) y +accumulate f g = Echo-comp-iso-from f g + +-- δ for a FIXED factoring (f, g): split the combined echo back into the +-- layered data. Total ONLY because the factoring is supplied as data — +-- contrast (3), where no factoring is given. +split-with-factoring : + (f : A → B) (g : B → C) {y : C} → + Echo (g ∘ f) y → Σ B (λ b → Echo f b × (g b ≡ y)) +split-with-factoring f g = Echo-comp-iso-to f g + +---------------------------------------------------------------------- +-- (2) RECOVERABILITY IS EXACT ON THE FIBRE. +-- +-- For a FIXED factoring the two maps are mutually inverse — both +-- round-trips are `refl`. The fibre stores the loss precisely: no +-- over-approximation, no stored complement. This is the +-- "exact-on-a-homotopy-fibre" half of the verdict at the level of a +-- single layered computation. +---------------------------------------------------------------------- + +accumulate-split-id : + (f : A → B) (g : B → C) {y : C} (e : Echo (g ∘ f) y) → + accumulate f g (split-with-factoring f g e) ≡ e +accumulate-split-id f g = Echo-comp-iso-from-to f g + +split-accumulate-id : + (f : A → B) (g : B → C) {y : C} + (r : Σ B (λ b → Echo f b × (g b ≡ y))) → + split-with-factoring f g (accumulate f g r) ≡ r +split-accumulate-id f g = Echo-comp-iso-to-from f g + +-- The grade-0 instance: A ≅ Σ B (Echo f). The unit (encode) / counit +-- (decode) of the section/retraction ADJUNCTION live on the grade-0 +-- fibre. This is the "section/retraction pair whose round-trip is exact +-- on a homotopy fibre", pinned as a genuine ↔. +recoverable-fibre : (f : A → B) → A ↔ Σ B (Echo f) +recoverable-fibre = A↔ΣEcho + +---------------------------------------------------------------------- +-- (3) THE COMONAD DIRECTION FAILS FOR GENUINE LOSS. +-- +-- A graded COMONAD would supply a NATURAL δ on the BARE residual functor: +-- recover the intermediate / layered data from a residue WITHOUT being +-- handed a factoring. For genuine loss that is the irreversibility +-- obstruction. The canonical collapse `collapse : Bool → ⊤` has NO +-- section: no `raise : ⊤ → Bool` satisfies `raise ∘ collapse ≡ id`. The +-- forgotten bit cannot be recovered from the residue alone — genuine loss +-- does NOT store its complement. +---------------------------------------------------------------------- + +no-bare-recovery : + ¬ Σ (⊤ → Bool) (λ raise → ∀ b → raise (collapse b) ≡ b) +no-bare-recovery = + no-section-of-collapsing-map collapse true false (λ ()) refl + +-- The fibre nevertheless retains the lost bit EXACTLY: `echo-true` and +-- `echo-false` are distinct echoes over the SAME residue `tt`. The loss +-- is stored on the FIBRE, not as a recoverable residue-complement — which +-- is exactly why `no-bare-recovery` holds while `accumulate-split-id` +-- is `refl`. +fibre-retains-lost-bit : echo-true ≢ echo-false +fibre-retains-lost-bit = echo-true≢echo-false + +---------------------------------------------------------------------- +-- (4) THE "GRADED COMONAD" READING IS THE COMPLEMENT-STORING NEIGHBOUR. +-- +-- `EchoGradedComonadF1` is a genuine nested graded comonad, but its model +-- `D r A = A × Boolʳ` RETAINS its residue layers. Its comultiplication is +-- `δ = coe (D-+ m n A)` along the TYPE EQUALITY `D (m+n) A ≡ D m (D n A)`, +-- so it is INVERTIBLE. We exhibit the inverse `μ-writer` and prove both +-- round-trips: the writer is simultaneously a graded comonad AND a graded +-- monad. That bi-directionality is the signature of a COMPLEMENT-STORING +-- (resource / coeffect) modality — precisely what echo-types is NOT. +-- +-- `μ-writer : D_m (D_n A) → D_{m+n} A` — note the type literally adds the +-- grades m + n, the additive (⊗ = +) axis of the tropical semiring. +---------------------------------------------------------------------- + +coe-sym : ∀ {X Y : Set} (p : X ≡ Y) (x : X) → coe (sym p) (coe p x) ≡ x +coe-sym refl x = refl + +coe-sym′ : ∀ {X Y : Set} (p : X ≡ Y) (y : Y) → coe p (coe (sym p) y) ≡ y +coe-sym′ refl y = refl + +μ-writer : ∀ m n {A : Set} → D m (D n A) → D (m + n) A +μ-writer m n {A} = coe (sym (D-+ m n A)) + +-- μ-writer is a SECTION of F1's δ: combining-then-splitting is the +-- identity. (δ m n = coe (D-+ m n A).) +writer-μ-section : + ∀ m n {A : Set} (x : D (m + n) A) → μ-writer m n (δ m n x) ≡ x +writer-μ-section m n {A} = coe-sym (D-+ m n A) + +-- μ-writer is also a RETRACTION of δ: splitting-then-combining is the +-- identity. Together these show δ is an isomorphism — the writer is +-- LOSSLESS, hence both a graded comonad and a graded monad. +writer-δ-section : + ∀ m n {A : Set} (y : D m (D n A)) → δ m n (μ-writer m n y) ≡ y +writer-δ-section m n {A} = coe-sym′ (D-+ m n A) + +---------------------------------------------------------------------- +-- Honest scope. Matched-negatives as ⊤-aliases (so `grep NotProved` +-- catches them). The verdict is about the SHAPE of the canonical +-- structure maps and the LOCUS of recoverability — not a universal +-- categorical impossibility theorem. +---------------------------------------------------------------------- + +-- NOT claimed: that no graded comonad of any kind touches Echo. F1 is one +-- — on the complement-storing writer. The claim is that GENUINE +-- (fibre-based, non-complement-storing) loss is not a graded comonad. +NotProved-no-graded-comonad-of-any-kind : Set +NotProved-no-graded-comonad-of-any-kind = ⊤ + +-- NOT claimed: a numeric realisation of the min-plus grade semiring with +-- ∞ and the full graded-monad law triangle. The MEASURE seam +-- (`Echo.Measure.Examples.tropical-cost-measure`) supplies the tropical +-- carrier; this module pins only the variance SHAPE. +NotProved-full-min-plus-graded-monad-laws : Set +NotProved-full-min-plus-graded-monad-laws = ⊤ + +-- NOT claimed: that `split-with-factoring` is non-canonical. Given the +-- factoring it is the unique inverse (2). The obstruction (3) is strictly +-- about recovery from a BARE residue with no factoring supplied. +NotProved-no-split-even-with-factoring : Set +NotProved-no-split-even-with-factoring = ⊤ diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index cc9f949..4650d83 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -940,6 +940,28 @@ open import EchoGradedComonadInstance2 using ; list-instance -- the second graded-comonad instance ) +-- Variance verdict (docs/echo-types/variance-resolution.adoc): the +-- monad / comonad / adjunction status of loss accumulation, resolved in +-- --safe Agda rather than asserted. Accumulation is the graded-MONAD +-- multiplication (total + canonical); recoverability is exact on the +-- grade-0 fibre (the section/retraction adjunction); the graded-COMONAD +-- direction fails for genuine loss (no bare-residue recovery); the +-- "graded comonad" reading (F1) is the LOSSLESS complement-storing writer +-- (δ invertible). Pinned so a slide back to an unqualified "graded +-- comonad of loss" claim fails CI fast. +open import EchoVariance using + ( accumulate -- μ : D_r (D_s A) → D_{r+s} A — accumulation is monadic + ; split-with-factoring -- δ given the factoring (its inverse) + ; accumulate-split-id -- exact on the fibre (round-trip refl) + ; split-accumulate-id -- exact on the fibre (round-trip refl) + ; recoverable-fibre -- A ↔ Σ B (Echo f): the grade-0 section/retraction adjunction + ; no-bare-recovery -- the comonad obstruction: collapse has no section + ; fibre-retains-lost-bit -- the lost bit lives on the fibre, not as a complement + ; μ-writer -- F1 writer's accumulation (inverse of δ) + ; writer-μ-section -- writer δ is invertible ⇒ LOSSLESS (complement-storing) + ; writer-δ-section -- … both round-trips + ) + open import EchoTropical using ( Candidate ; score