proof(L3): add T_Echo_L1 typing rule for runtime echo values (slice 3a)

PROOF-NEEDS.md

@@ -105,6 +105,7 @@ enters the typing rules" and (for the diagram) in §6 (to be added).
 |---|---|---|
 | ✅ Extend AST with [TEcho : ty -> ty] and [EEcho : ty -> expr -> expr] | Type former + runtime value form for L3 echoes | done 2026-05-27 (L3 wiring slice 1 — Syntax.v + free_regions + value/shift/subst cases) |
 | ✅ Add `T_Observe_L1` typing rule + `EObserve` expr form | Consumes a `TEcho T` echo, returns `TBase TUnit` | done 2026-05-27 (L3 wiring slice 2 — modality-polymorphic single rule; mandatoriness via `is_linear_ty TEcho`/implicit-drop discipline is a follow-up) |
+| ✅ Add `T_Echo_L1` typing rule | Types runtime [EEcho T v] residue values at `TEcho T` | done 2026-05-27 (L3 wiring slice 3a — typing-side counterpart of forthcoming `S_Region_Exit_Echo` / `S_Drop_Echo` step rules; mode-polymorphic) |
 | Add collapse-function emission to step rules at irreversible boundaries | `S_Region_Exit` emits `Echo (LiveAt_r) (ExitedAt_r) v_pre`; `S_Drop` emits `Echo T ⊤ v_pre` | Each irreversible step has an associated collapse function `f : A → B`; the echo is the proof-relevant preimage |
 | Thread `G` (echo context) alongside `R` (region context) through compound rules | New context parameter on every L1 compound rule | Parallel to R-threading; no overlap |
 | State and prove `preservation_l3` | Per-layer preservation theorem against the L3 invariants | Cross-layer dependency annotated in `PRESERVATION-DESIGN.md §5.1` |

formal/Semantics_L1.v

@@ -188,11 +188,10 @@ Proof.
       inversion Hv.
     + (* T_Borrow_Val_L1 *)
       split; reflexivity.
-  - (* VEcho T v — no L1 typing rule produces EEcho yet (L3 wiring is
-       a separate slice; see PROOF-NEEDS.md §2). The hypothesis [Ht]
-       on [EEcho T v] is therefore vacuous: [inversion] discharges
-       all impossible constructor cases. *)
-    inversion Ht.
+  - (* VEcho T v — T_Echo_L1 (slice 3a) types this at [TEcho T]
+       with R_out = R and G_out = G by construction; both invariants
+       hold immediately. *)
+    inversion Ht; subst; split; reflexivity.
 Qed.
 
 (** ** Helper: region-environment shrinkage for value typings.
@@ -548,6 +547,11 @@ Proof.
     eapply T_Drop_L1; [exact H | eapply IHHt; auto].
   - (* T_Copy_L1 *)
     eapply T_Copy_L1; [exact H | eapply IHHt; auto].
+  - (* T_Echo_L1 — region shrink under an echo value preserves the
+     value structure (region-free witness implies a region-free echo). *)
+    eapply T_Echo_L1.
+    + exact H.
+    + eapply IHHt; auto.
   - (* T_Observe_L1 — region shrink commutes with the witness sub-expression *)
     eapply T_Observe_L1. eapply IHHt; auto.
 Admitted.
@@ -940,6 +944,12 @@ Proof.
   - eapply T_Drop_L1; [exact H |]. apply IHHtype. assumption.
   (* T_Copy_L1 *)
   - eapply T_Copy_L1; [exact H |]. apply IHHtype. assumption.
+  (* T_Echo_L1 — runtime echo value typing; shift commutes with the
+     witness sub-expression. The is_value premise is preserved by
+     [shift_preserves_value]. *)
+  - eapply T_Echo_L1.
+    + apply shift_preserves_value. exact H.
+    + apply IHHtype. assumption.
   (* T_Observe_L1 — shift commutes with the witness sub-expression *)
   - eapply T_Observe_L1. apply IHHtype. assumption.
 Qed.
@@ -1446,6 +1456,13 @@ Proof.
   (* T_Copy_L1 *)
   - eapply T_Copy_L1; [exact H |]. eapply IHHtype; eassumption.
 
+  (* T_Echo_L1 — substitution under an echo value: the witness is a
+     value, so [subst_preserves_value] preserves [is_value]. The
+     witness's typing is preserved by the IH. *)
+  - eapply T_Echo_L1.
+    + apply subst_preserves_value. assumption.
+    + eapply IHHtype; eassumption.
+
   (* T_Observe_L1 *)
   - eapply T_Observe_L1. eapply IHHtype; eassumption.
 Qed.

formal/TypingL1.v

@@ -291,6 +291,25 @@ Inductive has_type_l1
       R ; G |=L1[m] e : T -| R' ; G' ->
       R ; G |=L1[m] ECopy e : TProd T T -| R' ; G'
 
+  (** ===== L3 — Echo / residue value typing =====
+
+      [T_Echo_L1] types the runtime [EEcho T v] residue at [TEcho T],
+      provided the witness [v] is itself a value typed at [T]. This
+      is the typing-side counterpart of the (forthcoming, slice 3b /
+      3c) step rules that emit echoes at irreversible boundaries:
+      [S_Region_Exit_Echo] and [S_Drop_Echo] will both produce
+      [EEcho T v_pre] residues which must be typable for preservation
+      to hold.
+
+      Modality-polymorphic: holds in both [Linear] and [Affine]. The
+      [is_value v] premise mirrors [T_Borrow_Val_L1] — echoes are
+      runtime-only values, not surface syntax. *)
+
+  | T_Echo_L1 : forall m R G v T,
+      is_value v ->
+      R ; G |=L1[m] v : T -| R ; G ->
+      R ; G |=L1[m] EEcho T v : TEcho T -| R ; G
+
   (** ===== L3 — Echo / residue observation =====
 
       [T_Observe_L1] discharges an echo by witnessing it. The rule is