docs(L2): CHANGELOG + PROOF-NEEDS — L2 modality landing + L2-β tracking (#177)

## Summary

Follow-up doc PR for L2 landing (PR #176, merged as `c9683d1`). Updates
human-readable docs + cleans an accidentally-tracked aux file:

- **CHANGELOG.md**: new "Four-layer preservation redesign" section
summarising L1 (PR #153-line), L2 (PR #176), L3 (PR #166/#167) with file
pointers and the ephapax-affine ≠ AffineScript disambiguation hook.
- **PROOF-NEEDS.md**: updates current-state inventory to list
`TypingL1.v`, `Modality.v`, `Semantics_L1.v`, `TypingL2.v`, `Echo.v`,
`Counterexample.v` with their L2 status (linear_to_affine Qed zero
axioms; 6 L1 lemmas L2-β regressed). Splits "What needs proving" into
L2-β follow-up + legacy-preservation entries.
- **`formal/.Semantics_admitted.aux`**: untracked (build artifact, per
`.gitignore` `.*.aux` policy).

No code changes — docs + dotfile cleanup only.

## Test plan

- [x] No conflict markers in PROOF-NEEDS.md (clean merge with main's
Path-3 at-pre helper additions)
- [x] Build still clean locally
- [ ] CI burn-in

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

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

Author: hyperpolymath

CHANGELOG.md

@@ -5,6 +5,37 @@ All notable changes to Ephapax are documented here.
 
 ## [Unreleased]
 
+### Four-layer preservation redesign (2026-05-26 → 2026-05-27)
+
+- **L1 — region capabilities** (PRs #153-line, integration branch
+  `proof/l1-region-threading-design`): introduces `has_type_l1` with
+  R-threading in `formal/TypingL1.v`. Supporting lemmas in
+  `formal/Semantics_L1.v`. Counterexample regression (`bad_input_untypable_l1`)
+  Qed in `formal/Counterexample.v`. `preservation_l1` Admitted with 4
+  residual admits in R-weakening territory.
+- **L2 — Linear/Affine modality** (PR #176, this entry): `has_type_l1`
+  carries `m : Modality` parameter so a single judgment specialises to
+  ephapax-linear AND ephapax-affine. New `formal/Modality.v` with K-free
+  thin poset (`modality_le` at `Type` sort + `_refl`/`_trans`/`_prop`).
+  Mode-split constructors for `T_Lam` / `T_Case` / `T_If`; remaining 21
+  rules modality-polymorphic. **`linear_to_affine` Qed, closed under the
+  global context (zero axioms).** Mirrors `EchoLinear.agda:38-58`'s
+  `weaken : LEcho linear → LEcho affine`. `weaken_modality` at the L2
+  layer dispatches through `linear_to_affine`. Six pre-L2 `Semantics_L1.v`
+  lemmas regressed to `Admitted` (bullet-structure rewrite needed for
+  the 3 new Affine-only constructors); restoration tracked as L2-β.
+  `Counterexample.bad_input_untypable_l1` generalised to `forall m,
+  ~ has_type_l1 m ...` — Qed under both indices.
+- **L3 — Echo / residue** (PRs #166, #167-line, parallel track):
+  `formal/Echo.v` scaffold with `Mode + LEcho + decoration-commuting
+  weakening`; `EchoR` residue + no-section irreversibility headline.
+  Decouples residue layer from typing layer; couples through L2's
+  thin-poset structure.
+- **Disambiguation, durable**: `ephapax-affine ≠ AffineScript`. They are
+  separate languages sharing only the typed-wasm target. Per `README`,
+  `CLAUDE.md`, `.machine_readable/disambiguation.a2ml` hooks landed via
+  PRs #152 / affinescript#393 / typed-wasm#73.
+
 ### Proof state (2026-05-20 → 2026-05-21)
 - **Coq `preservation` reduction campaign**: 910 open goals → 12 (98.7% reduction). PR chain:
   - **#92** — honest framing: replaced unsubstantiated "Qed 2026-04-27" claim with `Admitted.`

PROOF-NEEDS.md

@@ -2,13 +2,19 @@
 
 ## Current state
 - `formal/Syntax.v` — Coq formalization of Ephapax syntax (clean)
-- `formal/Semantics.v` — Coq operational semantics
+- `formal/Semantics.v` — Coq legacy operational semantics
   - `step_preserves_type` — **Qed** (closed 2026-05-26 via [Path 3 at-pre helper](#path-3-at-pre-helper))
   - `step_output_context_eq` (Lemma B) — **Qed** (closed 2026-05-26 via Path 3)
   - `step_preserves_type_at_pre` — **Admitted** (NEW helper; 8 of 35 cases remain admitted, falls through to `all: admit.` catch-all)
   - `step_output_context_eq_at_pre` — **Admitted** (NEW helper; analogous shape)
-  - `preservation` — **Admitted** (12 cascading goals — separate problem, region-env weakening for non-values)
-- `formal/Typing.v` — Coq typing rules (clean)
+  - `preservation` — **Admitted** (12 cascading goals — separate problem, region-env weakening for non-values; superseded by L1 redesign — see `formal/PRESERVATION-DESIGN.md`)
+- `formal/Typing.v` — Coq typing rules, legacy (clean)
+- `formal/TypingL1.v` — **L2** Coq typing rules: `has_type_l1` indexed by `m : Modality ∈ {Linear, Affine}`. 21 modality-polymorphic constructors + 3 mode-split rule pairs (T_Lam / T_Case / T_If Linear vs Affine). `linear_to_affine` **Qed (zero axioms)**. Mode-split mechanises the PRESERVATION-DESIGN.md §5 distinction.
+- `formal/Modality.v` — K-free `Modality` datatype + `modality_le` thin poset + `_refl`/`_trans`/`_prop` lemmas. Mirrors `echo-types/proofs/agda/EchoLinear.agda:75-101`.
+- `formal/Semantics_L1.v` — L1 operational semantics; `preservation_l1` Admitted under `forall m : Modality, ...`. Six supporting lemmas L2-β regressed (bullet-structure rewrite needed for the new Affine-only constructors).
+- `formal/TypingL2.v` — thin re-indexing wrapper: `has_type_l2 m R G e T R' G' := L2_lift_l1 m (TypingL1.has_type_l1 m ...)`. `weaken_modality` dispatches through `TypingL1.linear_to_affine`.
+- `formal/Echo.v` — **L3** echo residue scaffold (`Mode + LEcho + decoration-commuting weakening + EchoR + no-section irreversibility`).
+- `formal/Counterexample.v` — `bad_input_untypable_l1 : forall m, ~ has_type_l1 m ...` Qed (regression witness under both modes).
 - `src/formal/Ephapax/Formal/RegionLinear.idr` — Idris2 region-based linearity proof (explicitly states "REAL proof — not believe_me, not assert_total")
 - 17 Idris2 files across formal verification layer
 - No `believe_me`, `sorry`, or `assert_total` in Idris2 source code
@@ -22,6 +28,12 @@ The at-pre helpers' S_Region_Step case is structurally simpler than the original
 Most of the helpers' OTHER cases were closed by copying step_preserves_type's and step_output_context_eq's tactic blocks verbatim (patterns use `?R`/`?R'` polymorphically and match at-pre framing trivially). What remains in each helper is the per-goal cases (~8 of 35), pending case-by-case closure.
 
 ## What needs proving
+
+### L2-β follow-up (post-PR #176)
+- **6 L1 supporting lemmas in `Semantics_L1.v`** — bullet-structure rewrite of the `induction Htype` proofs to account for the 3 new Affine-only constructors (T_Lam_L1_Affine, T_Case_L1_Affine, T_If_L1_Affine). Each restoration adds 3 `discriminate` dispatches on the `Linear = Affine` equality and re-aligns case bullets. Mechanical; ~2-3 hours.
+- **`preservation_l1` body** under `forall m`: Linear branch is the old partial proof (12 admits in R-weakening territory); Affine branch needs the supporting lemmas above plus mode-aware handling for T_Lam_Affine / T_Case_Affine / T_If_Affine. Estimated 3-4 sessions once the supporting lemmas are restored.
+
+### Legacy preservation
 - **`step_preserves_type_at_pre`**: Close the remaining ~8 admitted cases (the per-goal cases of step_preserves_type's structure that need explicit blocks: S_StringConcat_Step2, S_Let_Step, S_LetLin_Step, S_App_Step2, S_If_Step, S_Pair_Step1, S_Pair_Step2, S_Case_Step). Each ~30 LOC, ported from step_preserves_type's "Per-goal" section (lines 5033-5562). Estimated 2-3h.
 - **`step_output_context_eq_at_pre`**: Close ~11 remaining admitted cases (the per-goal cases + S_Region_Step). Patterns parallel step_output_context_eq's body. Estimated 2-3h.
 - **`preservation`**: Close the remaining **12 open goals** — the RIGHT branch (R' = remove_first r R) sub-cases of each congruence step rule. These need a **region-env weakening for non-values** lemma that doesn't follow trivially from current infrastructure. Per the handoff doc, this is a deeper problem: when a binder steps to exit region r, the sibling expression might still mention r and not be typeable at the post-step R'. Closing requires either (a) a strengthened type invariant preventing such configurations, (b) a weakened preservation statement, or (c) a region-env weakening helper that case-analyses on the sibling's syntactic shape. Estimated 4-8h.