docs: Phase C deferred (2026-05-28) — option (c) analytical infeasibility

.machine_readable/6a2/STATE.a2ml

@@ -6,9 +6,9 @@
 
 @state(version="2.0"):
 phase: "implementation"
-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
+next_action: "Phase D — L2 effect-typed TFun (~4 sub-slices, per project_ephapax_post_slice4_plan). Adds new constructor TFunEff T1 T2 R_in R_out (legacy TFun preserved per CLAUDE.md directive). Cascade: Syntax.v free_regions/shift/subst/is_value → TypingL1.v T_Lam_L1_*_Eff + T_App_L1_Eff parallel rules → Semantics_L1.v closes lambda-rigidity admit at line 1694 + naturally enables Phase B Slice 1 wire AND Phase C body-input-shrinkage."
+last_action: "Phase A merged via PR #197 (d87b459) / Phase B Slice 1 DEFERRED 2026-05-28 / Phase C 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). Phase C (L1 list-vs-multiset structural bridge) investigated 2026-05-28 across all four design options (perm-modulo, multiset reformulation, rule redesign, defer) — rule redesign attempted in-flight on branch `proof/phase-c-l1-multiset-bridge` but proven to close only sub-sub-case (ii) (R has exactly 1 rr) while sub-sub-case (i) (R has ≥2 rr) requires body-input-shrinkage which is NOT a theorem (T_Loc_L1 counterexample at count=1; T_Let composition unstable). Owner chose option (d) defer as most mathematically safe + elegant. Both deferrals close at Phase D's L2 effect-typed TFun where the lambda body's R-flow becomes effect-typed."
+updated: 2026-05-28T11:30:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
 # Captured durable directive — preservation work is the four-layer redesign,

PROOF-NEEDS.md

@@ -111,6 +111,7 @@ enters the typing rules" and (for the diagram) in §6 (to be added).
 | ~~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. |
+| ⏸ Close the L1 list-vs-multiset structural admits at `Semantics_L1.v:553/621` (Phase C) — DEFERRED 2026-05-28 | The `T_Region_Active_L1`-shadowed sub-case of `region_shrink_preserves_typing_l1_gen_m` requires bridging body derivations across input shrinkage when the outer region matches a body-internal active occurrence | **deferred until Phase D**. Four design paths surfaced + analytically evaluated 2026-05-28 (recorded in this session's memory + companion design note `Semantics_L1.v:366-402`): (a) Permutation-based perm-l1 leaves a list-structure output mismatch (concrete counterexample at `R_body = [a; rr; b; c]` vs `R_body' = [b; rr; a; c]`); (b) multiset reformulation of `remove_first_L1` cascades through every L1 rule's output threading; (c) `T_Region_*_L1` rule redesign (Permutation premise on body output) was implemented in-flight on `proof/phase-c-l1-multiset-bridge` — closes sub-sub-case (ii) (R has exactly 1 rr via count-vacuity) but leaves sub-sub-case (i) (R has ≥2 rr) requiring body-input-shrinkage, which itself is NOT a theorem (T_Loc_L1 counterexample at count=1; T_Let composition fails for the count-≥-2 precondition); (d) defer was selected as the most mathematically safe + elegant path. Phase D (L2 effect-typed TFun) introduces the natural setting: lambda bodies' R-flow becomes effect-typed, which gives the structural invariant that lets body-input-shrinkage discharge. The 2 admits at lines 553/621 remain as documented L1 debt, and the outer `Admitted.` at line 653 + the `preservation_l3` dependency annotation in PRESERVATION-DESIGN.md §5.1 continue to attribute them correctly. |
 
 ### Mid-term (L4 — scaffold landed 2026-05-28)