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

[hyperpolymath]

Summary

Gate F1 of the earn-back plan — the MAKE-OR-BREAK retraction from
R-2026-05-18 — 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:

δ-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

• agda proofs/agda/All.agda exit 0 under --safe --without-K
• agda proofs/agda/Smoke.agda exit 0 under --safe --without-K
• grep -nE '^\s*postulate\b|BUILTIN REWRITE|NON_TERMINATING|TERMINATING' proofs/agda/EchoGradedComonadF1.agda returns no matches in code
• --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 (theory: EchoSearch — Axis 8 witness-search machine (thin slice) #80 EchoSearch, examples: Example 5 — database provenance (K-provenance semiring) #81 EchoExampleProvenance,
  examples: Example 9 — parser residue (balanced parens) #83 EchoExampleParser) added — restored their imports cleanly
  during the rebase onto fresh origin/main.

🤖 Generated with Claude Code