diff --git a/THEORY.md b/THEORY.md
index af2f2fa..eca42a5 100644
--- a/THEORY.md
+++ b/THEORY.md
@@ -458,6 +458,24 @@ Dual to graded monads, graded comonads model *coeffects* (context requirements):
 D_C(A) = A @requires C
 ```
 
+**Example (Echo — the graded comonad of structured loss).** For a map
+`f : A → B`, the echo type `Echo[A, B]` (the fibre `Echo f y := Σ(x:A). f x ≡ y`)
+carries, alongside each observed base `y = f x`, the witness `x` that `f`
+collapsed. Reading it as a graded comonad of *loss*:
+- the counit `ε = echo_base : Echo[A, B] → B` extracts the observable output,
+  discarding the witness;
+- the witness is the retained coeffect — the context `f` erased;
+- the grade is the *thermodynamic* cost of that erasure. Collapsing a fibre of
+  `N` distinguishable witnesses to one base erases `log₂ N` bits, costing
+  `k_B · T · ln N` of energy by Landauer's principle. Retaining the echo keeps
+  the computation reversible (Bennett): grade `0`.
+
+This makes information loss a first-class citizen of the same resource economy
+as energy/time/carbon: `landauer_cost(N, T) : Resource[Energy]` prices it, and
+`formal/coq/src/EchoThermo.v` proves the discrete shadow (reversible ⇔ zero
+cost; every genuine collapse costs ≥ 1 bit; erasure is monotone). The fibre /
+total-space soundness lives in `formal/coq/src/Echo.v` (`A ≃ Σ(y:B). Echo f y`).
+
 ### 5.6 Adjunctions
 
 **Proposition 5.1.** There is an adjunction:
diff --git a/compiler/eclexia-ast/src/types.rs b/compiler/eclexia-ast/src/types.rs
index 9bd2b2e..2486f21 100644
--- a/compiler/eclexia-ast/src/types.rs
+++ b/compiler/eclexia-ast/src/types.rs
@@ -37,6 +37,24 @@ pub enum Ty {
         dimension: Dimension,
     },
 
+    /// Echo type: the fiber (preimage space) of a map `domain -> codomain`.
+    ///
+    /// `Echo[A, B]` is Eclexia's first-class notion of *structured loss*:
+    /// the type of echoes of some collapsing map `f : A -> B`, each echo
+    /// pairing a retained witness `x : A` with the observed base `f x : B`
+    /// (the type-theoretic fibre `Echo f y := Σ (x : A). f x ≡ y`, from the
+    /// echo-types development). Distinct inputs that `f` collapses to the
+    /// same output remain distinguishable as distinct echoes — loss that is
+    /// not total erasure. Read as a graded comonad of loss (THEORY.md §5.5),
+    /// `echo_base` is the counit (the observable residue) and the witness is
+    /// the retained context.
+    Echo {
+        /// The domain `A` (the type of retained witnesses).
+        domain: Box<Ty>,
+        /// The codomain `B` (the type of observed bases).
+        codomain: Box<Ty>,
+    },
+
     /// Type variable (for inference)
     Var(TypeVar),
 
@@ -59,6 +77,7 @@ impl Ty {
             Ty::Function { params, ret } => params.iter().any(|t| t.has_vars()) || ret.has_vars(),
             Ty::Tuple(elems) => elems.iter().any(|t| t.has_vars()),
             Ty::Array { elem, .. } => elem.has_vars(),
+            Ty::Echo { domain, codomain } => domain.has_vars() || codomain.has_vars(),
             Ty::ForAll { body, .. } => body.has_vars(),
             _ => false,
         }
@@ -344,6 +363,9 @@ impl std::fmt::Display for Ty {
             Ty::Resource { base, dimension } => {
                 write!(f, "{}[{}]", base.name(), dimension)
             }
+            Ty::Echo { domain, codomain } => {
+                write!(f, "Echo[{}, {}]", domain, codomain)
+            }
             Ty::Var(v) => write!(f, "?{}", v.0),
             Ty::ForAll { vars, body } => {
                 write!(f, "∀")?;
@@ -360,3 +382,43 @@ impl std::fmt::Display for Ty {
         }
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    fn echo(domain: Ty, codomain: Ty) -> Ty {
+        Ty::Echo {
+            domain: Box::new(domain),
+            codomain: Box::new(codomain),
+        }
+    }
+
+    #[test]
+    fn echo_displays_with_bracket_syntax() {
+        let t = echo(Ty::int(), Ty::bool());
+        assert_eq!(t.to_string(), "Echo[Int, Bool]");
+    }
+
+    #[test]
+    fn echo_nests_in_display() {
+        let t = echo(Ty::int(), echo(Ty::string(), Ty::bool()));
+        assert_eq!(t.to_string(), "Echo[Int, Echo[String, Bool]]");
+    }
+
+    #[test]
+    fn echo_has_vars_follows_components() {
+        // No variables in either component.
+        assert!(!echo(Ty::int(), Ty::bool()).has_vars());
+        // A variable in the domain is observed.
+        assert!(echo(Ty::Var(TypeVar::new(0)), Ty::bool()).has_vars());
+        // A variable in the codomain is observed.
+        assert!(echo(Ty::int(), Ty::Var(TypeVar::new(1))).has_vars());
+    }
+
+    #[test]
+    fn echo_is_not_a_resource() {
+        // Echo is its own former, distinct from the Resource former.
+        assert!(!echo(Ty::int(), Ty::int()).is_resource());
+    }
+}
diff --git a/compiler/eclexia-codegen/src/lib.rs b/compiler/eclexia-codegen/src/lib.rs
index 4ae71e2..6bb5bf7 100644
--- a/compiler/eclexia-codegen/src/lib.rs
+++ b/compiler/eclexia-codegen/src/lib.rs
@@ -172,6 +172,7 @@ pub fn size_of_type(ty: &Ty) -> usize {
             size.map(|s| elem_size * s).unwrap_or(8) // Unknown size = pointer
         }
         Ty::Named { .. } => 8, // Placeholder for named types
+        Ty::Echo { .. } => 8,  // (witness, base) pair, heap-allocated: pointer
         Ty::ForAll { body, .. } => size_of_type(body),
         Ty::Var(_) | Ty::Error | Ty::Never => 8, // Fallback
     }
@@ -198,6 +199,7 @@ pub fn align_of_type(ty: &Ty) -> usize {
         Ty::Tuple(types) => types.iter().map(align_of_type).max().unwrap_or(1),
         Ty::Array { elem, .. } => align_of_type(elem),
         Ty::Named { .. } => 8,
+        Ty::Echo { .. } => 8,
         Ty::ForAll { body, .. } => align_of_type(body),
         Ty::Var(_) | Ty::Error | Ty::Never => 8,
     }
diff --git a/compiler/eclexia-interp/src/builtins.rs b/compiler/eclexia-interp/src/builtins.rs
index a6d3166..9d96f93 100644
--- a/compiler/eclexia-interp/src/builtins.rs
+++ b/compiler/eclexia-interp/src/builtins.rs
@@ -737,6 +737,128 @@ pub fn register(env: &Environment) {
             func: builtin_unwrap,
         }),
     );
+
+    // Echo (structured-loss) intrinsics. `echo` itself is intercepted in
+    // the evaluator (call_value_inner) because it must apply the function
+    // argument to compute the base; the stub below only fires if it is
+    // somehow called outside that path. `echo_witness` / `echo_base` are
+    // pure projections over the runtime echo value (a tagged "Echo" struct
+    // with `witness` and `base` fields).
+    env.define(
+        SmolStr::new("echo"),
+        Value::Builtin(BuiltinFn {
+            name: "echo",
+            func: builtin_echo_stub,
+        }),
+    );
+    env.define(
+        SmolStr::new("echo_witness"),
+        Value::Builtin(BuiltinFn {
+            name: "echo_witness",
+            func: builtin_echo_witness,
+        }),
+    );
+    env.define(
+        SmolStr::new("echo_base"),
+        Value::Builtin(BuiltinFn {
+            name: "echo_base",
+            func: builtin_echo_base,
+        }),
+    );
+
+    // Landauer cost of erasing structured loss — wires Echo into the
+    // energy resource economy (see formal/coq/src/EchoThermo.v).
+    env.define(
+        SmolStr::new("landauer_cost"),
+        Value::Builtin(BuiltinFn {
+            name: "landauer_cost",
+            func: builtin_landauer_cost,
+        }),
+    );
+}
+
+/// `landauer_cost(states, temperature_K) : Resource[Energy]`.
+///
+/// The minimum energy to irreversibly erase a fibre of `states`
+/// distinguishable witnesses down to its single base: `E = k_B * T *
+/// ln(states)` joules. A reversible collapse (`states <= 1`, i.e. the echo
+/// retains its witness) erases nothing and costs zero — Bennett's result,
+/// the runtime image of `EchoThermo.bennett_reversible_is_free`.
+fn builtin_landauer_cost(args: &[Value]) -> RuntimeResult<Value> {
+    if args.len() != 2 {
+        return Err(RuntimeError::ArityMismatch {
+            expected: 2,
+            got: args.len(),
+            hint: Some("landauer_cost(states, temperature_K)".to_string()),
+        });
+    }
+    let states = args[0]
+        .as_int()
+        .ok_or_else(|| RuntimeError::type_error("Int (number of states)", args[0].type_name()))?;
+    let temp_k = args[1]
+        .as_float()
+        .ok_or_else(|| RuntimeError::type_error("Float (temperature in K)", args[1].type_name()))?;
+
+    // Boltzmann constant (J/K). Reversible collapses (<= 1 state) are free.
+    const K_B: f64 = 1.380_649e-23;
+    let nats = if states <= 1 { 0.0 } else { (states as f64).ln() };
+    let energy = K_B * temp_k * nats;
+
+    Ok(Value::Resource {
+        value: energy,
+        dimension: eclexia_ast::dimension::Dimension::energy(),
+        unit: Some(SmolStr::new("J")),
+    })
+}
+
+/// Construct a runtime echo value: a tagged struct carrying the retained
+/// witness and the observed base. Shared by the evaluator's `echo`
+/// interception and any other producer.
+pub fn make_echo(witness: Value, base: Value) -> Value {
+    let mut fields = HashMap::new();
+    fields.insert(SmolStr::new("witness"), witness);
+    fields.insert(SmolStr::new("base"), base);
+    Value::Struct {
+        name: SmolStr::new("Echo"),
+        fields,
+    }
+}
+
+/// Read a field of a runtime echo value, checking the tag.
+fn echo_field(args: &[Value], field: &str, who: &str) -> RuntimeResult<Value> {
+    if args.len() != 1 {
+        return Err(RuntimeError::ArityMismatch {
+            expected: 1,
+            got: args.len(),
+            hint: None,
+        });
+    }
+    match &args[0] {
+        Value::Struct { name, fields } if name.as_str() == "Echo" => fields
+            .get(field)
+            .cloned()
+            .ok_or_else(|| RuntimeError::custom(format!("malformed echo value passed to {}", who))),
+        other => Err(RuntimeError::type_error("Echo", other.type_name())),
+    }
+}
+
+/// `echo_witness(e)` — the retained witness (proj1 of the fibre).
+fn builtin_echo_witness(args: &[Value]) -> RuntimeResult<Value> {
+    echo_field(args, "witness", "echo_witness")
+}
+
+/// `echo_base(e)` — the observed base value `f x` (the collapsed output).
+fn builtin_echo_base(args: &[Value]) -> RuntimeResult<Value> {
+    echo_field(args, "base", "echo_base")
+}
+
+/// Defensive stub: `echo` is handled in the evaluator so it can apply the
+/// function argument. Reaching here means it was used as a bare value in a
+/// position the evaluator does not intercept.
+fn builtin_echo_stub(_args: &[Value]) -> RuntimeResult<Value> {
+    Err(RuntimeError::custom(
+        "echo must be applied directly, e.g. echo(f, x)".to_string(),
+    ))
 }
 
 fn builtin_println(args: &[Value]) -> RuntimeResult<Value> {
diff --git a/compiler/eclexia-interp/src/eval.rs b/compiler/eclexia-interp/src/eval.rs
index c04a863..144a86c 100644
--- a/compiler/eclexia-interp/src/eval.rs
+++ b/compiler/eclexia-interp/src/eval.rs
@@ -1568,6 +1568,25 @@ impl Interpreter {
                 })
             }
 
