feat(L1): Phase D slice 4 Phase 1 — ground_nonlinear_retype_l1_m for TBase TUnit/TBool/TI32

Phase 1 of the non-linear substitution-lemma generalisation per
`formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` §"Phase 1".

Adds NEW infrastructure to L1 (orthogonal to legacy preservation in
`Semantics.v` — that theorem remains correctly Admitted, provably false
per `Counterexample.v`, per owner directive 2026-05-27):

- `is_ground_nonlinear_ty : ty -> bool` in `formal/Syntax.v` (after
  `is_linear_ty`), recognising `TBase TUnit` / `TBase TBool` / `TBase TI32`.

- `ground_nonlinear_retype_l1_m` in `formal/Semantics_L1.v` (after
  `loc_retype_at_R_l1_m`):

    forall m R R' G v T,
      is_value v ->
      is_ground_nonlinear_ty T = true ->
      has_type_l1 m R G v T R G ->
      has_type_l1 m R' G v T R' G.

  Proof destructs on the `is_value v` witness; in EUnit/EBool/EI32 cases
  inverts the typing derivation (uniquely produced by
  T_Unit_L1/T_Bool_L1/T_I32_L1, each R-polymorphic) and re-applies the
  constructor at R'. Non-ground value cases (ELam/EPair/EInl/EInr/ELoc/
  EBorrow/EEcho) discriminate Hgrd against the non-ground codomain type
  every typing-rule inversion produces.

Phase 1 unblocks Phase 2 — the parallel substitution lemma
`subst_typing_gen_l1_m_ground_nonlinear` that the
`T_App_L2_Eff` β-case of `preservation_l2` needs for non-linear `T1`
in `TFunEff T1 T2 R_in R_out` lambdas.

Build oracle: coqc 8.18.0 clean across all 10 .v files (clean rebuild).
Zero new admits/axioms. `Semantics.v`/`Typing.v`/`Counterexample.v`
untouched.

STATE.a2ml `next_action` shifts to Phase 2 design (sibling lemma rather
than case-split into existing `subst_typing_gen_l1_m` — preserves the
~30 Qed downstreams).

Refs hyperpolymath/standards#134 (sub-issue of hyperpolymath/standards#124).

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 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 2 — ship `subst_typing_gen_l1_m_ground_nonlinear` per `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` §'Phase 2'. Parallel substitution lemma for ground non-linear `T1` (TBase TUnit / TBase TBool / TBase TI32). Structure mirrors the existing `subst_typing_gen_l1_m` 28-case induction at `formal/Semantics_L1.v:1358`. Key divergences: (i) `T_Var_Lin_L1` with `i = k0` discharges via `is_linear_ty T1 = false` vs T_Var_Lin_L1's `is_linear_ty T = true` premise (exfalso); (ii) `T_Var_Unr_L1` with `i = k0` becomes a CONSTRUCTIVE case — apply `Hv_type` directly (in the existing lemma this is vacuous via `Hlin`); (iii) compound cases use `ground_nonlinear_retype_l1_m` (NEW — Phase 1, just landed) in place of `loc_retype_at_R_l1_m` for R-shift retypes. Estimated ~250-300 lines paralleling existing proof. Ships as sibling lemma (NOT case-split into existing one) to avoid breaking ~30 Qed downstreams of `subst_typing_gen_l1_m`. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no closure of residual `Semantics_L1.v` admits via this work — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
+last_action: "Phase D slice 4 Phase 1 LANDED (2026-05-30): `is_ground_nonlinear_ty` predicate added to `formal/Syntax.v` (after `is_linear_ty`); `ground_nonlinear_retype_l1_m` lemma added to `formal/Semantics_L1.v` (after `loc_retype_at_R_l1_m`). Signature: `forall m R R' G v T, is_value v → is_ground_nonlinear_ty T = true → has_type_l1 m R G v T R G → has_type_l1 m R' G v T R' G`. Proof: destruct on `is_value v` witness; in EUnit/EBool/EI32 cases invert typing and re-apply T_Unit_L1/T_Bool_L1/T_I32_L1 at R'; in non-ground value cases (ELam/EPair/EInl/EInr/ELoc/EBorrow/EEcho) every typing-rule inversion gives a non-ground T discriminated by Hgrd. Total addition: ~30 lines in Semantics_L1.v + ~12 lines in Syntax.v. Coqc 8.18.0 clean across all 10 .v files. Zero new admits/axioms. `Semantics.v`/`Typing.v`/`Counterexample.v` untouched. Unblocks Phase 2 (parallel substitution lemma for ground non-linear T1)."
+updated: 2026-05-30T00:00:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
 # Captured durable directive — preservation work is the four-layer redesign,

