|
| 1 | +// SPDX-License-Identifier: CC-BY-SA-4.0 |
| 2 | +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += Echo Types — Variance Resolution (monad / comonad / adjunction) |
| 4 | +:date: 2026-06-19 |
| 5 | +:toc: macro |
| 6 | +:toclevels: 3 |
| 7 | +:sectnums: |
| 8 | +:sectnumlevels: 3 |
| 9 | + |
| 10 | +[.lead] |
| 11 | +This note resolves, *in `--safe` Agda rather than by assertion*, the |
| 12 | +precise variance of the loss-graded echo modality: is it a graded |
| 13 | +comonad, a graded monad, or a graded adjunction? The resolution is |
| 14 | +mechanised in `proofs/agda/EchoVariance.agda` and its headlines are |
| 15 | +pinned in `Smoke.agda`. It is written to *inform the redesign* of the |
| 16 | +repository's modality/measure architecture. |
| 17 | + |
| 18 | +toc::[] |
| 19 | + |
| 20 | +== The live question |
| 21 | + |
| 22 | +The current, sharpened understanding of an echo-type: |
| 23 | + |
| 24 | +[quote] |
| 25 | +____ |
| 26 | +An echo-type is a tropically-graded modality of structured information |
| 27 | +loss — an instance of graded-(co)monad machinery over the min-plus |
| 28 | +semiring (ℕ ∪ {∞}, min, +), with a section/retraction pair whose |
| 29 | +round-trip is *exact on a homotopy fibre* rather than over-approximating |
| 30 | +or complement-storing — whose monad/comonad/adjunction status is being |
| 31 | +pinned down formally. |
| 32 | +____ |
| 33 | + |
| 34 | +The variance was genuinely unsettled, and for a concrete reason. The |
| 35 | +*combining* direction of loss is monadic: accumulation has the shape |
| 36 | +`μ : D_r (D_s A) → D_{r+s} A`. So the right word — "graded comonad", |
| 37 | +"graded monad", or "graded adjunction (with the section as |
| 38 | +unit/counit)" — was a live question to be *resolved in Agda, not |
| 39 | +asserted*. |
| 40 | + |
| 41 | +Two pre-existing facts framed the question: |
| 42 | + |
| 43 | +* *R-2026-05-18* (`docs/retractions.adoc`) already RETRACTED the |
| 44 | + unqualified "graded comonad" claim on `EchoGradedComonad`, reframing |
| 45 | + it as a loss-graded *reindexing* modality with **no nested |
| 46 | + `D_r D_s`**. So the structure the question is actually about — the |
| 47 | + nested comultiplication/multiplication — had not been built where the |
| 48 | + retraction left things. |
| 49 | +* *Gate F1* (`EchoGradedComonadF1`) DID build a genuine nested graded |
| 50 | + comonad with `δ : D (m+n) ⇒ D m (D n)`. But — see §4 — its model |
| 51 | + stores its residue, which turns out to be the crux. |
| 52 | + |
| 53 | +== How the tropical semiring already splits across two axes |
| 54 | + |
| 55 | +The repository architecture (the `Echo.Modality.*` / `Echo.Measure.*` |
| 56 | +foundation surface) already decomposes the min-plus semiring along |
| 57 | +exactly the two axes the variance question lives on: |
| 58 | + |
| 59 | +[cols="1,3,3a",options="header"] |
| 60 | +|=== |
| 61 | +| Tropical op | Role | Where it lives |
| 62 | + |
| 63 | +| `min` (⊕, the order / lattice) |
| 64 | +| The thin echo *index*. `degrade` reindexes along it. This is the |
| 65 | + proof-relevant modality *core* — deliberately semiring-free |
| 66 | + (the *measure-independence invariant*). |
| 67 | +| `Echo.Index.ThinPoset`, `Echo.Modality.{Interface,Core}` |
| 68 | + |
| 69 | +| `+` (⊗, accumulation) |
| 70 | +| The residue *measure*: a lossy, monotone *observation* |
| 71 | + (`measure x ≤ measure (degrade p x)`). The accumulation |
| 72 | + `μ : D_r D_s → D_{r+s}` the live question names lives on *this* axis. |
| 73 | +| `Echo.Measure.{Interface,Examples}` (incl. `tropical-cost-measure`) |
| 74 | +|=== |
| 75 | + |
| 76 | +So "is loss a comonad or a monad?" is really two questions on two axes: |
| 77 | +what is the variance of the `min`-graded reindexing (the modality core), |
| 78 | +and what is the variance of the `+`-graded accumulation (the measure / |
| 79 | +nesting)? |
| 80 | + |
| 81 | +== The verdict |
| 82 | + |
| 83 | +Each clause below is a *pinned theorem* in `EchoVariance.agda`, not a |
| 84 | +slogan. `--safe --without-K`, zero postulates; every artefact reuses an |
| 85 | +existing kernel theorem. |
| 86 | + |
| 87 | +=== (1) Accumulation is monadic |
| 88 | + |
| 89 | +`accumulate : Σ B (λ b → Echo f b × (g b ≡ y)) → Echo (g ∘ f) y` |
| 90 | +(`= Echo-comp-iso-from`) is the combining map: a nested loss (an |
| 91 | +`f`-echo sitting under a `g`-step) collapses to a single |
| 92 | +`(g ∘ f)`-echo. It is *total* and *canonical*: it is definable from the |
| 93 | +layered data alone — the factoring `(f, g)` is exactly its input, so no |
| 94 | +choice is made. This is the graded-MONAD multiplication shape |
| 95 | +`μ : D_r (D_s A) → D_{r+s} A`; the loss magnitudes add. |
| 96 | + |
| 97 | +=== (2) Recoverability is exact on the fibre |
| 98 | + |
| 99 | +For a *fixed factoring*, `accumulate` and `split-with-factoring` |
| 100 | +(`= Echo-comp-iso-to`) are mutually inverse — both round-trips are |
| 101 | +`refl` (`accumulate-split-id`, `split-accumulate-id`). The fibre stores |
| 102 | +the loss *precisely*: no over-approximation, no stored complement. |
| 103 | + |
| 104 | +At grade 0 this is the totality isomorphism |
| 105 | +`recoverable-fibre : A ↔ Σ B (Echo f)` (`= A↔ΣEcho`). Its `encode` |
| 106 | +(unit) and `decode` (counit) ARE the section/retraction pair — the |
| 107 | +unit/counit of the *adjunction* reading. So the "graded adjunction" |
| 108 | +candidate is correct, and it is *exact on a homotopy fibre*, precisely as |
| 109 | +the sharpened understanding requires. |
| 110 | + |
| 111 | +=== (3) The comonad direction fails for genuine loss |
| 112 | + |
| 113 | +A graded *comonad* would supply a *natural* `δ` on the BARE residual |
| 114 | +functor: recover the intermediate/layered data from a residue *without |
| 115 | +being handed a factoring*. For genuine loss that is exactly the |
| 116 | +irreversibility obstruction. The canonical collapse |
| 117 | +`collapse : Bool → ⊤` has *no section*: `no-bare-recovery` (via |
| 118 | +`no-section-of-collapsing-map`) refutes any `raise : ⊤ → Bool` with |
| 119 | +`raise ∘ collapse ≡ id`. |
| 120 | + |
| 121 | +The forgotten bit is retained on the *fibre* |
| 122 | +(`fibre-retains-lost-bit : echo-true ≢ echo-false`, two distinct echoes |
| 123 | +over the same residue `tt`) but is *not* a recoverable complement of the |
| 124 | +residue — which is exactly why `no-bare-recovery` holds while |
| 125 | +`accumulate-split-id` is `refl`. |
| 126 | + |
| 127 | +=== (4) The "graded comonad" reading is the complement-storing neighbour |
| 128 | + |
| 129 | +`EchoGradedComonadF1` is a genuine nested graded comonad — but its model |
| 130 | +`D r A = A × Boolʳ` (`R X = X × Bool`) *retains* its residue layers. Its |
| 131 | +comultiplication is `δ = coe (D-+ m n A)` along the *type equality* |
| 132 | +`D (m+n) A ≡ D m (D n A)`, hence INVERTIBLE. `EchoVariance` exhibits the |
| 133 | +inverse `μ-writer = coe (sym (D-+ m n A))` and proves both round-trips |
| 134 | +(`writer-μ-section`, `writer-δ-section`): the writer is *simultaneously* |
| 135 | +a graded comonad and a graded monad. |
| 136 | + |
| 137 | +That bi-directionality is the signature of a COMPLEMENT-STORING |
| 138 | +(resource / coeffect) modality — the loss is not actually lost, it is |
| 139 | +filed in the `Bool` layer. This is precisely what the sharpened |
| 140 | +understanding says echo-types is *not*: "exact on a homotopy fibre rather |
| 141 | +than ... complement-storing". So the graded-comonad reading does not |
| 142 | +contradict the verdict; it silently *changes the modality* to the |
| 143 | +lossless resource neighbour. |
| 144 | + |
| 145 | +=== One-line resolution |
| 146 | + |
| 147 | +[.lead] |
| 148 | +Echo-types (fibre-based loss) is a *graded monad* of accumulation (the |
| 149 | +`+` axis) together with a section/retraction *adjunction* that is exact on |
| 150 | +the grade-0 fibre; it is *not* a graded comonad. The `min` axis (order / |
| 151 | +`degrade`) carries the reindexing modality; the `+` axis (accumulation) |
| 152 | +carries the monad. The graded-comonad reading is available only on the |
| 153 | +complement-storing writer, which is lossless and hence a different |
| 154 | +(resource-flavoured) modality. |
| 155 | + |
| 156 | +This sits the echo modality exactly where the landscape places it: at the |
| 157 | +intersection of the grading axis (Katsumata; Fujii–Katsumata–Melliès; |
| 158 | +Orchard–Petricek coeffects) and the modal axis, with the modality's |
| 159 | +content being *information loss* rather than resource usage, distinguished |
| 160 | +from its neighbours by the tropical (worst-case, non-probabilistic) grade |
| 161 | +and by carrying recoverability as *fibre-level* rather than |
| 162 | +*complement-level* structure. |
| 163 | + |
| 164 | +== Consequences for the redesign |
| 165 | + |
| 166 | +. *Keep the modality/measure split; it IS the variance answer.* The |
| 167 | + `min` axis (`Echo.Modality.*`, thin-poset `degrade`) and the `+` axis |
| 168 | + (`Echo.Measure.*`, accumulation) should remain separate surfaces. The |
| 169 | + variance question dissolves once they are not conflated: reindexing |
| 170 | + (order) and accumulation (measure) have different variances. |
| 171 | + |
| 172 | +. *Name the accumulation monad on the measure axis.* The `+`-graded |
| 173 | + accumulation `μ : D_r D_s → D_{r+s}` is the graded-monad multiplication. |
| 174 | + A future `Echo.Measure.Accumulation` (or similar) can package |
| 175 | + `accumulate` + the grade-0 unit as the graded monad of loss, with the |
| 176 | + tropical `+` (and `∞` as the absorbing "fully unrecoverable" grade) as |
| 177 | + the grade monoid. `EchoVariance.accumulate` is the kernel-level witness |
| 178 | + it would build on. |
| 179 | + |
| 180 | +. *Read `EchoGradedComonad` / F1 / F3 as the complement-storing |
| 181 | + neighbour, on the record.* They are correct Agda and a useful |
| 182 | + contrast object (the resource sibling), but they are *not* the echo |
| 183 | + modality of genuine loss. Any downstream prose that calls echo "a |
| 184 | + graded comonad of loss" without the complement-storing caveat is |
| 185 | + re-introducing the R-2026-05-18 overclaim. `EchoVariance` is the pin |
| 186 | + that fails CI if that slide recurs. |
| 187 | + |
| 188 | +. *The adjunction is the honest headline for recoverability.* "Exact on |
| 189 | + a homotopy fibre" = the grade-0 `A ↔ Σ B (Echo f)` section/retraction. |
| 190 | + Recoverability should be stated as this adjunction unit/counit, never as |
| 191 | + an all-grade comonadic `extract`/`duplicate` (which would falsely imply |
| 192 | + recovery off the fibre). |
| 193 | + |
| 194 | +== Honest scope |
| 195 | + |
| 196 | +The verdict is about the *shape* of the canonical structure maps and the |
| 197 | +*locus* of recoverability — not a universal categorical impossibility |
| 198 | +theorem. Matched-negatives are pinned in `EchoVariance` as `NotProved-*` |
| 199 | +⊤-aliases: |
| 200 | + |
| 201 | +* *Not claimed:* that no graded comonad of any kind touches Echo — F1 is |
| 202 | + one, on the complement-storing writer. The claim is that *genuine* |
| 203 | + (fibre-based, non-complement-storing) loss is not a graded comonad. |
| 204 | +* *Not claimed:* a numeric realisation of the full min-plus grade semiring |
| 205 | + (with `∞`) carrying the entire graded-monad law triangle. The measure |
| 206 | + seam (`tropical-cost-measure`) supplies the tropical carrier; this work |
| 207 | + pins only the variance *shape*. Completing the law triangle over |
| 208 | + `ℕ ∪ {∞}` is the natural next rung (consequence 2 above). |
| 209 | +* *Not claimed:* that `split-with-factoring` is non-canonical. Given the |
| 210 | + factoring it is the unique inverse (clause 2). The obstruction (clause |
| 211 | + 3) is strictly about recovery from a *bare* residue with no factoring |
| 212 | + supplied. |
| 213 | + |
| 214 | +== Provenance |
| 215 | + |
| 216 | +* Mechanisation: `proofs/agda/EchoVariance.agda` (`--safe --without-K`, |
| 217 | + zero postulates); pinned in `proofs/agda/Smoke.agda`; wired into |
| 218 | + `proofs/agda/All.agda`; classified in |
| 219 | + `docs/echo-types/echo-kernel-note.adoc` and `docs/echo-types/MAP.adoc`. |
| 220 | +* Reused kernel theorems: `Echo.Echo-comp-iso-{to,from,to-from,from-to}`, |
| 221 | + `EchoNoSectionGeneric.no-section-of-collapsing-map`, |
| 222 | + `EchoTotalCompletion.A↔ΣEcho`, and `EchoGradedComonadF1.{δ,D-+,coe}`. |
| 223 | +* Relationship to the ledger: this *resolves* the variance left open by |
| 224 | + R-2026-05-18; it does not resurrect any retracted prose. |
| 225 | + |
| 226 | +== Revision history |
| 227 | + |
| 228 | +[cols="1,3",options="header"] |
| 229 | +|=== |
| 230 | +| Date | Change |
| 231 | + |
| 232 | +| 2026-06-19 |
| 233 | +| Initial resolution. `EchoVariance.agda` lands the five-clause verdict; |
| 234 | + this note records it and the redesign consequences. |
| 235 | +|=== |
0 commit comments