theory: EchoApprox composition rung — first slice (retract direction) (#70)

## Summary

Extends `proofs/agda/EchoApprox.agda` with the first slice of the
axis-2 composition rung from the design note (drafted in
`/tmp/echo-types-exploration/axis2-approximate.md`, §7 obligations
2 + 6, plus the canonical-split retract direction). Refs
`docs/echo-types/roadmap.md` Axis 2 entry and
`docs/echo-types/composition.md`
§Q3 — does **not** close either.

## Obligations landed

- **`echo-strict→approx`** (§7 #2). General strict ⇒ zero-tolerance
  approximate. Generalises `echo-approx-intro` from own-fibre points
  to arbitrary `y` via the codomain equation `p : f x ≡ y`. One
  extra `subst` along `p`.

- **`echo-approx-comp-sound`** (§7 #6). Sound RHS-to-LHS direction
  of the retract shape from `composition.md` §Q3 / design-note §5.
  Unpacks the existential and calls `echo-approx-compose`.

- **`echo-approx-comp-retract-to`**. Canonical-split LHS → RHS-Σ
  section of the retract: picks `b := f x`, `ε₁ := zero`, `ε₂ := ε`.
  Uses `echo-approx-intro` for the inner echo, original bound for
  the outer.

- **`echo-approx-comp-retract-A`**. A-component round-trip
  `proj₁ ∘ sound ∘ retract-to ≡ proj₁`, proved by `refl`. The
  retraction direction holds definitionally on the A-component as
  the design note (§5) predicts.

## Obligations deferred (out of this rung)

- §7 #7 separated zero-collapse — needs a separation predicate on
  the `PseudoMetric` record.
- §7 #8 axis-1 shadow agreement — cross-axis classification.
- Full retract B-component and tolerance-budget round-trip — needs a
  `+`-left-identity axiom on `Tolerance` (`zero + ε ≡ ε`) not in the
  current record. Adding it commits the carrier to a left-unital
  monoid; deferred as a separate decision.
- Lipschitz generalisation (`L_g ≠ 1`) — needs scalar multiplication
  on `Tol`.

## Docs updated

- `docs/echo-types/composition.md` §Q3 promoted from "entirely
  speculative" to landed-retract-shape with deferred items called out.
- `docs/echo-types/roadmap.md` adds a "landed" entry for the
  composition rung first slice.

## Invariants preserved

- `--safe --without-K`
- No postulates
- No escape pragmas
- Funext untouched

## Test plan

- [x] `LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda` exits 0
- [x] `LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda` exits
0
- [x] No new `postulate`, no escape pragmas, funext not imported
- [x] `Smoke.agda` already pins `module Approx` following project
      convention (per-lemma pins inside parameterised modules require
      instantiation, which the project does not do for `EchoApprox`).

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

Author: hyperpolymath

docs/echo-types/composition.md

@@ -150,8 +150,27 @@ is a Lipschitz constant of `g`. This is a crude first guess — the
 right form may involve sup-norms, dilation-operators, or
 coarser bounds.
 
-*Status.* Entirely speculative. Requires a formal definition of
-approximate echo first.
+*Status (updated).* No longer entirely speculative. The
+non-expansive case (`L_g = 1`) is landed as
+`EchoApprox.Approx.echo-approx-compose` in additive form
+`(ε₁ + ε₂)-echo(g ∘ f)`. The compositional *shape* — whether the
+forward/backward maps form a strict iso analogous to
+`Echo-comp-iso` — is settled in the negative: it is a *retract*,
+not an iso, because the RHS Σ admits multiple splits of the budget
+and the chosen intermediate `b` is not pinned by the input. The
+axis-2 design note (`/tmp/echo-types-exploration/axis2-approximate.md`
+§5) gives the full discussion.
+
+First slice of the retract landed in `EchoApprox.agda`:
+`echo-approx-comp-sound` (RHS-Σ → LHS via `echo-approx-compose`),
+`echo-approx-comp-retract-to` (canonical-split LHS → RHS-Σ section
+at `b := f x`, `ε₁ := zero`, `ε₂ := ε`), and
+`echo-approx-comp-retract-A` (A-component round-trip preserves the
+witness up to `refl`). The B-component round-trip and the
+tolerance-budget round-trip need a `+`-left-identity axiom on
+`Tolerance` (`zero + ε ≡ ε`) — not in the current record. The full
+retract proof and the Lipschitz generalisation (`L_g ≠ 1`) are
+deferred to subsequent rungs.
 
 ### Q4. Associativity — landed
 

docs/echo-types/roadmap.md

@@ -92,6 +92,22 @@ Paths marked **[unblocked]** can proceed today. Paths marked
   (monotone in ε), and `echo-approx-compose` (additive composition
   under a non-expansive outer leg, realising the taxonomy §2
   conjecture). Wired into `All.agda` and `Smoke.agda`.
+- **[landed]** Composition rung first slice (Axis 2): the §Q3
+  retract-shape. `EchoApprox.agda` now also ships
+  `echo-strict→approx` (general strict ⇒ zero-tolerance, generalises
+  `echo-approx-intro` from own-fibre to arbitrary `y` via the
+  codomain equation), `echo-approx-comp-sound` (RHS-Σ → LHS via
+  `echo-approx-compose`), `echo-approx-comp-retract-to`
+  (canonical-split LHS → RHS-Σ section, picking `b := f x`,
+  `ε₁ := zero`, `ε₂ := ε`), and `echo-approx-comp-retract-A` (the
+  A-component round-trip `proj₁ ∘ sound ∘ retract-to ≡ proj₁`,
+  proved by `refl`). The retraction direction on the A-witness holds
+  definitionally as the design note (§5) predicts. The B-component
+  and tolerance-budget round-trips are deferred to a subsequent
+  rung — they need a `+`-left-identity axiom on `Tolerance`
+  (`zero + ε ≡ ε`) which the current record does not supply.
+  §7 obligations 7 (separated zero-collapse) and 8 (axis-1 shadow
+  agreement) likewise deferred.
 - **[landed]** Per-decoration composition lemmas across the
   five-decoration family — **sweep complete** (2026-04-28):
   `EchoGraded.degrade-compose`, `EchoLinear.degradeMode-compose`,

proofs/agda/EchoApprox.agda

@@ -12,23 +12,48 @@
 --
 -- Headline lemmas:
 --
---   * echo-approx-intro    -- exact match is a zero-tolerance approximate echo
---   * echo-approx-relax    -- ε is monotone: ε₁ ≤ ε₂ ⇒ EchoR ε₁ ⊑ EchoR ε₂
---   * echo-approx-compose  -- non-expansive composition with additive error,
---                             realising the taxonomy §2 conjecture
+--   * echo-approx-intro          -- exact own-fibre match is zero-tolerance
+--   * echo-strict→approx         -- general strict ⇒ zero-tolerance (any y)
+--   * echo-approx-relax          -- ε is monotone: ε₁ ≤ ε₂ ⇒ EchoR ε₁ ⊑ EchoR ε₂
+--   * echo-approx-compose        -- non-expansive composition with additive
+--                                   error, realising the taxonomy §2 conjecture
+--   * echo-approx-comp-sound     -- repackages compose into the retract RHS-Σ
+--                                   shape from `composition.md` §Q3 (§5 of the
+--                                   axis-2 design note)
+--   * echo-approx-comp-retract-to  -- canonical-split LHS → RHS section:
+--                                     picks b := f x, ε₁ := zero, ε₂ := ε
+--   * echo-approx-comp-retract-A   -- A-component round-trip (sound ∘ retract-to)
+--                                     preserves the A-witness up to `refl`,
+--                                     witnessing the retraction direction
+--                                     definitionally
 --
 -- The non-expansiveness side condition on the outer leg is the
 -- minimal hypothesis under which tolerances accumulate additively;
 -- without it the conjecture has no general proof (an amplifying
 -- second leg can blow ε₁ up arbitrarily on the way through).
+--
+-- Composition-track context (§5 of the axis-2 design note,
+-- `/tmp/echo-types-exploration/axis2-approximate.md`). The approximate
+-- analogue of `Echo-comp-iso` is a *retraction*, not a strict
+-- isomorphism: the RHS Σ-shape admits multiple splits of the ε
+-- budget and the chosen intermediate `b` is not pinned by the input.
+-- This module ships the first slice of that retract — soundness (#6),
+-- the canonical-split forward section, and an A-component round-trip
+-- witness. The B-component round-trip and the full tolerance round-trip
+-- need a `+`-left-identity axiom on `Tolerance` (`zero + ε ≡ ε`, not
+-- currently in the record); §7 obligations 7 (zero-collapse under
+-- separation) and 8 (axis-1 shadow agreement) are deferred to
+-- subsequent rungs.
 
 module EchoApprox where
 
 open import Level                                 using (Level; _⊔_; suc)
 open import Function.Base                         using (_∘_; id)
-open import Data.Product.Base                     using (Σ; _,_; proj₁; proj₂)
+open import Data.Product.Base                     using (Σ; _,_; _×_; proj₁; proj₂)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst)
 
+open import Echo                                  using (Echo)
+
 ----------------------------------------------------------------------
 -- Tolerance carrier and pseudo-metric structure
 ----------------------------------------------------------------------
@@ -89,6 +114,28 @@ module Approx
   echo-approx-intro f x =
     x , subst (_≤ zero) (sym (dist-self (f x))) ≤-refl
 
+  ----------------------------------------------------------------------
+  -- Headline 1ʹ: general strict ⇒ zero-tolerance approximate.
+  --
+  -- Realises §7 obligation 2 of the axis-2 design note: every strict
+  -- echo `Echo f y` lifts to a zero-tolerance approximate echo
+  -- `EchoR zero f y` (any y, not just own-fibre points). When `y ≡ f x`
+  -- with `p ≡ refl` this collapses to `echo-approx-intro`; otherwise
+  -- the codomain equation `p : f x ≡ y` is used to transport the
+  -- self-distance bound from `(f x, f x)` to `(f x, y)`.
+  --
+  -- This generalises `echo-approx-intro` from own-fibre points
+  -- `(f x)` to arbitrary `y` reached via a strict echo. The cost of
+  -- the generalisation is one extra `subst` along `p`.
+  ----------------------------------------------------------------------
+
+  echo-strict→approx :
+    ∀ {f : A → B} {y : B} → Echo f y → EchoR zero f y
+  echo-strict→approx {f = f} (x , p) =
+    x , subst (λ z → dist (f x) z ≤ zero)
+              p
+              (subst (_≤ zero) (sym (dist-self (f x))) ≤-refl)
+
   ----------------------------------------------------------------------
   -- Headline 2: tolerance is monotone in `ε`. A tighter approximation
   -- is also a looser one. The proof is one transitivity step.
@@ -139,3 +186,78 @@ module Approx
 
     bound : dist (g (f x)) y ≤ (ε₁ + ε₂)
     bound = ≤-trans leg contract
+
+  ----------------------------------------------------------------------
+  -- Retraction-shaped composition (composition.md §Q3 / design-note §5).
+  --
+  -- The approximate analogue of `Echo-comp-iso` is *retract-shaped*:
+  --
+  --   LHS  := EchoR ε (g ∘ f) y
+  --   RHS  := Σ B (λ b → EchoR ε₁ f b × dist (g b) y ≤ ε₂)
+  --
+  -- with the budget split `ε = ε₁ + ε₂`. The RHS admits multiple
+  -- splits of the budget and the chosen intermediate `b` is not
+  -- pinned by the input, so a full iso fails by design. What does
+  -- hold is a retraction: a forward section that picks a canonical
+  -- representative on the RHS and a backward map (`echo-approx-comp-sound`,
+  -- a thin repackaging of `echo-approx-compose`) that round-trips
+  -- the A-witness definitionally.
+  --
+  -- This block lands the first slice: soundness (#6), the canonical-
+  -- split forward section, and the A-component round-trip. The
+  -- B-component and tolerance-budget round-trips need a `+`-left-
+  -- identity axiom on `Tolerance` (`zero + ε ≡ ε`, not in the record).
+  ----------------------------------------------------------------------
+
+  -- §7 obligation 6: sound RHS-to-LHS direction.
+  -- Unpacks the existential and calls `echo-approx-compose`.
+  echo-approx-comp-sound :
+    ∀ {ε₁ ε₂ : Tol}
+    (f : A → B) (g : B → B) →
+    NonExpansive g →
+    ∀ {y : B} →
+    Σ B (λ b → EchoR ε₁ f b × dist (g b) y ≤ ε₂) →
+    EchoR (ε₁ + ε₂) (g ∘ f) y
+  echo-approx-comp-sound f g g-nonexp (b , ef , dgby≤ε₂) =
+    echo-approx-compose f g g-nonexp {b = b} ef dgby≤ε₂
+
+  -- Canonical-split LHS-to-RHS section of the retract.
+  --
+  -- Given an `EchoR ε (g ∘ f) y` witness `(x , p : dist (g (f x)) y ≤ ε)`,
+  -- produce the RHS Σ-shape at the canonical split `(ε₁, ε₂) := (zero, ε)`:
+  --
+  --   * intermediate `b := f x` (the canonical lift),
+  --   * inner echo `EchoR zero f (f x)` via `echo-approx-intro`,
+  --   * outer bound is just the original `p`.
+  --
+  -- This is the "section" half of the retract: a one-sided splitting
+  -- of the §Q3 conjecture that always exists, with no extra hypothesis
+  -- beyond what `EchoR ε (g ∘ f) y` already supplies. The "wrong"
+  -- intermediates are not enumerable, which is precisely why the
+  -- approximate analogue is a retract and not a full iso.
+  echo-approx-comp-retract-to :
+    ∀ {ε : Tol} (f : A → B) (g : B → B) {y : B} →
+    EchoR ε (g ∘ f) y →
+    Σ B (λ b → EchoR zero f b × dist (g b) y ≤ ε)
+  echo-approx-comp-retract-to f g (x , dgfx≤ε) =
+    f x , echo-approx-intro f x , dgfx≤ε
+
+  -- A-component round-trip. Starting from an `EchoR ε (g ∘ f) y`,
+  -- pushing through the canonical-split section then through
+  -- soundness lands back on the *same A-witness `x`* (the tolerance
+  -- budget weakens from `ε` to `zero + ε`, which is why this is a
+  -- retraction in the A-component rather than a full equality of
+  -- echoes). The proof is `refl` — the A-component is preserved
+  -- definitionally because every step of the round-trip keeps
+  -- `proj₁` pinned to the original `x`.
+  --
+  -- This pins the "retract direction holds definitionally" promise
+  -- of the design note: the witness-on-A round-trips on the nose,
+  -- even though the tolerance and intermediate-B components do not.
+  echo-approx-comp-retract-A :
+    ∀ {ε : Tol} (f : A → B) (g : B → B) (g-nonexp : NonExpansive g)
+    {y : B} (e : EchoR ε (g ∘ f) y) →
+    proj₁ (echo-approx-comp-sound f g g-nonexp
+            (echo-approx-comp-retract-to f g e))
+    ≡ proj₁ e
+  echo-approx-comp-retract-A f g g-nonexp (x , _) = refl