hyperpolymath
diff --git a/‎docs/echo-types/earn-back-plan.adoc‎
Lines changed: 50 additions & 1 deletion b/‎docs/echo-types/earn-back-plan.adoc‎
Lines changed: 50 additions & 1 deletion
diff --git a/‎docs/retractions.adoc‎
Lines changed: 80 additions & 0 deletions b/‎docs/retractions.adoc‎
Lines changed: 80 additions & 0 deletions
diff --git a/‎proofs/agda/All.agda‎
Lines changed: 3 additions & 0 deletions b/‎proofs/agda/All.agda‎
Lines changed: 3 additions & 0 deletions
diff --git a/‎proofs/agda/EchoGradedComonadInstance1.agda‎
Lines changed: 65 additions & 0 deletions b/‎proofs/agda/EchoGradedComonadInstance1.agda‎
Lines changed: 65 additions & 0 deletions
@@ -209,7 +209,16 @@ single index; it moves no claim.
 | A3
 | *F3* — independent second model of the comonad at a different grade
   monoid (no `× ⊤` carrier, no `⊑-prop`-equivalent field).
-| Unstarted. Gated on F1.
+| *PASSED 2026-05-20* — `proofs/agda/EchoGradedComonadInterface.agda`
+  + `EchoGradedComonadInstance1.agda` (F1 at the *commutative*
+  monoid `(ℕ, +, 0)`) + `EchoGradedComonadInstance2.agda`
+  (free-monoid `(List Tag, ++, [])` over a two-element `Tag` with
+  per-element residue `R smol A = A × Bool` / `R big A = A × ℕ`).
+  The two grade monoids are non-isomorphic (one commutative, one
+  not; witness `tag-list-non-commutative`); the interface record
+  carries no `⊑-prop`-equivalent field. `--safe --without-K`, zero
+  postulates, no funext. Wired into `All`/`Smoke`. Retraction
+  follow-up F-2026-05-20b.
 
 | A4
 | *F4* — strict universal property as a function of an explicit
@@ -274,6 +283,10 @@ single index; it moves no claim.
   independently of F1.
 . *F1 coassoc* (A1) — *DONE 2026-05-20*: passed via the predicted
   `δ`-naturality-over-`R` factoring; unblocks *F3* (A3).
+. *F3* (A3) — *DONE 2026-05-20*: passed via the
+  `GradedComonadStructure` interface plus two non-isomorphic-
+  grade-monoid instances. Closes the second-models claim *for the
+  graded comonad witness* — see follow-up F-2026-05-20b for scope.
 . *Doc-integrity* (D) — reconcile alongside step 1; removes a drift
   vector at near-zero cost.
 . *Buchholz* (B) — separate long-tail; keep the `ExtendedOrder`
@@ -347,3 +360,39 @@ 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.
+
+* *2026-05-20 — Gate F3 PASSED.*
+  `EchoGradedComonadInterface.GradedComonadStructure` is an abstract
+  record packaging the F1 graded-comonad signature (grade monoid +
+  graded functor + counit + nested comultiplication + monoid laws +
+  functor laws + the three comonad laws) without a `⊑-prop`-equivalent
+  field. Two non-isomorphic-grade-monoid instances inhabit it:
++
+[loweralpha]
+. `EchoGradedComonadInstance1.nat-instance` — F1 at the commutative
+  monoid `(ℕ, +, 0)`;
+. `EchoGradedComonadInstance2.list-instance` — the free monoid
+  `(List Tag, ++, [])` over a two-element `Tag` with per-element
+  residue layers `R smol A = A × Bool` and `R big A = A × ℕ`. All
+  three comonad laws proved (`gc-counit-r` definitional;
+  `gc-counit-l`/`gc-coassoc` by structural induction on the list,
+  cons step splitting on the head `Tag`, mirroring F1's
+  `δ`-naturality + `subst-D-suc` factoring).
++
+The grade monoids are non-isomorphic — one commutative, one not;
+the witness `tag-list-non-commutative` discharges this directly. The
+interface record contains no `⊑-prop`-equivalent field; both
+instances inhabit it cleanly without one. `--safe --without-K`,
+zero postulates, no funext; wired into `All.agda` and pinned in
+`Smoke.agda`. Retraction follow-up F-2026-05-20b.
++
+*Strictly scoped (re-read with care):* F3 earns back the
+"two-models" claim *for the graded-comonad witness* introduced by
+F1 — there are two genuinely non-isomorphic grade-monoid models of
+that interface. It does *not* earn back the older `EchoRelModel`
+two-models claim retracted at R-2026-05-18 finding 3, which was
+about `GCLaws` instantiated at `set-model` and `rel-model`. Those
+instantiations remain at the same grade poset with `⊑-prop` baked
+in as a field; that retraction stands. The two earn-backs (F3 here,
+and the original `GCLaws` claim) are about different abstract
+interfaces and are not interconvertible.
@@ -260,6 +260,86 @@ new contribution paragraph mentioning the F1 side-construction
 (without altering the title / thesis / reindexing-modality
 framing).
 
