proof(L3.K): rewrite Echo.v K-free — eliminate eq_rect_eq dependency (#173)

## Summary

Discharges the K proof-debt documented in `formal/Echo.v`'s top-of-file
comment (introduced in PR #166, tracked in `docs/proof-debt.adoc` via
#169). Rewrites two definitions/lemmas that previously pulled in Coq's
`Eqdep.Eq_rect_eq.eq_rect_eq` (K / UIP) axiom via `dependent
destruction`, using the K-free motive-trick template established in
`formal/Modality.v` (#168).

## Changes

1. **New helper** `mode_le_affine_first : mode_le Affine m2 -> m2 =
Affine` — raw dependent match with sort-indexed motive. Mirrors
`Modality.v`'s `modality_le_affine_first`.
2. **`mode_le_trans` rewritten as a `Definition`** (not tactic-derived)
using the same shape as `Modality.v`'s `modality_le_trans`: pattern
match on `H12`; the `Linear_le_Affine` case uses `mode_le_affine_first`
+ `eq_rect` to transport the result through `m3 = Affine`.
3. **`degrade_mode_comp` no longer uses `dependent destruction`**. In
each non-trivial case:
   ```coq
   pose proof (mode_le_affine_first m3 p23) as Heq.
   generalize dependent p23. rewrite Heq. intros p23.
   rewrite (mode_le_prop _ _ p23 Affine_le_Affine).
   reflexivity.
   ```
This canonicalises `m3` to `Affine` via `mode_le_affine_first`, then
collapses `p23` to the unique `Affine_le_Affine` constructor via
`mode_le_prop` (already K-free from #166).
4. Top-of-file comment changed from "Proof-debt note (axiom
dependencies)" to "K-freedom" documentation.
5. `Coq.Program.Equality` import removed.

## Verification

`Print Assumptions` on every previously-K-using or K-inheriting lemma:

| Lemma | Status |
|---|---|
| `mode_le_trans` | Closed under the global context |
| `degrade_mode_comp` | Closed under the global context |
| `degrade_mode_compose` | Closed under the global context |
| `degrade_mode_via_join` | Closed under the global context |
| `no_section_collapse_to_residue` | Closed under the global context |
| `mode_le_prop` | Closed under the global context |

The entire `formal/` project (9 .v files) builds clean with zero admits
and zero axiom dependencies beyond the documented L1 admits in
`Semantics_L1.v`.

## Why this matters

Aligns Echo.v with:
- The Agda upstream's `--safe --without-K` discipline
(`echo-types/proofs/agda/EchoLinear.agda`).
- The rest of the Ephapax Coq codebase (per `Print Assumptions` on
`value_R_G_preserving_l1`, `subst_preserves_typing_l1`,
`weaken_modality`, etc. — all K-free).

Closes the L3.K proof-debt item.

## Branch base

Stacked off `proof/l1-region-threading-design` (head `30ce697`,
post-#172). Will rebase to `main` when #153 lands.

## Test plan

- [x] `coqc 8.18.0` builds `Echo.v` cleanly, 0 admits
- [x] Clean full-project rebuild passes — 9 .v files
- [x] `Print Assumptions` confirms K elimination
- [x] No semantic changes — same lemmas, K-free proofs only
- [ ] CI green
- [ ] Review: K-free template matches `Modality.v`; proof-debt closure
note in commit can also be added to `docs/proof-debt.adoc` as a
follow-up doc tweak

Refs PR #166, PR #168, PR #169.

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

Author: hyperpolymath

formal/Echo.v

@@ -61,26 +61,23 @@
     satisfies all three constraints. This file does not introduce
     contradictions with them. *)
 
-(** ** Proof-debt note (axiom dependencies)
-
-    Two lemmas in this file ([mode_le_trans] and [degrade_mode_comp])
-    use [dependent destruction] from [Coq.Program.Equality] to
-    discriminate impossible cases on the indexed inductive
-    [mode_le]. This pulls in Coq's standard [eq_rect_eq] (K / UIP)
-    axiom.
-
-    The Agda upstream ([EchoLinear.agda]) is [--safe --without-K]
-    and discharges these cases without K. The rest of the Ephapax
-    Coq codebase (per [Print Assumptions] on [value_R_G_preserving_l1],
-    [subst_preserves_typing_l1]) is also K-free.
-
-    A follow-up slice should rewrite [mode_le_trans] and
-    [degrade_mode_comp] using raw dependent pattern matching with
-    motive tricks to be K-free, aligning with the Agda upstream and
-    the rest of the Coq codebase. Tracked as L3.K proof-debt. *)
+(** ** K-freedom
+
+    Every Qed/Definition in this file is closed under the global
+    context — zero axioms, zero K, zero UIP. The earlier L3 Phase 1
+    version (PR #166) used [dependent destruction] for
+    [mode_le_trans] + [degrade_mode_comp], pulling in
+    [Eqdep.Eq_rect_eq.eq_rect_eq] (K / UIP). This file's discharge of
+    that proof-debt mirrors the K-free template established in
+    [Modality.v]'s [modality_le_trans]: a raw dependent match with a
+    "motive trick" that returns [True] for impossible constructor /
+    index combinations and the genuine target type for the reachable
+    cases.
+
+    Aligns with the Agda upstream's [--safe --without-K] discipline
+    and with the rest of the Ephapax Coq codebase. *)
 
 Require Import Coq.Bool.Bool.
-Require Import Coq.Program.Equality.
 
 (** ===== Modes =====
 
@@ -110,20 +107,45 @@ Inductive mode_le : Mode -> Mode -> Type :=
 Lemma mode_le_refl : forall m, mode_le m m.
 Proof. intros [|]; constructor. Qed.
 
+(** Helper: when the first mode is [Affine], the second mode is also
+    [Affine] (the only [mode_le] constructor whose first index is
+    [Affine] is [Affine_le_Affine]). K-free via a motive trick on
+    the constructor's sort indices.
+
+    Mirrors [Modality.v]'s [modality_le_affine_first]. *)
+
+Definition mode_le_affine_first
+  (m2 : Mode) (H : mode_le Affine m2) : m2 = Affine :=
+  match H in mode_le mA mB
+    return
+      (match mA return Prop with
+       | Affine => mB = Affine
+       | Linear => True
+       end)
+  with
+  | Linear_le_Linear => I
+  | Linear_le_Affine => I
+  | Affine_le_Affine => eq_refl
+  end.
+
 (** [Defined] (not [Qed]) so [mode_le_trans] is transparent and
-    [degrade_mode_comp] can [simpl] through its applications. Uses
-    [dependent destruction] (K-dependent) — see the proof-debt note
-    at the top of the file. *)
+    [degrade_mode_comp] can [simpl] through its applications. Built
+    by raw dependent pattern matching; K-free.
+
+    Mirrors [Modality.v]'s [modality_le_trans]. *)
 
 Definition mode_le_trans
   (m1 m2 m3 : Mode)
-  (H12 : mode_le m1 m2) (H23 : mode_le m2 m3) : mode_le m1 m3.
-Proof.
-  destruct H12.
-  - exact H23.
-  - dependent destruction H23. exact Linear_le_Affine.
-  - exact H23.
-Defined.
+  (H12 : mode_le m1 m2) : mode_le m2 m3 -> mode_le m1 m3 :=
+  match H12 in mode_le mA mB return mode_le mB m3 -> mode_le mA m3 with
+  | Linear_le_Linear => fun h => h
+  | Linear_le_Affine =>
+      fun h =>
+        eq_rect Affine (fun m => mode_le Linear m)
+                Linear_le_Affine m3
+                (eq_sym (mode_le_affine_first m3 h))
+  | Affine_le_Affine => fun h => h
+  end.
 
 (** Propositionality of the mode order. Each pair [(m1, m2)] has at
     most one inhabitant in [mode_le]. This is what lets us collapse
@@ -303,9 +325,21 @@ Lemma degrade_mode_comp :
 Proof.
   intros m1 m2 m3 p12 p23 e.
   destruct p12.
-  - reflexivity.
-  - dependent destruction p23. reflexivity.
-  - dependent destruction p23. reflexivity.
+  - (* p12 = Linear_le_Linear: both sides reduce to [degrade_mode p23 e]. *)
+    reflexivity.
+  - (* p12 = Linear_le_Affine, p23 : mode_le Affine m3.
+       Canonicalise m3 via [mode_le_affine_first], then collapse the two
+       possible derivations of [mode_le Affine Affine] using
+       [mode_le_prop]. K-free. *)
+    pose proof (mode_le_affine_first m3 p23) as Heq.
+    generalize dependent p23. rewrite Heq. intros p23.
+    rewrite (mode_le_prop _ _ p23 Affine_le_Affine).
+    reflexivity.
+  - (* p12 = Affine_le_Affine, p23 : mode_le Affine m3. Same shape. *)
+    pose proof (mode_le_affine_first m3 p23) as Heq.
+    generalize dependent p23. rewrite Heq. intros p23.
+    rewrite (mode_le_prop _ _ p23 Affine_le_Affine).
+    reflexivity.
 Qed.
 
 (** Free-factoring composition law: any direct ordering proof