Earn-back: Gates F4 + F2 PASSED (retraction follow-up F-2026-05-18a)

docs/echo-types/conservativity.adoc

@@ -142,6 +142,14 @@ proof*. Any reintroduction of a postulate or weakening of
   dependency. The real funext-relativity is the *pointwise-only*
   mediator property of the pullback presentation (`paper.adoc` §3),
   now disclosed as the boundary rather than presented as a feature.
+* Earn-back, scoped (follow-up F-2026-05-18a, 2026-05-18): the
+  pullback's strict terminality is now mechanised *conditional on an
+  explicit `funext` parameter* (`EchoPullbackUnivF4.agda`; not a
+  postulate — the trusted base is unchanged), and a genuine second
+  model of the *bare Echo functor* (not the modality) exists on the
+  non-graph relation `StepND` (`EchoStepNDModelF2.agda`). These do
+  *not* widen the conservativity claim above: it remains *evidence
+  for*, not a proof, and the modality-level retractions stand.
 
 == Revision policy
 
@@ -169,3 +177,12 @@ recorded reason. Append-only revision history.
   and `paper.adoc` §"Reframing note". No Agda module changed; the
   artefacts are exactly as strong as before — only the prose claims
   are corrected downward.
+* *2026-05-18 — Gates F4/F2 earned back (scoped).* Added the
+  scope/non-claims bullet recording that strict terminality is now
+  mechanised conditional on an explicit `funext` parameter
+  (`EchoPullbackUnivF4.agda`, no postulate) and that a genuine second
+  model of the *bare Echo functor* exists on the non-graph relation
+  `StepND` (`EchoStepNDModelF2.agda`). The conservativity statement
+  <<thm-conservativity>> is unchanged: still *evidence for*, not a
+  proof; modality-level retractions stand. Recorded reason:
+  `docs/retractions.adoc` follow-up F-2026-05-18a.

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

@@ -196,7 +196,9 @@ single index; it moves no claim.
 | A2
 | *F2* — real second model of the bare Echo functor via
   `EchoRelational.StepND`, non-`refl` agreement lemma.
-| Unstarted. Independent of F1. Rated tractable.
+| *PASSED 2026-05-18* — `proofs/agda/EchoStepNDModelF2.agda`,
+  `--safe --without-K`, zero postulates, wired into `All`/`Smoke`.
+  Retraction follow-up F-2026-05-18a.
 
 | A3
 | *F3* — independent second model of the comonad at a different grade
@@ -206,7 +208,9 @@ single index; it moves no claim.
 | A4
 | *F4* — strict universal property as a function of an explicit
   `funext` *module parameter* (never a postulate).
-| Unstarted. Independent of F1. Expected tractable.
+| *PASSED 2026-05-18* — `proofs/agda/EchoPullbackUnivF4.agda`,
+  `--safe --without-K`, zero postulates, pointwise corollary kept,
+  wired into `All`/`Smoke`. Retraction follow-up F-2026-05-18a.
 
 | B
 | Buchholz order: `Ordinal/Buchholz/Order.agda` `_<ᵇ_` compares ψ by
@@ -254,10 +258,12 @@ single index; it moves no claim.
 
 === Recommended order of attack
 
-. *F4 + F2 in parallel* (A4, A2) — tractable, independent of F1, each
-  earns back a qualified/real claim regardless of F1. Highest ROI.
+. *F4 + F2 in parallel* (A4, A2) — *DONE 2026-05-18*: both passed,
+  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).
+  make-or-break and unlocks *F3* (A3). Now the next action.
 . *Doc-integrity* (D) — reconcile alongside step 1; removes a drift
   vector at near-zero cost.
 . *Buchholz* (B) — separate long-tail; keep the `ExtendedOrder`
@@ -294,3 +300,15 @@ single index; it moves no claim.
   obligation — *not postulated, not softened*. No reframed claim has
   moved (F1 requires all three laws); the gate stays open until
   `gc-coassoc` closes `--safe --without-K` zero-postulate.
+* *2026-05-18 — Gates F4 and F2 PASSED.*
+  `EchoPullbackUnivF4.agda` (F4: terminal-cone UP as a function of an
+  explicit `funext` parameter, never a postulate; pointwise corollary
+  kept) and `EchoStepNDModelF2.agda` (F2: genuine second model of the
+  bare Echo functor on the non-graph relation `StepND`, content-bearing
+  agreement). Both `--safe --without-K`, zero postulates; wired into
+  `All.agda` and pinned in `Smoke.agda`; full + smoke build green.
+  Scoped claims moved in `paper.adoc` / `conservativity.adoc` /
+  `types-abstract.adoc`; logged as retraction follow-up F-2026-05-18a.
+  *Strictly scoped:* F2 is the Echo functor only — the graded-comonad,
+  model-independence, and conservativity claims remain retracted; F1
+  (coassoc) and F3 remain open.

