syntax(L2 Phase 2 / Phase D slice 1): add TFunEff effect-typed function constructor (#200)

## Summary
- Adds `TFunEff T1 T2 R_in R_out` to `ty` in `Syntax.v`, paralleling the
existing `TFun T1 T2` (which is preserved per CLAUDE.md owner directive
— the legacy `TFun` + `preservation`'s falsity is load-bearing for
`Counterexample.v`).
- `TFunEff` exposes a lambda body's R-flow at the type level: required
for closing the lambda-rigidity admit at `Semantics_L1.v:1694` and
naturally unblocking the deferred Phase B Slice 1 + Phase C work.
- Slice 1 of 4 — syntax-only landable shape, mirrors L3 wiring slice 1 +
Phase A's docs-only PR #197.

## What changed
- `Syntax.v` — `TFunEff : ty -> ty -> list region_name -> list
region_name -> ty` constructor.
- `Typing.v` `free_regions` — extends fixpoint with TFunEff case (union
of argument/return free regions + R_in + R_out).
- `is_linear_ty` (catch-all `_ => false`) — automatically false for
TFunEff. No change needed.

## What's NOT in this PR
- Typing rules `T_Lam_L1_*_Eff` / `T_App_L1_Eff` → slice 2
- Preservation closure for lambda-rigidity → slice 3
- Phase B + Phase C re-attempt → slice 4

## Test plan
- [x] `coqc 8.18.0` clean rebuild — 10/10 .v files Qed (no proof
regressions)
- [x] Zero new Admitted / Axiom (per CLAUDE.md directive)
- [x] No legacy Semantics.v / Typing.v judgment patching (only fixpoint
extended for new case)
- [ ] Slice 2 to follow once this lands

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

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

formal/Syntax.v

@@ -60,7 +60,28 @@ Inductive ty : Type :=
       Observation discipline is modality-dispatched at the typing-
       rule boundary, not encoded in the type — see
       [formal/PRESERVATION-DESIGN.md §6.3] and [formal/Echo.v]. *)
-  | TEcho   : ty -> ty.
+  | TEcho   : ty -> ty
+
+  (** L2 Phase 2 / Phase D slice 1 — Effect-typed function former.
+      [TFunEff T1 T2 R_in R_out] is the type of a function from [T1]
+      to [T2] whose body requires the region environment [R_in] on
+      entry and produces [R_out] on exit. The legacy [TFun T1 T2] is
+      preserved (per CLAUDE.md owner directive 2026-05-27 — its
+      falsity in conjunction with `preservation` is load-bearing for
+      `Counterexample.v`); new code uses [TFunEff] to expose lambda
+      bodies' R-flow at the type level.
+
+      Closes the structural-blocker root cause: at function-call
+      sites, the body's region requirements become visible to
+      preservation reasoning, unblocking the lambda-rigidity admit
+      at `Semantics_L1.v:1694` and naturally enabling
+      body-input-shrinkage for the Phase C list-vs-multiset bridge.
+
+      Slice 1 (this PR): syntax-only landing. Typing rules
+      (`T_Lam_L1_*_Eff` + `T_App_L1_Eff`) ship in slice 2. Per the
+      L3 wiring playbook (slices 1→4) this is the lightest landable
+      shape. *)
+  | TFunEff : ty -> ty -> list region_name -> list region_name -> ty.
 
 (** ** Expressions *)
 

formal/Typing.v

@@ -54,15 +54,20 @@ From Ephapax Require Import Syntax.
 
 Fixpoint free_regions (T : ty) : list region_name :=
   match T with
-  | TBase _          => []
-  | TString r        => [r]
-  | TRef _ T'        => free_regions T'
-  | TFun T1 T2       => free_regions T1 ++ free_regions T2
-  | TProd T1 T2      => free_regions T1 ++ free_regions T2
-  | TSum T1 T2       => free_regions T1 ++ free_regions T2
-  | TRegion r T'     => r :: free_regions T'
-  | TBorrow T'       => free_regions T'
-  | TEcho T'         => free_regions T'
+  | TBase _                  => []
+  | TString r                => [r]
+  | TRef _ T'                => free_regions T'
+  | TFun T1 T2               => free_regions T1 ++ free_regions T2
+  | TProd T1 T2              => free_regions T1 ++ free_regions T2
+  | TSum T1 T2               => free_regions T1 ++ free_regions T2
+  | TRegion r T'             => r :: free_regions T'
+  | TBorrow T'               => free_regions T'
+  | TEcho T'                 => free_regions T'
+  | TFunEff T1 T2 R_in R_out =>
+      (** Phase D slice 1: free regions of [TFunEff] include those of
+          the argument and return types AND the input/output region
+          environments that annotate the body's R-flow. *)
+      free_regions T1 ++ free_regions T2 ++ R_in ++ R_out
   end.
 
 (* Note: We don't need a separate determinism lemma for free_regions