proof(solo-core): coherent additive product & (TWith) — F1.4 phase 3a

Replaces the incoherent `TPair` with the genuine additive product
`TWith` (a & b). The old `Pair` split usage at introduction (the (X)
multiplicative cost) yet eliminated by projection (the & additive
payoff), making it neither product and strictly weaker than both —
sound under the affine kernel but the wrong product.

`TWith` introduces under SHARED usage (both components typed with the
SAME D, no uadd): only one component survives Fst/Snd elimination, so
reusing a linear resource across the two components is safe. The
multiplicative product (X) (TTensor + let-pair) is deferred to a
follow-up (user steer: "additive & first").

  * Syntax.v    TPair->TWith, Pair->With (shift/subst updated).
  * Typing.v    T_With shares D (drops D1/D2/uadd); T_Fst/T_Snd
                retargeted to TWith.
  * Soundness.v VWith / S_With1 / S_With2 / S_Fst / S_Snd / canon_with;
                progress With-intro case simplified (no split to clear).

Verification: full chain compiles under Coq 8.18; `progress` remains
"Closed under the global context" (zero axioms, zero admits).

NOTE: the Idris twin keeps `Pair`/`TPair` for now — Coq/Idris product
naming diverges until the dual-track parity pass (phase 5). The Rust
checker's product handling should follow the &/(X) split too.

Author: claude

proofs/verification/coq/solo-core/Soundness.v

@@ -35,7 +35,7 @@ Require Import Typing.
 Inductive value : tm -> Prop :=
   | VUnit : value UnitT
   | VLam  : forall q a t, value (Lam q a t)
-  | VPair : forall t1 t2, value t1 -> value t2 -> value (Pair t1 t2)
+  | VWith : forall t1 t2, value t1 -> value t2 -> value (With t1 t2)
   | VInl  : forall b t, value t -> value (Inl b t)
   | VInr  : forall a t, value t -> value (Inr a t)
   (* an echo with a fully-evaluated residue is a value; [Weaken] is
@@ -54,9 +54,9 @@ Inductive step : tm -> tm -> Prop :=
   | S_App   : forall q a t v,
       value v -> step (App (Lam q a t) v) (subst0 v t)
   | S_Fst   : forall v1 v2,
-      value v1 -> value v2 -> step (Fst (Pair v1 v2)) v1
+      value v1 -> value v2 -> step (Fst (With v1 v2)) v1
   | S_Snd   : forall v1 v2,
-      value v1 -> value v2 -> step (Snd (Pair v1 v2)) v2
+      value v1 -> value v2 -> step (Snd (With v1 v2)) v2
   | S_CaseL : forall b v tL tR,
       value v -> step (Case (Inl b v) tL tR) (subst0 v tL)
   | S_CaseR : forall a v tL tR,
@@ -68,10 +68,10 @@ Inductive step : tm -> tm -> Prop :=
       step t1 t1' -> step (App t1 t2) (App t1' t2)
   | S_App2  : forall v1 t2 t2',
       value v1 -> step t2 t2' -> step (App v1 t2) (App v1 t2')
-  | S_Pair1 : forall t1 t1' t2,
-      step t1 t1' -> step (Pair t1 t2) (Pair t1' t2)
-  | S_Pair2 : forall v1 t2 t2',
-      value v1 -> step t2 t2' -> step (Pair v1 t2) (Pair v1 t2')
+  | S_With1 : forall t1 t1' t2,
+      step t1 t1' -> step (With t1 t2) (With t1' t2)
+  | S_With2 : forall v1 t2 t2',
+      value v1 -> step t2 t2' -> step (With v1 t2) (With v1 t2')
   | S_Fst1  : forall t t',
       step t t' -> step (Fst t) (Fst t')
   | S_Snd1  : forall t t',
@@ -164,9 +164,9 @@ Proof.
   - inversion Ht.
 Qed.
 
