hygiene: per-lemma Smoke pins for EchoApprox via concrete instance module

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; PR #70 (Lane C of
the multi-lane swarm) added the retract-direction lemmas 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 can be re-pointed
at it.

Headlines now pinned in Smoke.agda (9 names):

  * 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 verified in parent session (sandbox quirk denied positional-
argument agda invocations in this worktree):

  $ 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. No postulates, no funext, no
path algebra — every field is tt or refl.

Refs PR #70 (Lane C surfaced the gap).
Refs CLAUDE.md "Working rules" invariant.

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

Author: hyperpolymath

proofs/agda/All.agda

@@ -18,6 +18,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