proof(L2): complete L2-modality migration of L1 preservation development

The L2-modality commit (4e87a05) added the `modality` index to
`has_type_l1` and split Lam/Case/If into `_Linear`/`_Affine` variants in
TypingL1.v, but never migrated Semantics_L1.v — leaving the entire
1515-line L1 preservation development (and Counterexample.v) broken.
This completes that migration so the development compiles again.

TypingL1.v:
- Replace the free-floating `T_Forget_Affine_L1` rule (which prepended an
  extra binding to the output context, falsifying
  `typing_preserves_length_l1` and `value_R_G_preserving_l1`) with proper
  per-binder mode splits: `T_Let_L1_Linear`/`_Affine` and
  `T_LetLin_L1_Linear`/`_Affine`, mirroring the existing Lam/Case
  treatment. Affine variants relax the bound-var output flag to any `u`
  (the affine "implicit drop"); all rules stay length-preserving.

Semantics_L1.v:
- Quantify every lemma over an explicit modality `m` (a Section variable
  fails: `induction Htype` generalises the index, severing
  cross-references to other m-dependent lemmas).
- Make the structural lemmas case-count-robust.
- Thread `m` and the mode-split through region-shrink, shift, subst, and
  the 33-case preservation dispatch (econstructor auto-selects the mode
  variant in congruence-step cases).
- The 4 affine-β subcases (Let/LetLin-Val, Case-Inl/Inr) are admitted with
  documentation: they need a generalised affine substitution lemma,
  tracked as L2 follow-up — distinct from the pre-existing linear
  App/Pair/region-liveness soundness gaps.

Counterexample.v:
- `bad_input_untypable_l1` / `t_loc_l1_R_preserving` now quantify over `m`:
  the bad input is untypable in every modality.

Full development builds clean from scratch (coqc 8.18, all 6 modules).
Legacy `Semantics.v` untouched.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

formal/Counterexample.v

@@ -164,30 +164,31 @@ Section L1Fix.
   (** Helper: T_Loc_L1 has [R_out = R_in], [G_out = G_in]. By inversion. *)
 
   Lemma t_loc_l1_R_preserving :
-    forall R G l r R' G' T,
-      has_type_l1 R G (ELoc l r) T R' G' ->
+    forall m R G l r R' G' T,
+      has_type_l1 m R G (ELoc l r) T R' G' ->
       R' = R /\ G' = G.
   Proof.
-    intros R G l r R' G' T H.
+    intros m R G l r R' G' T H.
     inversion H; subst; split; reflexivity.
   Qed.
 
-  (** The L1 regression theorem. *)
+  (** The L1 regression theorem: the bad input is untypable in EVERY
+      modality (linear and affine alike). *)
   Lemma bad_input_untypable_l1 :
-    forall R_out G_out,
-      ~ has_type_l1 (r0 :: r1 :: nil) nil e_bad T_bad R_out G_out.
+    forall m R_out G_out,
+      ~ has_type_l1 m (r0 :: r1 :: nil) nil e_bad T_bad R_out G_out.
   Proof.
-    intros R_out G_out Htype.
+    intros m R_out G_out Htype.
     unfold e_bad, T_bad in Htype.
     (* Invert T_Pair_L1; only rule matching EPair. *)
     inversion Htype; subst.
     (* Hte1 = typing of (ERegion r1 (ELoc l0 r0)); Hte2 = typing of (ELoc l1 r1). *)
     match goal with
-    | [ H : has_type_l1 _ _ (ERegion r1 (ELoc l0 r0)) _ ?R1 _ |- _ ] =>
+    | [ H : has_type_l1 _ _ _ (ERegion r1 (ELoc l0 r0)) _ ?R1 _ |- _ ] =>
         rename H into Hte1; rename R1 into R1_e1
     end.
     match goal with
-    | [ H : has_type_l1 _ _ (ELoc l1 r1) _ _ _ |- _ ] =>
+    | [ H : has_type_l1 _ _ _ (ELoc l1 r1) _ _ _ |- _ ] =>
         rename H into Hte2
     end.
     (* From Hte2 = T_Loc_L1: In r1 R1_e1. *)
@@ -204,7 +205,7 @@ Section L1Fix.
     - (* T_Region_Active_L1: body ([ELoc l0 r0]) is a value; t_loc_l1_R_preserving
          gives body's R_out = R_in = [r0; r1].  Hence R1_e1 = remove_first_L1 r1 [r0; r1]. *)
       match goal with
-      | [ Hbody : has_type_l1 _ _ (ELoc _ _) _ ?Rbody _ |- _ ] =>
+      | [ Hbody : has_type_l1 _ _ _ (ELoc _ _) _ ?Rbody _ |- _ ] =>
           assert (HRb : Rbody = r0 :: r1 :: nil)
             by (eapply t_loc_l1_R_preserving; eassumption)
       end.