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

## Summary

- Records the 2026-05-28 investigation finding that **Phase B Slice 1**
(TEcho linearity wire) is structurally larger than the saved plan
implied, and the owner directive to **defer until Phase D**.
- Reorients \`STATE.a2ml\` next_action to **Phase C** — closure of the
two list-vs-multiset structural admits at
\`formal/Semantics_L1.v:553/621\` inside
\`region_shrink_preserves_typing_l1_gen_m\`.
- **No proof changes** — \`coqc 8.18.0\` clean rebuild verified (9/9 .v
files \`Qed\`).

## Background — the Phase B Slice 1 deferral

The original Phase B Slice 1 plan was a one-line definitional
refinement: add \`| TEcho _ => true\` to \`is_linear_ty\` in
\`formal/Syntax.v\`, realising the design intent annotated at
\`TypingL1.v:T_Observe_L1\`.

Investigation 2026-05-28 revealed the wire's true scope:

- **Legacy \`Semantics.v\` impact**: vacuous. \`linear_value_is_loc\`
(Semantics.v:2625) gains a TEcho branch closeable by \`inversion Htype;
discriminate\` because legacy \`Typing.v\` has zero typing rules
producing \`TEcho\` (grep-verified).
- **L1 impact**: structurally non-vacuous. At L1, \`EEcho T v\` is both
a value (\`VEcho\` in Syntax.v:152) AND typed at \`TEcho T\` (via
\`T_Echo_L1\` in TypingL1.v:351-354). This refutes the conclusion of
\`linear_value_is_loc_l1\` (Semantics_L1.v:891) — the lemma claims
\"linear-typed value ⇒ \`ELoc\` with \`TString r\`\", but \`EEcho T v\`
is a linear-typed value that is neither. The lemma feeds 9 call-sites
inside \`subst_typing_gen_l1_m\` (Semantics_L1.v:1326-1605, \`Qed\`),
which is foundational L1 substitution scaffolding for
\`preservation_l1\`.

Three resolution paths were surfaced (\`AskUserQuestion\` 2026-05-28):

1. **Disjunctive rewrite + 9-caller updates**: structurally correct but
adds ~9 forward-looking \`Admitted\` sites to the L1 substitution chain.
2. **Layered predicate split**: introduce \`is_linear_ty_l3\` keeping
legacy \`is_linear_ty\` alone. Zero legacy touch but adds definitional
duplication.
3. **Defer until Phase D**: Phase D (L2 effect-typed \`TFun\`) will
reshape the L1 substitution chain anyway. The wire lands naturally once
that infrastructure exists.

**Owner chose (3) defer** — Phase D will create the right shape for the
wire to land cleanly without the disjunctive rewrite.

## Phase C scoping (this commit)

\`STATE.a2ml\` next_action now reads: \"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\`.\"

Mapping verified:
- **Lines 553 + 621**: both inside
\`region_shrink_preserves_typing_l1_gen_m\`, T_Region_Active_L1 \`rr =
r\` shadowed case + T_Region_Active_L1_Echo mirror. **Phase C scope.**
- **Lines 1256 + 1276**: in \`region_liveness_at_split_l1_gen\`,
\"GENUINELY FALSE at L1\" per source comment at 1253 — closes naturally
at Phase D's L2 effect-typed TFun. **NOT Phase C scope.**
- **Line 1694**: lambda-rigidity admit inside \`preservation_l1\`'s
outer Admitted. **Phase D scope.**

Closure of 553 + 621 ⇒ outer \`Admitted\` at line 653
(\`region_shrink_preserves_typing_l1_gen_m\`) flips to \`Qed\`. That
makes the value-restricted wrapper at line 666-676
(\`region_shrink_preserves_typing_l1\`) actually-\`Qed\` (currently
\`Qed\` only under the outer \`Admitted\`).

## Test plan

- [x] \`coqc 8.18.0\` clean rebuild — all 9 .v files \`Qed\`
- [x] No proof changes; only PROOF-NEEDS.md row + STATE.a2ml refresh
- [ ] CI: standard governance + scorecard

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

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

Author: hyperpolymath

.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)