+            // `echo(f, x)` is the structured-loss intro. It is handled here
+            // rather than as a plain builtin because it must apply `f` to `x`
+            // to compute the observed base `f x`; the resulting echo value
+            // retains the witness `x` alongside that base, so inputs that `f`
+            // collapses to the same output stay distinguishable.
+            Value::Builtin(builtin) if builtin.name == "echo" => {
+                if args.len() != 2 {
+                    return Err(RuntimeError::ArityMismatch {
+                        expected: 2,
+                        got: args.len(),
+                        hint: Some("echo(f, x): a function and a witness".to_string()),
+                    });
+                }
+                let f = args[0].clone();
+                let witness = args[1].clone();
+                let base = self.call_value(&f, std::slice::from_ref(&witness), file)?;
+                Ok(crate::builtins::make_echo(witness, base))
+            }
+
             Value::Builtin(builtin) => (builtin.func)(args),
 
             _ => Err(RuntimeError::NotCallable {
diff --git a/compiler/eclexia-llvm/src/lib.rs b/compiler/eclexia-llvm/src/lib.rs
index 3543d88..776d898 100644
--- a/compiler/eclexia-llvm/src/lib.rs
+++ b/compiler/eclexia-llvm/src/lib.rs
@@ -87,9 +87,12 @@ fn ty_to_llvm(ty: &Ty, ctx: &mut ModuleContext) -> String {
             let struct_name = ctx.declare_struct(name);
             format!("ptr %struct.{}", struct_name)
         }
-        Ty::Function { .. } | Ty::ForAll { .. } | Ty::Var(_) | Ty::Error | Ty::Never => {
-            "ptr".to_string()
-        }
+        Ty::Echo { .. }
+        | Ty::Function { .. }
+        | Ty::ForAll { .. }
+        | Ty::Var(_)
+        | Ty::Error
+        | Ty::Never => "ptr".to_string(),
     }
 }
 
diff --git a/compiler/eclexia-parser/src/lib.rs b/compiler/eclexia-parser/src/lib.rs
index 0cd501e..6aaf74b 100644
--- a/compiler/eclexia-parser/src/lib.rs
+++ b/compiler/eclexia-parser/src/lib.rs
@@ -54,6 +54,9 @@ impl<'src> Parser<'src> {
         let mut file = SourceFile::new();
 
         while !self.is_eof() {
+            // Token offset before this iteration, used to guarantee forward
+            // progress below.
+            let before = self.peek().span.start;
             match self.parse_item(&mut file) {
                 Ok(item) => file.items.push(item),
                 Err(e) => {
@@ -65,6 +68,18 @@ impl<'src> Parser<'src> {
                     file.items.push(eclexia_ast::Item::Error(error_span));
                 }
             }
+            // Guarantee forward progress. `recover_to_item` stops on
+            // item-start tokens, but `parse_item` rejects some of them
+            // (e.g. a top-level `enum`, which is not a supported item
+            // shorthand). Without this guard the loop would re-error on the
+            // same token forever, accumulating errors + placeholders until
+            // it runs out of memory (found by fuzzing — OOM in
+            // `parse_file` -> `parse_item` -> `unexpected_token`). If a whole
+            // iteration consumed no input, force one token so we always
+            // advance.
+            if !self.is_eof() && self.peek().span.start == before {
+                self.advance();
+            }
         }
 
         (file, std::mem::take(&mut self.errors))
@@ -2491,4 +2506,26 @@ mod tests {
         assert!(has_error, "Expected an error item node");
         assert!(has_function, "Expected the good function to be parsed");
     }
+
+    #[test]
+    fn parse_file_terminates_on_unhandled_item_token() {
+        // Regression (found by fuzzing — OOM): `enum` is a recovery
+        // stop-token in `recover_to_item`, but `parse_item` rejects it, so
+        // before the forward-progress guard in `parse_file` the loop spun
+        // forever, accumulating errors + Item::Error placeholders until it
+        // ran out of memory. Parsing must now terminate with a parse error.
+        let (file, errors) = parse("enum Foo {}");
+        assert!(!errors.is_empty(), "expected a parse error for top-level enum");
+        // It also makes progress past the offending token rather than
+        // emitting a single error in an unbounded loop.
+        assert!(
+            file.items.len() < 100,
+            "parser emitted an unbounded number of items: {}",
+            file.items.len()
+        );
+
+        // A run of unhandled stop-tokens must also terminate.
+        let (_f, errs) = parse("enum enum enum");
+        assert!(!errs.is_empty());
+    }
 }
diff --git a/compiler/eclexia-typeck/src/infer.rs b/compiler/eclexia-typeck/src/infer.rs
index 429ac04..219a614 100644
--- a/compiler/eclexia-typeck/src/infer.rs
+++ b/compiler/eclexia-typeck/src/infer.rs
@@ -74,6 +74,11 @@ impl TypeChecker<'_> {
             }
             Ty::Tuple(elems) => elems.iter().flat_map(|e| self.free_vars(e)).collect(),
             Ty::Array { elem, .. } => self.free_vars(&elem),
+            Ty::Echo { domain, codomain } => {
+                let mut vars = self.free_vars(&domain);
+                vars.extend(self.free_vars(&codomain));
+                vars
+            }
             Ty::ForAll { vars, body } => {
                 // Variables bound by ForAll are not free
                 let mut free = self.free_vars(&body);
@@ -119,6 +124,10 @@ impl TypeChecker<'_> {
                 elem: Box::new(self.substitute_vars(elem, subst)),
                 size: *size,
             },
+            Ty::Echo { domain, codomain } => Ty::Echo {
+                domain: Box::new(self.substitute_vars(domain, subst)),
+                codomain: Box::new(self.substitute_vars(codomain, subst)),
+            },
             Ty::ForAll { vars, body } => Ty::ForAll {
                 vars: vars.clone(),
                 body: Box::new(self.substitute_vars(body, subst)),
diff --git a/compiler/eclexia-typeck/src/lib.rs b/compiler/eclexia-typeck/src/lib.rs
index ff0b7d0..bb1362e 100644
--- a/compiler/eclexia-typeck/src/lib.rs
+++ b/compiler/eclexia-typeck/src/lib.rs
@@ -158,6 +158,65 @@ impl<'a> TypeChecker<'a> {
             },
         );
 
