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

[hyperpolymath]

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 theory: EchoApprox composition rung — first slice (retract direction) #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

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

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

[github-actions]

🔍 Hypatia Security Scan

Findings: 10 issues detected

Severity	Count
🔴 Critical	0
🟠 High	5
🟡 Medium	5

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/cache@v4 needs attention",
    "type": "unpinned_action",
    "file": "agda.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "No dependabot.yml or renovate.json found in echo-types",
    "type": "DependencyUpdate",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "high",
    "remediation": "Add .github/dependabot.yml or renovate.json configuration.",
    "scorecard_check": "Dependency-Update-Tool"
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "1 workflow(s) with tag-pinned (not SHA-pinned) actions in echo-types",
    "type": "DependencyPinning",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Pin GitHub Actions and Docker base images by SHA hash.",
    "scorecard_check": "Pinned-Dependencies"
  },
  {
    "reason": "Repository has 1 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence