state: shift next_action to Phase 1 (ground_nonlinear_retype_l1_m)

.machine_readable/6a2/STATE.a2ml

@@ -6,9 +6,9 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Phase D slice 4 next sub-slice — generalise `subst_typing_gen_l1_m` (`formal/Semantics_L1.v:1358`) to handle non-linear `T1`. The full `preservation_l2` over `has_type_l2` is blocked at the `T_App_L2_Eff` β-case (`S_App_Fun`) because that lemma's `is_linear_ty T1 = true` precondition doesn't hold for `TFunEff T1 T2 R_in R_out` lambdas with non-linear `T1` (`TUnit` / `TBool` / `TI32`). Approach: (a) read existing proof at Semantics_L1.v:1358-1656 (~300 lines, induction on Htype); (b) identify cases that use `is_linear_ty T1 = true` (primarily `T_Var_Lin_L1` via `flag_false_to_true_implies_linear_l1`); (c) ship a sibling lemma `subst_typing_gen_l1_m_nonlinear` rather than folding case-split into existing lemma (to avoid breaking 30+ Qed downstreams). Once this lands, the T_App_L2_Eff β-case in preservation_l2 closes via: inversion on has_type_l2 → L2_lift_l1 inner → T_Lam_L1_*_Eff inner → value_R_G_preserving_l1 on v2 → apply (general or non-linear) subst lemma → L2_lift_l1 wrap. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close `T_App_L2_Eff` cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no re-attempt of option 4; no side-conditions on `T_Lam_L1_*_Eff`/`T_App_L2_Eff` to dodge the substitution-lemma generality issue. Coqc 8.18.0 is the only authority."
-last_action: "Phase D slice 4 partial landing session 7 (2026-05-28): `preservation_l2_via_l1` + `preservation_l2_lift_case` corollary + comprehensive doc block landed in `formal/TypingL2.v` (PR #211 OPEN, auto-merge SQUASH armed at 2026-05-28T13:41:20Z, GPG-signed commit 1131141, single-file diff +109/-1). Theorem closes the `L2_lift_l1` case of `preservation_l2` by deferring to `Semantics_L1.preservation_l1` (legacy admit honestly carried forward via `Print Assumptions`). `T_App_L2_Eff` β-case escalated per owner directive §'DO escalate before patching' — `subst_typing_gen_l1_m`'s `is_linear_ty T1 = true` precondition blocks closure for non-linear lambda parameter types. Doc block in TypingL2.v specifies the full preservation_l2 goal, the planned structural-induction proof, and the next-slice infrastructure required (subst-lemma generalisation + has_type_l2 inversion principles + T_Lam_L1_*_Eff inversion). Coqc 8.18.0 clean across all 10 .v files. Zero new admits/axioms in TypingL2.v. `Semantics.v`/`Typing.v`/`Counterexample.v`/`Semantics_L1.v` untouched."
-updated: 2026-05-28T13:42:00Z
+next_action: "Phase D slice 4 Phase 1 (per `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`) — implement `ground_nonlinear_retype_l1_m` in `formal/Semantics_L1.v`. ~10-line lemma covering EUnit/EBool/EI32 retype across R-shifts. Steps: (a) add `is_ground_nonlinear_ty` predicate to `formal/Syntax.v` near `is_linear_ty` at line 450 (returns true for TUnit/TBool/TI32 only); (b) implement the retype lemma in `formal/Semantics_L1.v` after `loc_retype_at_R_l1_m` at line 1168. Phase 1 unblocks Phase 2 (`subst_typing_gen_l1_m_ground_nonlinear`, ~250 lines, 1-2 sessions). Full 5-phase plan documented in `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` with 4 open questions for owner. Anti-patterns to refuse (per CLAUDE.md owner directive + design-doc): no `Admitted` to close T_App_L2_Eff cases; no folding case-split into existing `subst_typing_gen_l1_m` (breaks 30+ Qed downstreams); no closing TFun lambda retype (legacy slice 4b gap, out of scope); no touching `Semantics.v`/`Typing.v`/`Counterexample.v`. Coqc 8.18.0 is the only authority."
+last_action: "Phase D slice 4 design session 8 (2026-05-28): SUBST-LEMMA-GENERALIZATION-DESIGN.md (~210 lines) landed in `formal/` directory (PR #213 MERGED at 2026-05-28T13:53:37Z, GPG-signed commit 79c6368, single-file doc-only diff). Investigation found that the previously-scoped 'sibling lemma' for `subst_typing_gen_l1_m_nonlinear` is substantially more complex than session 7's STATE shift assumed — non-linear-T1 substitution interacts with body-R-rigidity for non-linear ELam values (the same gap that blocks legacy preservation_l1 slice 4b). Doc captures: 2 distinct uses of Hlin (linear_value_is_loc_l1 extraction + T_Var_Unr_L1 contradiction discharge); per-value-shape retype-feasibility table (ground ✅ / TFunEff ⚠️ / TFun ❌ / compound ⚠️); recommended 5-phase plan (1: ground_nonlinear_retype_l1_m; 2: subst_typing_gen_l1_m_ground_nonlinear; 3: tfuneff_lambda_retype; 4: close preservation_l2 β-case; 5 deferred: compound non-linear values); 4 open design questions for owner. No code shipped this session (intentional escalation per CLAUDE.md §'DO escalate before patching'). `Semantics.v`/`Semantics_L1.v`/`TypingL1.v`/`TypingL2.v`/`Typing.v`/`Counterexample.v` untouched."
+updated: 2026-05-28T13:54:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
 # Captured durable directive — preservation work is the four-layer redesign,
@@ -93,6 +93,9 @@ updated: 2026-05-28T13:42:00Z
 #                                preservation_l2_via_l1 (Phase D slice 4 partial)
 #   formal/L4.v               — ProgramMode labelling discipline (Phase A)
 #   formal/L4-DYADIC.md       — L4 design doc
+#   formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md
+#                              — Phase D slice 4 follow-on 5-phase plan
+#                                + 4 open questions for owner (PR #213)
 # Doc lockdown:
 #   CLAUDE.md                       — owner directive §
 #   formal/PRESERVATION-DESIGN.md   — CANONICAL banner