docs/echo-types/paper.adoc

@@ -152,6 +152,22 @@ category theorist accepts echo as the limit of a cospan" were
 retracted on 2026-05-18 (see <<reframing-note>>).
 ====
 
+[NOTE]
+====
+*Earned back, conditionally (Gate F4, 2026-05-18).*
+`proofs/agda/EchoPullbackUnivF4.agda` discharges strict terminality
+`m' ≡ m` as a *function of an explicit `funext` hypothesis* — a
+module parameter `FunExt₀`, **not a postulate**, in the same idiom by
+which `Echo.agda` parameterises `cancel-iso` by the triangle
+identities. The honest reading is therefore not "retracted →
+unconditional" but "retracted → *true, conditional on funext*": a
+category theorist who accepts funext gets the genuine universal
+property; the trusted base is unchanged (no funext is introduced),
+and the funext-free pointwise mediator above is retained verbatim as
+the corollary. The *unconditional* claim stays retracted. Logged as
+retraction follow-up F-2026-05-18a.
+====
+
 == The loss-graded reindexing modality
 
 === Structure
@@ -249,6 +265,25 @@ the "graph = fibration bridge" `bridge-natural` is the identity on
 Σ-pairs (`refl`). We no longer claim a relational model of the
 modality.
 
+[NOTE]
+====
+*Earned back, scoped (Gate F2, 2026-05-18).*
+`proofs/agda/EchoStepNDModelF2.agda` gives a genuine second model of
+the *bare Echo functor* (explicitly **not** of the graded modality —
+that retraction stands). It instantiates the same interface the
+deterministic model uses (`EchoFunctorModel`; functor laws by the
+generic `map-rel-id`/`map-rel-comp`) at `EchoRelational.StepND`, a
+relation that is **not the graph of any function under any state
+relabelling** — `nd-not-graph`, a checked `true ≢ false`. The
+agreement carries content: the `StepND` fibre is the disjoint sum of
+its deterministic branches by constructor case analysis
+(`nd-sum-fromto`, `nd-fibre-not-prop`), *not* `refl` and *not* Σ-η on
+`× ⊤` — exactly the defect §6 records for `EchoRelModel`. This earns
+back the R2 "fixable with bounded work" item at functor level only;
+model-independence of the *modality* remains retracted. Logged as
+retraction follow-up F-2026-05-18a.
+====
+
 === The conservativity claim, narrowed
 
 Because `Echo = Σ` definitionally and the whole development is
@@ -346,6 +381,17 @@ following claims were retracted, not weakened cosmetically:
 The full per-attack analysis and the codebase pressure-test are in
 `docs/retractions.adoc`.
 
+*Partial earn-back (follow-up F-2026-05-18a, 2026-05-18).* Two rows
+above are now partially recovered, each strictly to its mechanised
+strength under the Pillar F gate discipline
+(`docs/echo-types/earn-back-plan.adoc`): the universal-property row is
+earned back *conditional on an explicit `funext` parameter* (never a
+postulate; §3 NOTE, `EchoPullbackUnivF4.agda`), and the
+model-independence row is earned back *for the bare Echo functor only*
+via a genuine non-graph `StepND` model (§6 NOTE,
+`EchoStepNDModelF2.agda`). The graded-comonad, modality-level
+model-independence, and conservativity rows remain fully retracted.
+
 == Conclusion
 
 Echo is the homotopy fibre equipped with a loss-grade lattice,

docs/echo-types/types-abstract.adoc

@@ -69,6 +69,10 @@ which this abstract's own correction is an instance.
   `∀ v → m' v ≡ m v`. This is *not* a universal property: full
   terminality (`m' ≡ m`) is neither stated nor provable here without
   funext. The honest claim is a funext-relative mediator property.
+  *Earned back conditionally (F4, F-2026-05-18a):* strict terminality
+  is mechanised as a function of an explicit `funext` parameter
+  (`EchoPullbackUnivF4.agda`, not a postulate); the unconditional
+  claim stays retracted, the pointwise corollary is kept.
 . *Loss-graded reindexing modality (Pillar B-2).* Over the loss-grade
   join-semilattice `(Grade, ⊔, keep)`: `gextract` is the identity
   coercion (`keep` is the definitional bottom), `gduplicate` is the