+==== Follow-up F-2026-05-20b (2026-05-20) — Gate F3 passed
+
+Gate F3 — a *genuinely independent* second model of the graded
+comonad at a *different grade monoid* (not the same monoid with a
+`× ⊤` carrier, no field equivalent to `⊑-prop`) — also passes,
+following F1. The combined F1 + F3 result earns back the
+"two-models" claim *for the graded-comonad witness specifically*;
+the older retracted "two-models" claim about `EchoRelModel`/`GCLaws`
+remains retracted (see scope qualifier at end).
+
+[cols="1,4", options="header"]
+|===
+| Gate | Earned-back claim (exact strength — nothing beyond)
+
+| *F3*
+| `proofs/agda/EchoGradedComonadInterface.GradedComonadStructure`
+  packages the F1 graded-comonad signature into an abstract record:
+  a grade monoid `(G, 1G, _·G_)` with the three monoid laws; a
+  graded carrier `D : G → Set → Set` with functorial action and the
+  two functor laws; counit `ε` at the unit grade; *nested*
+  comultiplication `δ : D (g ·G h) A → D g (D h A)`; and the three
+  graded-comonad laws stated against `subst` along the monoid's
+  propositional identities. The record contains **no
+  `⊑-prop`-equivalent field** — only structure, monoid laws, and
+  comonad laws. Two non-isomorphic-grade-monoid instances inhabit
+  it: `nat-instance` at the commutative monoid `(ℕ, +, 0)` (F1)
+  and `list-instance` at the non-commutative free monoid
+  `(List Tag, ++, [])` over a two-element `Tag` with per-element
+  residue layers `R smol A = A × Bool`, `R big A = A × ℕ`. The
+  non-isomorphism is constructively witnessed
+  (`tag-list-non-commutative`: one monoid is commutative, the other
+  isn't). All three comonad laws hold at both instances —
+  definitional `gc-counit-r`, structural-induction `gc-counit-l` and
+  `gc-coassoc` with the same `δ`-naturality + `subst`-over-residue
+  factoring used for F1. `--safe --without-K`, zero postulates, no
+  funext, no escape pragmas; wired into `All.agda`, pinned in
+  `Smoke.agda`.
+|===
+
+*Strictly scoped (re-read with care).* F3 earns back the
+two-models claim **for the graded-comonad witness introduced by F1**.
+There are two genuinely non-isomorphic grade-monoid models of the
+`GradedComonadStructure` interface, the laws hold at each, the
+interface itself is `⊑-prop`-free. That is exactly what the gate
+asked for, and the gate passes at exactly that strength.
+
+What is **NOT** earned back by F3. The retraction's finding 3 ("Not
+two models") was about `EchoRelModel`'s `GCLaws`, instantiated at
+`set-model` and `rel-model` — both fixing the *same* grade poset
+(`_≤g_`, `≤g-prop`, `_⊔g_`, `keep`), with `rel-model`'s carrier
+being the Set carrier `× ⊤` and `model-agreement` being `refl`. The
+`GradedLossModel` interface bakes `⊑-prop` in as a field. That
+situation is unchanged: `EchoRelModel` still has its retracted
+"two-models" claim retracted; the `⊑-prop` field is still there;
+`rel-model` is still `set-model × ⊤`. F3 here is about a
+*different* abstract interface (`GradedComonadStructure`, no order,
+no `⊑-prop`) and a *different* pair of models. The two earn-backs
+are not interconvertible; do not cite one as evidence for the other.
+
+*What this unblocks.* No further earn-back gates depend on F3. The
+sequence F1 → F3 closes the comonad-side earn-back programme as
+specified. The remaining open earn-back debt (`paper.adoc` /
+`types-abstract.adoc` / `conservativity.adoc` prose updates, which
+F1's follow-up F-2026-05-20a deferred as owner-gated) is now an
+even stronger candidate for a bounded "new contribution" paragraph
+— but the bodies of those documents are still about `EchoGraded`'s
+thin-poset structure, which F3 does not change. The owner-gated
+decision stands.
+
+*Artefacts edited 2026-05-20 pursuant to this follow-up:*
+`proofs/agda/EchoGradedComonadInterface.agda` (new — abstract
+record); `proofs/agda/EchoGradedComonadInstance1.agda` (new — F1
+packaged); `proofs/agda/EchoGradedComonadInstance2.agda` (new —
+free-monoid instance); `proofs/agda/All.agda` (wired both new
+modules); `proofs/agda/Smoke.agda` (pinned the record, both
+instances, `tag-list-non-commutative`, `D-nontrivial`);
+`docs/echo-types/earn-back-plan.adoc` (ledger row A3, Sequencing,
+Status). No edits to `paper.adoc`, `types-abstract.adoc`, or
+`conservativity.adoc` — owner-gated, as for F1's follow-up.
+
 == Revision policy
 
 Append-only. New retractions get the next `R-YYYY-MM-DD` id. An entry
 
@@ -62,6 +62,9 @@ open import EchoRelModel        -- Pillar D (scaffold)
 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)
+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, ++, [])
 
 -- Foundation P1: external-fibre triangulation. Echo agrees with the
 -- standard library's OWN independently-authored notions
 
