proof(L2): complete L2-modality migration of L1 preservation (Stage A); soundness fix to follow (#294)

## Summary

Completes the **L2-modality migration** of the L1 preservation
development so the Coq formalisation compiles again, and replaces a
**malformed scaffolding rule** discovered en route. This is **Stage A**
of the soundness work; the calculus-level soundness fix (App/Pair gaps +
the false `region_liveness_at_split_l1` axiom) is **Stage B**,
intentionally separated for review (see *Next* below).

## Background

Commit `4e87a05` (`proof/l2-modality`) 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` (the
1515-line preservation development) or `Counterexample.v`. The whole
`formal/` build was broken on that branch.

## Changes

**`TypingL1.v` — replace the malformed `T_Forget_Affine_L1`:**
- The committed `T_Forget_Affine_L1` prepended an extra binding to the
output context, **provably falsifying** `typing_preserves_length_l1` and
`value_R_G_preserving_l1` (e.g. `EUnit` typed with output context one
longer than input).
- Replaced with proper per-binder mode splits —
`T_Let_L1_{Linear,Affine}`, `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), modelled at the
binder so every rule stays length-preserving.

**`Semantics_L1.v` — modality + mode-split migration:**
- Every lemma quantified over explicit `m` (a `Section` variable fails:
`induction Htype` generalises the index, severing cross-references).
- Structural lemmas made case-count-robust; `m`/mode-split threaded
through region-shrink, shift, substitution, and the 33-case preservation
dispatch (`econstructor` auto-selects the mode variant in
congruence-step cases).
- 4 **new** affine-β subcases (`Let`/`LetLin`-Val, `Case`-Inl/Inr) are
admitted with documentation — they need a generalised affine
substitution lemma (bound var may be left unused). These are **L2/affine
follow-up**, distinct from the pre-existing linear 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.

## Verification

- Full development builds clean from scratch: `coqc 8.18`, all 6 modules
(`Syntax Typing TypingL1 Semantics Semantics_L1 Counterexample`), `make
-f build.mk clean && make -f build.mk` → exit 0.
- Legacy `Semantics.v` untouched (its provably-false preservation stays
as-is, per directive).
- No previously-closed case regressed.

## Next (Stage B — needs a design call)

The **linear** soundness gaps remain pre-existing admits/axiom:
- `region_liveness_at_split_l1` is currently a **false `Axiom`**
(general `In rv R → In rv R'`, refuted by `ERegion rv …`) — an
inconsistency that must be removed.
- `S_App_Step2` / `S_Pair_Step2` admits (§4.8 lambda-rigidity + variable
over-permissiveness).

Probing the Option 3 fix (strengthen `T_Var_*_L1` with `incl
(free_regions T) R`) shows it ripples into
`region_shrink_preserves_typing_l1_gen` (type-region variables) and
likely needs pairing with an `T_Lam` restriction to close `S_App_Step2`.
Holding for direction before mechanising.

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

Author: hyperpolymath

.machine_readable/bot_directives/README.adoc

@@ -27,6 +27,7 @@ These 7 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY:
 1. **Formal Proof Integrity** — Coq proofs are layered per the four-layer redesign (`formal/PRESERVATION-DESIGN.md`). The legacy `preservation` in `Semantics.v` is provably FALSE per `Counterexample.v` (5 Qed lemmas) and remains `Admitted`. The L1 preservation chain (`Semantics_L1.v`) is in flight; explicit `Admitted` / `admit.` / `Axiom` sites are enumerated by `file:line` in `docs/proof-debt.adoc` per the standards#203 trusted-base reduction policy. Idris2 source has no `believe_me` / `assert_total` / `sorry`. ANY new escape hatch must be enumerated in `docs/proof-debt.adoc` before the trusted-base CI check will pass.
 2. **Dyadic Separation** - The boundary between affine and linear types must be strictly enforced.
 3. **SPDX Headers** - All source files MUST carry `SPDX-License-Identifier: MPL-2.0`.
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 4. **Author Attribution** - Always "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>".
 
 ## REPOSITORY STRUCTURE

.machine_readable/svc/k9/README.adoc

@@ -1,4 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 # SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
 
 [workspace]

0-AI-MANIFEST.a2ml

@@ -1,4 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 # Ephapax build recipes
 
 # Default recipe
@@ -126,6 +127,7 @@ tour:
     echo "═══════════════════════════════════════════════════"
     echo ""
     echo '// SPDX-License-Identifier: MPL-2.0'
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
     echo ""
     echo "Key directories:"
     echo "  src/                      Source code" 

CHANGELOG.md

@@ -1,4 +1,5 @@
 SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 ------------------------------------------------------------------------