-Lemma canon_pair : forall a b v,
-  value v -> has_type TEmpty UEmpty v (TPair a b) ->
-  exists v1 v2, v = Pair v1 v2 /\ value v1 /\ value v2.
+Lemma canon_with : forall a b v,
+  value v -> has_type TEmpty UEmpty v (TWith a b) ->
+  exists v1 v2, v = With v1 v2 /\ value v1 /\ value v2.
 Proof.
   intros a b v Hv Ht.
   destruct Hv as [ | q0 a0 tb | u1 u2 Hu1 Hu2 | b0 u0 Hu0 | a0 u0 Hu0
@@ -223,7 +223,7 @@ Proof.
     |                 (* UnitT *)
     | q tyL t1 IHt1   (* Lam  *)
     | t1 IHt1 t2 IHt2 (* App  *)
-    | t1 IHt1 t2 IHt2 (* Pair *)
+    | t1 IHt1 t2 IHt2 (* With *)
     | t1 IHt1         (* Fst  *)
     | t1 IHt1         (* Snd  *)
     | bAnn t1 IHt1    (* Inl  *)
@@ -257,32 +257,33 @@ Proof.
       end
     end.
 
-  - (* Pair t1 t2 *)
-    inversion Ht; subst; empty_uvec.
+  - (* With t1 t2 : additive pair — a value once both components are.
+       T_With shares usage (no split), so nothing to clear here. *)
+    inversion Ht; subst.
     match goal with HT1 : has_type TEmpty UEmpty t1 _ |- _ =>
       match goal with HT2 : has_type TEmpty UEmpty t2 _ |- _ =>
         destruct (IHt1 _ HT1) as [Hv1 | [t1' Hs1]];
         [ destruct (IHt2 _ HT2) as [Hv2 | [t2' Hs2]];
-          [ left; apply VPair; assumption
-          | right; exists (Pair t1 t2'); apply S_Pair2; [exact Hv1 | exact Hs2] ]
-        | right; exists (Pair t1' t2); apply S_Pair1; exact Hs1 ]
+          [ left; apply VWith; assumption
+          | right; exists (With t1 t2'); apply S_With2; [exact Hv1 | exact Hs2] ]
+        | right; exists (With t1' t2); apply S_With1; exact Hs1 ]
       end
     end.
 
   - (* Fst t1 *)
-    inversion Ht; subst; empty_uvec.
-    match goal with HT : has_type TEmpty UEmpty t1 (TPair _ _) |- _ =>
+    inversion Ht; subst.
+    match goal with HT : has_type TEmpty UEmpty t1 (TWith _ _) |- _ =>
       destruct (IHt1 _ HT) as [Hv | [t1' Hs]];
-      [ destruct (canon_pair _ _ _ Hv HT) as [v1 [v2 [Heqv [Hv1 Hv2]]]]; subst t1;
+      [ destruct (canon_with _ _ _ Hv HT) as [v1 [v2 [Heqv [Hv1 Hv2]]]]; subst t1;
         right; exists v1; apply S_Fst; [exact Hv1 | exact Hv2]
       | right; exists (Fst t1'); apply S_Fst1; exact Hs ]
     end.
 
   - (* Snd t1 *)
-    inversion Ht; subst; empty_uvec.
-    match goal with HT : has_type TEmpty UEmpty t1 (TPair _ _) |- _ =>
+    inversion Ht; subst.
+    match goal with HT : has_type TEmpty UEmpty t1 (TWith _ _) |- _ =>
       destruct (IHt1 _ HT) as [Hv | [t1' Hs]];
-      [ destruct (canon_pair _ _ _ Hv HT) as [v1 [v2 [Heqv [Hv1 Hv2]]]]; subst t1;
+      [ destruct (canon_with _ _ _ Hv HT) as [v1 [v2 [Heqv [Hv1 Hv2]]]]; subst t1;
         right; exists v2; apply S_Snd; [exact Hv1 | exact Hv2]
       | right; exists (Snd t1'); apply S_Snd1; exact Hs ]
     end.

proofs/verification/coq/solo-core/Syntax.v

@@ -4,7 +4,8 @@
 (* ========================================================== *)
 (* my-lang Solo core: syntax (Coq twin of Syntax.idr)         *)
 (*                                                            *)
-(* Simply-typed lambda calculus + Unit + pairs + sums + let,  *)
+(* Simply-typed lambda calculus + Unit + additive pairs (&) + *)
+(* sums + let,                                                *)
 (* every binder annotated by a QTT quantity. de Bruijn terms. *)
 (* ========================================================== *)
 
@@ -16,7 +17,10 @@ Require Import EchoMode.
 
 Inductive ty : Type :=
   | TUnit : ty
-  | TPair : ty -> ty -> ty
+  | TWith : ty -> ty -> ty          (* additive product  a & b  (shared usage,
+                                       projected by Fst/Snd). The multiplicative
+                                       product  a (X) b  is deferred to a
+                                       follow-up (TTensor + let-pair). *)
   | TSum  : ty -> ty -> ty
   | TArr  : Q -> ty -> ty -> ty     (* (q x : a) -> b *)
   | TEcho : Mode -> ty -> ty -> ty. (* echo residue: [m] Echo<a => b> *)
@@ -28,7 +32,7 @@ Inductive tm : Type :=
   | UnitT : tm
   | Lam   : Q -> ty -> tm -> tm
   | App   : tm -> tm -> tm
-  | Pair  : tm -> tm -> tm
+  | With  : tm -> tm -> tm    (* additive pair  <t1, t2> : a & b *)
   | Fst   : tm -> tm
   | Snd   : tm -> tm
   | Inl   : ty -> tm -> tm    (* annotation = the other summand *)
@@ -64,7 +68,7 @@ Fixpoint shift (c : nat) (t : tm) : tm :=
   | UnitT        => UnitT
   | Lam q a t1   => Lam q a (shift (S c) t1)
   | App t1 t2    => App (shift c t1) (shift c t2)
-  | Pair t1 t2   => Pair (shift c t1) (shift c t2)
+  | With t1 t2   => With (shift c t1) (shift c t2)
   | Fst t1       => Fst (shift c t1)
   | Snd t1       => Snd (shift c t1)
   | Inl b t1     => Inl b (shift c t1)
@@ -90,7 +94,7 @@ Fixpoint subst_at (j : nat) (u : tm) (t : tm) : tm :=
   | UnitT        => UnitT
   | Lam q a t1   => Lam q a (subst_at (S j) (shift 0 u) t1)
   | App t1 t2    => App (subst_at j u t1) (subst_at j u t2)
-  | Pair t1 t2   => Pair (subst_at j u t1) (subst_at j u t2)
+  | With t1 t2   => With (subst_at j u t1) (subst_at j u t2)
   | Fst t1       => Fst (subst_at j u t1)
   | Snd t1       => Snd (subst_at j u t1)
   | Inl b t1     => Inl b (subst_at j u t1)

proofs/verification/coq/solo-core/Typing.v

@@ -63,18 +63,24 @@ Inductive has_type : tctx -> uvec -> tm -> ty -> Prop :=
       uadd D1 (uscale q D2) = Some D ->
       has_type G D (App t1 t2) b
 
-  | T_Pair : forall G D D1 D2 a b t1 t2,
-      has_type G D1 t1 a ->
-      has_type G D2 t2 b ->
-      uadd D1 D2 = Some D ->
-      has_type G D (Pair t1 t2) (TPair a b)
+  (* Additive product  a & b  (the coherent additive pair). Both
+     components are typed under the SAME usage [D] — NOT split — because
+     only one component ever survives elimination (Fst / Snd), so reusing
+     a linear resource across the two components is safe. This is the
+     genuine `&`; the earlier conflated `Pair` split usage at intro yet
+     projected at elim, making it neither `&` nor `(X)` and strictly
+     weaker than both. *)
+  | T_With : forall G D a b t1 t2,
+      has_type G D t1 a ->
+      has_type G D t2 b ->
+      has_type G D (With t1 t2) (TWith a b)
 
   | T_Fst : forall G D a b t,
-      has_type G D t (TPair a b) ->
+      has_type G D t (TWith a b) ->
       has_type G D (Fst t) a
 
   | T_Snd : forall G D a b t,
-      has_type G D t (TPair a b) ->
+      has_type G D t (TWith a b) ->
       has_type G D (Snd t) b
 
   | T_Inl : forall G D a b t,