proof(L2.A): modality scaffolding + has_type_l1 m-index + linear_to_affine Qed

Closes 3 of 3 success criteria for L2 in TypingL1.v:

1. Mode datatype + thin poset (modality, le_mod with 3 ctors, join_mod)
   plus 6 lemmas: refl, trans, prop, join_left, join_right, join_univ.
   Mirrors echo-types/proofs/agda/EchoLinear.agda:30-101.

2. has_type_l1 refactored to take m : modality as first parameter.
   Notation R ; G |=L1[m] e : T -| R' ; G'.

   - 23 modality-polymorphic constructors (values, vars, strings,
     let/letlin, app, products, sums, regions, borrow, drop, copy)
     just thread m through to recursive premises.
   - 3 rules SPLIT per mode:
       T_Lam_L1_Linear  : body ends at (T1, true) :: G (obligation)
       T_Lam_L1_Affine  : body ends at (T1, u) :: G for any u : bool
       T_Case_L1_{Linear,Affine} : Linear requires branch agreement;
         Affine allows per-branch binding-flag disagreement
       T_If_L1_{Linear,Affine}   : symmetry placeholder (Linear has
         existing branch-agreement; Affine separates for future
         per-branch G' relaxation in L2-β)
   - 1 new Affine-only structural rule:
       T_Forget_Affine_L1 : unused linear binding may persist past e
         in Affine mode (the "implicit drop" relaxation).

   T_Drop_L1 remains modality-polymorphic with output TBase TUnit
   marked as residue placeholder; full residue mechanisation is L3
   (PRESERVATION-DESIGN.md §6).

3. linear_to_affine : has_type_l1 Linear ... -> has_type_l1 Affine ...
   Qed via `remember Linear as m; induction; try discriminate;
   try (econstructor; eauto; fail)`. Closed under the global context
   (no axioms, no admits). Mirror of EchoLinear.agda:38-58 [weaken].

Disambiguation: this is L2 of ephapax's internal four-layer redesign.
ephapax-affine != AffineScript (separate project; shares only the
typed-wasm target). See PRESERVATION-DESIGN.md §5.

This commit only touches TypingL1.v and builds clean for that file
in isolation. Downstream Semantics_L1.v + Counterexample.v not yet
updated to the new 7-arg has_type_l1 signature; full build will be
restored in follow-up commits L2.B (preservation_l1 re-statement)
and L2.C (supporting-lemma mode threading).

Refs: PRESERVATION-DESIGN.md §5; EchoLinear.agda:30-101;
feedback_affinescript_ephapax_siblings_not_impl_proof.

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

Author: hyperpolymath