+        // Echo (structured-loss) intrinsics.
+        //   echo         : ((A) -> B, A) -> Echo[A, B]   -- intro: echo of f at x
+        //   echo_witness : (Echo[A, B]) -> A             -- retained witness (proj1)
+        //   echo_base    : (Echo[A, B]) -> B             -- observed base f x
+        // A and B are the shared builtin type variables 0 and 1, matching the
+        // Some/Ok convention in this prelude.
+        let echo_ty = || Ty::Echo {
+            domain: Box::new(Ty::Var(TypeVar::new(0))),
+            codomain: Box::new(Ty::Var(TypeVar::new(1))),
+        };
+        env.insert_mono(
+            SmolStr::new("echo"),
+            Ty::Function {
+                params: vec![
+                    Ty::Function {
+                        params: vec![Ty::Var(TypeVar::new(0))],
+                        ret: Box::new(Ty::Var(TypeVar::new(1))),
+                    },
+                    Ty::Var(TypeVar::new(0)),
+                ],
+                ret: Box::new(echo_ty()),
+            },
+        );
+        env.insert_mono(
+            SmolStr::new("echo_witness"),
+            Ty::Function {
+                params: vec![echo_ty()],
+                ret: Box::new(Ty::Var(TypeVar::new(0))),
+            },
+        );
+        env.insert_mono(
+            SmolStr::new("echo_base"),
+            Ty::Function {
+                params: vec![echo_ty()],
+                ret: Box::new(Ty::Var(TypeVar::new(1))),
+            },
+        );
+
+        // landauer_cost(states, temperature_K) : Resource[Energy]
+        //   The Landauer energy to irreversibly erase a fibre of `states`
+        //   distinguishable witnesses down to one base, k_B * T * ln(states).
+        //   This is how Echo's structured information loss enters the resource
+        //   economy (THEORY.md S5.5): keeping the echo's witness is reversible
+        //   (states = 1, zero cost, Bennett); collapsing it costs energy
+        //   (Landauer). Proven in formal/coq/src/EchoThermo.v.
+        env.insert_mono(
+            SmolStr::new("landauer_cost"),
+            Ty::Function {
+                params: vec![
+                    Ty::Primitive(PrimitiveTy::Int),
+                    Ty::Primitive(PrimitiveTy::Float),
+                ],
+                ret: Box::new(Ty::Resource {
+                    base: PrimitiveTy::Float,
+                    dimension: Dimension::energy(),
+                }),
+            },
+        );
+
         // Collection builtins: HashMap
         let hashmap_ty = Ty::Named {
             name: SmolStr::new("HashMap"),
@@ -717,6 +776,10 @@ impl<'a> TypeChecker<'a> {
                 base: *base,
                 dimension: *dimension,
             },
+            Ty::Echo { domain, codomain } => Ty::Echo {
+                domain: Box::new(self.freshen_ty_with_map(domain, mapping)),
+                codomain: Box::new(self.freshen_ty_with_map(codomain, mapping)),
+            },
             Ty::Var(var) => {
                 let entry = mapping.entry(*var).or_insert_with(|| {
                     let fresh = self.fresh_var();
@@ -1048,6 +1111,17 @@ impl<'a> TypeChecker<'a> {
                             }
                         }
                     }
+                    // Echo[A, B] — the fiber / structured-loss type of a
+                    // map A -> B (the type-theoretic fibre, see Ty::Echo).
+                    // First-class like Resource, recognised by name here.
+                    if name.as_str() == "Echo" && args.len() == 2 {
+                        let domain = self.resolve_ast_type(args[0]);
+                        let codomain = self.resolve_ast_type(args[1]);
+                        return Ty::Echo {
+                            domain: Box::new(domain),
+                            codomain: Box::new(codomain),
+                        };
+                    }
                     let arg_tys: Vec<Ty> = args.iter().map(|a| self.resolve_ast_type(*a)).collect();
                     Ty::Named {
                         name: name.clone(),
diff --git a/compiler/eclexia-typeck/src/unify.rs b/compiler/eclexia-typeck/src/unify.rs
index 386460d..8dd758a 100644
--- a/compiler/eclexia-typeck/src/unify.rs
+++ b/compiler/eclexia-typeck/src/unify.rs
@@ -23,6 +23,9 @@ impl TypeChecker<'_> {
             }
             Ty::Tuple(elems) => elems.iter().any(|e| self.occurs_check(v, e)),
             Ty::Array { elem, .. } => self.occurs_check(v, &elem),
+            Ty::Echo { domain, codomain } => {
+                self.occurs_check(v, &domain) || self.occurs_check(v, &codomain)
+            }
             Ty::ForAll { body, .. } => self.occurs_check(v, &body),
             _ => false,
         }
@@ -126,6 +129,20 @@ impl TypeChecker<'_> {
                 self.unify_with_occurs_check(e1, e2, span)
             }
 
