chore(policy): recognise Agda + echo-types as canonical loss-with-residue formalism (#36)

## Summary

Recognise **Agda** as a Tier-1 language and
**`hyperpolymath/echo-types`** as the canonical loss-with-residue
formalism in the agent-facing policy and tier docs.

## What changed

### Tier-1 list (3 RSR_OUTLINE.adoc copies)

```diff
- * **Tier 1** (Gold): Rust, Elixir, Zig, Ada, Haskell, ReScript
+ * **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda
```

Adds Agda alongside the existing tier. Replaces ReScript with
AffineScript and qualifies Rust as Rust(+SPARK), tracking the broader
ReScript→AffineScript migration in PR #35 (this PR's diff includes those
updates so the file builds without conflict; #35 may need a rebase but
the resolutions are mechanical).

Files updated:
- `0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc` line 149
- `0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc` line 149
- `consent-aware-http/RSR_OUTLINE.adoc` line 149

### Agent-facing language policy (`.claude/CLAUDE.md`)

Adds two new rows to the allowed-languages table:

```
| **Agda**            | Formal verification (foundational / type-theoretic constructions) | Used by hyperpolymath/echo-types ... |
| **echo-types library** | Loss-with-residue formalism (Agda) | hyperpolymath/echo-types — canonical formalisation of Echo f y := Σ (x : A) , (f x ≡ y) ... |
```

Reframes Idris2 from "Formal verification (sole option)" to "Formal
verification (primary, ABI-style proofs)" since Agda now formally
complements it for foundational constructions where Idris2's specific
dependent-type idiom isn't the right tool.

### `ai-instruction/sonnet.md`

The hard-rules language-policy line now lists AffineScript first,
includes Agda explicitly, bans ReScript, and references the
AffineScript→typed-wasm direction:

```diff
- - <Language policy: ReScript / Rust / Deno / Zig / Idris2 / Gleam; no
-   TypeScript, Node, npm/bun/yarn, Go, general Python>
+ - <Language policy: AffineScript / Rust(+SPARK) / Deno / Zig / Idris2 / Agda / Gleam; no
+   TypeScript, ReScript, Node, npm/bun/yarn, Go, general Python (RS/TS/JS → AffineScript → typed-wasm; Agda for foundational proofs incl. echo-types)>
```

## Why

Echo-types (`hyperpolymath/echo-types`) is an active, well-developed
Agda formalisation that the `coord-mcp` TODO file already aspires to
dogfood. Until now, the standards' policy docs name only Idris2 as the
ecosystem's formal-verification language, which understates Agda's role
for the foundational-construction track. This PR makes the actual
two-prover posture explicit.

The echo-types row is added because the canonical fiber/echo
construction `Echo f y := Σ (x : A) , (f x ≡ y)` should not be
re-derived in downstream design docs and proofs — they should cite the
library. Naming it explicitly in CLAUDE.md prevents accidental
reinvention.

## Coordinated companion PRs

- `hyperpolymath/echo-types#29` — `.scm` → `.a2ml` 6a2 file rename +
Justfile `make` → `just`. (Bringing echo-types into compliance with the
canonical extension rule.)
- `hyperpolymath/echo-types#30` — RSR template floor (23 new files:
githealth + RSR docs + dotfiles + 4 mandatory workflows + contractiles +
stapeln). (Bringing echo-types to file-presence floor.)
- `#33` — `.scm` → `.a2ml` doc fix in
REQUIRED-FILES.adoc + workflow-count drift fix.
- `#35` — ReScript → AffineScript estate-wide
sweep. (Some line-overlap with this PR; mechanical rebase at merge.)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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

Author: hyperpolymath

.claude/CLAUDE.md

@@ -36,7 +36,9 @@ for the canonical statement.
 | **Deno** | Runtime & package management | Replaces Node/npm/bun |
 | **Rust/SPARK** | Performance-critical, systems, WASM, CLI tools, safety-critical | "Rust" always means "Rust/SPARK" per terminology note above. Preferred over Ada where reachable. |
 | **Zig** | FFI layer (hyperpolymath ABI/FFI standard), memory-safe systems where Rust/SPARK is overkill | Also the migration target for V-lang |
-| **Idris2** | Formal verification (sole option) | ATS2 rejected. Proven-library status in `proven` repo. |
+| **Idris2** | Formal verification (primary, ABI-style proofs) | ATS2 rejected. Proven-library status in `proven` repo. |
+| **Agda** | Formal verification (foundational / type-theoretic constructions) | Used by `hyperpolymath/echo-types` (loss-with-residue / proof-relevant fibers) and other foundational formalisations. Constructive only — no postulates in load-bearing tracks. |
+| **echo-types library** | Loss-with-residue formalism (Agda) | `hyperpolymath/echo-types` — canonical formalisation of `Echo f y := Σ (x : A) , (f x ≡ y)`. Cite from this lib rather than reinventing in downstream code. |
 | **Tauri 2.0+** | Mobile apps (iOS/Android) | Rust backend + web UI |
 | **Dioxus** | Mobile apps (native UI) | Pure Rust, React-like |
 | **Gleam** | Backend services | Runs on BEAM or compiles to JS |

0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc

@@ -146,7 +146,7 @@ project/
 
 === Language Tiers
 
-* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript
+* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda
 * **Tier 2** (Silver): Nickel, Racket, Guile Scheme, Nix
 * **Infrastructure**: Guix channels, derivations
 

0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc

@@ -146,7 +146,7 @@ project/
 
 === Language Tiers
 
-* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript
+* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda
 * **Tier 2** (Silver): Nickel, Racket, Guile Scheme, Nix
 * **Infrastructure**: Guix channels, derivations
 

ai-instruction/sonnet.md

@@ -83,8 +83,8 @@ You are implementing <one-line task statement> in <repo path>.
 
 - <License headers: SPDX-License-Identifier: PMPL-1.0-or-later unless otherwise
   stated (AGPL-3.0-or-later for IDApTIK / Airborne Submarine Squadron)>
-- <Language policy: AffineScript / Rust(+SPARK) / Deno / Zig / Idris2 / Gleam; no
-  TypeScript, ReScript, Node, npm/bun/yarn, Go, general Python (RS/TS/JS → AffineScript → typed-wasm)>
+- <Language policy: AffineScript / Rust(+SPARK) / Deno / Zig / Idris2 / Agda / Gleam; no
+  TypeScript, ReScript, Node, npm/bun/yarn, Go, general Python (RS/TS/JS → AffineScript → typed-wasm; Agda for foundational proofs incl. echo-types)>
 - <Testing: run tests before claiming completion; "dune build passes" is NOT
   the same as "behaviourally correct" — cite a behavioural check>
 - <No dangerous patterns: believe_me, assert_total, Admitted, sorry,

consent-aware-http/RSR_OUTLINE.adoc

@@ -146,7 +146,7 @@ project/
 
 === Language Tiers
 
-* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript
+* **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda
 * **Tier 2** (Silver): Nickel, Racket, Guile Scheme, Nix
 * **Infrastructure**: Guix channels, derivations