@@ -100,6 +104,11 @@ definitionally.
   `--safe --without-K` build is *evidence for* conservativity over
   MLTT+Σ; it is not a mechanised conservativity metatheorem and is no
   longer claimed as one.
+  *Earned back, scoped (F2, F-2026-05-18a):* a genuine second model of
+  the *bare Echo functor* (not the modality) exists on the non-graph
+  relation `StepND` (`EchoStepNDModelF2.agda`; `nd-not-graph` checked),
+  with content-bearing agreement — not Σ-η on `× ⊤`. Modality-level
+  model-independence and the conservativity narrowing are unchanged.
 
 == The artefact and its discipline
 

docs/retractions.adoc

@@ -139,6 +139,59 @@ integration narrowness; R-2026-05-18 concerns the graded-comonad /
 model-independence / conservativity framing. Both are calibration
 retractions, not invalidations of the mechanised artefacts.
 
+==== Follow-up F-2026-05-18a (2026-05-18) — Gates F4 and F2 passed
+
+Two of the R-2026-05-18 retractions are partially *earned back*, each
+strictly to its mechanised strength, under the Pillar F gate
+discipline (`docs/echo-types/earn-back-plan.adoc`). Both spikes
+typecheck `--safe --without-K` with *zero postulates*, are now wired
+into `proofs/agda/All.agda`, and pinned in `proofs/agda/Smoke.agda`.
+The full suite and smoke build green with them included.
+
+[cols="1,4", options="header"]
+|===
+| Gate | Earned-back claim (exact strength — nothing beyond)
+
+| *F4*
+| `proofs/agda/EchoPullbackUnivF4.agda`. The terminal-cone universal
+  property `m' ≡ m` holds *as a function of an explicit `funext`
+  hypothesis* — a module parameter `FunExt₀`, **never a postulate**,
+  the same idiom by which `Echo.agda` parameterises `cancel-iso` by
+  the triangle identities. The retraction stands for the
+  *unconditional* claim; what is earned is the *conditional* one
+  ("retracted → true, conditional"). The funext-free pointwise
+  mediator property is retained verbatim as the corollary
+  (`echo-pullback-univ-pointwise`). No funext is introduced into the
+  trusted base.
+
+| *F2*
+| `proofs/agda/EchoStepNDModelF2.agda`. A genuine second model of the
+  *bare Echo functor* on `EchoRelational.StepND` — a relation that is
+  provably **not the graph of any function under any state
+  relabelling** (`nd-not-graph`, a checked `true ≢ false`). It
+  inhabits the *same* interface the deterministic model does
+  (`EchoFunctorModel`; functor laws by the generic
+  `map-rel-id`/`map-rel-comp`), and the agreement has content — the
+  `StepND` fibre is the disjoint sum of its deterministic branches by
+  constructor case analysis (`nd-sum-fromto`/`nd-fibre-not-prop`),
+  *not* `refl` and *not* Σ-η on `× ⊤`. This addresses precisely the
+  R2 item rated "fixable with bounded work".
+|===
+
+*What is NOT earned back by this follow-up.* The graded-comonad claim
+(no nested `D_r D_s`), model-independence of the *graded* structure,
+and the conservativity metatheorem remain fully retracted. F2 concerns
+the Echo functor only, not the comonad; it does not reinstate
+`EchoRelModel`'s retracted "second model"/"model-independence". Gates
+F1 (coassociativity open) and F3 (gated on F1) remain open.
+
+*Artefacts edited 2026-05-18 pursuant to this follow-up:*
+`docs/echo-types/paper.adoc` (pullback §, second-model §, reframing
+note), `docs/echo-types/conservativity.adoc` (scope), and
+`docs/echo-types/types-abstract.adoc` (contributions) — each updated
+to the *conditional/scoped* earned claim, never beyond it;
+`docs/echo-types/earn-back-plan.adoc` ledger rows A2/A4 and Status.
+
 == Revision policy
 
 Append-only. New retractions get the next `R-YYYY-MM-DD` id. An entry

proofs/agda/All.agda

@@ -40,6 +40,12 @@ open import EchoGradedComonad   -- Pillar B (scaffold)
 open import EchoSeparating      -- Pillar C (scaffold)
 open import EchoRelModel        -- Pillar D (scaffold)
 
+-- Pillar F earn-back (docs/echo-types/earn-back-plan.adoc). Wired in
+-- on the gate passing (Sequencing pt 4); see docs/retractions.adoc
+-- 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 Ordinal.Base
 open import Ordinal.Closure
 open import Ordinal.CNF

proofs/agda/EchoPullbackUnivF4.agda

@@ -0,0 +1,83 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Gate F4 feasibility spike (docs/echo-types/earn-back-plan.adoc §"Gate
+-- F4 — Universal property, honestly qualified").
+--
+-- The R-2026-05-18 retraction narrowed `EchoPullback.echo-pullback-univ`
+-- to a *pointwise* mediator property (`∀ v → m' v ≡ m v`); the
+-- terminal-cone universal property `m' ≡ m` was unstatable there
+-- without funext, and a funext postulate is forbidden estate-wide.
+--
+-- F4's earn-back is NOT "retracted → unconditional"; it is
+-- "retracted → *true, conditional*": parameterise the strict
+-- terminality result by an EXPLICIT funext hypothesis (a module
+-- parameter — never a postulate), exactly as `Echo.agda` parameterises
+-- `cancel-iso-from-to` / `cancel-iso-to-from` by the triangle-identity
+-- coherences. Then `echo-pullback-univ-strict` is a genuine universal
+-- property *given funext*, with zero postulates retained, and the
+-- unconditional pointwise result stays as the funext-free corollary.
+--
+-- Result of the spike: it closes in three lines on top of the
+-- already-landed pointwise lemma. No K, no funext in the trusted
+-- base (funext is a hypothesis the caller must supply, exactly like
+-- `triangle₁`/`triangle₂` in `Echo.agda`), zero postulates. Not wired
+-- into `All.agda` / `Smoke.agda` until Gate F4 is recorded passed.
+
+module EchoPullbackUnivF4 where
+
+open import Echo using (Echo)
+open import EchoPullback using (EchoCone; IsMediator; echo-pullback-univ)
+open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+----------------------------------------------------------------------
+-- The funext hypothesis, as an explicit (level-0) coherence — NOT a
+-- postulate. `Set₁` because it quantifies over `Set`; this is exactly
+-- the universe `EchoPullback` lives at (`{A B : Set}`, `V : Set`,
+-- `Echo f y : Set`), so no `Setω` and no extra level machinery.
+
+FunExt₀ : Set₁
+FunExt₀ =
+  {A : Set} {B : A → Set} {f g : (x : A) → B x} →
+  (∀ x → f x ≡ g x) → f ≡ g
+
+----------------------------------------------------------------------
+-- Strict terminality, parameterised by funext.
+--
+-- `echo-cone` is the terminal cone *strictly*: every cone morphism is
+-- equal — as a function — to the mediator, not merely pointwise. The
+-- proof is one application of the supplied `funext` to the pointwise
+-- uniqueness already proved (funext-free, K-free) in
+-- `EchoPullback.echo-pullback-univ`.
+
+module _ (funext : FunExt₀) where
+
+  echo-pullback-univ-strict :
+    {A B : Set} (f : A → B) (y : B) {V : Set} (c : EchoCone f y V) →
+    Σ (V → Echo f y) (λ m →
+      IsMediator f y c m
+      × (∀ (m' : V → Echo f y) → IsMediator f y c m' → m' ≡ m))
+  echo-pullback-univ-strict f y c with echo-pullback-univ f y c
+  ... | m , med , uniq-pt =
+        m , med , λ m' med' → funext (uniq-pt m' med')
+
+----------------------------------------------------------------------
+-- The funext-free corollary is kept verbatim: it is exactly
+-- `EchoPullback.echo-pullback-univ`, re-exported here so the
+-- conditional/unconditional pair lives in one place. Reading:
+--
+--   * unconditional, zero hypotheses : pointwise mediator property
+--       (`echo-pullback-univ`        — `∀ v → m' v ≡ m v`);
+--   * conditional on `funext`        : strict terminal cone
+--       (`echo-pullback-univ-strict` — `m' ≡ m`).
+--
+-- No claim is upgraded beyond what its hypothesis license: the strict
+-- form is *true given funext*, stated as such.
+
+echo-pullback-univ-pointwise :
+  {A B : Set} (f : A → B) (y : B) {V : Set} (c : EchoCone f y V) →
+  Σ (V → Echo f y) (λ m →
+    IsMediator f y c m
+    × (∀ (m' : V → Echo f y) → IsMediator f y c m' →
+         ∀ v → m' v ≡ m v))
+echo-pullback-univ-pointwise = echo-pullback-univ