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

Adds Agda to Tier-1 alongside the existing Tier-1 set in three
RSR_OUTLINE.adoc copies (with the ReScript -> AffineScript and
Rust -> Rust(+SPARK) updates from PR #35 inlined to avoid build
conflict).

Adds two new rows to .claude/CLAUDE.md:
  - Agda (formal verification, foundational/type-theoretic)
  - echo-types library (canonical loss-with-residue formalism;
    cite from hyperpolymath/echo-types rather than reinventing)

Reframes Idris2 row from 'sole option' to 'primary, ABI-style
proofs' since Agda now formally complements it.

Updates ai-instruction/sonnet.md hard-rules language-policy line
to list AffineScript first, include Agda explicitly, ban ReScript,
and reference RS/TS/JS -> AffineScript -> typed-wasm.

Coordinates with:
  hyperpolymath/echo-types#29 (.scm -> .a2ml + Justfile fix)
  hyperpolymath/echo-types#30 (RSR floor scaffolding)
  #33 (REQUIRED-FILES doc-drift fix)
  #35 (ReScript -> AffineScript sweep;
    line-overlap with this PR; mechanical rebase at merge)

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