F1 PASSED: gc-coassoc closed (earn-back gate, R-2026-05-18 follow-up) (#86)

## Summary

Gate **F1** of the earn-back plan — the MAKE-OR-BREAK retraction from
[R-2026-05-18](../blob/main/docs/retractions.adoc) — now passes.

The 2026-05-18 spike `EchoGradedComonadF1.agda` had two of three
graded-comonad laws closed (`gc-counit-l`, `gc-counit-r`) and named
the remaining obstruction precisely: an isolated proof-engineering
type-mismatch at the inductive step of `gc-coassoc`, requiring an
explicit δ-naturality lemma over the outer `R` layer rather than the
ad-hoc `coe-cong-R ∘ sym` push. This PR discharges that obligation:

```agda
δ-suc : ∀ m n {A} (x : D (m + n) A) (b : Bool) →
        δ (suc m) n {A} (x , b) ≡ (δ m n x , b)
δ-suc m n {A} x b = coe-cong-R (D-+ m n A) x b
```

This factor + the existing `subst-D-suc` let `gc-coassoc` close as a
six-step `≡-Reasoning` chain. Stdlib's `+-assoc (suc m) n p` reduces
*definitionally* to `cong suc (+-assoc m n p)`, so the two ℕ-equation
proofs at the chain ends are syntactically identical and **ℕ-UIP is
not needed for `gc-coassoc` itself** (`gc-counit-l` still uses ℕ-UIP,
which is K-free via Hedberg / decidable equality).

## Mechanised content of F1

* Grade monoid `(ℕ, +, 0)`; `D 0 A = A`; `D (suc r) A = R (D r A)`
  where `R X = X × Bool` — a non-collapsing residue layer.
* `mapD r f` functorial (`mapD-id`, `mapD-∘`).
* `ε : D 0 A → A` — counit at the unit grade.
* `δ : D (m + n) A → D m (D n A)` — **NESTED** comultiplication.
* `gc-counit-r` (definitional), `gc-counit-l` (induction on grade),
  `gc-coassoc` (this PR).
* `D2-nontrivial` — separating witness that `D r` is not `⊤` / a prop.
* Echo is the grade-unit object: `D 0 (Echo f y) ≡ Echo f y`.

`--safe --without-K`, **zero postulates**, zero escape pragmas, no
funext. Wired into `All.agda` and pinned in `Smoke.agda`.

## Scope (please re-read with care)

F1 earns back the **existence** of a graded comonad with Echo as the
grade-unit object — that's the claim R-2026-05-18 retracted at its
strongest reading. It does **NOT** retroactively make `EchoGraded`
itself a graded comonad: `EchoGraded` remains a thin-poset reindexing
modality on a three-element lattice, with no nested family, no monoid
multiplication, no `D r r' ⇒ D r ∘ D r'`. The paper's title and central
thesis (Echo as a reindexing modality) stand unchanged; F1 enters the
codebase as an *additional* mechanised contribution beside
`EchoGraded`.

## What this unblocks

Gate **F3** — a genuinely independent second model of the comonad at
a different grade monoid (e.g. tropical or multiplicative semiring),
without a `× ⊤` carrier or a `⊑-prop`-equivalent field — is now in
scope. F3 is **not** started by this PR.

## Doc changes (gated, scoped)

* `docs/echo-types/earn-back-plan.adoc` — ledger row A1 + Status
  entry (F1 PASSED 2026-05-20), with the scope qualifier pinned.
* `docs/retractions.adoc` — follow-up **F-2026-05-20a** appended
  (append-only revision policy preserved); no edits to other doc
  bodies.
* `paper.adoc`, `types-abstract.adoc`, `conservativity.adoc` —
  **intentionally untouched** in this PR. Their bodies are about
  `EchoGraded`'s thin-poset structure, which F1 does not change.
  Whether to add a bounded new-contribution paragraph mentioning the
  F1 side-construction is **owner-gated**.

## Test plan

* [x] `agda proofs/agda/All.agda` exit 0 under `--safe --without-K`
* [x] `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`
* [x] `grep -nE '^\s*postulate\b|BUILTIN
REWRITE|NON_TERMINATING|TERMINATING'
      proofs/agda/EchoGradedComonadF1.agda` returns no matches in code
* [x] `--safe --without-K` OPTIONS line preserved on the F1 module
* [ ] (owner) confirm the scope language in `retractions.adoc`
      F-2026-05-20a matches intent
* [ ] (owner) decide whether `paper.adoc` / `types-abstract.adoc` /
      `conservativity.adoc` should gain a bounded contribution
      paragraph in a separate PR

## Non-overlap with parallel sessions

Touches: `EchoGradedComonadF1.agda` (existing 2026-05-18 spike,
finishing it), `All.agda` (one-line F1 import), `Smoke.agda` (F1 pin
block), `earn-back-plan.adoc`, `retractions.adoc`.

Stays clear of:
* `proofs/agda/Ordinal/**` — the Brouwer-arithmetic / `_<ᵇ⁻_` /
  rank-mono session's territory.
* Any module the recent estate PRs (#80 EchoSearch, #81
EchoExampleProvenance,
  #83 EchoExampleParser) added — restored their imports cleanly
  during the rebase onto fresh `origin/main`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/echo-types/earn-back-plan.adoc

@@ -189,9 +189,13 @@ single index; it moves no claim.
 
 | A1
 | *F1* — `gc-coassoc` (graded-comonad coassociativity),
-  `proofs/agda/EchoGradedComonadF1.agda`. Needs an explicit
-  δ-naturality-over-`R` lemma. Spike not wired into `All`/`Smoke`.
-| Open, *not postulated*. Feasibility decided *positive* (see Status).
+  `proofs/agda/EchoGradedComonadF1.agda`.
+| *PASSED 2026-05-20* — `gc-coassoc` closed via the predicted
+  `δ`-naturality-over-`R` (`δ-suc`) + `subst-D-suc` factoring; stdlib
+  `+-assoc (suc m) n p` reduces to `cong suc (+-assoc m n p)`, so
+  ℕ-UIP was *not* needed for coassoc. `--safe --without-K`, zero
+  postulates, wired into `All`/`Smoke`. Retraction follow-up
+  F-2026-05-20a. Unblocks A3 / F3.
 
 | A2
 | *F2* — real second model of the bare Echo functor via
@@ -262,8 +266,8 @@ single index; it moves no claim.
   spikes wired into `All`/`Smoke`, scoped claims moved (follow-up
   F-2026-05-18a). Each earned back a qualified/real claim
   independently of F1.
-. *F1 coassoc* (A1) — one obligation, feasibility decided; closes the
-  make-or-break and unlocks *F3* (A3). Now the next action.
+. *F1 coassoc* (A1) — *DONE 2026-05-20*: passed via the predicted
+  `δ`-naturality-over-`R` factoring; unblocks *F3* (A3).
 . *Doc-integrity* (D) — reconcile alongside step 1; removes a drift
   vector at near-zero cost.
 . *Buchholz* (B) — separate long-tail; keep the `ExtendedOrder`
@@ -312,3 +316,28 @@ single index; it moves no claim.
   *Strictly scoped:* F2 is the Echo functor only — the graded-comonad,
   model-independence, and conservativity claims remain retracted; F1
   (coassoc) and F3 remain open.
+
+* *2026-05-20 — Gate F1 PASSED.* `gc-coassoc` closed via the
+  predicted `δ`-naturality-over-`R` (`δ-suc`) + `subst-D-suc`
+  factoring; stdlib `+-assoc (suc m) n p` reduces definitionally to
+  `cong suc (+-assoc m n p)` (recursion on left), so the two
+  ℕ-equation proofs on the chain ends are syntactically identical
+  and ℕ-UIP was *not* needed for coassoc itself. `EchoGradedComonadF1.agda`
+  now ships all three graded-comonad laws + the separating witness
+  `D2-nontrivial`; `--safe --without-K`, zero postulates, no funext;
+  wired into `All.agda` and pinned in `Smoke.agda`. Full + smoke
+  build green. Retraction follow-up F-2026-05-20a.
++
+*Strictly scoped (re-read with care):* F1 earns back the
+*existence* of a graded comonad with Echo as the grade-unit object
+(`D 0 (Echo f y)` is the bare echo, the nested comultiplication is
+real, all three laws hold, the carrier is non-trivial). It does
+*not* retroactively make `EchoGraded` a graded comonad — `EchoGraded`
+remains a thin-poset reindexing modality per R-2026-05-18, on a
+different structure (`Grade = 3-element lattice`, no nested family,
+no monoid multiplication, no `D r r' ⇒ D r ∘ D r'`). The paper's
+title and central thesis (Echo as a reindexing modality) stand
+unchanged; the F1 result is an *additional* mechanised contribution
+sitting beside `EchoGraded`, not a reinstatement of it. F3
+(independent second comonad model at a different grade monoid) is
+now unblocked.

docs/retractions.adoc

@@ -192,6 +192,74 @@ note), `docs/echo-types/conservativity.adoc` (scope), and
 to the *conditional/scoped* earned claim, never beyond it;
 `docs/echo-types/earn-back-plan.adoc` ledger rows A2/A4 and Status.
 
+==== Follow-up F-2026-05-20a (2026-05-20) — Gate F1 passed
+
+The make-or-break gate of R-2026-05-18 — Gate F1, a *genuine*
+graded comonad with Echo as the grade-unit object and a nested
+comultiplication — *passes* under the `EchoGradedComonadF1.agda`
+candidate (monoid-graded iterated-residue carrier `D : ℕ → Set →
+Set`, grade monoid `(ℕ, +, 0)`, `R X = X × Bool` informative
+residue layer).
+
+[cols="1,4", options="header"]
+|===
+| Gate | Earned-back claim (exact strength — nothing beyond)
+
+| *F1*
+| `proofs/agda/EchoGradedComonadF1.agda`. There exists a graded
+  functor `D : ℕ → Set → Set` with: `mapD` functorial
+  (`mapD-id`/`mapD-∘`); counit `ε : D 0 A → A` at the unit grade;
+  *nested* comultiplication `δ : D (m + n) A → D m (D n A)`; all
+  three graded-comonad laws (`gc-counit-l`, `gc-counit-r`,
+  `gc-coassoc`) discharged as propositional equalities; a separating
+  witness `D2-nontrivial` that `D r` is *not* `⊤`/a proposition; and
+  `D 0 (Echo f y)` is the bare echo (Echo is the grade-unit
+  object). The proof uses `δ`-naturality over the outermost `R`
+  layer (`δ-suc`) plus the `subst`-over-`R` interchange
+  (`subst-D-suc`) to factor the coassociativity inductive step;
+  stdlib's `+-assoc (suc m) n p` reduces definitionally to
+  `cong suc (+-assoc m n p)`, so the two ℕ-equation proofs on the
+  chain ends are syntactically identical and ℕ-UIP was *not*
+  required for `gc-coassoc` (only `gc-counit-l` uses ℕ-UIP, which
+  is itself K-free via Hedberg / decidable equality and was
+  already present in the 2026-05-18 spike). `--safe --without-K`,
+  zero postulates, no funext, no escape pragmas.
+|===
+
+*What is NOT earned back by this follow-up.* The retraction's
+target was `EchoGraded` and its surrounding scaffold — and the
+retraction stands for `EchoGraded`. The F1 contribution is a
+*separate, additional* mechanised structure: it shows that a
+genuine graded comonad over Echo *exists*, but it does not
+retroactively re-classify `EchoGraded` as a graded comonad.
+`EchoGraded` remains a thin-poset reindexing modality on a
+three-element lattice, with no nested family, no monoid
+multiplication, and `⊑-prop` baked in — as R-2026-05-18 stated.
+The paper's title, central thesis, and most of the "honest
+qualifications" therefore stand verbatim; F1 enters the codebase
+as an *additional* mechanised contribution at the side of
+`EchoGraded`, not as a reinstatement of it.
+
+*What this unblocks.* Gate *F3* (a genuinely independent second
+model of the *comonad* at a different grade monoid — e.g. a
+multiplicative or tropical semiring — without a `× ⊤` carrier or
+a `⊑-prop`-equivalent field) is now in scope; it was gated on F1.
+F3 is *not* started by this follow-up.
+
+*Artefacts edited 2026-05-20 pursuant to this follow-up:*
+`proofs/agda/EchoGradedComonadF1.agda` (closed `gc-coassoc`;
+introduced `δ-suc`); `proofs/agda/All.agda` (wired F1 in);
+`proofs/agda/Smoke.agda` (pinned the F1 headlines and the
+`D2-nontrivial` separating witness);
+`docs/echo-types/earn-back-plan.adoc` (ledger row A1 + Status). No
+edits to `paper.adoc`, `types-abstract.adoc`, or
+`conservativity.adoc` in this follow-up — the body of those
+documents is about `EchoGraded`'s thin-poset structure, which F1
+does not change. Owner-gated decision: whether to add a *bounded*
+new contribution paragraph mentioning the F1 side-construction
+(without altering the title / thesis / reindexing-modality
+framing).
+
 == Revision policy
 
 Append-only. New retractions get the next `R-YYYY-MM-DD` id. An entry

proofs/agda/All.agda

@@ -59,6 +59,7 @@ open import EchoRelModel        -- Pillar D (scaffold)
 -- follow-up F-2026-05-18a.
 open import EchoPullbackUnivF4  -- Gate F4 PASSED (funext-qualified UP)
 open import EchoStepNDModelF2   -- Gate F2 PASSED (StepND second model)
+open import EchoGradedComonadF1 -- Gate F1 PASSED (graded comonad on iterated-residue)
 
 -- Foundation P1: external-fibre triangulation. Echo agrees with the
 -- standard library's OWN independently-authored notions

proofs/agda/EchoGradedComonadF1.agda

@@ -114,6 +114,14 @@ coe-D-irr : ∀ {A} {j k : ℕ} (p q : D j A ≡ D k A) (x : D j A) →
             (e : j ≡ k) → p ≡ q → coe p x ≡ coe q x
 coe-D-irr p .p x e refl = refl
 
+-- δ-naturality over the R layer.  Peels the outermost R off both
+-- sides of δ.  Direct corollary of `coe-cong-R` at p := D-+ m n A,
+-- isolated as a lemma so the coassociativity proof can rewrite the
+-- nested `δ` without re-deriving the coe push at every step.
+δ-suc : ∀ m n {A} (x : D (m + n) A) (b : Bool) →
+        δ (suc m) n {A} (x , b) ≡ (δ m n x , b)
+δ-suc m n {A} x b = coe-cong-R (D-+ m n A) x b
+
 ----------------------------------------------------------------------
 -- LAW 1 — counit-right.  e · r = 0 + r = r definitionally, so
 -- δ 0 r = coe refl = id and ε is id: the law is definitional.
@@ -155,25 +163,39 @@ gc-counit-l (suc r) {A} (d , b) = begin
 --   D ((m+n)+p) A --subst +-assoc--> D (m+(n+p)) A --δ m (n+p)-->
 --                  D m (D (n+p) A) --mapD m (δ n p)--> D m (D n (D p A))
 
--- LAW 3 — coassociativity.  OPEN OBLIGATION (F1 not yet passed).
---
--- Spike finding (2026-05-18): the base case (`zero`) and the
--- structural skeleton close; the inductive step has an isolated
--- type-mismatch in the chain that re-expresses
---   mapD (suc m) (δ n p) (δ (suc m) (n+p) (subst (cong suc +-assoc)))
--- back through `coe-cong-R`/`sym` — `m != m + (n + p)` at the
--- penultimate rewrite.  This is a PROOF-ENGINEERING bug, NOT a
--- foundational obstruction: Agda demanded NO K, NO funext, NO
--- postulate anywhere; ℕ-UIP (K-free) is the only non-structural
--- tool, exactly as predicted.  The remaining work is to factor the
--- inductive step through an explicit `δ`-naturality lemma
---   δ (suc m) q (x , b) ≡ (δ m q x , b)   [over the R layer]
--- and a `mapD`/`subst` interchange, rather than the ad-hoc
--- `coe-cong-R ∘ sym` push used above.  Tracked as Gate F1 in
--- docs/echo-types/earn-back-plan.adoc §"Status".  NOT postulated,
--- NOT softened: stated here as the precise open obligation.
+-- LAW 3 — coassociativity.  Closed 2026-05-20.
 --
--- gc-coassoc : ∀ m n p {A} (x : D ((m + n) + p) A) →
---   δ m n (δ (m + n) p x)
---   ≡ mapD m (δ n p)
---       (δ m (n + p) (subst (λ k → D k A) (+-assoc m n p) x))
+-- The inductive step factors cleanly through `δ-suc` (δ-naturality
+-- over the outer R layer) and `subst-D-suc` (subst commutes with the
+-- outer R layer).  Stdlib's `+-assoc (suc m) n p` is *definitionally*
+-- `cong suc (+-assoc m n p)` (recursion on left arg), so the
+-- ℕ-equation proofs on the two sides are syntactically identical and
+-- ℕ-UIP is *not* needed — only ℕ-equation transport along the
+-- structural lemmas.  No K, no funext, no postulate.
+
+gc-coassoc : ∀ m n p {A} (x : D ((m + n) + p) A) →
+  δ m n (δ (m + n) p x)
+  ≡ mapD m (δ n p)
+      (δ m (n + p) (subst (λ k → D k A) (+-assoc m n p) x))
+gc-coassoc zero    n p x       = refl
+gc-coassoc (suc m) n p {A} (x , b) = begin
+  δ (suc m) n (δ (suc m + n) p (x , b))
+    ≡⟨ cong (δ (suc m) n) (δ-suc (m + n) p x b) ⟩
+  δ (suc m) n (δ (m + n) p x , b)
+    ≡⟨ δ-suc m n (δ (m + n) p x) b ⟩
+  (δ m n (δ (m + n) p x) , b)
+    ≡⟨ cong (_, b) (gc-coassoc m n p x) ⟩
+  (mapD m (δ n p) (δ m (n + p) (subst (λ k → D k A) (+-assoc m n p) x)) , b)
+    ≡⟨ sym (cong (mapD (suc m) (δ n p))
+                 (δ-suc m (n + p)
+                        (subst (λ k → D k A) (+-assoc m n p) x) b)) ⟩
+  mapD (suc m) (δ n p)
+    (δ (suc m) (n + p)
+       (subst (λ k → D k A) (+-assoc m n p) x , b))
+    ≡⟨ cong (λ z → mapD (suc m) (δ n p) (δ (suc m) (n + p) z))
+            (sym (subst-D-suc (+-assoc m n p) x b)) ⟩
+  mapD (suc m) (δ n p)
+    (δ (suc m) (n + p)
+       (subst (λ k → D k A) (+-assoc (suc m) n p) (x , b)))
+    ∎
+  where open ≡-Reasoning

proofs/agda/Smoke.agda

@@ -450,6 +450,27 @@ open import EchoStepNDModelF2 using
   ; nd-fibre-not-prop             -- the fibre is not a proposition
   )
 
+-- Pillar F, Gate F1 — the MAKE-OR-BREAK gate (docs/echo-types/
+-- earn-back-plan.adoc §F1). A genuine graded comonad on the
+-- iterated-residue carrier `D r A = r nested R-layers`, with grade
+-- monoid (ℕ, +, 0), Echo as the grade-unit object (D 0 (Echo f y) is
+-- the bare echo), NESTED comultiplication δ : D (m+n) ⇒ D m ∘ D n,
+-- all three graded-comonad laws proved, and a separating witness
+-- showing D 2 is not collapsing to ⊤. --safe --without-K, zero
+-- postulates, no funext. Scope: this earns back the graded-comonad
+-- claim FOR THIS WITNESS ONLY; `EchoGraded` itself remains a
+-- thin-poset reindexing modality per R-2026-05-18.
+open import EchoGradedComonadF1 using
+  ( D                              -- the graded functor
+  ; mapD ; mapD-id ; mapD-∘        -- functor laws
+  ; ε                              -- counit at the unit grade
+  ; δ                              -- NESTED comultiplication
+  ; D2-nontrivial                  -- D 2 is not ⊤ / a prop
+  ; gc-counit-r                    -- counit-right law (definitional)
+  ; gc-counit-l                    -- counit-left law
+  ; gc-coassoc                     -- coassociativity law (the F1 keystone)
+  )
+
 open import EchoTropical using
   ( Candidate
   ; score