docs: Phase B Slice 1 deferral + Phase C scoping (2026-05-28)

.machine_readable/6a2/STATE.a2ml

@@ -6,9 +6,9 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Phase B — TEcho linearity / observation discipline. Wire `is_linear_ty (TEcho T) = ...` in TypingL1.v so a Linear unobserved echo fails typing, then cascade through every `is_linear_ty T = true` premise site. Phase C (L1 structural list-vs-multiset bridge) and Phase D (L2 effect-typed TFun) follow, per the saved 4-phase plan (project_ephapax_post_slice4_plan in user auto-memory). All work is layered per CLAUDE.md owner directive 2026-05-27: no patching of legacy Semantics.v/Typing.v, no new Admitted/Axiom, no ad-hoc cross-layer reasoning to close L1 admits."
-last_action: "Phase A — L4 dyadic scaffold (docs only, no proof changes). Added formal/L4-DYADIC.md design page extracting PRESERVATION-DESIGN.md §7 + formal/L4.v with [ProgramMode] enum and [program_mode_to_modality] mapping to L2's [Modality]. Wired into _CoqProject; full-tree coqc 8.18.0 clean rebuild passes. Slice 4 capstone (preservation_l3) landed on main 2026-05-27 as PR #196."
-updated: 2026-05-28T08:25:00Z
+next_action: "Phase C — L1 structural list-vs-multiset bridge (1-2 PRs). Closes Semantics_L1.v structural admits at ~line 553/621 + 1 outer Admitted that depend on them. Bridge predicate choice (rotation vs permutation vs abstract multiset) is the first design decision. Branch: proof/phase-c-l1-multiset-bridge."
+last_action: "Phase A merged via PR #197 (d87b459) / Phase B Slice 1 DEFERRED 2026-05-28. Phase A (L4 dyadic scaffold) docs-only landed cleanly: formal/L4-DYADIC.md design page + formal/L4.v ProgramMode labelling discipline. Phase B Slice 1 (TEcho linearity wire) investigated and deferred until Phase D: adding `| TEcho _ => true` to is_linear_ty is structurally non-vacuous at L1 (EEcho values typed at TEcho via T_Echo_L1 refute linear_value_is_loc_l1's conclusion + break 9 call-sites in subst_typing_gen_l1_m). Owner chose option (c) defer; the wire will land naturally once Phase D reshapes the L1 substitution chain."
+updated: 2026-05-28T08:50:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
 # Captured durable directive — preservation work is the four-layer redesign,

PROOF-NEEDS.md

@@ -110,6 +110,7 @@ enters the typing rules" and (for the diagram) in §6 (to be added).
 | ✅ Add collapse-function emission to step rules at irreversible boundaries | `S_Region_Exit_Echo` emits `EEcho T v` paralleling `S_Region_Exit` (untouched); `S_Drop_Echo` emits `EEcho T (ELoc l r)` paralleling `S_Drop` | done 2026-05-27 (L3 wiring slice 3c — owner-approved parallel-rule strategy in Semantics.v; updated `step_from_eregion` to 4-disjunct classification + `step_R_change_shape` + `no_leaks_gen` cascade); rules quantified over witness type T |
 | ~~Thread `G` (echo context) alongside `R` (region context) through compound rules~~ | ~~New context parameter on every L1 compound rule~~ | **OBSOLETE 2026-05-27**: under the owner-approved parallel-rules design (slices 3a–3c), echoes are values of type `TEcho T` that flow through the existing `ctx` G. No separate echo-context parameter is needed. |
 | ✅ State and prove `preservation_l3` | Per-layer preservation theorem against the L3 invariants for the new echo-emitting step rules + echo-typed paths | done 2026-05-27 (L3 wiring slice 4 — capstone). Two per-case Qed lemmas (`preservation_l3_region_active_echo` for `S_Region_Exit_Echo` × `T_Region_Active_L1_Echo`, and `preservation_l3_drop_echo` for `S_Drop_Echo` × `T_Drop_L1_Echo`) plus an umbrella `preservation_l3` (their conjunction, Qed). Zero new admits or axioms. Per-case alignment forced by `T_Echo_L1`'s witness-type premise; non-deterministic crossover cases are non-preserving by design (typing derivation pins the path). Conditionally Qed under the pre-existing `region_shrink_preserves_typing_l1_gen_m` L1 structural admit per PRESERVATION-DESIGN.md §5.1. |
+| ⏸ Register `TEcho` as linear via `is_linear_ty` (Phase B Slice 1) — DEFERRED 2026-05-28 | Realises the design intent annotated at `TypingL1.v:T_Observe_L1`: under Linear discipline, unobserved `TEcho` must fail typing closure | **deferred until Phase D**. Investigation 2026-05-28: adding `| TEcho _ => true` to `is_linear_ty` is structurally non-vacuous at L1 — `EEcho T v` is both a value (`VEcho`) and typed at `TEcho T` (via `T_Echo_L1`, TypingL1.v:351-354), refuting the conclusion of `linear_value_is_loc_l1` (Semantics_L1.v:891) and breaking 9 call-sites in `subst_typing_gen_l1_m` (Semantics_L1.v:1326-1605, Qed). Realising the wire requires a disjunctive rewrite of `linear_value_is_loc_l1` plus per-caller handling of the TEcho disjunct — substantially larger than the original "1-line definitional" framing. Owner deferred to after Phase D (L2 effect-typed TFun) when the L1 substitution chain reshapes naturally. The legacy `Semantics.v` branch is vacuous (no rule produces `TEcho`) and would have closed trivially. |
 
 ### Mid-term (L4 — scaffold landed 2026-05-28)