@@ -0,0 +1,65 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Gate F3 phase 1 — instance 1 of N.
+--
+-- Packages the F1 iterated-residue construction
+-- (`EchoGradedComonadF1.agda`) as an inhabitant of the
+-- `EchoGradedComonadInterface.GradedComonadStructure` record at the
+-- grade monoid `(ℕ, +, 0)`. The structure and laws are reused
+-- verbatim — F1 already discharged them — so this module is purely
+-- structural: it shows the abstract interface is *inhabitable* by
+-- the existing F1 witness, with no shape mismatch and no extra
+-- assumptions imported.
+--
+-- F1's gc-counit-l/r/coassoc are stated against ℕ's specific
+-- equation proofs (`+-identityˡ`, `+-identityʳ`, `+-assoc`), so the
+-- interface's monoid-equation `subst` reduces exactly to F1's
+-- existing equations. The `gc-counit-r` field reduces by `refl`
+-- because stdlib's `+-identityˡ` is itself `refl` for every
+-- argument (`+` recurses on the left; `0 + n` is `n` definitionally).
+--
+-- F3 only PASSES when at least two non-isomorphic-grade-monoid
+-- instances of the interface are mechanised. This module is one of
+-- them; instance 2 (e.g. `(List X, ++, [])` for a non-trivial `X`)
+-- is the phase-2 follow-up.
+
+module EchoGradedComonadInstance1 where
+
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Nat.Properties using (+-identityˡ; +-identityʳ; +-assoc)
+
+open import EchoGradedComonadInterface using (GradedComonadStructure)
+open import EchoGradedComonadF1 using
+  ( D
+  ; mapD ; mapD-id ; mapD-∘
+  ; ε
+  ; δ
+  ; gc-counit-l
+  ; gc-counit-r
+  ; gc-coassoc
+  )
+
+----------------------------------------------------------------------
+-- The ℕ-graded instance.
+
+nat-instance : GradedComonadStructure
+nat-instance = record
+  { G            = ℕ
+  ; 1G           = 0
+  ; _·G_         = _+_
+  ; ·G-identityˡ = +-identityˡ
+  ; ·G-identityʳ = +-identityʳ
+  ; ·G-assoc     = +-assoc
+
+  ; D            = D
+  ; mapD         = mapD
+  ; mapD-id      = mapD-id
+  ; mapD-∘       = mapD-∘
+
+  ; ε            = ε
+  ; δ            = δ
+
+  ; gc-counit-r  = gc-counit-r
+  ; gc-counit-l  = gc-counit-l
+  ; gc-coassoc   = gc-coassoc
+  }