proof(Semantics_L1): close subst_typing_gen_l1 via m-polymorphic generalisation (L2-β #2) (#188)

## Summary

Closes `subst_typing_gen_l1` (the substitution lemma) by m-polymorphic
generalisation, mirroring the `shift_typing_gen_l1_m` pattern landed in
#187.

Net debt in `formal/Semantics_L1.v`: **19 Qed + 4 Admitted → 25 Qed + 3
Admitted**.

## What changed

- New `subst_typing_gen_l1_m` (m-polymorphic, 29 explicit bullets
covering all L1 constructors).
- `subst_typing_gen_l1` becomes a Linear wrapper around `_m`.
- `typing_preserves_bindings_l1` and `output_shape_at_l1` generalised to
modality-polymorphic (mechanical signature change; body unchanged — only
used by `subst_typing_gen_l1` internally, no other estate callers).
- New `loc_retype_at_R_l1_m` (m-polymorphic sibling of the existing
Linear wrapper) so the substituted-value retyping at compound-rule split
points works at the active modality `m`.
- Internal calls switched to `region_liveness_at_split_l1_gen`
(m-polymorphic) instead of the Linear wrapper.

## Why this shape

The substituted-value premise `Hv_type` stays at Linear — callers
(`subst_preserves_typing_l1`, `preservation_l1`) always have a Linear
v-typing. Inside the m-polymorphic body it is unpacked via
`linear_value_is_loc_l1` and reconstructed at the active `m` via
`loc_retype_at_R_l1_m`.

Mode-split rules — T_Lam_L1_{Linear,Affine}, T_Case_L1_{Linear,Affine},
T_If_L1_{Linear,Affine} — each get their own bullet. Affine cases mirror
Linear because substitution threading is modality-independent (the
Affine rules differ only in permitted output flags, which are quantified
inside each rule and transparent to the IH).

## Residual admits in `Semantics_L1.v` (3, down from 4)

1. `region_shrink_preserves_typing_l1_gen` — list-vs-multiset structural
mismatch in T_Region_Active_L1 shadowed case.
2. `region_liveness_at_split_l1_gen` — 1 narrow admit in
T_Region_Active_L1 `[r = rv]` sub-case (genuinely false per documented
counterexample `ERegion rv (EI32 5)`).
3. `preservation_l1` — capstone; depends on closing (1)+(2) under L2
dispatch + lambda-rigidity gap resolution.

## Doctrine compliance (CLAUDE.md 2026-05-27)

- ✅ No new \`Axiom\` declarations.
- ✅ No ad-hoc side conditions on compound rules.
- ✅ No strengthened lemma signatures dodging the L2 dispatch — the
generalisation moves \`m\` *into* the signature, exposing the modality
dispatch, not hiding it.
- ✅ Legacy \`formal/Semantics.v\` and \`formal/Typing.v\` untouched.

## Test plan

- [x] \`coqc\` clean build via \`cd formal && just clean && just all\`
(Coq 8.18.0).
- [x] \`grep -c "Admitted\.$" Semantics_L1.v\` → 3 (was 4).
- [x] \`grep -c "Qed\.$" Semantics_L1.v\` → 25 (was 19).
- [x] No new \`Axiom\` introduced (\`grep -c "^Axiom " formal/*.v\`
unchanged).
- [ ] CI passes.

## Stacking

This PR is stacked on #187 (the 3 affine-only bullet-structure
regressions). GitHub will auto-retarget to \`main\` when #187
squash-merges.

---

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

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

Author: hyperpolymath

PROOF-NEEDS.md

@@ -56,7 +56,7 @@ For the architectural background see
 | L1 judgment indexed by modality `m : Modality` | `formal/TypingL1.v` | landed via PRs #176 + #177 |
 | L2 modality core (`Modality.v`, `linear_to_affine`) | `formal/Modality.v` | 1 Qed, zero axioms |
 | L3 calculus (echo / residue fiber + degrade + no-section proof) | `formal/Echo.v` | 12 Qed, 0 admits |
-| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 19 Qed; 4 residual admits (L2-β follow-up) |
+| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 25 Qed; 3 residual admits (L2-β follow-up) |
 | Counterexample regression witness | `formal/Counterexample.v` | 5 Qed (`bad_input_untypable_l1` proved under both modes) |
 | Operational checker (Rust, ephapax-linear sublanguage) | `ephapax-linear/src/linear.rs` | working — discharges resource-exact obligation |
 
@@ -68,7 +68,7 @@ For the architectural background see
 | Linear ⇒ Affine weakening | `formal/TypingL1.v` `linear_to_affine` | Qed, zero axioms |
 | Operational checker (Rust, ephapax-affine sublanguage) | `ephapax-linear/src/affine.rs` | working — permits weakening / graceful abandonment |
 | Affine-mode echo discipline (LEcho Affine = lowered triple) | `formal/Echo.v` (calculus) | calculus done; rule wiring pending |
-| Affine forward progress lemmas | `formal/Semantics_L1.v` | bullet-structure rewrites for 3 lemmas landed 2026-05-27; remaining 4 admits are L2-β deeper-than-bullet debt (see §2) |
+| Affine forward progress lemmas | `formal/Semantics_L1.v` | bullet-structure rewrites + subst_typing_gen_l1_m m-polymorphic generalisation landed 2026-05-27; remaining 3 admits are L2-β deeper-than-bullet debt (see §2) |
 
 ### Counterexample regression
 
@@ -89,9 +89,9 @@ For the architectural background see
 |---|---|---|
 | ✅ Close 3 pure bullet-structure regressions (typing_preserves_bindings_l1, unrestricted_flag_unchanged_l1, shift_typing_gen_l1) | `formal/Semantics_L1.v` | done 2026-05-27 |
 | ✅ Generalise typing_preserves_length_l1 to modality-polymorphic | `formal/Semantics_L1.v` | done 2026-05-27 |
-| Generalise subst_typing_gen_l1 to modality-polymorphic + Linear wrapper | `formal/Semantics_L1.v` | ~1-2 hours (L2-β follow-up #2) |
+| ✅ Generalise subst_typing_gen_l1 to modality-polymorphic + Linear wrapper (also generalised typing_preserves_bindings_l1, output_shape_at_l1, loc_retype_at_R_l1) | `formal/Semantics_L1.v` | done 2026-05-27 (L2-β follow-up #2) |
 | Close region_shrink_preserves_typing_l1_gen T_Region_Active_L1 case (list-vs-multiset bridge) | `formal/Semantics_L1.v` | structural; deeper than bullet-restoration |
-| State and prove `preservation_l1` for both modes | `formal/Semantics_L1.v` | depends on subst_typing_gen_l1 closure |
+| State and prove `preservation_l1` for both modes | `formal/Semantics_L1.v` | depends on region_shrink + region_liveness narrow admit |
 
 ### Near-term (L3 wiring — design + mechanisation)
 
@@ -222,7 +222,7 @@ to the owner**:
 | `formal/Typing.v` (legacy) | n/a | 0 | 🛑 archaeology — `Counterexample.v` depends on falsity |
 | `formal/Counterexample.v` | **5** | 0 | ✅ pinned regression witness |
 | `formal/TypingL1.v` | **2** | 0 | ✅ active — L1 judgment, modality-indexed |
-| `formal/Semantics_L1.v` | **19** | **4** | ✅ active — bullet-structure regressions closed 2026-05-27; 4 residual admits are deeper L2-β debt (subst_typing_gen_l1 m-poly generalisation, region_shrink T_Region_Active_L1 list-vs-multiset case, region_liveness_at_split narrow admit, preservation_l1 cap) |
+| `formal/Semantics_L1.v` | **25** | **3** | ✅ active — bullet-structure regressions + subst_typing_gen_l1_m closed 2026-05-27; 3 residual admits are deeper L2-β debt (region_shrink T_Region_Active_L1 list-vs-multiset case, region_liveness_at_split narrow admit per ERegion counterexample, preservation_l1 cap) |
 | `formal/Modality.v` | **1** | 0 | ✅ active — L2 core, zero axioms |
 | `formal/Echo.v` | **12** | 0 | ✅ active — L3 calculus, not yet wired into L1 |
 | `formal/TypingL2.v` | (wrapper) | (wrapper) | ✅ thin re-indexing through `TypingL1.has_type_l1` |