formal/Semantics_L1.v

@@ -1177,6 +1177,46 @@ Lemma loc_retype_at_R_l1 :
     R_inner; G |=L1 ELoc l r : TString r -| R_inner; G.
 Proof. intros. apply T_Loc_L1. assumption. Qed.
 
+(** Ground non-linear retype across any [R → R'].
+
+    For ground non-linear types ([TBase TUnit] / [TBase TBool] /
+    [TBase TI32]) the typing derivation of a value is uniquely
+    produced by [T_Unit_L1] / [T_Bool_L1] / [T_I32_L1], each of
+    which is polymorphic in the region environment. The retype is
+    therefore the trivial "invert and re-apply" pattern.
+
+    Used by the Phase D slice 4 non-linear substitution-lemma
+    generalisation: any β-reduction with [T1 ∈ {TBase TUnit,
+    TBase TBool, TBase TI32}] feeds a substituend whose typing
+    must be re-stated at sub-expression-internal region environments
+    inside [ebody]. See [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md]
+    Phase 1.
+
+    Orthogonal to legacy [preservation] in [Semantics.v]: this lemma
+    adds NEW infrastructure constrained to the post-redesign
+    [has_type_l1] judgment carrying the modality parameter [m]. It
+    does not extend or patch [Semantics.v]. *)
+Lemma ground_nonlinear_retype_l1_m :
+  forall (m : Modality) (R R' : region_env) (G : ctx) (v : expr) (T : ty),
+    is_value v ->
+    is_ground_nonlinear_ty T = true ->
+    has_type_l1 m R G v T R G ->
+    has_type_l1 m R' G v T R' G.
+Proof.
+  intros m R R' G v T Hval Hgrd Ht.
+  destruct Hval as
+    [ | b | n
+    | T0 e0 | v1 v2 Hv1 Hv2
+    | T0 v0 Hv0 | T0 v0 Hv0
+    | l r
+    | v0 Hv0
+    | T0 v0 Hv0 ];
+    inversion Ht; subst; try discriminate Hgrd.
+  - (* v = EUnit, T = TBase TUnit *) apply T_Unit_L1.
+  - (* v = EBool b, T = TBase TBool *) apply T_Bool_L1.
+  - (* v = EI32 n, T = TBase TI32 *) apply T_I32_L1.
+Qed.
+
 (** Narrower axiom (region-liveness at compound-rule split points).
 
     Given a well-typed sub-derivation [R; G |=L1 e1 : T1 -| R1; G']

formal/Syntax.v

@@ -455,6 +455,23 @@ Fixpoint is_linear_ty (T : ty) : bool :=
   | _ => false
   end.
 
+(** Check if a type is a ground non-linear base type — [TUnit], [TBool],
+    or [TI32]. Values at these types are R-irrelevant: their typing
+    derivations (via [T_Unit_L1] / [T_Bool_L1] / [T_I32_L1]) are
+    polymorphic in the region environment, so a retype across any
+    [R → R'] is constructively trivial.
+
+    Introduced for [Semantics_L1.ground_nonlinear_retype_l1_m] and the
+    Phase D slice 4 non-linear substitution-lemma generalisation
+    (formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 1). *)
+Definition is_ground_nonlinear_ty (T : ty) : bool :=
+  match T with
+  | TBase TUnit => true
+  | TBase TBool => true
+  | TBase TI32  => true
+  | _ => false
+  end.
+
 (** Check if all linear variables in context have been used *)
 Fixpoint ctx_all_linear_used (G : ctx) : Prop :=
   match G with