feat(check): make Echo types operational — typing rules for echo operations (#56)

## Summary

Echo types were **inert type formers**: `bet-check`'s unifier handled
`Echo T` / `EchoR T` (distinct from `T`, structural recursion, distinct
from each other), but **no expression could introduce or eliminate
one**. The design doc listed all the operations as "deferred".

This integrates the structured-loss operations **into the type system**
as genuinely polymorphic builtins, each instantiated with a **fresh
carrier variable per use site**:

| Operation | Typing rule | Role |
|-----------|-------------|------|
| `echo` | `'a -> Echo 'a` | introduction (`echo-intro`, unary collapse
of the fibre core) |
| `echo_output` | `Echo 'a -> 'a` | **explicit** projection to the base
value (never an implicit coercion) |
| `echo_to_residue` | `Echo 'a -> EchoR 'a` | lower a full echo to its
strict, non-recoverable residue |
| `sample_echo` | `Dist 'a -> Echo 'a` | probabilistic-support bridge:
retains the residue `sample` discards |

Wired through `Expr::Var` so **lexical bindings shadow** the builtins.
Surface syntax is ordinary application (`echo(x)`), so no grammar change
was needed.

## Design fidelity

- **Types-only / ghost.** `Echo T` / `EchoR T` still erase to `T` at
runtime — no residue payload is materialised, matching
`docs/echo-types.adoc` §"Runtime representation strategy". No
runtime/effect commitment.
- **Distinctness preserved.** Enforced *through the operations* as well
as the formers — `echo_output` on a bare carrier is rejected. No
implicit `Echo T -> T`.
- **Canonical names** mirror `hyperpolymath/echo-types` (source of
truth) and `EchoTypes.jl`.
- Deliberately **not** added: `echo_input` (coincides with `echo_output`
for the unary former), `residue_strictly_loses` (a propositional
witness, not a term), `bet_echo` (needs ternary surface form).

## Verification

- **34/34** `bet-check` tests pass (27 baseline + 7 new: intro, explicit
projection, residue lowering, `sample_echo` bridge + composition,
polymorphic reuse, bare-carrier rejection, shadowing).
- `tools/proof-scan.sh` clean — no banned soundness escape hatches.
- New library code is clippy-clean.

## Formal-proof follow-up

Lean keeps `echo`/`echoR` as type *formers* only, so
Progress/Preservation remain intact. Mirroring the operation typing
rules in Lean (and re-establishing the metatheory) is registered as
obligation **TP-5** in `PROOF-NEEDS.md` / `PROOF-STATUS.md`, deferred
until the runtime residue representation is settled.

## Files

- `compiler/bet-check/src/lib.rs` — `echo_builtin_type` + `Expr::Var`
wiring + tests
- `docs/echo-types.adoc` — new "Operations (typing rules)" section;
narrowed deferral list
- `README.adoc` — Echo Types section updated
- `PROOF-NEEDS.md` / `PROOF-STATUS.md` — TP-5 registered
- `proofs/BetLang.lean` — comment-only pointer to the landed rules +
TP-5

https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs

---
_Generated by [Claude
Code](https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -28,6 +28,7 @@ This file defines *what* must be proven. Completion is tracked in
 | TP-2   | Preservation (typing preserved under step)          | TP   | Lean4  | P1 | ✅ done |
 | TP-3   | Distribution monad laws (×3)                        | TP   | Lean4  | P1 | ✅ done |
 | TP-4   | Discharge `substTop_preserves_typing` axiom         | TP   | Lean4  | P1 | remaining |
+| TP-5   | Echo-operation typing rules + metatheory (Progress/Preservation) | TP | Lean4 | P2 | remaining |
 | SEM-1  | Continuous measure-theoretic denotation             | SEM  | Lean4  | P2 | remaining |
 | STAT-1 | Maximum entropy of uniform ternary = log₂3          | STAT | Lean4  | P2 | remaining |
 | STAT-2 | SLLN for bet sample means                           | STAT | Lean4  | P2 | remaining |

PROOF-STATUS.md

@@ -12,14 +12,14 @@ See `docs/AFFINESCRIPT-ALIGNMENT.adoc` for the phased plan and
 
 | Category | Total | Done | In Progress | Blocked | Remaining |
 |----------|-------|------|-------------|---------|-----------|
-| Typing / metatheory (TP)   | 4 | 3 | 0 | 0 | 1 |
+| Typing / metatheory (TP)   | 5 | 3 | 0 | 0 | 2 |
 | Semantics (SEM)            | 1 | 0 | 0 | 0 | 1 |
 | Statistics (STAT)          | 2 | 0 | 0 | 0 | 2 |
 | ABI / FFI (ABI)            | 5 | 0 | 0 | 0 | 5 |
 | Concurrency (CONC)         | 1 | 0 | 0 | 0 | 1 |
-| **Total**                  | **13** | **3** | **0** | **0** | **10** |
+| **Total**                  | **14** | **3** | **0** | **0** | **11** |
 
-**Overall**: 23% proven (3 / 13). Lean core metatheory mechanised and
+**Overall**: 21% proven (3 / 14). Lean core metatheory mechanised and
 (as of Phase 1) machine-checked in CI.
 
 ## Proofs Done
@@ -52,6 +52,7 @@ See `docs/AFFINESCRIPT-ALIGNMENT.adoc` for the phased plan and
 | ID | Proof | Category | Prover | Phase | Priority |
 |----|-------|----------|--------|-------|----------|
 | TP-4   | Discharge `substTop_preserves_typing` (de Bruijn subst lemma) | TP   | Lean4  | 2 | P1 |
+| TP-5   | Echo-operation typing rules + metatheory — mirror `bet-check`'s functor/comonad surface (`echo`, `echo_map`, `echo_output`, `echo_duplicate`, `echo_to_residue`, `sample_echo`), incl. the comonad laws from `EchoGradedComonad.agda` | TP | Lean4 | 2 | P2 |
 | SEM-1  | Continuous measure-theoretic denotational semantics           | SEM  | Lean4  | 2 | P2 |
 | STAT-1 | Maximum entropy of uniform ternary = log₂3 bits               | STAT | Lean4  | 2 | P2 |
 | STAT-2 | SLLN for bet sample means (a.s. convergence to expectation)   | STAT | Lean4  | 2 | P2 |
@@ -82,3 +83,4 @@ classified `axiom` is permitted by policy (standards#203).
 | Date | Change | By |
 |------|--------|-----|
 | 2026-06-02 | Phase 1: Lean proofs made CI-machine-checked; status table created. | alignment branch |
+| 2026-06-03 | Echo operations typed in `bet-check` (`echo`/`echo_output`/`echo_to_residue`/`sample_echo`); registered TP-5 for the Lean metatheory mirror. | echo-types pass |

README.adoc

@@ -136,13 +136,21 @@ link:https://github.com/hyperpolymath/echo-types[`hyperpolymath/echo-types`] (Ag
   _Distinct from `T`_: `unify(Echo T, T)` fails by design.
 
 | `EchoR T`
-| The strict, non-recoverable residue of `Echo T`. Reserved; operations deferred.
+| The strict, non-recoverable residue of `Echo T`. Introduced by
+  `echo_to_residue`; further operations deferred.
 |===
 
 `Echo T` and `EchoR T` erase to `T` at runtime (ghost types) until operations
 demand a payload. The canonical introduction site is probabilistic support retention:
 `sample : Dist T → T` discards which branch fired;
-`sample_echo : Dist T → Echo T` retains that residue — deferred for a future pass.
+`sample_echo : Dist T → Echo T` retains that residue. The operations now
+type-check in `bet-check` (type-level; the runtime residue payload remains
+deferred): introduction `echo` (`'a → Echo 'a`); the **functor + comonad
+surface** `echo_map` (`('a→'b) → Echo 'a → Echo 'b`), `echo_output`
+(`Echo 'a → 'a`, the counit), `echo_duplicate` (`Echo 'a → Echo (Echo 'a)`);
+the residue lowering `echo_to_residue` (`Echo 'a → EchoR 'a`); and the
+probabilistic bridge `sample_echo` (`Dist 'a → Echo 'a`). These mirror the
+graded comonad proved in `hyperpolymath/echo-types`.
 
 See link:docs/echo-types.adoc[`docs/echo-types.adoc`] for the full design rationale.
 
@@ -437,7 +445,7 @@ BetLang is built on three principles:
 | Racket frontend | ✅ Authoritative | Canonical semantics
 | Julia backend | 🟡 Active development | Primary compute kernel
 | Lean 4 proofs | ✅ Machine-checked | Progress + Preservation + monad laws
-| Rust type-checker | ✅ Active | bet-check / bet-core (incl. Echo T)
+| Rust type-checker | ✅ Active | bet-check / bet-core (incl. Echo T + operations)
 | VS Code extension | 🟡 In progress | AffineScript source (replaces ReScript)
 | Web Playground (ui/) | ✅ Available | Quantum-inspired features
 | FFI (Zig) | 🟡 Experimental | playground/ffi/zig/