+            (
+                Ty::Echo {
+                    domain: d1,
+                    codomain: c1,
+                },
+                Ty::Echo {
+                    domain: d2,
+                    codomain: c2,
+                },
+            ) => {
+                self.unify_with_occurs_check(d1, d2, span)?;
+                self.unify_with_occurs_check(c1, c2, span)
+            }
+
             (Ty::Named { name: n1, args: a1 }, Ty::Named { name: n2, args: a2 }) if n1 == n2 => {
                 if a1.len() != a2.len() {
                     return Err(TypeError::Mismatch {
diff --git a/compiler/eclexia/src/commands.rs b/compiler/eclexia/src/commands.rs
index 5de7187..b02940e 100644
--- a/compiler/eclexia/src/commands.rs
+++ b/compiler/eclexia/src/commands.rs
@@ -753,6 +753,10 @@ fn freshen_type_with_map(
             base: *base,
             dimension: *dimension,
         },
+        Ty::Echo { domain, codomain } => Ty::Echo {
+            domain: Box::new(freshen_type_with_map(checker, domain, mapping)),
+            codomain: Box::new(freshen_type_with_map(checker, codomain, mapping)),
+        },
         Ty::Var(var) => {
             let entry = mapping.entry(*var).or_insert_with(|| {
                 let fresh = checker.fresh_var();
diff --git a/docs/proof-debt.md b/docs/proof-debt.md
new file mode 100644
index 0000000..857c429
--- /dev/null
+++ b/docs/proof-debt.md
@@ -0,0 +1,76 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -->
+
+# Proof debt
+
+Ledger of soundness-relevant escape hatches in this repository's
+proof-bearing code, per the estate
+[Trusted-Base Reduction Policy](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc).
+
+Scope of this repo's trusted base:
+
+- **Coq** (`formal/coq/`) — `Typing.v` (Progress, Preservation, Soundness,
+  Dimensional Safety) and `Echo.v` (echo-type soundness) are **fully
+  constructive, axiom-free, 0 `Admitted`** — verified by `coqc 8.18.0`,
+  `Print Assumptions` reports "Closed under the global context". They carry
+  **no** entries here. The only escape hatches are the five linear-programming
+  duality axioms in `ShadowPrices.v`, dispositioned below.
+- **Agda** (`formal/agda/ResourceTracking.agda`) — no `postulate`s.
+- **Rust** (`compiler/`, `runtime/`) — `unsafe` blocks exist only at FFI
+  boundaries; none use `unsafePerformIO`/`unsafeCoerce`, so none are
+  soundness-relevant under the policy's marker set.
+
+> Note: `ShadowPrices.v` is **not** built by CI (it is commented out in
+> `formal/coq/_CoqProject`); it is a standalone research artefact. Its axioms
+> are therefore not on the path of any CI-verified theorem.
+
+## (a) Discharged in this repo
+- (none — entries are removed when the proof lands)
+
+## (b) Budgeted — tested with refutation budget
+- (none)
+
+## (c) Necessary axiom
+
+- `formal/coq/src/ShadowPrices.v:187` — `Axiom complementary_slackness`
+  - **Justification**: complementary slackness for an optimal primal/dual
+    pair. The standard constructive proof invokes strong duality, whose
+    standard constructive proof in turn certifies the pivot via complementary
+    slackness; the cycle is broken by axiomatising both (see
+    `strong_duality`). Load-bearing for the shadow-price theorems.
+  - **Citation**: Bertsimas & Tsitsiklis, *Introduction to Linear
+    Optimization* (1997), §4.
+
+- `formal/coq/src/ShadowPrices.v:215` — `Axiom lp_sensitivity`
+  - **Justification**: the optimal value's sensitivity to the right-hand side
+    equals the dual optimum (the shadow price), with a Lipschitz bound from
+    `‖λ*‖₁`. Establishing the piecewise-linear / Lipschitz structure of the
+    value function is not derivable from Coq's standard library.
+  - **Citation**: requires Coquelicot real analysis or Mathlib4
+    `LinearProgramming.duality.sensitivity`; Bertsimas & Tsitsiklis §5.
+
+- `formal/coq/src/ShadowPrices.v:246` — `Axiom strong_duality`
+  - **Justification**: strong LP duality (equal primal/dual optima). The
+    constructive proof needs the LP fundamental theorem and matrix-rank
+    infrastructure beyond what this file formalises.
+  - **Citation**: Bertsimas & Tsitsiklis, *Introduction to Linear
+    Optimization* (1997), Theorem 4.4.
+
+## (d) DEBT — actively to be closed
+
+- `formal/coq/src/ShadowPrices.v:161` — `Axiom weak_duality`
+  - **Owner**: @hyperpolymath
+  - **Plan**: dischargeable without external infrastructure — it reduces to
+    list-level dot-product associativity and the transpose identity
+    `(Aᵀλ)ᵀx = λᵀ(Ax)` over `lp_constraints`. Prove those two list lemmas and
+    promote this to category (a).
+  - **Deadline**: INDEFINITE — low priority; `ShadowPrices.v` is not on any
+    CI-verified path.
+
+- `formal/coq/src/ShadowPrices.v:519` — `Axiom dual_simplex_converges_to_optimal`
+  - **Owner**: @hyperpolymath
+  - **Plan**: requires a formalised pivot step, finite basis enumeration, and
+    Bland's-rule cycle prevention — none defined in this file. The axiom is
+    **not used** by any current theorem; it documents intended future work and
+    could alternatively be deleted until that work begins.
+  - **Deadline**: INDEFINITE — dependent on a formalised simplex kernel.
diff --git a/examples/echo_thermo.ecl b/examples/echo_thermo.ecl
new file mode 100644
index 0000000..d9f195f
--- /dev/null
+++ b/examples/echo_thermo.ecl
@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: MPL-2.0
+// Echo + Landauer: information loss, priced into the resource economy.
+//
+// Eclexia prices what you give up (shadow prices). An echo is what you give
+// up, retained. The bridge is thermodynamic: irreversibly erasing an echo's
+// witness costs energy by Landauer's principle (E = k_B * T * ln N), and that
+// is exactly the Resource[Energy] the language tracks. Keeping the echo is
+// reversible (Bennett): zero cost. See formal/coq/src/EchoThermo.v.
+
+fn main() {
+    println("=== Echo + Landauer: pricing structured loss ===")
+
+    // `collapse` sends every input to the same output: 8 distinct states
+    // would land on one base, losing 3 bits (log2 8).
+    let collapse = |n: Int| 0
+    let e = echo(collapse, 5)
+
+    // Reversible: the echo retains its witness, so nothing is erased.
+    let free: Resource[Energy] = landauer_cost(1, 300.0)
+    println("reversible (echo kept) @300K:", free)
+
+    // Irreversible: erasing a fibre of 8 states costs Landauer energy.
+    let cost: Resource[Energy] = landauer_cost(8, 300.0)
+    println("erase 8 states @300K:", cost)
+
+    // ...but the input is still recoverable from the echo: reversible
+    // representation of an otherwise irreversible computation.
+    println("recovered witness:", echo_witness(e))
+    println("observed base:", echo_base(e))
+}
diff --git a/examples/echo_types.ecl b/examples/echo_types.ecl
new file mode 100644
index 0000000..c05f6f4
--- /dev/null
+++ b/examples/echo_types.ecl
@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: MPL-2.0
+// Echo types: structured loss as a first-class type.
+//
+// An echo of a map `f : A -> B` at an input `x` is the value `echo(f, x)`
+// of type `Echo[A, B]`. It pairs the *retained witness* `x` with the
+// *observed base* `f x`. When `f` collapses several inputs to the same
+// output, their echoes share a base but keep distinct witnesses — loss
+// that is not total erasure. (See THEORY.md §5.5: Echo is a graded
+// comonad of structured loss; `echo_base` is the counit.)
+
+fn main() {
+    println("=== Echo Types: loss that is not erasure ===")
+
+    // `sign` collapses every non-negative input to 1.
+    let sign = |n: Int| if n >= 0 { 1 } else { 0 }
+
+    // Two distinct inputs the function cannot tell apart.
+    let e3: Echo[Int, Int] = echo(sign, 3)
+    let e7: Echo[Int, Int] = echo(sign, 7)
+
+    // The observed bases agree: `f` lost the distinction.
+    println("base(echo(sign, 3)) =", echo_base(e3))
+    println("base(echo(sign, 7)) =", echo_base(e7))
+
+    // But each echo still carries its own witness: the loss is recoverable.
+    println("witness(echo(sign, 3)) =", echo_witness(e3))
+    println("witness(echo(sign, 7)) =", echo_witness(e7))
+
+    // A negative input lands in the other fibre.
+    let em: Echo[Int, Int] = echo(sign, -4)
+    println("base(echo(sign, -4)) =", echo_base(em))
+    println("witness(echo(sign, -4)) =", echo_witness(em))
+}
diff --git a/formal/coq/.gitignore b/formal/coq/.gitignore
index 79e9b51..48cc3fa 100644
--- a/formal/coq/.gitignore
+++ b/formal/coq/.gitignore
@@ -8,6 +8,9 @@
 Makefile.coq
 Makefile.coq.conf
 .Makefile.coq.d
+build.mk
+build.mk.conf
+.build.mk.d
 target/
 node_modules/
 _build/
diff --git a/formal/coq/Makefile b/formal/coq/Makefile
new file mode 100644
index 0000000..5ea03f7
--- /dev/null
+++ b/formal/coq/Makefile
@@ -0,0 +1,28 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
+#
+# Makefile for the Eclexia Coq formal-verification project.
+#
+# The CI workflow (.github/workflows/verify-coq-proofs.yml) invokes a
+# bare `make` in this directory. Coq projects are built by generating a
+# rule file from _CoqProject with `coq_makefile` and then running it;
+# this Makefile wires that two-step process to the default target so a
+# plain `make` builds every file listed in _CoqProject (Syntax.v,
+# Typing.v) under the same loadpath the proofs were checked with.
+#
+# (The repo also ships a Justfile with the same recipe for local use;
+# this Makefile is the make-native entry point CI expects.)
+
+COQMAKEFILE := build.mk
+
+.PHONY: all clean
+
+all: $(COQMAKEFILE)
+	$(MAKE) -f $(COQMAKEFILE)
+
+$(COQMAKEFILE): _CoqProject
+	coq_makefile -f _CoqProject -o $(COQMAKEFILE)
+
+clean:
+	@if [ -f $(COQMAKEFILE) ]; then $(MAKE) -f $(COQMAKEFILE) clean; fi
+	rm -f $(COQMAKEFILE) $(COQMAKEFILE).conf .$(COQMAKEFILE).d
diff --git a/formal/coq/_CoqProject b/formal/coq/_CoqProject
index d24ff39..7185147 100644
--- a/formal/coq/_CoqProject
+++ b/formal/coq/_CoqProject
@@ -10,6 +10,8 @@
 # Source files (in dependency order)
 src/Syntax.v
 src/Typing.v
+src/Echo.v
+src/EchoThermo.v
 # TODO: Add these as they are implemented:
 # src/Semantics.v
 # src/Substitution.v
diff --git a/formal/coq/src/Echo.v b/formal/coq/src/Echo.v
new file mode 100644
index 0000000..0a033a7
--- /dev/null
+++ b/formal/coq/src/Echo.v
@@ -0,0 +1,104 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell *)
+(* Echo types: structured loss as fibres, with the total-space equivalence. *)
+
+(** * Echo types — semantic justification for Eclexia's [Echo[A, B]]
+
+    This module mechanises the load-bearing core of the echo-types
+    development (hyperpolymath/echo-types) that justifies Eclexia's
+    [Echo[A, B]] type former and its [echo] / [echo_witness] / [echo_base]
+    intrinsics (see compiler/eclexia-typeck and compiler/eclexia-interp).
+
+    An echo of a map [f : A -> B] at a base [y] is a fibre element: a
+    retained witness [x : A] together with a proof that [f x = y]. The
+    runtime mirrors this exactly — an echo value pairs the witness with the
+    observed base [f x]. We prove the two properties that make echoes a
+    notion of *structured loss*:
+
+      - structured loss: when [f] collapses distinct inputs to one output,
+        their echoes agree on the observed base but keep distinct
+        witnesses (the distinction [f] erased is recovered);
+
+      - total-space equivalence [A ≃ Σ (y : B), Echo f y]: recording every
+        echo makes an irreversible [f] reversible. This is the echo-types
+        "irreversible computation + echo = reversible representation"
+        keystone (EchoTotalCompletion).
+
+    Everything is constructive and axiom-free; it builds under coqc 8.18. *)
+
+Section Echo.
+
+  Context {A B : Type}.
+  Variable f : A -> B.
+
+  (** An echo of [f] at [y] is the fibre of [f] over [y]. *)
+  Definition Echo (y : B) : Type := { x : A & f x = y }.
+
+  (** Introduction: every input sits in its own fibre, at base [f x]. *)
+  Definition echo_intro (x : A) : Echo (f x) := existT _ x eq_refl.
+
+  (** The retained witness (first projection of the fibre). *)
+  Definition echo_witness {y : B} (e : Echo y) : A := projT1 e.
+
+  (** The observed base of an echo (the fibre index). *)
+  Definition echo_base {y : B} (_ : Echo y) : B := y.
+
+  (** ** Computation / coherence rules (these mirror the interpreter). *)
+
+  (** The witness of an introduced echo is exactly the input. *)
+  Lemma echo_witness_intro : forall x : A, echo_witness (echo_intro x) = x.
+  Proof. intro x. reflexivity. Qed.
+
+  (** The base of an introduced echo is exactly [f x]. *)
+  Lemma echo_base_intro : forall x : A, echo_base (echo_intro x) = f x.
+  Proof. intro x. reflexivity. Qed.
+
+  (** Fibre coherence: applying [f] to the retained witness always recovers
+      the observed base. This is the invariant the runtime maintains by
+      construction (it stores [base = f witness]). *)
+  Lemma echo_base_witness :
+    forall (y : B) (e : Echo y), f (echo_witness e) = echo_base e.
+  Proof. intros y [x p]. exact p. Qed.
+
+  (** ** Structured loss
+
+      If [f] collapses two distinct inputs to the same output, their echoes
+      agree on the observed base yet disagree on the retained witness:
+      loss that is not erasure. *)
+  Theorem echo_structured_loss :
+    forall x1 x2 : A,
+      f x1 = f x2 ->     (* the map collapses them to one base ... *)
+      x1 <> x2 ->        (* ... though they are distinct ... *)
+      echo_base (echo_intro x1) = echo_base (echo_intro x2)        (* bases agree *)
+      /\ echo_witness (echo_intro x1) <> echo_witness (echo_intro x2). (* witnesses differ *)
+  Proof.
+    intros x1 x2 Hbase Hneq. split.
+    - simpl. exact Hbase.
+    - simpl. exact Hneq.
+  Qed.
+
+  (** ** Total-space equivalence : A ≃ Σ (y : B), Echo f y
+
+      Bundling each echo with its base reconstructs the entire domain, so an
+      irreversible [f] becomes reversible once its echoes are recorded. *)
+
+  Definition echo_total_to (x : A) : { y : B & Echo y } :=
+    existT _ (f x) (echo_intro x).
+
+  Definition echo_total_from (p : { y : B & Echo y }) : A :=
+    echo_witness (projT2 p).
+
+  (** One round-trip is definitional. *)
+  Theorem echo_total_from_to :
+    forall x : A, echo_total_from (echo_total_to x) = x.
+  Proof. intro x. reflexivity. Qed.
+
+  (** The other holds by eliminating the fibre's equality proof. *)
+  Theorem echo_total_to_from :
+    forall p : { y : B & Echo y }, echo_total_to (echo_total_from p) = p.
+  Proof.
+    intros [y [x p]]. simpl.
+    destruct p. reflexivity.
+  Qed.
+
+End Echo.
diff --git a/formal/coq/src/EchoThermo.v b/formal/coq/src/EchoThermo.v
new file mode 100644
index 0000000..6fb7702
--- /dev/null
+++ b/formal/coq/src/EchoThermo.v
@@ -0,0 +1,71 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell *)
+(* Landauer / Bennett: the thermodynamic price of erasing an echo's witness. *)
+
+Require Import Coq.Arith.PeanoNat.
+
+(** * Thermodynamic cost of structured loss
+
+    Bridges Echo (formal/coq/src/Echo.v) to Eclexia's energy resource.
+
+    Collapsing a fibre of [n] distinguishable witnesses down to its single
+    observed base erases [log2 n] bits of information. By Landauer's
+    principle that costs at least [k * T * ln 2] of energy per bit — exactly
+    the [Resource[Energy]] that Eclexia prices via the [landauer_cost]
+    intrinsic (compiler/eclexia-typeck, compiler/eclexia-interp). Retaining
+    the echo's witness keeps the computation reversible (Bennett): nothing is
+    erased, so the cost is zero. Information loss thereby enters the resource
+    economy — the graded-comonad-of-loss reading of THEORY.md S5.5.
+
+    This module proves the discrete (bit-count) shadow of that story,
+    axiom-free; the real-valued [k T ln 2] scaling lives in the runtime
+    intrinsic. It mirrors echo-types' EchoThermodynamics (bennett-reversible,
+    landauer-collapse). *)
+
+(** Bits erased when a fibre of [fibre_size] witnesses is collapsed to its
+    single base. (The fibre size is the number of distinct witnesses an echo
+    map sends to one observed output — see Echo.v.) *)
+Definition erasure_bits (fibre_size : nat) : nat := Nat.log2 fibre_size.
+
+(** A collapse is *reversible* exactly when at most one witness reaches the
+    base: there is nothing to erase, and the input is recoverable. *)
+Definition reversible (fibre_size : nat) : Prop := fibre_size <= 1.
+
+(** ** Bennett: a reversible collapse erases no information, so it is free. *)
+Theorem bennett_reversible_is_free :
+  forall n : nat, reversible n -> erasure_bits n = 0.
+Proof.
+  intros n Hrev. unfold erasure_bits, reversible in *.
+  apply Nat.log2_null. exact Hrev.
+Qed.
+
+(** Conversely, the only free collapses are the reversible ones: a strictly
+    collapsing map (two or more witnesses on a base) always has a cost. *)
+Theorem free_iff_reversible :
+  forall n : nat, erasure_bits n = 0 <-> reversible n.
+Proof.
+  intro n. unfold erasure_bits, reversible. apply Nat.log2_null.
+Qed.
+
+(** ** Landauer: any genuine collapse costs at least one bit of erasure. *)
+Theorem irreversible_costs_at_least_one_bit :
+  forall n : nat, 2 <= n -> 1 <= erasure_bits n.
+Proof.
+  intros n Hn. unfold erasure_bits.
+  change 1 with (Nat.log2 2).
+  apply Nat.log2_le_mono. exact Hn.
+Qed.
+
+(** Collapsing a larger fibre never costs less — erasure is monotone in the
+    amount of information discarded. *)
+Theorem erasure_monotone :
+  forall n m : nat, n <= m -> erasure_bits n <= erasure_bits m.
+Proof.
+  intros n m H. unfold erasure_bits. apply Nat.log2_le_mono. exact H.
+Qed.
+
+(** The witness of an echo over a one-element fibre is recoverable from the
+    base, hence reversible and free — the type-level keystone (Echo.v's
+    total-space equivalence) cashed out thermodynamically. *)
+Corollary singleton_echo_is_free : erasure_bits 1 = 0.
+Proof. apply bennett_reversible_is_free. unfold reversible. apply Nat.le_refl. Qed.
diff --git a/formal/coq/src/ShadowPrices.v b/formal/coq/src/ShadowPrices.v
index 0739f1d..9f81e0a 100644
--- a/formal/coq/src/ShadowPrices.v
+++ b/formal/coq/src/ShadowPrices.v
@@ -156,7 +156,7 @@ Definition shadow_price (lp : LinearProgram) (sol : Solution) (i : nat) (lambda
     (A^T λ ≥ c). Then c^T x ≤ (A^T λ)^T x = λ^T (Ax) ≤ λ^T b.
     All three steps are elementwise list operations on (lp_constraints lp).
 
-    Axiomatic: requires list-level dot-product associativity and the matrix
+    Why an axiom: requires list-level dot-product associativity and the matrix
     transpose lemma (A^T λ)^T x = λ^T (Ax). *)
 Axiom weak_duality :
   forall (lp : LinearProgram) (primal_sol : Solution) (dual_sol : DualSolution),
@@ -180,7 +180,7 @@ Axiom weak_duality :
     is ≥ 0 (feasibility: b_i ≥ a_i^T x*, non-negativity: λ*_i ≥ 0), all
     terms must be zero.
 
-    Axiomatic alongside strong_duality: the circular dependency arises because
+    Why an axiom, alongside strong_duality: the circular dependency arises because
     proofs of complementary_slackness typically invoke strong_duality, and the
     standard "constructive" proof of strong_duality uses complementary slackness
     to certify the pivot. We break the cycle by axiomatizing both. *)
@@ -209,7 +209,7 @@ Axiom complementary_slackness :
     dual optimal). The bound Rabs(Δv - λ_i ε) ≤ ε comes from the Lipschitz
     constant of v being bounded by ‖λ*‖_1.
 
-    Axiomatic: requires Coquelicot's real analysis or Mathlib4's
+    Why an axiom: requires Coquelicot's real analysis or Mathlib4's
     LinearProgramming.duality.sensitivity for the Lipschitz / piecewise-linear
     structure proof. *)
 Axiom lp_sensitivity :
@@ -512,7 +512,7 @@ Qed.
     The optimal dual at that basis satisfies strong duality (Theorem 4.4,
     Bertsimas & Tsitsiklis, "Introduction to Linear Optimization", 1997).
 
-    Axiomatic: requires a formalized pivot step, a finite basis enumeration,
+    Why an axiom: requires a formalized pivot step, a finite basis enumeration,
     and the Bland's-rule cycle-prevention argument. None of these are defined
     in this file. The axiom is NOT USED in current theorems — this section
     documents proof debt for future formalization. *)
diff --git a/formal/coq/src/Syntax.v b/formal/coq/src/Syntax.v
index d091c28..39f5a50 100644
--- a/formal/coq/src/Syntax.v
+++ b/formal/coq/src/Syntax.v
@@ -2,11 +2,17 @@
 (** SPDX-License-Identifier: MPL-2.0 *)
 (** SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell *)
 
-From Stdlib Require Import ZArith.ZArith.
-From Stdlib Require Import QArith.QArith.
-From Stdlib Require Import Strings.String.
-From Stdlib Require Import Lists.List.
-From Stdlib Require Import Lia.
+(* NOTE: use the portable bare [Require Import] spelling rather than
+   [From Stdlib Require Import ...]. The [Stdlib] namespace root only
+   exists on newer Coq (the post-8.20 stdlib rename); the CI toolchain
+   pins Coq 8.18.0, where these libraries resolve under the bare /
+   [Coq] root. Bare [Require Import] resolves on 8.18 and remains
+   forward-compatible via the stdlib compatibility aliases. *)
+Require Import ZArith.ZArith.
+Require Import QArith.QArith.
+Require Import Strings.String.
+Require Import Lists.List.
+Require Import Lia.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/formal/coq/src/Typing.v b/formal/coq/src/Typing.v
index 1747539..19787ec 100644
--- a/formal/coq/src/Typing.v
+++ b/formal/coq/src/Typing.v
@@ -4,6 +4,11 @@
 
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
+(* PeanoNat provides the boolean nat comparisons [=?], [<?], [<=?]
+   (Nat.eqb / Nat.ltb / Nat.leb) and their [nat_scope] notations used
+   by the small-step comparison rules below. Without it the comparison
+   notations are unbound on Coq 8.18. *)
+Require Import Coq.Arith.PeanoNat.
 Import ListNotations.
 
 (** * Type System Soundness for Eclexia
@@ -233,7 +238,8 @@ Inductive step : expr -> expr -> Prop :=
   | STBinOpInt : forall op n1 n2 n3,
       (op = OpAdd /\ n3 = n1 + n2) \/
       (op = OpSub /\ n3 = n1 - n2) \/
-      (op = OpMul /\ n3 = n1 * n2) ->
+      (op = OpMul /\ n3 = n1 * n2) \/
+      (op = OpDiv /\ n3 = Nat.div n1 n2) ->
       EBinOp op (EInt n1) (EInt n2) → EInt n3
 
   (* Boolean operations *)
@@ -246,7 +252,7 @@ Inductive step : expr -> expr -> Prop :=
   | STBinOpCmp : forall op n1 n2 b,
       (op = OpEq /\ b = (n1 =? n2)) \/
       (op = OpLt /\ b = (n1 <? n2)) \/
-      (op = OpGt /\ b = (n1 >? n2)) ->
+      (op = OpGt /\ b = (n2 <? n1)) ->
       EBinOp op (EInt n1) (EInt n2) → EBool b
 
   | STBinOpLeft : forall op e1 e1' e2,
@@ -270,25 +276,94 @@ Inductive multi_step : expr -> expr -> Prop :=
 
 Notation "e '→*' e'" := (multi_step e e') (at level 40).
 
-(** ** Weakening Lemma *)
+(** ** Lookup monotonicity under context extension *)
+
+(** If [ctx] is included in [ctx'] as a partial map (every successful
+    lookup in [ctx] agrees in [ctx']), the inclusion is preserved when
+    both contexts are extended with the same binding. This is the one
+    structural fact the weakening induction needs at the binder cases
+    ([TLet_typed], [TFun_typed]). *)
+Lemma lookup_incl_cons : forall x T1 ctx ctx',
+  (forall y S, lookup y ctx = Some S -> lookup y ctx' = Some S) ->
+  (forall y S, lookup y ((x, T1) :: ctx) = Some S ->
+               lookup y ((x, T1) :: ctx') = Some S).
+Proof.
+  intros x T1 ctx ctx' Hincl y S.
+  simpl. destruct (String.eqb y x).
+  - intro H; exact H.
+  - intro H; apply Hincl; exact H.
+Qed.
+
+(** ** General weakening (lookup-monotone)
+
+    Typing is preserved along any partial-map inclusion of contexts,
+    proved by induction on the typing derivation. The original
+    [weakening] lemma below is the special case [ctx = []]. *)
+Lemma weakening_gen : forall ctx e T,
+  ctx ⊢ e ∈ T ->
+  forall ctx',
+    (forall y S, lookup y ctx = Some S -> lookup y ctx' = Some S) ->
+    ctx' ⊢ e ∈ T.
+Proof.
+  intros ctx e T Htyped.
+  induction Htyped; intros ctx' Hincl;
+    eauto 10 using TInt_typed, TFloat_typed, TBool_typed, TVar_typed,
+                   TLet_typed, TFun_typed, TApp_typed, TIf_typed,
+                   TBinOp_Int_typed, TBinOp_Bool_typed, TBinOp_Cmp_typed,
+                   TDimLit_typed, lookup_incl_cons.
+Qed.
 
+(** ** Weakening Lemma
+
+    A term typeable in the empty context is typeable in any context.
+    The [value e] hypothesis is retained for backward compatibility
+    with existing callers; the result in fact holds for every term
+    typeable in [[]], because the empty context is vacuously included
+    in every context. The previous proof discharged the function-value
+    case with a bare [assumption], which cannot succeed: a closed
+    function's body is typed under [(x,T1)::[]] but weakening demands
+    it under [(x,T1)::ctx]. [weakening_gen] supplies exactly that. *)
 Lemma weakening : forall ctx e T,
   [] ⊢ e ∈ T ->
   value e ->
   ctx ⊢ e ∈ T.
 Proof.
-  intros ctx e T Htyped Hval.
-  inversion Hval; subst; inversion Htyped; subst.
-  - (* VInt *)
-    apply TInt_typed.
-  - (* VFloat *)
-    apply TFloat_typed.
-  - (* VBool *)
-    apply TBool_typed.
-  - (* VFun *)
-    apply TFun_typed. assumption.
-  - (* VDimLit *)
-    apply TDimLit_typed.
+  intros ctx e T Htyped _.
+  apply (weakening_gen [] e T Htyped).
+  intros y S Hlook. simpl in Hlook. discriminate.
+Qed.
+
+(** ** Context exchange and shadowing (corollaries of [weakening_gen])
+
+    These are the structural facts the substitution lemma needs at the
+    binder cases. Both are instances of [weakening_gen]: two contexts
+    that agree as partial maps type the same terms. *)
+
+(** Two adjacent bindings with distinct keys may be swapped. *)
+Lemma context_exchange : forall x1 T1' x2 T2' ctx e T,
+  x1 <> x2 ->
+  ((x1, T1') :: (x2, T2') :: ctx) ⊢ e ∈ T ->
+  ((x2, T2') :: (x1, T1') :: ctx) ⊢ e ∈ T.
+Proof.
+  intros x1 T1' x2 T2' ctx e T Hne H.
+  apply (weakening_gen _ _ _ H).
+  intros y S. simpl.
+  destruct (String.eqb y x1) eqn:E1; destruct (String.eqb y x2) eqn:E2;
+    intro HL; try exact HL.
+  exfalso. apply Hne.
+  apply String.eqb_eq in E1. apply String.eqb_eq in E2. congruence.
+Qed.
+
+(** An inner binding shadowed by a later one with the same key is
+    redundant and may be dropped. *)
+Lemma context_shadow : forall x T1' T2' ctx e T,
+  ((x, T1') :: (x, T2') :: ctx) ⊢ e ∈ T ->
+  ((x, T1') :: ctx) ⊢ e ∈ T.
+Proof.
+  intros x T1' T2' ctx e T H.
+  apply (weakening_gen _ _ _ H).
+  intros y S. simpl.
+  destruct (String.eqb y x) eqn:E; intro HL; exact HL.
 Qed.
 
 (** ** Substitution Lemma *)
@@ -310,28 +385,41 @@ Proof.
   - (* EBool *)
     apply TBool_typed.
   - (* EVar *)
-    unfold lookup in H1. simpl in H1.
+    (* [lookup] compares [String.eqb s x] but [subst] compares
+       [String.eqb x s]; reconcile the two orders with [eqb_sym] so a
+       single case split decides both the goal and the hypothesis. *)
+    simpl in H1. rewrite String.eqb_sym in H1.
     destruct (String.eqb x s) eqn:Heq.
-    + (* x = s: substitute *)
-      injection H1 as H1. subst.
-      (* Apply weakening lemma: value well-typed in [] is well-typed in any context *)
+    + (* x = s: the variable is the one being substituted *)
+      injection H1 as H1. subst T2.
       apply (weakening ctx v T1 Hv Hval).
-    + (* x <> s: keep variable *)
-      apply TVar_typed. assumption.
+    + (* x <> s: the variable is preserved *)
+      apply TVar_typed. exact H1.
   - (* ELet *)
-    apply TLet_typed.
-    + apply IHe1. assumption.
-    + destruct (String.eqb x s) eqn:Heq.
-      * (* x = s: shadowed, e2 keeps original typing *)
-        assumption.
-      * (* x <> s: substitute in e2 *)
-        apply IHe2. assumption.
+    (* [TLet_typed]'s intermediate type is not in its conclusion, so we
+       use [eapply ...; [ .. | .. ]] to share the resulting existential
+       between the two premises rather than shelving it. *)
+    destruct (String.eqb x s) eqn:Heq.
+    + (* x = s: the let-binder shadows x, so e2 is not substituted *)
+      apply String.eqb_eq in Heq. subst s.
+      eapply TLet_typed;
+        [ apply IHe1; eassumption
+        | eapply context_shadow; eassumption ].
+    + (* x <> s: substitute into e2 under the swapped binder *)
+      eapply TLet_typed;
+        [ apply IHe1; eassumption
+        | apply IHe2; apply context_exchange;
+            [ apply String.eqb_neq in Heq; intro Hc; apply Heq; symmetry; exact Hc
+            | eassumption ] ].
   - (* EFun *)
     destruct (String.eqb x s) eqn:Heq.
-    + (* x = s: parameter shadows, no substitution *)
-      apply TFun_typed. assumption.
-    + (* x <> s: substitute in body *)
-      apply TFun_typed. apply IHe. assumption.
+    + (* x = s: parameter shadows x, no substitution in the body *)
+      apply String.eqb_eq in Heq. subst s.
+      apply TFun_typed. eapply context_shadow. eassumption.
+    + (* x <> s: substitute into the body under the swapped binder *)
+      apply TFun_typed. apply IHe. apply context_exchange.
+      * apply String.eqb_neq in Heq. intro Hc. apply Heq. symmetry. exact Hc.
+      * eassumption.
   - (* EApp *)
     eapply TApp_typed.
     + apply IHe1. eassumption.
@@ -351,6 +439,31 @@ Proof.
     apply TDimLit_typed.
 Qed.
 
+(** ** Canonical forms
+
+    A value of a given type has the expected head shape. These three
+    lemmas drive the value cases of [progress]: each inverts the value
+    and then the typing derivation, so the constructors that disagree
+    with the type are discharged automatically. *)
+Lemma canonical_forms_bool : forall ctx e,
+  ctx ⊢ e ∈ TBool -> value e -> exists b, e = EBool b.
+Proof.
+  intros ctx e HT Hv. inversion Hv; subst; inversion HT; subst; eexists; reflexivity.
+Qed.
+
+Lemma canonical_forms_int : forall ctx e,
+  ctx ⊢ e ∈ TInt -> value e -> exists n, e = EInt n.
+Proof.
+  intros ctx e HT Hv. inversion Hv; subst; inversion HT; subst; eexists; reflexivity.
+Qed.
+
+Lemma canonical_forms_fun : forall ctx e T1 T2,
+  ctx ⊢ e ∈ TFun T1 T2 -> value e -> exists x body, e = EFun x T1 body.
+Proof.
+  intros ctx e T1 T2 HT Hv.
+  inversion Hv; subst; inversion HT; subst; eexists; eexists; reflexivity.
+Qed.
+
 (** ** Type Soundness *)
 
 (** Progress: Well-typed expressions either are values or can step *)
@@ -376,10 +489,12 @@ Proof.
     destruct IHHtyped1 as [Hval1 | [e1' Hstep1]]; auto.
     + (* e1 is value *)
       destruct IHHtyped2 as [Hval2 | [e2' Hstep2]]; auto.
-      * (* e2 is value *)
-        (* e1 must be function *)
-        inversion Hval1; subst.
-        exists (subst x e2 e). apply STApp. assumption.
+      * (* e2 is value: e1 is a function by canonical forms *)
+        match goal with
+        | [ HT : _ ⊢ e1 ∈ TFun _ _ |- _ ] =>
+            destruct (canonical_forms_fun _ _ _ _ HT Hval1) as [y [body Hb]]
+        end. subst e1.
+        eexists. apply STApp. assumption.
       * (* e2 steps *)
         exists (EApp e1 e2'). apply STAppArg; assumption.
     + (* e1 steps *)
@@ -387,8 +502,11 @@ Proof.
   - (* TIf *)
     right.
     destruct IHHtyped1 as [Hval1 | [e1' Hstep1]]; auto.
-    + (* e1 is value *)
-      inversion Hval1; subst.
+    + (* e1 is value: it is a boolean by canonical forms *)
+      match goal with
+      | [ HT : _ ⊢ e1 ∈ TBool |- _ ] =>
+          destruct (canonical_forms_bool _ _ HT Hval1) as [b Hb]
+      end. subst e1.
       destruct b.
       * exists e2. apply STIfTrue.
       * exists e3. apply STIfFalse.
@@ -398,14 +516,20 @@ Proof.
     right.
     destruct IHHtyped1 as [Hval1 | [e1' Hstep1]]; auto.
     + destruct IHHtyped2 as [Hval2 | [e2' Hstep2]]; auto.
-      * (* Both values *)
-        inversion Hval1; subst.
-        inversion Hval2; subst.
+      * (* Both values: both integers by canonical forms *)
+        match goal with
+        | [ HT : _ ⊢ e1 ∈ TInt |- _ ] =>
+            destruct (canonical_forms_int _ _ HT Hval1) as [n Hn1]
+        end. subst e1.
+        match goal with
+        | [ HT : _ ⊢ e2 ∈ TInt |- _ ] =>
+            destruct (canonical_forms_int _ _ HT Hval2) as [n0 Hn2]
+        end. subst e2.
         destruct H as [HAdd | [HSub | [HMul | HDiv]]]; subst.
         { exists (EInt (n + n0)). apply STBinOpInt. left. split; reflexivity. }
         { exists (EInt (n - n0)). apply STBinOpInt. right. left. split; reflexivity. }
         { exists (EInt (n * n0)). apply STBinOpInt. right. right. left. split; reflexivity. }
-        { contradiction. }
+        { exists (EInt (Nat.div n n0)). apply STBinOpInt. right. right. right. split; reflexivity. }
       * (* e2 steps *)
         exists (EBinOp op e1 e2'). apply STBinOpRight; assumption.
     + (* e1 steps *)
@@ -414,9 +538,15 @@ Proof.
     right.
     destruct IHHtyped1 as [Hval1 | [e1' Hstep1]]; auto.
     + destruct IHHtyped2 as [Hval2 | [e2' Hstep2]]; auto.
-      * (* Both values *)
-        inversion Hval1; subst.
-        inversion Hval2; subst.
+      * (* Both values: both booleans by canonical forms *)
+        match goal with
+        | [ HT : _ ⊢ e1 ∈ TBool |- _ ] =>
+            destruct (canonical_forms_bool _ _ HT Hval1) as [b Hb1]
+        end. subst e1.
+        match goal with
+        | [ HT : _ ⊢ e2 ∈ TBool |- _ ] =>
+            destruct (canonical_forms_bool _ _ HT Hval2) as [b0 Hb2]
+        end. subst e2.
         destruct H as [HAnd | HOr]; subst.
         { exists (EBool (andb b b0)). apply STBinOpBool. left. split; reflexivity. }
         { exists (EBool (orb b b0)). apply STBinOpBool. right. split; reflexivity. }
@@ -426,13 +556,19 @@ Proof.
     right.
     destruct IHHtyped1 as [Hval1 | [e1' Hstep1]]; auto.
     + destruct IHHtyped2 as [Hval2 | [e2' Hstep2]]; auto.
-      * (* Both values *)
-        inversion Hval1; subst.
-        inversion Hval2; subst.
+      * (* Both values: both integers by canonical forms *)
+        match goal with
+        | [ HT : _ ⊢ e1 ∈ TInt |- _ ] =>
+            destruct (canonical_forms_int _ _ HT Hval1) as [n Hn1]
+        end. subst e1.
+        match goal with
+        | [ HT : _ ⊢ e2 ∈ TInt |- _ ] =>
+            destruct (canonical_forms_int _ _ HT Hval2) as [n0 Hn2]
+        end. subst e2.
         destruct H as [HEq | [HLt | HGt]]; subst.
         { exists (EBool (n =? n0)). apply STBinOpCmp. left. split; reflexivity. }
         { exists (EBool (n <? n0)). apply STBinOpCmp. right. left. split; reflexivity. }
-        { exists (EBool (n >? n0)). apply STBinOpCmp. right. right. split; reflexivity. }
+        { exists (EBool (n0 <? n)). apply STBinOpCmp. right. right. split; reflexivity. }
       * exists (EBinOp op e1 e2'). apply STBinOpRight; assumption.
     + exists (EBinOp op e1' e2). apply STBinOpLeft. assumption.
   - (* TDimLit *)
@@ -445,63 +581,58 @@ Theorem preservation : forall e e' T,
   e → e' ->
   [] ⊢ e' ∈ T.
 Proof.
-  intros e e' T Htyped Hstep.
-  generalize dependent e'.
-  remember [] as ctx.
-  induction Htyped; intros e' Hstep; subst; inversion Hstep; subst.
-  - (* Impossible: values don't step *)
-    inversion H1.
-  - (* Impossible *)
-    inversion H1.
-  - (* Impossible *)
-    inversion H1.
-  - (* TLet STLet *)
-    eapply subst_preserves_typing; eauto.
-  - (* TLet STLetStep *)
-    apply TLet_typed.
-    + apply IHHtyped1. assumption. reflexivity.
-    + assumption.
-  - (* Impossible *)
-    inversion H1.
-  - (* TApp STApp *)
-    eapply subst_preserves_typing; eauto.
-  - (* TApp STAppFun *)
-    apply TApp_typed with (T1 := T1).
-    + apply IHHtyped1. assumption. reflexivity.
-    + assumption.
-  - (* TApp STAppArg *)
-    apply TApp_typed with (T1 := T1).
-    + assumption.
-    + apply IHHtyped2. assumption. reflexivity.
-  - (* TIf STIfTrue *)
-    assumption.
-  - (* TIf STIfFalse *)
-    assumption.
-  - (* TIf STIfStep *)
-    apply TIf_typed.
-    + apply IHHtyped1. assumption. reflexivity.
-    + assumption.
-    + assumption.
-  - (* TBinOp Int — STBinOpInt: result is EInt n3 *)
-    apply TBinOp_Int_typed with (op := op); auto.
-  - (* TBinOp Int — STBinOpLeft: e1 steps *)
-    eapply TBinOp_Int_typed; eauto.
-  - (* TBinOp Int — STBinOpRight: e2 steps *)
-    eapply TBinOp_Int_typed; eauto.
-  - (* Impossible: TBinOp Bool values don't reduce via STBinOpInt *)
-    destruct H as [HA | [HB | HC]]; subst; discriminate.
-  - (* TBinOp Bool — STBinOpLeft *)
-    eapply TBinOp_Bool_typed; eauto.
-  - (* TBinOp Bool — STBinOpRight *)
-    eapply TBinOp_Bool_typed; eauto.
-  - (* Impossible: TBinOp Cmp (OpEq/OpLt/OpGt) doesn't reduce via STBinOpInt (OpAdd/OpSub/OpMul) *)
-    destruct H as [HEq | [HLt | HGt]]; destruct H0 as [[HA _] | [[HB _] | [HC _]]]; subst; discriminate.
-  - (* TBinOp Cmp — STBinOpLeft *)
-    eapply TBinOp_Cmp_typed; eauto.
-  - (* TBinOp Cmp — STBinOpRight *)
-    eapply TBinOp_Cmp_typed; eauto.
-  - (* Impossible *)
-    inversion H3.
+  (* Induction on the step relation. The step's shape pins the redex,
+     [inversion Htyped] recovers the typing premises, and the residual
+     goals are discharged uniformly:
+       - if-true/false: the taken branch's typing hypothesis;
+       - beta (application): invert the function's typing, then the
+         substitution lemma;
+       - let: the substitution lemma directly;
+       - congruence: the matching typing constructor + the IH (found by
+         [eauto] over all constructors, which also re-types literal
+         results such as [EInt n3 : TInt]);
+       - spurious binop typing subcases ([inversion Htyped] offers an
+         Int/Bool/Cmp reading for every [EBinOp]): a literal cannot have
+         the wrong base type, and the operator tag sets are disjoint. *)
+  intros e e' T Htyped Hstep. generalize dependent T.
+  (* [Tres] avoids a name clash with the [T] bound by step constructors
+     such as [STApp] (the function's domain annotation). *)
+  induction Hstep; intros Tres Htyped; inversion Htyped; subst;
+    try (solve [assumption]);
+    try (solve [ match goal with
+                 | [ Hf : _ ⊢ EFun _ _ _ ∈ _ |- _ ] => inversion Hf; subst
+                 end;
+                 eapply subst_preserves_typing; eauto ]);
+    try (solve [eapply subst_preserves_typing; eauto]);
+    try (solve [eauto 8 using TInt_typed, TFloat_typed, TBool_typed,
+                  TVar_typed, TLet_typed, TFun_typed, TApp_typed, TIf_typed,
+                  TBinOp_Int_typed, TBinOp_Bool_typed, TBinOp_Cmp_typed,
+                  TDimLit_typed]);
+    try (solve [ exfalso;
+                 repeat match goal with
+                        | [ H : _ ⊢ EInt _ ∈ TBool |- _ ] => inversion H
+                        | [ H : _ ⊢ EBool _ ∈ TInt |- _ ] => inversion H
+                        | [ H : _ ⊢ EInt _ ∈ TFun _ _ |- _ ] => inversion H
+                        | [ H : _ ⊢ EBool _ ∈ TFun _ _ |- _ ] => inversion H
+                        | [ H : _ \/ _ |- _ ] => destruct H
+                        | [ H : _ /\ _ |- _ ] => destruct H
+                        end;
+                 subst; discriminate ]).
+Qed.
+
+(** Preservation lifts to the reflexive-transitive closure. Stated as
+    its own lemma so the typing hypothesis is generalised correctly
+    across the [multi_step] induction (inducting on [Hmulti] with the
+    typing left in the context would silently fix the start term). *)
+Lemma multi_preservation : forall e e' T,
+  [] ⊢ e ∈ T ->
+  e →* e' ->
+  [] ⊢ e' ∈ T.
+Proof.
+  intros e e' T Htyped Hmulti. revert T Htyped.
+  induction Hmulti as [e | e1 e2 e3 Hstep Hmulti IH]; intros T Htyped.
+  - assumption.
+  - apply IH. eapply preservation; eauto.
 Qed.
 
 (** ** Type Soundness (Combined) *)
@@ -513,34 +644,26 @@ Theorem soundness : forall e e' T,
   value e' \/ exists e'', e' → e''.
 Proof.
   intros e e' T Htyped Hmulti.
-  induction Hmulti.
-  - (* Base case: e → e *)
-    apply progress. assumption.
-  - (* Inductive case *)
-    assert ([] ⊢ e2 ∈ T).
-    { eapply preservation; eauto. }
-    apply IHHmulti. assumption.
+  apply (progress e' T).
+  eapply multi_preservation; eauto.
 Qed.
 
 (** ** Dimensional Type Safety *)
 
 (** Dimension errors cannot occur at runtime *)
-Theorem dimensional_safety : forall e T d,
+Theorem dimensional_safety : forall e d,
   [] ⊢ e ∈ TDimensional d ->
   forall e', e →* e' -> value e' ->
   exists n, e' = EDimLit n d.
 Proof.
-  intros e T d Htyped e' Hmulti Hval.
-  (* By soundness, e' is well-typed with type TDimensional d *)
-  assert (Htyped' : [] ⊢ e' ∈ TDimensional d).
-  { clear Hval.
-    induction Hmulti.
-    - assumption.
-    - apply IHHmulti. eapply preservation; eauto.
-  }
-  (* A value of type TDimensional d must be EDimLit n d *)
+  intros e d Htyped e' Hmulti Hval.
+  (* Typing is preserved along the reduction, so e' still has type
+     TDimensional d; a value of that type must be a dimensioned
+     literal with the same dimension. *)
+  assert (Htyped' : [] ⊢ e' ∈ TDimensional d)
+    by (eapply multi_preservation; eauto).
   inversion Hval; subst; inversion Htyped'; subst.
-  exists n. reflexivity.
+  eexists. reflexivity.
 Qed.
 
 (** ** Summary *)
diff --git a/tests/conformance/invalid/echo_type_mismatch.ecl b/tests/conformance/invalid/echo_type_mismatch.ecl
new file mode 100644
index 0000000..97275a4
--- /dev/null
+++ b/tests/conformance/invalid/echo_type_mismatch.ecl
@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: MPL-2.0
+// Invalid: echo_witness requires an Echo[A, B], not an Int.
+//
+// This must fail type checking — it exercises that Echo is a real type in
+// the checker (unified structurally), not an ignored annotation.
+
+fn main() {
+    let bad = echo_witness(42)
+    println(bad)
+}
diff --git a/tests/conformance/invalid/toplevel_enum.ecl b/tests/conformance/invalid/toplevel_enum.ecl
new file mode 100644
index 0000000..18b1793
--- /dev/null
+++ b/tests/conformance/invalid/toplevel_enum.ecl
@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MPL-2.0
+// Invalid: `enum` is not a supported top-level item shorthand (use `type`).
+//
+// Regression for a parser error-recovery infinite loop (found by fuzzing):
+// `enum` is a recovery stop-token but `parse_item` rejects it, which used to
+// spin forever accumulating errors until OOM. This must now fail fast with a
+// parse error rather than hang.
+
+enum Foo {}
diff --git a/tests/conformance/valid/echo_landauer.ecl b/tests/conformance/valid/echo_landauer.ecl
new file mode 100644
index 0000000..b922039
--- /dev/null
+++ b/tests/conformance/valid/echo_landauer.ecl
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MPL-2.0
+// Valid: Echo's structured loss priced via Landauer; the type checker
+// accepts landauer_cost(...) as a Resource[Energy], and a retained echo
+// witness is recoverable (reversible representation).
+
+fn main() {
+    let collapse = |n: Int| 0
+    let e: Echo[Int, Int] = echo(collapse, 5)
+
+    // Reversible retention costs nothing; collapsing a fibre costs energy.
+    let _free: Resource[Energy] = landauer_cost(1, 300.0)
+    let _cost: Resource[Energy] = landauer_cost(8, 300.0)
+
+    // The witness survives in the echo.
+    assert(echo_witness(e) == 5)
+    assert(echo_base(e) == 0)
+
+    println("echo + landauer: ok")
+}
diff --git a/tests/conformance/valid/echo_structured_loss.ecl b/tests/conformance/valid/echo_structured_loss.ecl
new file mode 100644
index 0000000..c8c9485
--- /dev/null
+++ b/tests/conformance/valid/echo_structured_loss.ecl
@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: MPL-2.0
+// Valid: echo types retain witnesses across a collapsing map.
+//
+// `constant` maps every input to 0, so distinct inputs share a base, yet
+// their echoes keep distinct witnesses — structured loss, not erasure.
+
+fn main() {
+    let constant = |n: Int| 0
+
+    let a: Echo[Int, Int] = echo(constant, 11)
+    let b: Echo[Int, Int] = echo(constant, 22)
+
+    // The map collapses both inputs to the same observed base.
+    assert(echo_base(a) == 0)
+    assert(echo_base(b) == 0)
+    assert(echo_base(a) == echo_base(b))
+
+    // But each echo retains its own witness.
+    assert(echo_witness(a) == 11)
+    assert(echo_witness(b) == 22)
+
+    println("echo structured-loss: ok")
+}