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

[hyperpolymath]

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)

- * **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:

- - <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.)
• hyperpolymath/standards#33 — .scm → .a2ml doc fix in REQUIRED-FILES.adoc + workflow-count drift fix.
• hyperpolymath/standards#35 — ReScript → AffineScript estate-wide sweep. (Some line-overlap with this PR; mechanical rebase at merge.)

🤖 Generated with Claude Code

[chatgpt-codex-connector]

Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits.
Credits must be used to enable repository wide code reviews.