proofs(P43): port canonical_* forms to the L1 modality-polymorphic judgment

Closes proof-debt P43 prerequisite from the comprehensive inventory.
Prerequisite for P42 (progress_l1).

What lands

Seven modality-polymorphic canonical-forms lemmas at the end of
formal/Semantics_L1.v, mirroring the legacy Linear-only versions at
formal/Semantics.v:603-630:

  - canonical_unit_l1_m   : v : TBase TUnit  + is_value v → v = EUnit
  - canonical_bool_l1_m   : v : TBase TBool  + is_value v → ∃ b, v = EBool b
  - canonical_i32_l1_m    : v : TBase TI32   + is_value v → ∃ n, v = EI32 n
  - canonical_fun_l1_m    : v : TFun T1 T2   + is_value v → ∃ body, v = ELam T1 body
  - canonical_prod_l1_m   : v : TProd T1 T2  + is_value v → ∃ v1 v2, v = EPair v1 v2 ∧ ...
  - canonical_sum_l1_m    : v : TSum T1 T2   + is_value v → (∃ v0, v = EInl T v0 ∧ ...) ∨ (∃ v0, v = EInr T v0 ∧ ...)
  - canonical_string_l1_m : v : TString r    + is_value v → ∃ l, v = ELoc l r

The `_m` suffix follows the convention established by
region_shrink_preserves_typing_l1_gen_m and subst_typing_gen_l1_m.
A pre-existing Linear-only canonical_string_l1 at line 908 is left
untouched (it predates the L2 modality hybrid; the new _m version
generalises it).

All 7 proofs are single-line inversions:
  intros; inversion H0; subst; inversion H; subst; <discharge>

Same structural pattern as the legacy proofs — the L1 judgment's
value-typing rules are sufficiently rigid that inversion on
is_value v + the typing derivation pins the constructor.

Build oracle: just -f formal/Justfile all clean. All 7 Print
Assumptions blocks (added inline) print "Closed under the global
context" — these lemmas surface ZERO axioms, exactly as the
canonical-forms framework requires.

Next: progress_l1 (P42) uses these as the case analysis on the type
of a closed well-typed value. Stated separately because it requires
the step relation's totality on non-value terms.

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

Author: hyperpolymath

formal/Semantics_L1.v

@@ -3265,3 +3265,86 @@ Proof.
   - exact preservation_l3_region_active_echo.
   - exact preservation_l3_drop_echo.
 Qed.
+
+(** ============================================================
+    Canonical forms for the L1 judgment (proof-debt P43)
+    ============================================================
+
+    Mirror of the legacy [canonical_*] lemmas at [Semantics.v:603-630]
+    on the [has_type_l1] judgment. Together these are the
+    prerequisite for [progress_l1] (proof-debt P42).
+
+    A canonical-forms lemma reads: "if [v] is a value of type [T],
+    then [v] is of the canonical syntactic shape for [T]". This is
+    invertibility of value-typing rules from the value side: it
+    inverts the [is_value v] view of a closed [has_type_l1] derivation
+    into the constructor pattern of [v].
+
+    Modality-polymorphic by design — the structural property holds
+    in both [Linear] and [Affine] modes; the modality parameter
+    threads through inversion unchanged.
+
+    All 7 follow the same pattern as the legacy proofs: inversion on
+    [is_value v] (case-splits the value constructors), then inversion
+    on the typing derivation (rules that don't produce [T] are
+    contradictory). [eauto] discharges the existential witnesses. *)
+
+Lemma canonical_unit_l1_m :
+  forall m R R' G G' v,
+    has_type_l1 m R G v (TBase TUnit) R' G' -> is_value v -> v = EUnit.
+Proof. intros; inversion H0; subst; inversion H; subst; reflexivity. Qed.
+
+Lemma canonical_bool_l1_m :
+  forall m R R' G G' v,
+    has_type_l1 m R G v (TBase TBool) R' G' -> is_value v ->
+    exists b, v = EBool b.
+Proof. intros; inversion H0; subst; inversion H; subst; eauto. Qed.
+
+Lemma canonical_i32_l1_m :
+  forall m R R' G G' v,
+    has_type_l1 m R G v (TBase TI32) R' G' -> is_value v ->
+    exists n, v = EI32 n.
+Proof. intros; inversion H0; subst; inversion H; subst; eauto. Qed.
+
+Lemma canonical_fun_l1_m :
+  forall m R R' G G' v T1 T2,
+    has_type_l1 m R G v (TFun T1 T2) R' G' -> is_value v ->
+    exists body, v = ELam T1 body.
+Proof. intros; inversion H0; subst; inversion H; subst; eauto. Qed.
+
+Lemma canonical_prod_l1_m :
+  forall m R R' G G' v T1 T2,
+    has_type_l1 m R G v (TProd T1 T2) R' G' -> is_value v ->
+    exists v1 v2, v = EPair v1 v2 /\ is_value v1 /\ is_value v2.
+Proof. intros; inversion H0; subst; inversion H; subst; eexists _, _; auto. Qed.
+
+Lemma canonical_sum_l1_m :
+  forall m R R' G G' v T1 T2,
+    has_type_l1 m R G v (TSum T1 T2) R' G' -> is_value v ->
+    (exists T v0, v = EInl T v0 /\ is_value v0) \/
+    (exists T v0, v = EInr T v0 /\ is_value v0).
+Proof.
+  intros; inversion H0; subst; inversion H; subst;
+    [left|right]; eexists _, _; auto.
+Qed.
+
+Lemma canonical_string_l1_m :
+  forall m R R' G G' v r,
+    has_type_l1 m R G v (TString r) R' G' -> is_value v ->
+    exists l, v = ELoc l r.
+Proof. intros; inversion H0; subst; inversion H; subst; eauto. Qed.
+
+(** ============================================================
+    Print Assumptions — Canonical-forms axiom audit
+    ============================================================
+    Verify each canonical-forms lemma is clean: their statement is
+    structurally derivable from the typing-rule shapes + [is_value]
+    inversion, so they should not surface any axiom. *)
+
+Print Assumptions canonical_unit_l1_m.
+Print Assumptions canonical_bool_l1_m.
+Print Assumptions canonical_i32_l1_m.
+Print Assumptions canonical_fun_l1_m.
+Print Assumptions canonical_prod_l1_m.
+Print Assumptions canonical_sum_l1_m.
+Print Assumptions canonical_string_l1_m.