hygiene: per-lemma Smoke pins for EchoApprox via concrete instance module (#71)

## Summary

Closes a silent violation of the CLAUDE.md "Working rules" invariant —
*"Every headline theorem must be pinned in `Smoke.agda` via `using`
clause"* — for parameterised modules. `EchoApprox.Approx` lemmas could
not be named in `Smoke.agda` until *some* `PseudoMetric` was supplied,
so the invariant has been quietly skipped for every `echo-approx-*` and
`echo-strict→approx` lemma. PR #70 (Lane C of the multi-lane swarm)
added the retract-direction lemmas (`echo-approx-comp-sound`,
`echo-approx-comp-retract-to`, `echo-approx-comp-retract-A`) but,
following existing convention, left them unpinned for the same reason.
This PR closes the gap with the smallest, most honest possible instance.

**Instance chosen:** the trivial / collapse-to-strict pseudometric on
the unit carrier `⊤`.

- `Tol  := ⊤`,  `zero := tt`,  `_+_  := λ _ _ → tt`
- `_≤_  := λ _ _ → ⊤`
- `dist := λ _ _ → tt` on `B := ⊤`

Every order / monotonicity / triangle obligation discharges to `tt`.
Every approximate echo collapses to `Σ A (λ _ → ⊤)`, so each pinned
lemma is a proof-of-life sanity check that the parameterised module's
term is well-typed at *some* instance — exactly the hygiene contract the
invariant asks for. No new mathematical content. When a genuine metric
instance lands in the repo, the per-lemma pins below can be re-pointed
at it (this is option 1 of two candidates considered; option 2, a
discrete metric over `Bool`, adds nothing for the pinning purpose).

## Headlines now pinned in `Smoke.agda` (9 names)

| New top-level name | Underlying `Approx` term |
|---|---|
| `approx-EchoR` | `EchoR` |
| `approx-intro` | `echo-approx-intro` |
| `approx-strict→approx` | `echo-strict→approx` |
| `approx-relax` | `echo-approx-relax` |
| `approx-NonExpansive` | `NonExpansive` |
| `approx-compose` | `echo-approx-compose` |
| `approx-comp-sound` | `echo-approx-comp-sound` |
| `approx-comp-retract-to` | `echo-approx-comp-retract-to` |
| `approx-comp-retract-A` | `echo-approx-comp-retract-A` |

Plus the instance constructors `trivialTolerance`,
`trivialPseudoMetric`.

## Build status

Verified in the parent session (a sandbox quirk in this worktree denied
positional-argument `agda` invocations despite project
`.claude/settings.json` allowing them; the call worked from the parent):

```
$ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda
exit: 0
$ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda
exit: 0
```

`--safe --without-K` invariants intact (Agda would have errored
otherwise). No postulates, no funext, no path algebra — every field is
`tt` or `refl`.

## Files

- New: `proofs/agda/EchoApproxInstance.agda` (instance + 9 per-lemma
re-bindings)
- Modified: `proofs/agda/All.agda` (one `open import` line, keeps
orphan-module-as-dead-code rule satisfied)
- Modified: `proofs/agda/Smoke.agda` (per-lemma `using` clause adjacent
to the existing `Approx` block)

## Refs

- Refs #70 — Lane C surfaced the gap by landing retract-direction lemmas
in a parameterised module.
- Refs CLAUDE.md "Working rules" invariant: *"Every headline theorem
must be pinned in `Smoke.agda` via `using` clause."*
- Does **not** Close any issue.

## Test plan

- [x] `LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda` exits 0
under `--safe --without-K` (verified parent session)
- [x] `LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda` exits
0 under `--safe --without-K` (verified parent session)
- [x] No new postulates introduced
- [x] No `--safe` weakening or escape pragmas
- [ ] CI green on this branch

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

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

Author: hyperpolymath

proofs/agda/All.agda

@@ -19,6 +19,7 @@ open import EchoIntegration
 open import EchoCNOBridge
 
 open import EchoApprox
+open import EchoApproxInstance
 open import EchoIndexed
 open import EchoDecidable
 open import EchoAccess

proofs/agda/EchoApproxInstance.agda

@@ -0,0 +1,98 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- A concrete `Tolerance` + `PseudoMetric` instance for `EchoApprox.Approx`,
+-- whose sole purpose is to give `Smoke.agda` a typeable identifier per
+-- headline lemma of the parameterised `EchoApprox.Approx` module.
+--
+-- Repo invariant (`CLAUDE.md`, "Working rules"):
+--
+--     "Every headline theorem must be pinned in `Smoke.agda` via
+--      `using` clause."
+--
+-- Lemmas living inside the parameterised submodule `EchoApprox.Approx`
+-- cannot be named in `Smoke.agda` until *some* `PseudoMetric` is
+-- supplied, so the invariant is silently violated for every
+-- `echo-approx-*` and `echo-strict→approx` lemma. This module closes
+-- that gap.
+--
+-- Design call: the trivial / collapse-to-strict pseudometric on `⊤`.
+--
+--   * `Tol`     := `⊤`,  `zero` := `tt`,  `_+_` := `λ _ _ → tt`
+--   * `_≤_`     := `λ _ _ → ⊤`
+--   * `dist`    := `λ _ _ → tt` on the carrier `B := ⊤`
+--
+-- Every order / monotonicity / triangle obligation discharges to `tt`.
+-- Every approximate echo `EchoR ε f y = Σ A (λ x → dist (f x) y ≤ ε)`
+-- collapses to `Σ A (λ _ → ⊤)`, so each pinned lemma here is a trivial
+-- sanity check that the parameterised module's term is well-typed at
+-- *some* instance. That is exactly the hygiene contract the invariant
+-- asks for — proof-of-life, not new content.
+--
+-- We choose `A := ⊤` and `B := ⊤` so each pinned name resolves to a
+-- single top-level identifier with no remaining type parameters, which
+-- lets `Smoke.agda` enumerate them in a `using` clause one-for-one.
+--
+-- A non-trivial pseudometric (e.g. the discrete metric over `Bool`)
+-- would also work, but adds nothing the trivial one does not give for
+-- the purposes of `Smoke.agda` pinning. When a genuine metric instance
+-- lands in the repo, the per-lemma pins below can be re-pointed at it.
+
+module EchoApproxInstance where
+
+open import Level                                 using (Level)
+open import Data.Unit.Base                        using (⊤; tt)
+open import Relation.Binary.PropositionalEquality using (refl)
+
+open import EchoApprox using (Tolerance; PseudoMetric; module Approx)
+
+----------------------------------------------------------------------
+-- The trivial tolerance carrier
+----------------------------------------------------------------------
+
+-- All fields are tt / Unit; every law obligation is met by `tt`.
+trivialTolerance : Tolerance Level.zero
+trivialTolerance = record
+  { Tol      = ⊤
+  ; zero     = tt
+  ; _+_      = λ _ _ → tt
+  ; _≤_      = λ _ _ → ⊤
+  ; ≤-refl   = tt
+  ; ≤-trans  = λ _ _ → tt
+  ; +-mono-≤ = λ _ _ → tt
+  }
+
+----------------------------------------------------------------------
+-- The trivial pseudometric on the carrier `⊤`
+----------------------------------------------------------------------
+
+-- Distance is constantly `tt`; self-distance is `refl`; triangle is `tt`.
+trivialPseudoMetric : PseudoMetric ⊤ trivialTolerance
+trivialPseudoMetric = record
+  { dist      = λ _ _ → tt
+  ; dist-self = λ _   → refl
+  ; dist-tri  = λ _ _ _ → tt
+  }
+
+----------------------------------------------------------------------
+-- Per-lemma proof-of-life pins for `Approx` at the trivial instance.
+--
+-- Top-level identifiers, one per `EchoApprox.Approx` headline, with
+-- `A := ⊤` and `B := ⊤` so each is a closed term that `Smoke.agda`
+-- can enumerate in a `using` clause. Definitions use `=` (no explicit
+-- type signature) so the original term's type is inferred — which is
+-- exactly the typeability check the hygiene invariant asks for.
+----------------------------------------------------------------------
+
+private
+  open module ApproxT⊤ =
+    Approx {A = ⊤} {B = ⊤} {T = trivialTolerance} trivialPseudoMetric
+
+approx-EchoR              = EchoR
+approx-intro              = echo-approx-intro
+approx-strict→approx      = echo-strict→approx
+approx-relax              = echo-approx-relax
+approx-NonExpansive       = NonExpansive
+approx-compose            = echo-approx-compose
+approx-comp-sound         = echo-approx-comp-sound
+approx-comp-retract-to    = echo-approx-comp-retract-to
+approx-comp-retract-A     = echo-approx-comp-retract-A

proofs/agda/Smoke.agda

@@ -75,6 +75,23 @@ open import EchoApprox using
   ; module Approx
   )
 
+-- Per-lemma pins for the parameterised EchoApprox via EchoApproxInstance
+-- (hygiene; closes the CLAUDE.md "Working rules" invariant gap for
+-- parameterised modules — see follow-up to PR #70).
+open import EchoApproxInstance using
+  ( trivialTolerance
+  ; trivialPseudoMetric
+  ; approx-EchoR
+  ; approx-intro
+  ; approx-strict→approx
+  ; approx-relax
+  ; approx-NonExpansive
+  ; approx-compose
+  ; approx-comp-sound
+  ; approx-comp-retract-to
+  ; approx-comp-retract-A
+  )
+
 open import EchoIndexed using
   ( Echoᵢ
   ; echoᵢ-intro