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

## Summary

Phase 1 of the non-linear substitution-lemma generalisation per
[`formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`](https://github.com/hyperpolymath/ephapax/blob/main/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md)
§"Phase 1" (design doc landed in #213).

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`).
- `ground_nonlinear_retype_l1_m` in `formal/Semantics_L1.v` (after
`loc_retype_at_R_l1_m`):

```coq
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; EUnit/EBool/EI32 cases
invert + re-apply the corresponding R-polymorphic ground 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.

## Why this matters

The `T_App_L2_Eff` β-case of `preservation_l2` is blocked at non-linear
`T1` (in `TFunEff T1 T2 R_in R_out` lambdas) because
`subst_typing_gen_l1_m`'s `is_linear_ty T1 = true` precondition can't
fire for non-linear ground types (`TBase TUnit` / `TBase TBool` / `TBase
TI32`). Phase 1 ships the ground-non-linear retype primitive that Phase
2's parallel substitution lemma will use in place of
`loc_retype_at_R_l1_m` for R-shift retypes.

## Owner-directive compliance

Per `CLAUDE.md` 2026-05-27 (escalated again in #213 design doc
§"Owner-directive compliance check"):

- Does NOT close `Theorem preservation` in `Semantics.v`.
- Does NOT extend `Semantics.v` / `Typing.v` / `Counterexample.v` (all
untouched in diff).
- Does NOT close residual `Semantics_L1.v` admits via this work —
strictly NEW infrastructure orthogonal to legacy.
- Adds no new `Axiom` or `Admitted` declarations.
- Follows post-2026-05-26 four-layer redesign per
`PRESERVATION-DESIGN.md`.

## Test plan

- [x] `just clean && just all` in `formal/` — clean rebuild of all 10
`.v` files (coqc 8.18.0).
- [x] Zero new admits/axioms (proof is `Qed`).
- [x] `Semantics.v`/`Typing.v`/`Counterexample.v` untouched.
- [x] GPG-signed commit.
- [x] STATE.a2ml `next_action` shifted to Phase 2 design.

## Refs

Refs hyperpolymath/standards#134 (sub-issue of
hyperpolymath/standards#124 estate proof-debt epic). Follows #213
(design doc). Phase 2 (parallel substitution lemma) is the next slice.

🤖 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 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
+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, landed in PR #219) 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). PR #219."
+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