feat(spec): add FeishuUserId to FeishuProfile

飞书 user_id 是租户内身份,换应用不变;open_id 是应用内身份,换应用即变。
两者都存:user_id 更稳定,open_id 是 API 调用句柄。

spec/Spec/Prelude.lean

@@ -19,6 +19,8 @@ structure Identifiers where
   UserId : Type
   /-- 飞书用户 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
   FeishuOpenId : Type
+  /-- 飞书 user_id(`OPEN` 表示;租户内唯一,换 app 不变)。 -/
+  FeishuUserId : Type
   /-- 组织飞书应用连接标识(`OPEN` 表示;org-scoped)。 -/
   FeishuConnectionId : Type
   /-- Hub teacher team 标识(`OPEN` 表示;ADR-0020 org-scoped team)。 -/

spec/Spec/System/User.lean

@@ -13,11 +13,13 @@ variable (I : Identifiers)
 
 /-- 飞书用户信息(`PINNED`)。User 上的可选飞书绑定载荷。 -/
 structure FeishuProfile where
-  /-- 飞书 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
+  /-- 应用内身份(`OPEN` 表示);调飞书 API 的直接句柄,换应用即变。 -/
   openId : I.FeishuOpenId
-  /-- 绑定所属飞书应用连接(`PINNED`;org-scoped,不可跨 org)。 -/
+  /-- 租户内身份(`OPEN` 表示);换应用不变,比 open_id 稳定。 -/
+  userId : I.FeishuUserId
+  /-- 绑定所属飞书应用连接(`PINNED`;org-scoped)。 -/
   connection : I.FeishuConnectionId
-  /-- 飞书显示名(`OPEN`;是否预填 displayName 未定)。 -/
+  /-- 飞书显示名(`OPEN`)。 -/
   name : Option String
   /-- 飞书头像 URL(`OPEN`)。 -/
   avatarUrl : Option String